1
一階言語を拡張しFormというものを作ります。Formはいくつかの形をとりますが、機械にとって処理しやすいprefix形から説明します。
word
prefix Formで使用される記号はwordと呼ばれます。ほとんどのwordは(単独で)tex表記を持ちます。通常、人間が目にするのはtex表記ですが、注釈にtxt(機械への入力時に使用される記号本体)があります。例 \(=\)
tex表記が同じでも異なるwordがあります。例 クラスが等しいことを表す \(=\)
tex表記の無いwordもあります。
wordの列もtex表記およびtxtを持ちます。
txtは各wordのtxtをスペースで区切って並べたものです。例 \(x x\)
gram
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なので)が、一定の用途を持ちます。
2
prefix形は人間には読みにくいので、人間にとってまともな形を作ります。
使われる記号が増え、また一つの記号に多様な使い方を与えることも出てきます。
Form用の記号の列
word以外の記号もFormで使用されます。例 \(,\) （wordの \(,\) と同一表記）列のtxtにおいて ( ) { } の前後ではスペースを略せます。例 \(( x )\)
tex表記を作るためにしか使用されない記号があります。
\, \; \! はそのままtexコマンドとしてスペースを調整します。例 \(x \; x\)
{ } は前に ! をつけるとtexコマンドになります。例 \(x = x\) \(x { = } x\)
_ ^ _{ ^{ はそのままtexコマンドになります。例 \(x ^{ x ^ x }\)
\(x_{1} x_{2} \cdots x_{99}\) なんて表記もできます。
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\)
{ } Form
{ }形という、decent形よりさらに高度な形のFormを作ります。
{ }形→decent形 にはabbrというデータが使われます。abbrは
abbr0 ≈ abbr1
の形になり、これは「abbr0 を ( abbr1 ) に変形する規則」と捉えられます。
abbr内での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
( ) を補わない { } 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 )\)】
3
Formの取り扱いについて色々。
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 {\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 ) \}\)】
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}\) の var \({\tt x}\) に s-Form \({\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}\) をそれぞれ一つの記号として扱われます。
alias
convertされたp-Formは、proverの言語へ翻訳されます。
その際に同一視される記号があり ≅ で表されます。
aliasは証明におけるヒントを与えるためにあり、もとのwordとtex表記,gramなどが同一です。
集合の等号として =s ≅ = を用意し【\(X = \{ x , y \}\)】のように使用します。
一般にtxtで_aをつけたwordは元のwordのaliasになります。