Mathel
当システムで数学を記述する言語がMathelです。\(\dagger\)私たちは「分かりやすさ」「表現力の高さ」を追求しその開発をしました。
数学の基本概念は集合とクラスですが、Mathelではそれらを容易に明晰に扱えます。
なお「集合やクラスとは何か」には一切触れません。\(\dagger\)
次の例から見て下さい。
\(x \in X\)
青字のtex表記をクリックすると注釈にtxtと呼ばれるものが出てきます。
以下の説明を読むにあたっても、こまめにクリックをして確認して下さい。
2つの情報を持たせられることはwebの利点ですね？
wordとForm
Mathelで使われる記号をwordと言います。ほとんどのwordはライブラリで「紹介」されます。例えば
word(ss,p) … \(\in\)
この (ss,p) はgramと呼ばれます。gramに現れる型には v,s,c,p があります。\(\dagger\)
tex表記は同じでも異なるwordがあります。次のwordはMathelの肝と言えます。
word(sc,p) … \(\in\)
「wordの列」のうち文法をみたすものをFormと呼びます。
s-Form, c-Form, p-Formがあり、特別なs-Formにv-Formがあります。
\(X\) はv-Formで、最初の例はp-Formです。
結合力の差は自然に利用されます。例 \(x = y \Rightarrow y = x\) ≈ \(( x = y ) \Rightarrow ( y = x )\)
txtにおいて半角スペースはwordの区切りを意味しますが ( ) の前後では略せます。
特殊なword
Russelクラス \(\{ x \mid x \notin x \}\) がc-Formになることも見ていきましょう。{ } で挟まれたwordは「wordからwordを作る関数」のように働きます。
word(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
これで \(\notin\) はword(ss,p)になります。
次のwordは(単独では)tex表記を持ちません。
word(vp,c) … cls
なお {/} や {cls で { の後に半角スペースを入れてはいけません。
メタ自然数も利用されます。1以上の自然数 \({\tt n}\) に対して
word(s\(^{\tt n}\),s) … set\({\tt n}\)
ただし s\(^{\tt n}\) は s を\({\tt n}\)個並べたものです。
Formのtxtでは\({\tt n}\)は略せます。s-Form \(\{ x , \{ y \} \}\) ではset2とset1が使用されています。
\, \; \! { } _ ^ はtex cmdになるだけのwordです。
\(\text{id}\) というword(s,s)があります。「\(X\)上の恒等写像」は \(\text{id} X\) ではなく \(\text{id} _ X\) とされることが多いです。
\(x_{1} x_{2} \cdots x_{99}\) なんてのも使用されます。
abbr
Mathelでは省略記法も使用できます。その処理するための abbr という規則があります。例えば
abbr … \(\{ x \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , ( P ) \}\)
例 \(\{ x \in X \mid x \neq 0 \}\) ≈ \(\{ x \mid x \in X , x \neq 0 \}\)
なお \(( P )\) の \(( )\) は塊を維持するために必要です。
{ } は通常はFormとしての塊を作りますが、稀にその塊を崩すこともあります。
abbrを使用するときは ( ) を補いますが、補わないものは abbr* とされます。
pileというwordはtex表記が無く、次のabbr*はtex表記からは何が何だか。
abbr* … \( X\) ≈ \(X , X\)
例 \(x \in X \in \mathcal{X}\) ≈ \(x \in X , X \in \mathcal{X}\)