私たちは、数学を「単なる記号列を変形していくゲーム」とみなします。それを機械に行わせるべく、ルールを決めます。
数学の現場(大学の数学科)で使われる表現を、なるべくそのまま使用できるようにします。
web上でクリックすると出てくるものを注釈と言います。クイズなんかもできます。今日は？
記号の列
このシステムでは数学記号の列を扱います。ほとんどの数学記号は(単独で)tex表記を持ちます。通常、人間が目にするのはtex表記ですが、注釈にtxt(機械への入力時に使用される記号本体)があります。例 \(=\)
tex表記が同じでも異なる記号があります。例 クラスが等しいことを表す \(=\)
tex表記の無い記号も多くあります。
記号列もtex表記およびtxtを持ちます。txtは各記号のtxtをスペースで区切って並べたものです。例 \(x x\)
\((\) \()\) や { } の前後ではスペースを略せます。例 \(( x )\)
tex表記を作るためにしか使用されない記号があります。
\, \; \! はtex表記でスペースを調整します。例 \(x \; x\)
\(x_{1} x_{2} \cdots x_{99}\) なんて表記もできます。
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_{0}\) や
通常、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は表記法データも持ちます。それは次の3種類のどれかになります。
F ! 結合性(LかR)およびprecedの組
! は(単独では)表記を持たないことを意味します。結合性は通常は L です。
word(vp,p) … \(\forall\) \(\exists\) \(\)
precedは大小関係に意味があります。デフォルトでは次の値になります。
word[gram1 : sかc] … 300
word[gram0 : s,c以外を含まない、gram1 : p] … 700
word(vp,p) … 750
さらに
\(\neg\) … 730
\(\Rightarrow\) \(\Leftrightarrow\) … 770
\(,\) \(\mathbin{\rm o\!r}\) … 780
\(\Longrightarrow\) \(\Longleftrightarrow\) … 790
\({\bf ,}\) … 800
decent Form
wordと \((\) \(,\) \()\)の列で、読みやすい形を作ります。word[arity : 2] はinfixにされます。例 【\(P , Q\)】
\(\forall\) はinfixにはされません。例 【\(\forall x P\)】
表記法がFのword [arity : \(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 )\)】
なお、decentでは区別されますが、prefixでは次の同一視をして良いです。
\(\Rightarrow\) ≈ \(\Longrightarrow\)
\(\Leftrightarrow\) ≈ \(\Longleftrightarrow\)
Formの同値
word[arity : q]から始まるFormの中にあるvarは束縛varと言われます。【\(x = y \Rightarrow \forall x ( x = y )\)】の2,3番目の\(x\)は束縛varです。
積分では \(\int f(x)dx=\int f(y) dy\) と\(x\)を\(y\)に替えることができます。
束縛varの名前替えでできるFormはもとのFormと同一視されます。
例 【\(\forall x ( x \in A )\)】=【\(\forall y ( y \in A )\)】
詳しい定義は補足のページで。
3
Formのdecent形よりさらに高度な（人間にとってありがたい）形を作ります。
使われる記号が増え、また一つの記号に多様な使い方を与えることも出てきます。
$変数
「記号列の変換の規則」も記号列としてシステムに記述できるようにします。
記号(列)が代入されるものとして $var, $Var, $.var, $..var を導入します。txtは$で始まり、ローマ字およびそれらに自然数が付いたものになります。tex表記はサンセリフ体です。例 \({\sf a}\) \({\sf A}\) \(\mathop{{\sf a}}\) \(\mathop{{\sf a}}\)
【\(\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] が代入されます。その他の代入条件が課されることもあります(？)。
abbrによる超decent Form
一定の変形によってdecent Formになるものを超decent Formと言います。
超decent Formのtxtでは、塊を作るために { } が使われます。
decentへの変形にはabbrというデータが使われます。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} ) )\)】
例 【\(\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*による超decent form
{ } は通常はFormとしての塊を作りますが、稀に塊を崩すこともあります。
( ) を付けずに「abbr0 を abbr1 に変形する規則」と捉えらるものは abbr* とされます。
abbr* …【\( {\sf X}\)】≈【\({\sf X} , {\sf X}\)】
例 【\(x \in y\)】≈【\(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 )\)】
特殊表記
超decent Formでは表記が特殊になることが多いです。「一定の形の列」に対して表記が与えられます。clsは単独では表記無しのword(vp,c)で、次の式の右辺はtex表記できません。
abbr …【\(\{ {\sf X} \mid {\sf P} \}\)】≈ cls $X $P
次の左辺は$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 ) \}\)】
メタ自然数の利用
次の式は正確には無限個のabbrを生成します。abbr … 【\(\forall {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf P}\)】≈【\(\forall {\sf x}_{1} \cdots \forall {\sf x}_{\tt n} ( {\sf P} )\)】
例 【\(\forall x , y \, ( x = y )\)】≈【\(\forall x \, \forall y \, ( x = y )\)】
setはFormの中での使用され方でgramが変わるwordで、教科書では word(s\(^{\tt n}\),s)とされています。
abbr … 【\(\{ {\sf X}_{1} , \cdots , {\sf X}_{\tt n} \}\)】≈ set $X1 … $Xn
例えば【\(\{ x , \{ x , y \} \}\)】はs-Formで、現れる2つのsetはword(ss,s)です。