$変数
「記号列に関する何らかの規則」を記述するために $変数 を使用します。$変数のtxtは $ で始まります。
$var, $Var はサンセリフ体の小文字, 大文字およびそれらに自然数が付いたものになります。例 \({\sf a}\), \({\sf A}\)
他に $.var, $..var もありサンセリフ体の小文字になります(tex表記は $var と同じ)。例 \({\sf a}\), \({\sf a}\)
「var以外の数学記号と$変数」の列を $列 と言います。
規則を使用する際には、$varには１つのvar、$Varには記号列、$.var には word[arity : 1], $..var には word[arity : 2] が代入されます。その他の代入条件が課されることもあります。
例えば【\(\neg \neg {\sf P}\)】→【\({\sf P}\)】
という規則を【\(\neg \neg \neg Q\)】に適用するとき
【\(\neg\neg\neg Q\)】に【\(\neg\neg{\sf P}\)】を合わせる代入 \(({\sf P}\mapsto \neg Q)\) が計算され【\(\neg Q\)】という結果になります。
超decent Form
一定の変形によってdecent Formになるもので、さらに読みやすい形を作ります。
超decent → decent → prefix
と計算されます。超decent Formのtxtでは、塊を作るために { } が使われます。
phpでは前の→がform_decentで計算されます。
{ の直後の記号はtokenと呼ばれます。
超decent Formは
①decent Formの省略形
②特殊表記を持つ
あるいはその両方となります。①の場合、decentへの変形にはabbrというデータが使われます。特殊表記とは、一定の形の列に対する(各記号のtex表記を並べたものではない)tex表記です。
①
abbrは次の形になります。
abbr0 ≈ abbr1 ただし、abbr0,abbr1は$列
これは「abbr0をabbr1に変形する」という規則だと捉えられます。
abbr …【\(\forall {\sf x} {\sf A} . {\sf P}\)】≈【\(\forall {\sf x} \, ( {\sf x} {\sf A} \Rightarrow ( {\sf P} ) )\)】
abbr0のallはtokenで、abbr1のallはwordです。
phpの関数abbrは、tokenに対し変形規則としての使用に適したabbrを返します。abbr('all') は
{ all $x $A . $P } -> all $x ( $x $A xr ( $P ) )
【\(\forall x \in R . \forall x \in S . x \in T\)】≈【\(\forall x \, ( x \in R \forall x \, ( x \in S x \in T ) )\)】
{ } による塊が崩れないよう、内側から計算する方が良いでしょう。
abbr1の \(({\sf P})\) の \((\;)\) は必要です。\({\sf P}\)に代入されるp-Formに \(\Rightarrow\) よりprecedの大きいwordが含まれていても働くように。
②
単独表記を持たないwordは、紹介時に$列の特殊表記例が与えられます。例えば、クラスを生成する cls があります。word(vp,c)! …【\(\{ Array {\sf x} \mid {\sf P} \}\)】
【\(\{ Array x \mid x \in \{ Array y \mid x \in y \} \}\)】はc-Formで、②のパターンです。
特殊表記を持つFormのtxtで引数を区切るには ; や | が使われます。
clsは単独でtex表記を持たない代わりに、tex('cls') は
[ cls $x | $P ] → \{ $x | $P \}
というデータになります。\{ \} は \(\{\,\}\) で | は \(\mid\) というtex表記を持ちます。
特殊表記を計算する際にはまず { } → [ ] と変換してから、上のデータを使い、最後に各記号のtex commandを並べます。
例 【\(\{ Array x \mid P \}\)】≈ cls(x , P)
正確には、超decentの {cls x | P} におけるclsはtoken、decentの cls(x , P) におけるclsはwordです。
①②
abbrの紹介時にabbr1が特殊表記になります。例としてclsの仲間の_clsを取り上げてみます。abbr …【\(_{ {\sf P} } {\sf x}\)】≈【\(\{ Array {\sf x} \mid {\sf P} \}\)】
\(\sum_{i\in\{1,2\}}i=3\) の左辺を \(\sum\{i \mid i\in\{1,2\}\}\) と解釈することができるでしょう。
_clsは次のtex規則を持っています。
[ _clsx $X | $P | $T ] -> !_{ $P !} $T
!_{ と !} はtex command _{ と } を持ちます。