列について
ものを並べたものを列と言います。
\({\tt x}\) を \({\tt n}\) 個並べた列を \({\tt x}^{\tt n}\) とします。
自然言語では、単語列のうち文法を満たすものが「文」なります。文は意味が考慮され入れ子の列になります。
I think that that that that that boy wrote is wrong.
入れ子でない列→入れ子列 を parse、入れ子列→入れ子でない列 を flatten と言います。
列は誤解を生みうるものです。10 は「数字の十」とも「1,0の列」とも取れます。
自然言語で単語はsymbolの列です。文の列として文章が作られます。
英語では、symbolの列の区切りは無し、単語の列の区切りはスペース、文の列の区切りはドットです。
準備
メタ部分に、少しだけ数学から準備をします。
関数 \(f\) による \(x\) の対応先を \(f(x)\) や \(x^f\) と表します。
「\(x\)以外の対応は\(f\)と同じで、\(x\)には\(x\)を対応させる」関数を \(f\div x\) とします。
\(x\) を \(y\) に送るだけの関数を \(x\mapsto y\) とします。
列 \({\tt F}\) に対して\({\tt F}\)の\({\tt n+1}\)番要素を \({\tt F}[{\tt n}]\) とします。\([{\tt n}]\) もメタ記号です。
\({\tt F}\)の長さが\({\tt n+1}\)のとき \({\tt F}={\tt F}[0]\,{\tt F}[1]\,\cdots\,{\tt F}[{\tt n}]\)
3
Formには一階言語と同様の操作が定義されます。Formは帰納的に定義されましたが、操作も帰納的に定義されます。
ここでの関数や\([n]\)関数はprefixの入れ子列に変形した上で計算されます。
var以外のword[arity : 0]はconstと呼ばれます。
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 → s-Form は 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}]\) と書かれる事も多いようです。phpでは form_substi(F,x,T) で計算されます。
\(\chi\) : var → s-Form は s-Form → s-Form を導くこと等も帰納的に示せます。
\({\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可能かどうかは議論されません。
このページのルールは大幅に変更予定
1
私たちのシステムでは記号列の変換をたくさん行います。「変換の規則」も記号列としてシステムに記述できるようにします。
$Varを$_varに変更、サンセリフ体はFormでないもの用に？
そもそも$変数は人間はほとんど使用しない仕様に？
$Form
「var以外の数学記号と$変数」の列を $列 と言います。
$列のうちarityが正しく処理されているものを $Form を言います。
$Formを作るときには $var, $Var は arity : 0 で $.var は arity : 1, $..Var は arity : 2 とされます。
$.var, $..varについては\({\sf p},{\sf q},{\sf r}\)で始まるものはpreced : 700, それ以外はpreced : 300とされます。
$Formも入れ子列とされます。
$Formにも形(prefix、decentなど)があります。
$Formに対してもfvarは定義されます。
・\({\rm fvar}({\tt w})=\{\tt w\}\) if \({\tt w}\)が$var
\({\tt W}\)が$Varのときは、\({\rm fvar}({\tt W})\)はこれ以上計算されません。
Form → $Form
2つの$Formは、$var同士の変換、$Var同士の変換、等で移り変わるとき同じとみなされます。
Formを$Formに変換する関数 $ を作ります。varを$Varに置き換えます。例 $【\(X \in Y\)】=【\({\sf X} \in {\sf Y}\)】
ただし、束縛されたvarは$varに替えます。例 $【\(\forall X ( X \in Y )\)】=【\(\forall {\sf x} ( {\sf x} \in {\sf Y} )\)】