やる事
私たちは、数学を「単なる記号列を変形していくゲーム」とみなします。それを機械に行わせるべく、ルールを決めます。
ルールは完全・厳密でなくても機械化をするのに十分であればOKと考えます。
まずは数学を記述するための数学語を作ります。数学の現場(大学の数学科)で使われる表現をなるべくそのまま使用できるようにします。一階言語を拡張し、数学の土台である集合とクラスを平易に扱えるようにします。一階言語での項に当たるものをs-Form、式に当たるものをp-Formとし、さらにc-Formを扱います。
数学語以外の言語も作ります。どれも人間と機械が使用します。
単語
各言語はその言語の「単語」を持ちます。ほとんどの単語は(単独で)tex表記を持ちます。通常は、私たちが目にするのはtex表記ですが、web上でそれをクリックするとinput(機械への入力時に使用する単語本体)が出てきます。例 \(=\)
tex表記が同じでも異なる単語があります。tex表記が空の単語もあります。
「数学語の単語」をwordと呼びます。wordは正規word、補助wordに分けられます。特別な正規wordにvarがあり、ローマ字およびそれらに自然数が付いたものになります。例 \(x_0\)
補助word単語の例として \((\) \()\) とtex表記の無い { } があります。これらは塊を作るものです。
数学語などを説明するメタ言語でも = や \(=\) を使います。記号はどうしても足らなくなります。変数としてタイプライター体\({\tt x}\)を使います。
gram
正規wordはgramというデータを持ちます。gram は (gram0, gram1) という形になります。
・gram0 … s,c,p の列か vp (vsとかも？)
・gram1 … s,c,p のどれか
また、arity : gram0の長さ、ただし gram0がvsかvp ⇒ arity : q とされます。
varは word(,s) です。var以外のword[arity : 0]はconstと呼ばれます。
例えば word(c,s) や word(p,s) は使用できません。基準はまだわかっていません…
word(,c)とword(s,p)は等価で、後者はほとんど使用されません。
word(ss,p) … \(\in\)
word(sc,p) … \(\in\)
表記法
arityが0でない正規wordは表記法データも持ちます。それは次の3種類のどれかになります。
F ! 結合性(LかR)およびprecedの組
! は単独表記を持たないことを意味します。結合性は通常は L です。
word(vp,p)R … \(\forall\) \(\exists\) \(\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