$変数
「記号列に関する何らかの規則」を記述するために $変数 を使用します。$var, $Var はサンセリフ体の小文字, 大文字およびそれらに自然数が付いたものになります。例 \({\sf a}\), \({\sf A}\)
他に $.var, $..var もありサンセリフ体の小文字になります。例 \({\sf a}\), \({\sf a}\)
「var以外の数学記号と$変数」の列を $列 と言います。
【\(\neg \neg {\sf P}\)】→【\({\sf P}\)】という規則を【\(\neg \neg \neg Q\)】に適用するとき代入 \(({\sf P}\mapsto \neg Q)\) が計算され【\(\neg Q\)】という結果になります。
規則を使用する際には、$varには１つのvar、$Varには記号列、$.var には word[arity : 1], $..var には word[arity : 2] が代入されます。その他の代入条件が課されることもあります(？)。
超decent Form
一定の変形によってdecent Formになるもので、さらに読みやすい形を作ります。
超decent → decent → prefix
と計算されます。phpでは前の→がform_decentで計算されます。
超decent Formのtxtでは、塊を作るために { } が使われ、引数を区切るのに ; や | が使われます。
{ の直後の記号はtokenと呼ばれます。
超decent Formは
①decent Formの省略形
②特殊表記を持つ
あるいはその両方となります。
①の場合、decentへの変形にはabbrというデータが使われます。abbrは次の形になります。
abbr0 ≈ abbr1 ただし、abbr0,abbr1は$列
これは「abbr0をabbr1に変形する規則」と捉えられます。
①の例
abbrは次のように「紹介」されます。abbr …【\(\forall {\sf x} {\sf A} . {\sf P}\)】≈【\(\forall {\sf x} \, ( {\sf x} {\sf A} \Rightarrow ( {\sf P} ) )\)】
all はForm内部での使われ方によって、wordかtokenかが変わります。直前が { のときtokenです。
例 【\(\forall x \in R . \forall x \in S . x \in T\)】≈【\(\forall x \, ( x \in R \Rightarrow \forall x \, ( x \in S \Rightarrow x \in T ) )\)】
{ } による塊が崩れないよう、内側から計算する方が良いでしょう。
\(({\sf P})\) の \((\;)\) は必要です。\({\sf P}\)に代入先に \(\Rightarrow\) よりprecedの大きいwordが含まれていても働くように。
abbr … 【\(\forall {\sf x}_{1} , \cdots , {\sf x}_{\tt n} \, {\sf P}\)】≈【\(\forall {\sf x}_{1} \cdots \forall {\sf x}_{\tt n} ( {\sf P} )\)】
abbr … 【\(\forall {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf A} . {\sf P}\)】≈【\(\forall {\sf x}_{1} {\sf A} . \cdots \forall {\sf x}_{\tt n} {\sf A} . {\sf P}\)】
例 【\(\forall x , y \in M . x \cup y \in M\)】≈【\(\forall x \, \forall y \, ( x \in M \Rightarrow ( y \in M \Rightarrow x \cup y \in M ) )\)】
異なる単語を同じtxtで済ましてしまうことがあります。phpの関数form_supportが区別をしています。
{alls ～} 内に . があればallsをalls+に変換し、さらに内部にある ; の個数+1を alls あるいは alls+ の後に追加します。上の例では alls が alls+2 に変換されます。
abbr …【\( {\sf X}\)】≈【\({\sf X} , {\sf X}\)】
{ } は処理における塊を作りますが、Formとしての塊にもなります。pileを含むFormを除いて。
例 【\(x \in y \in z\)】≈【\(x \in y , y \in z\)】 【\(P \Leftrightarrow Q \Leftrightarrow R\)】≈【\(P \Leftrightarrow Q , Q \Leftrightarrow R\)】
②の例
特殊表記とは、一定の形の列に対する(各記号のtex表記を並べたものではない)tex表記です。単独表記を持たないwordは、紹介時に$列の特殊表記例が与えられます。例えば、クラスを生成する cls は次のように。
word(vp,c)! …【\(\{ {\sf x} \mid {\sf P} \} \)】
【\(\{ x \mid x \in \{ y \mid x \in y \} \} \)】はc-Formで、②のパターンです。
phpのform_texは、特殊表記の場合にはまず form_tex0 により非特殊化します。tex('cls') は
cls $x | $P → \{ $x | $P \}
というデータになっています。例えば \{ はtex表記のためだけの記号で tex('\{') は \{ です。
例 【\(\{ x \mid P \} \)】≈ cls(x , P)
①②の例
abbrも特殊表記になることがあります。clsには次のような使用もあります。abbr …【\(\{ {\sf x} {\sf A} \mid {\sf P} \}\)】≈【\(\{ {\sf x} \mid {\sf x} {\sf A} , {\sf P} \} \)】
例 【\(\{ x \in X \mid x \subset Y \}\)】 ≈ 【\(\{ x \mid x \in X , x \subset Y \} \)】
次の左辺はabbr0で$Xが表記上消える珍しい例です。
abbr …【\(\{ {\sf T} \mid {\sf P} \}\)】≈【\(\{ {\sf x} \mid \exists {\sf X} \, ( ( {\sf P} ) , {\sf x} = {\sf T} ) \} \)】
abbrを使用するとき、abbr0に含まれずabbr1に含まれる$var(例えば上の \({\sf x}\))には適当なvarを代入します。私たちはFormの同値類を見ていることに注意しましょう。
例 【\(\{ x \cup y \mid x \in X , y \in Y \}\)】≈【\(\{ z \mid \exists x , y \, ( x \in X , y \in Y ) , z = x \cup y \} \)】
clsxには次のような使用もあります。
abbr …【\(\{ {\sf T} {\sf A} \mid {\sf P} \}\)】≈【\(\{ {\sf x} {\sf A} \mid \exists {\sf X} \, ( {\sf P} ) , {\sf x} = {\sf T} \}\)】
{clsx ～ } 内で最初の | より前にword(ss,p)があるかどうかで、どちらの形か判断されます。\({\sf T}\)の代入先はword(ss,p)を含まないことが想定されています。