1
一階言語を拡張しFormというものを作ります。Formはいくつかの形をとりますが、機械にとって処理しやすいprefix形と人間にとってまともなdecent形を説明します。
word
prefix Formで使用される記号はwordと呼ばれます。wordはgramというデータを持ちます。gram は (gram0, gram1) という形になります。
・gram0 … s,c,p の列か vp (vsとかも？)
・gram1 … s,c,p のどれか
また、arity : gram0の長さ、ただし gram0がvp ⇒ arity : q とされます。
word(s,s)は1項関数、word(ss,p)は2項述語、等と呼ばれることもあります。注 varは特別なword(,s)で \(x\), \(a_{0}\) 等があります。
var以外のwordは数学の教科書において次のように「紹介」されます。
word(ss,p) … \(=\)
word(cc,p) … \(=\)
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 \top\)】\([1][0]\) = \(\neg\)
Formの中でもgramが正しく処理されているものに s-Form, c-Form, p-Form があります。
それらの細かい規則として、例えば
・\({\tt w}\)がword(s,p)，\({\tt S}\)がs-Form ⇒ \({\tt wS}\)がp-Form
【\(\neg P\)】はp-Formにはなっていません…【\(P\)】はs-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})\)】の形で使用されます。
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を作ります。
使われる記号が増え、また一つの記号に多様な使い方を与えることも出てきます。
abbr
{ }形→decent形 にはabbrというデータが使われます。abbrは
abbr0 ≈ abbr1
の形になり、これは「abbr0 を ( abbr1 ) に変形する規則」と捉えられます。
abbr0,abbr1におけるvarは「Formが代入される変数」となります。
abbr …【\(\forall x , y P\)】≈【\(\forall x \forall y ( P )\)】
これが変形規則として使用される際には、\(x,y\) には var が、\(P\) には p-Form が代入されます。
例 【\(\forall x , X ( x \in X )\)】≈【\(\forall x \forall X ( x \in X )\)】
\((P)\) の \((\;)\) は必要です。\(P\) の代入先に \(\forall\) よりprecedの大きいwordが含まれていても働くように。
注意すべきabbr
実際の教科書では次のように書かれ、正確には無限個のabbrが与えられます。1以上の自然数 \({\tt n}\) に対し
abbr …【\(\forall x_{1} , \cdots , x_{\tt n} P\)】≈【\(\forall x_{1} \cdots \forall x_{\tt n} ( P )\)】
サンセリフ体(例えば \({\sf A}\) )が、「Formでない記号列が代入される変数」として使用されます。
abbr …【\(\forall x {\sf A} . P\)】≈【\(\forall x ( x {\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 ) )\)】
{ } 形Formでは表記が特殊になることが多いです。「一定の形の列」に対して表記が与えられます。
clsは単独では表記無しのword(vp,c)で、次の式の右辺はtex表記できません。
abbr …【\(\{ X \mid P \}\)】≈ cls X P
abbr*
{ } は通常は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[arity : q]を含むFormでは束縛varが現れます。例 【\(x = y \Rightarrow \forall x ( x = y )\)】の束縛varは2,3番目の\(x\)
積分では \(\int f(x)dx=\int f(y) dy\) と\(x\)を\(y\)に替えることができます。
束縛varの名前替えでできるFormはもとのFormと同一視されます。
例 【\(\forall x ( x \in A )\)】=【\(\forall y ( y \in A )\)】
clsには次のような使用もあります。左辺は$Xが表記上消える珍しい例です。
abbr …【\(\{ T \mid P \}\)】≈【\(\{ x \mid \exists {\sf X} \, ( ( P ) , x = T ) \}\)】
abbrを使用するとき、右辺にのみ含まれるvar(例えば上の \(x\))には適当なvarを代入します。
例 【\(\{ 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 ) \}\)】
3
cvt
p-Formは一階言語へconvertされねばなりません。convertの結果が等しくなることは ≃ で表します。一階言語ではないword、例えば \(=\) 、に対してはcvtというデータが与えられます。
cvt …【\(X = Y\)】≃【\(\forall x \, ( x \in X \Leftrightarrow x \in Y )\)】
convertにおいては、一度cvtを使った後、新たに使える場所が出てくればそこにも使います(継時使用)。
cvtを適用する際、右辺にのみに現れるvar(例えば上の\(x)\)には適当なvarを代入します。
代入
私たちの言語でも代入が一階言語と同様に定義されます。Form \({\tt F}\) の \({\tt x}\) に \({\tt T}\) を代入したものを \({\tt F}^{\,{\tt x}\,\mapsto\,{\tt T}}\) とします。
私たちの言語では、次のような形で代入を記述することが可能です。
cvt … 【\([ x \mid X ] \, T\)】≃【\(X^{x\,\mapsto\,T}\)】
cvt … 【\(T \in \{ x \mid P \}\)】≃【\(P^{x\,\mapsto\,T}\)】
代入する前に束縛変数の名前替えをする必要があることがあります。
【\(x \in \{ y \mid \exists x \, x \neq y \}\)】=【\(x \in \{ y \mid \exists z \, z \neq y \}\)】=【\(\exists z \, z \neq x\)】
入れ子になっているとき代入計算は内側からやるのが良いです。
例 【\([ y \mid [ x \mid y ] \, z ] \, x\)】≃【\([y \mid y]\,x\)】≃【\(x\)】
外側からやっても結果は同じです。
≃【\([y \mid [u \mid y]\,z] \, x\)】≃【\([u \mid x]\,z\)】≃【\(x\)】
word関数
補助単語の中には word→word の働きをするものがあります。そのような単語は # と一文字になります。txtではword関数とwordの間にスペースを入れません。
tex表記は特殊になるので紹介時に記されます。紹介時にはgramの変換データも記されます。s,c,pを動く変数として\({\tt x}\),\({\tt y}\),\({\tt z}\)等が使われます。表記法データは変化させないものとします。
def … 【\(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表記が困難になるのでやめましょう。
Form内では、word関数 \({\tt f}\) とword \({\tt w}\) に対し \({\tt fw}\) で一つのwordとして扱われます。
defを適用するときには \({\tt f}\) と \({\tt w}\) をそれぞれ一つの記号として扱われます。