tokenのabbr
ほとんどのtokenにはabbrというデータが与えられます。
token \({\tt X}\) のabbrは abbr0 = abbr1 (abbr0,abbr1はvarを除いた単語の列) という形になります。
ただし、abbr0は\({\tt X}\)で始まり、abbr1は\({\tt X}\)を含まないです。
abbr …【\(\exists {\sf x} {\sf w} {\sf T} . {\sf P} \)】=【\(\exists {\sf x} \, ( {\sf x} {\sf w} {\sf T} , {\sf P} )\)】
abbr …【\(! {\sf x} {\sf w} {\sf T} . {\sf P} \)】=【\(! {\sf x} \, ( {\sf x} {\sf w} {\sf T} , {\sf P} )\)】
abbr …【\(\exists! {\sf x} {\sf w} {\sf T} . {\sf P} \)】=【\(\exists! {\sf x} \, ( {\sf x} {\sf w} {\sf T} , {\sf P} )\)】
wordとtokenの列に対し、abbrを基にtoken消去してFormを作ることが重要です。
例 【\(\forall x\in R . x\in C\)】=【\(\forall x\,(x\in R\Rightarrow x\in C)\)】
ここでは次の代入がされています。 \(({\sf x}\mapsto x, {\sf w}\mapsto{\in}, {\sf T}\mapsto R, {\sf P}\mapsto x\in C)\)
#varには１つの単語、#Varには単語列が代入されます。
連結記法
abbr …【\( {\sf X} \)】=【\({\sf X} \mathbin\& {\sf X}\)】例えば次のように使えます。
【\(x \in y \in z\)】=【\(x \in y \,\&\, y \in z\)】
【\(P \Rightarrow Q \Rightarrow R\)】=【\(P \Rightarrow Q \,\&\, Q \Rightarrow R\)】
classの生成(内包記法)
abbr …【\(\{ {\sf x} \mid {\sf P} \}\)】=【\(\text{cl} \, {\sf x} ( {\sf P} )\)】\({\rm cl}\)は内部で使用され、人間はあまり目にしないと思います。塊が崩れないよう\(({\sf P})\)とされてます。
abbr …【\(\{ {\sf x} {\sf w} {\sf T} \mid {\sf P} \}\)】=【\(\{ {\sf x} \mid {\sf x} {\sf w} {\sf T} , {\sf P} \}\)】
次の変形は %inの消去 と言われます。
【\({\sf T}\in\{{\sf x} \mid {\sf P}\}\)】=【\({\sf P}^{{\sf x}\,\mapsto\,{\sf T}}\)】 【\(x\in\{y \mid z\in\{x \mid x=y\}\}\)】のように入れ子になっているときは内側から計算されます。
=【\(x\in\{y \mid z=y\}\)】=【\(z=x\)】
ただし外側から計算しても同じ結果になります。
=【\(z\in\{u \mid u=x\}\)】=【\(z=x\)】
#Form
varを含まず#単語を含んだFormみたいな奴を #Form を言います。例 【\({\sf x}={\sf X}\)】#Formに対してもfvarは定義されます。
・\({\rm fvar}({\tt w})=\{\tt w\}\) if \({\tt w}\)が#var
\({\tt W}\)が#Varのときは、\({\rm fvar}({\tt W})\)はこれ以上計算されません。
wordのdef
wordの中にはdefというデータが与えられるものがあります。
word \({\tt X}\) のdefは def0 = def1 (def0,def1は#Form) という形になります。
ただし、def0\([0]\) = \({\tt X}\)で、def1は\({\tt X}\)を含まないです。また fvar(def0) = fvar(def1) となります。
def …【\(\exists! {\sf x} {\sf P}\)】=【\(\exists {\sf x} {\sf P} , ! {\sf x} {\sf P}\)】
defを基にFormのwordを消去することも重要です。
その際、def1に現れdef0に現れない#varには適当なvarの代入を指定しなければなりません。
Formに対し「必要なword消去」をすべてやった結果をdown形と言い、\({\tt F}\)のdown形を\(\downarrow{\tt F}\)とします。それは一階言語のFormになり、使用可能なwordが限られたものだけになることから長々となることが多いです。
Formのcheck
tex表記およびdown形を出力します。