単語
私たちは、数学を単語の列を変形していくゲームとみなします。
各単語はtex表記を持ちます。区別するため単語本体をinputコマンドと呼ぶことがあります。私たちが通常目にするのはtex表記ですが、web上でそれをクリックするとinputコマンドが出てきます。
tex表記が同じでも異なる単語があります。inputコマンドが%で始まる単語は、%を除いた単語とtex表記が同じになります。tex表記が無になる単語もあります。
特別なwordとして、ローマ字およびそれらに自然数が下付きしたものをvarとします。例 \(x_0\)
補助的なwordに、 \((\) \()\) \(,\) の3つとtex表記でスペースになる \, と \; があります。
word,tokenは基本的にDBに登録されていきます。
#単語には#varと#Varがあり、サンセリフ体のローマ小文字とローマ大文字になります。例 \({\sf a}\), \({\sf A}\)
wordのgram, preced
補助的でないwordはgramというデータを持ちます。
gram は (gram0, gram1) という形になります。
・gram0 … s,c,p という文字の列、または q
・gram1 … s,c,p のどれか
さらに、arity : gram0の長さ、ただし gram0 : q ⇒ arity : q とされます。
varは gram : (, s) です。
arityが0でないwordはprecedというデータも持ちます。
一般的にprecedは次の順に大きくなります。
word[gram1 : sかc]
word[gram0 : pを含まない、gram1 : p]
word[gram0 : pを含む、gram1 : p]
初等的なword
word(,p) … \(\top\) \(\perp\)word(p,p) … \(\neg\)
word(pp,p) … \(\mathbin\&\) \(,\) \(\mathbin{\rm o\!r}\) \(\Rightarrow\) \(\Longrightarrow\) \(\Leftrightarrow\) \(\Longleftrightarrow\)
word(ss,p) … \(\in\)
word(sc,p) … \(\in\)
word(q,c) … \(\text{cl}\)
word(q,p) … \(\forall\) \(\exists\) \(!\) \(\exists!\)
命題論理のwordのprecedは次の順に大きくなっています。
\(\neg\)
\(\Rightarrow\) \(\Leftrightarrow\)
\(\&\) \({\rm o\!r}\)
\(\Longrightarrow\) \(\Longleftrightarrow\)
\(,\)
同じ意味でもprecedの異なるwordがあります。
単語の検索
inputコマンドの入力に対し、[ ]内にtex表記を、その右に単語の種類を出力します。