Form③

関数

メタ言語に、少しだけ数学から準備をします。
関数 \(f\) による \(x\) の対応先を \(f(x)\) や \(x^f\) と表します。
「\(x\)以外の対応は\(f\)と同じで、\(x\)には\(x\)を対応させる」関数を \(f\div x\) とします。
\(x\) を \(y\) に送るだけの関数を \(x\mapsto y\) とします。

私たちの言語は一階言語を超越しますが、一階言語と同様にFormに対する関数が定義されます。
Formは帰納的に定義されていましたが、Formに対する関数も帰納的に定義されます。
ここでの関数や\([n]\)関数はprefixに変形した上で計算されます。

fvar

Form \({\tt F}\) に対し「\({\tt F}\)で自由なvar」の集合 \({\rm fvar}({\tt F})\) が定義されます。
・\({\rm fvar}({\tt w})=\{\tt w\}\)　if \({\tt w}\)がvar
・\({\rm fvar}({\tt w})=\emptyset\)　if \({\tt w}\)がconst
・\({\rm fvar}({\tt F})={\rm fvar}({\tt F}[1])\cup\cdots\cup{\rm fvar}({\tt F}[n])\)　if \({\tt F}[0]\)がarity : \(n\)
・\({\rm fvar}({\tt F})={\rm fvar}({\tt F}[2])\setminus{\rm fvar}({\tt F}[1])\)　if \({\tt F}[0]\)がarity : q

例　\({\rm fvar}【\exists y\;x \neq y】 = \{x\}\)

substi

\(\chi\) : var → Set は Form → Form に拡張されます。
・\({\tt w}^\chi={\tt w}\)　if \({\tt w}\)がconst
・\({\tt F}^\chi={\tt F}[0]\,{\tt F}[1]^\chi\,\cdots\,{\tt F}[n]^\chi\)　if \({\tt F}[0]\)がarity : \(n\)
・\({\tt F}^\chi={\tt F}[0]\,{\tt F}[1]\,{\tt F}[2]^{\chi\,\div\,{\tt F}[1]}\)　if \({\tt F}[0]\)がarity : q

例　\(【x=y】\!^{x\,\mapsto\,y}=【y=y】\)
\({\tt F}^{{\tt x}\,\mapsto\,{\tt T}}\) は \({\tt F}[{\tt T}/{\tt x}]\) と書かれる事も多いようです。
\(\chi\) : var → Set は Set → Set を導くこと等も帰納的に示せます。

\({\tt F}\)に\(\chi\)をsubsti可能であることを \({\rm can}({\tt F},\chi)\) と表します。
・\({\rm can}({\tt w},\chi) \Longleftrightarrow \top\)　if \({\tt w}\)がconst
・\({\rm can}({\tt F},\chi) \Longleftrightarrow {\rm can}({\tt F}[1],\chi),\,\cdots,\,{\rm can}({\tt F}[n],\chi)\)　if \({\tt F}[0]\)がarity : \(n\)
・\({\rm can}({\tt F},\chi) \Longleftrightarrow {\rm can}({\tt F}[2],\chi\div{\tt F}[1]),\,\forall{\tt v}\in{\rm fvar}({\tt F}).\,{\tt F}[1]\notin{\rm fvar}({\tt v}^\chi)\)　if \({\tt F}[0]\)がarity : q

例　\(\neg\,{\rm can}(【\exists y\,x\ne y】,x\mapsto y)\)
一般書では「substiが書かれたらsubsti可能であることを暗黙のうちに仮定する」というふざけたことも行われるので注意しましょう。

Formの同値

積分では \(\int f(x)dx=\int f(y) dy\) で、\(x\)を\(y\)に替えることができます。Formに対しても束縛varの名前替えは同一視されます。
同一視されることを \(\stackrel{\rm v}=\) を使って表します。Form \({\tt G}\) に対し
・\({\tt w}\stackrel{\rm v}={\tt G} \Longleftrightarrow {\tt w}={\tt G}\)　if \({\tt w}\)がarity：0
・\({\tt F}\stackrel{\rm v}={\tt G} \Longleftrightarrow {\tt F}[0]={\tt G}[0],\, {\tt F}[1]\stackrel{\rm v}={\tt G}[1],\,\cdots,\,{\tt F}[n]\stackrel{\rm v}={\tt G}[n]\)　if \({\tt F}[0]\)がarity : \(n\)
・\({\tt F}\stackrel{\rm v}={\tt G} \Longleftrightarrow {\tt F}[0]={\tt G}[0],\,{\tt F}[2]^\chi\stackrel{\rm v}={\tt G}[2],\,{\rm can}({\tt F}[2],\chi)\)　if \({\tt F}[0]\)がarity : q, \(\chi={\tt F}[1]\mapsto{\tt G}[1]\)

私たちは、正確にはFormではなくFormの同値類を取り扱うことが多いです。
同値類であることを明記したいときは \(\pi\) : Form → Form/\(\stackrel{\rm v}=\) を使用します。
fvar : Form → \(\wp\)(var) は自然に Form/\(\stackrel{\rm v}=\) → \(\wp\)(var) を誘導します。
Formの同値類に対して [1] などは定義できないです…

\(\chi\) : var → Set を Form/\(\stackrel{\rm v}=\) → Form/\(\stackrel{\rm v}=\) にもします。次を要請します。
　\({\rm can}({\tt F},\chi) \Longrightarrow (\pi{\tt F})^\chi=\pi({\tt F}^\chi)\)
例　\(\pi【\exists y\;x \neq y】^{x\,\mapsto\, y} = \pi【\exists z\;x \neq z】^{x\,\mapsto\, y} = \pi【\exists z\;y \neq z】\)
同値類に対してはsubsti可能かどうかは議論されません。