Form
wordの列のうちarityが正しく処理されているものをFormと言います。
一般に単語列は【】内にtex表記されます。
word[arity:0] はそれだけでFormになります。例 【\(x\)】
var以外の word[arity : 0] はconstと言われます。
ただし補助的なwordの前後にスペースは入れなくても良いです。例 【\(\neg(P \mathbin\& Q)\)】
precedの差を利用して\((\,)\)を略せます。例 【\(P \Rightarrow Q \Longleftrightarrow \neg P \mathbin{\rm o\!r} Q\)】
precedが等しいものは後ろから読まれます。例 【\(P \& Q \& R\)】=【\(P \& (Q \& R)\)】
Formの中でもgramが正しく処理されているものには Set, Class, Prop があります。上の3例はFormですがPropにはなっていません…(\(P\),\(Q\)はSetなので)
Propの例 【\(x=y \Rightarrow y=x\)】
prefix記法のForm
Formのtex表記は人間が読みやすい形になりますが、本来のFormは機械が処理しやすいprefix記法です。すなわち次の規則で帰納的に作成されます。
・\({\tt w}\)がword[arity : \(n\)], \({\tt F}_1,\cdots,{\tt F}_n\)がForm ⇒ \({\tt wF}_1\cdots{\tt F}_n\)がForm
・\({\tt w}\)がword[arity : q], \({\tt x}\)がvar, \({\tt F}\)がForm ⇒ \({\tt wxF}\)がForm
Formに対する関数の定義も帰納的にされます。
Set,Class,Propの細かい規則として、例えば
・\({\tt w}\)がword(s,p)，\({\tt S}\)がSet ⇒ \({\tt wS}\)がProp
入れ子列
一般に言語は入れ子の列になります。例 I think that [that that that [that boy wrote] is wrong].
列→入れ子列 を parse と言います。prefix記法のFormに対しては、arityの情報のみでparseできます。
入れ子の列→入れ子でない列 は flatten と言われます。
列 \({\tt F}\) に対して\({\tt F}\)の\(n+1\)番要素を \({\tt F}[n]\) とします。
例 \(【\neg\neg\top】[1][1]=\top\)
\({\tt F}\)の長さが\(n+1\)のとき \({\tt F}={\tt F}[0]\,{\tt F}[1]\,\cdots\,{\tt F}[n]\) となります。
fvar
\({\tt F}\) がFormのとき「\({\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\}\)
代入
関数 \(f\) による \(x\) の対応先を \(f(x)\) や \(x^f\) と表します。
「\(x\)以外の対応は\(f\)と同じで、\(x\)には\(x\)を対応させる」関数を \(f\div x\) とします。
\(\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\) とします。
例 \(【x=y】^{x\,\mapsto\,y}=【y=y】\)
\({\tt F}^{{\tt x}\,\mapsto\,{\tt T}}\) は \({\tt F}[{\tt T}/{\tt x}]\) と書かれるも多いようです。
代入可能
\({\tt F}\)に\(\chi\)を代入可能であることを \({\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)\)
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) を誘導します。
同値類の代入
\(\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】\)