1
一階言語を拡張しFormというものを作ります。Formはいくつかの形をとりますが、機械にとって処理しやすいprefix形から作ります。
人間にとってまともなdecent形を次に。
Formで使われる記号
ほとんどの記号は(単独で)tex表記を持ち、人間が通常目にするものになります。注釈にtxt(機械への入力時に使用される記号本体)があります。例 \(=\)
tex表記が同じでも異なる記号があります。例 クラスが等しいことを表す \(=\)
記号列のtxtは各記号のtxtをスペースで区切って並べたものです。例 \(x x\)
prefix Formで使用される記号はwordと呼ばれます。
wordはgramというデータを持ちます。gram は (gram0, gram1) という形になります。
・gram0 … s,c,p の列か vp
・gram1 … s,c,p のどれか
また、arity : gram0の長さ、ただし gram0がvp ⇒ arity : q とされます。
word(s,s)は1項関数、word(ss,p)は2項述語、等と呼ばれることもあります。\(\dagger\) 通常のwordは数学の教科書において次のように「紹介」されます。
word(ss,p) … \(=\)
word(cc,p) … \(=\)
var
phpの正規表現に倣って、数字を[0-9]とします。ローマ字の小文字を[a-z]、小文字と大文字を[a-zA-Z]とします。
ギリシャ字はローマ字にないもののみ用いられ [greek] とします。\(\dagger\)
0回以上の繰り返しを*、またはを|で表します。 v-Formは特別なword(,s)で ([a-zA-Z]|cal[A-Z]|frak[a-zA-Z]|[greek])[0-9]* が使用されます。
例 \(x\) \(\mathcal{X}_{0}\) \(\mathfrak{x}_{01}\) \(\chi_{1}\)
([a-zA-Z]|cal[A-Z])[0-9]*_ はword(,c)になります。例 \(x\) \(\mathcal{X}_{0}\)
|[A-C][0-9]* もword(,s)になります。例 \(A\)
|[P-R][0-9]* はword(,p)になります。例 \(P_{0}\)
prefix Form
Formは、wordの列で帰納的に作成されます。
・\({\tt w}\)がword[arity : \({\tt n}\)], \({\tt F}_1,\cdots,{\tt F}_{\tt n}\)がForm ⇒ \({\tt wF}_1\cdots{\tt F}_{\tt n}\)がForm
・\({\tt w}\)がword[arity : q], \({\tt x}\)がvar, \({\tt F}\)がForm ⇒ \({\tt wxF}\)がForm
word[arity : 0] はそれだけでFormになります。例 【\(x\)】
\([\;]\)を使うときは入れ子列としてみなされるので、例えば 【\(\neg \neg P\)】\([1][0]\) = \(\neg\)
Formの中でもgramが正しく処理されているものに v-Form, s-Form, c-Form, p-Form があります。
(variable, set, class, propositionの頭文字です)
それらの細かい規則として、例えば
・\({\tt w}\)がword(s,p)，\({\tt S}\)がs-Form ⇒ \({\tt wS}\)がp-Form
wordの表記法
arityが0でないwordは表記法データも持ちます。それは次の2種類のどちらかになります。
F 結合性(LかR)およびprecedの組
結合性は通常は L です。precedは自然数ですが、大小関係に意味があります。
word(vp,p)R … \(\forall\) \(\exists\)
decent Form
wordと \((\) \(,\) \()\)の列で、読みやすい形を作ります。word[arity : 2] はinfixにされます。例 【\(P , Q\)】
表記法Fのword [arity : \({\tt n}\)] \({\tt w}\) は【\({\tt w}({\tt x}_1,\cdots,{\tt x_n})\)】の形で使用されます。
列のtxtにおいて ( ) の前後ではスペースを略せます。例 \(( x )\)
prefixへの変形によって等しくなることを ≈ で表します。
infixでは\((\;)\)が必要になりますが、precedの差を利用して略せることがあります。
例 【\(x = y \Rightarrow y = x\)】≈【\(( x = y ) \Rightarrow ( y = x )\)】
例 【\(P \Rightarrow Q \Longleftrightarrow \neg P \mathbin{\rm o\!r} Q\)】≈【\(( P \Rightarrow Q ) \Longleftrightarrow ( ( \neg P ) \mathbin{\rm o\!r} Q )\)】
L結合性でprecedが等しいものは左から読まれます。例 【\(P , Q , R\)】≈【\(( P , Q ) , R\)】
\(\forall\) はR結合性で 【\(\forall x \forall y P\)】≈【\(\forall x ( \forall y P )\)】
word[arity : 1] はpostfixにされてもよいです。ふざけた例 【\(- x -\)】≈【\(- - x\)】
なお、decentでは区別されますが、prefixでは次の同一視をして良いです。
\(\Rightarrow\) ≈ \(\Longrightarrow\)
\(\Leftrightarrow\) ≈ \(\Longleftrightarrow\)
2
{ }形という、decent形よりさらに高度な形のFormを作ります。
Formの良い表記を作る仕組みも導入され、使用される記号が増えます。
abbr
{ }形→decent形 にはabbrというデータが使われます。abbrは
abbr0 ≈ abbr1
の形になり、これは「abbr0 を ( abbr1 ) に変形する規則」と捉えられます。
・Formが代入される … $[a-zA-Z][0-9]* 例 \(x\) \(X_{0}\)
・Formでない記号列が代入される … $_[a-zA-Z][0-9]* 例 \(\mathop{{\sf x}}\) \(\mathop{{\sf X}_{0}}\)
$_～ の後に $～ または $_～ を続けることはできません。
{ } Form
abbrは次のように「紹介」されます。abbr …【\(\forall x , y P\)】≈【\(\forall x \forall y ( P )\)】
例 【\(\forall x , X ( x \in X )\)】≈【\(\forall x \forall X ( x \in X )\)】
\((P)\) の \((\;)\) は必要です。\(P\) の代入先に \(\forall\) よりprecedの大きいwordが含まれていても働くように。
allには次のような使用法もあります。
abbr …【\(\forall x \mathop{{\sf A}} . P\)】≈【\(\forall x ( x \mathop{{\sf A}} \Rightarrow ( P ) )\)】
例 【\(\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 ) )\)】
{ } 内でのみ使われる区切り記号には次があります。
\(,\) \(.\) \(\mid\) tex表記の無い ;; 改行表記される //
％ を ;; に変更すべし
( ) を補わない { } Form
{ } は通常はFormとしての塊を作りますが、稀にその塊を崩すこともあります。
( ) を付けずに「abbr0 を abbr1 に変形する規則」と捉えらるものは abbr* とされます。
abbr* …【\( X\)】≈【\(X , X\)】
例 【\(x \in y \in z\)】≈【\(x \in y , y \in z\)】
precedに注意しなければなりません。
【\(x \in y \in z \Longrightarrow P\)】≈【\(( x \in y , y \in z ) \Longrightarrow P\)】
【\(x \in y \in z \Rightarrow P\)】≈【\(x \in y , ( y \in z \Rightarrow P )\)】
特殊表記
{ } 形Formは表記が特殊になることがあり、「一定の形の列」に対して表記が与えられます。単独では表記無しのwordは次のように紹介されます。
word(vp,c) … cls abbr …【\(\{ x \mid P \}\)】≈ cls $x ($P)
≈ の左辺が特殊表記になっています。
{ } は通常はtex表記されませんが、内部が cls で始まるときには \(\{\; \}\) とされるのです。
なお、≈ の右辺はtex表記ができません。
3
Formの取り扱いについて色々。
表記のためだけの記号
Formのtxtには次の2種類の処理が施されます。
tex表記(をするためのtex cmd)の計算
{ }形→decent形→prefix形 という syntax計算
\, \; \! はそのままtex cmdとしてスペースを調整します。例 \(x \; x\)
{ } は前に ! をつけるとtex cmdになります。例 \(x = x\) \(x { = } x\)
_ ^ _{ ^{ はそのままtex cmdになります。例 \(x ^{ x ^ x }\)
\(\text{id}\) というword(s,s)は、通常 \(\text{id} _ X\) のような形で使用されますがsyntax処理上は \(\text{id} X\) と同じです。
\(x_{1} x_{2} \cdots x_{99}\) なんて表記もできます。
メタ自然数
自然数は \({\tt n\,{\text -}\,1}\)等の形で使用できます。abbrの最初の例は実際の教科書には一般化された形で記述されています。
1以上の自然数 \({\tt n}\) に対し abbr …【\(\forall x_{1} , \cdots , x_{\tt n} P\)】≈【\(\forall x_{1} \cdots \forall x_{\tt n} ( P )\)】
正確には無限個のabbrが与えられます。
\n+1等も使えるように。xn は x\n に変更すべし。
Formの同値
word[arity : q]を含むFormでは束縛varが現れます。例 【\(x = y \Rightarrow \forall x ( x = y )\)】の束縛varは2,3番目の\(x\)
束縛varの名前替えはもとのFormと同一視されます。例 【\(\forall x ( x \in A )\)】=【\(\forall y ( y \in A )\)】
積分で \(\int f(x)dx=\int f(y) dy\) となるのと一緒です。
clsには次のような使用もあります。左辺は$Xが表記上消える珍しい例です。
abbr …【\(\{ T \mid P \}\)】≈【\(\{ x \mid \exists \mathop{{\sf X}} \, ( ( P ) , x = T ) \}\)】
abbrを適用するとき、右辺にのみ含まれるvar(例えば上の \(x\))には適当なv-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 ) \}\)】
word関数
word→word の働きをする word関数 というものがあります。
# と一文字になり、word関数とwordの間にはスペースを入れません。
tex表記は特殊になるので紹介時に記されます。紹介時にはgramの変換データも記されます。s,c,pを動く変数として\({\tt x}\),\({\tt y}\),\({\tt z}\)等が使われます。表記法データは変化させないものとします。
word関数の変形でも abbr が使われます。
abbr … 【\(A\!\not{\!{\sf p}}\,B\)】≈【\(\neg ( A \mathop{{\sf p}} B )\)】
例 【\(x \notin X\)】≈【\(\neg ( x \in X )\)】 【\(P \not\Rightarrow Q\)】≈【\(\neg ( P \Rightarrow Q )\)】 【\(\not\exists x P\)】≈【\(\neg ( \exists x P )\)】
同じword関数を重ねて使う事(例 #/#/$..p)はtex表記が困難になるのでやめましょう。