wordの紹介
一般のwordはbookで次のように「紹介」されます。\(\mathbb{W}\)(ss,p) … \(\in\) \(=\)
\(\mathbb{W}_+\)(sc,p) … \(\in\)
\(\mathbb{W}_+\)(cc,p) … \(=\)
この (ss,p) などはgramと呼ばれます。\(\mathbb{W}_+\) は一階言語への翻訳時に要処理であることを意味します。
wordの紹介時に表記法が付くことがあります。
表記法がRのwordは右結合です。例えば
\(\mathbb{W}\)(vp,p)R … \(\forall\) \(\exists\)
があり \(\forall x \forall y P\) ≈ \(\forall x ( \forall y P )\)
表記法がFのword \({\tt w}\) は \({\tt w}\)(\({\tt x}_1\), …, \({\tt x_n}\)) の形で使用されます。
仮に自分のbookで \(\in\) を\(\mathbb{W}\)(ss,p)Fとしたら、常に \(\in ( x , X )\) のように使用しなければなりません。
変数
v-Formはgramが(,s)で \(X\) などがあります。v_-Formはgramが(,c)で \(X\) などがあります。
v^-Formはgramが(,p)で \(P\) などがあります。
.v-Formはgramが(s,s)で \(\mathbin{f}\) などがあります。
.v^-Formはgramが(s,p)で \(\mathbin{p}\) などがあります。
..v-Formはgramが(ss,s)で \(\mathbin{f}\) などがあります。
..v^-Formはgramが(ss,p)で \(\mathbin{p}\) などがあります。
内包記法
Mathelには略記も多く準備されています。略記法の規則はabbrと呼ばれ、これもbookで紹介されます。次のものはクラスを生成する際に多用されます。
\(\mathbb{W}_+\)(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
ここで \(P\) はFormの穴(Formが代入されるもの)です。
そして変換規則の表現内では \(x\) はv-Formではなくv-Formの穴です。
\(\in\), \(\mathsf{cls}\) は定義を持ちませんが、翻訳においては次の規則で同時に処理が行われます。
cvt … \(T \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(T\) を代入したもの
次の翻訳は内側からやる方が楽です。
\(x \in \{ y \mid z \in \{ x \mid x \in y \} \}\) ≃ \(z \in x\)
外側からだと \(\int f(x)dx=\int f(y) dy\) みたいな束縛変数の名前替えが必要になります。
外延記法
\({\tt n}\) を自然数として利用できます。\({\tt n\,{\text -}\,1}\) 等の形にもできます。次のものは指定された元からなる集合を作ります。
\(\mathbb{W}\)(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
ただし s\(^{\tt n}\) は s を\({\tt n}\)個並べたものです。
\(\cdots\) や \({\tt n}\) はしかるべく処理されます。例 \(\{ x , \{ x , y \} \}\) ≈ \(\mathsf{set}_{2} ( x , \mathsf{set}_{2} ( x , y ) )\)
集合は自然にクラスと見なされます。
Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます(sc変換)。
setの定義は次のPropになります。
set\({\tt n}\). … \(\{ x_{1} , \cdots , x_{\tt n} \} = \{ v \mid v = x_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} v = x_{\tt n} \}\)
一階言語への翻訳は複数の段階を経て次になります。
set\({\tt n}\). ≃ \(\forall v \, ( v \in \{ x_{1} , \cdots , x_{\tt n} \} \Longleftrightarrow v = x_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} v = x_{\tt n} )\)
高階表現
Mathelは高階の表現も得意で、例えば否定を作るwordがあります。\(\mathbb{W}_{++}\)(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
これはwordからwordを作る関数のように使用され、引数のwordとの間にスペースは入れられません。
翻訳規則は次です。
lower … \(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃ \(\neg ( A \mathbin{{\sf p}} B )\)
例 \(x \notin X\) ≃ \(\neg ( x \in X )\)
\(=\) についての性質を記述したいとき等に \({=}\) で一つの個体のように扱うことがあります。
Mathelは次のwordと翻訳規則も持ちます。
\(\mathbb{W}_{++}\)([ss,p],p)R … \(:\mathsf{R}\)
lower … \({\mathbin{{\sf p}}} :\mathsf{R}\) ≃ \(\forall x ( x \mathbin{{\sf p}} x )\)
「= は反射律を満たす」ということを次のように表現できます。 \({=} :\mathsf{R}\)
Mathelの翻訳では、まず \(\mathbb{W}_{++}\) を消去し、次に \(\mathbb{W}_+\) を消去します。