1 cvt変換

1.1 クラスの基本

Matheliaはc-Form(クラス)をs-Form(もの)の集まりとして扱うことに特化しています。
「属する」が基本になります。
word(sc,p) … \(\in\)
\(x \in X\) はp-Formになります。「\(x\)というものがクラス\(X\)に入っている」と読むと良いでしょう。
\(=\) にも定義が与えられます。
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)

〇. は自然に cvt(〇.) という規則を生成します。例えば cvt(=_.) は
cvt … \(X = Y\) ≃ \(\forall x \, ( x \in X \Leftrightarrow x \in Y )\)

1.2 内包記法

内包記法はクラスを生成する標準的な道具です。自然な形で使用できるようにしておきます。
word(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)

次の cvt(cls.) という規則が重要です（cls.自体はありません）。
cvt … \(t \in \{ x \mid P \}\) ≃ substitution(\(P\), \(x\) ↦ \(t\))
例　 \(\mathrm{a} \in \{ x \mid x \subset X \}\) ≃ \(\mathrm{a} \subset X\)

1.3 アロー関数

\(\in\) と \(\mathsf{cls}\) はp-Formへのs-Formのsubstitutionを作る道具でしたが、s-Formへのs-Formのsubstitutionも可能にします。
word(vs,(s,s))F … \(\mathsf{fn}\)
abbr … \(\lceil x \mapsto X \rfloor\) ≈ \(\mathsf{fn} ( x , X )\)
次の cvt(fn.) という規則が重要です（fn.自体はありません）。なおソースの ｢ ｣ は半角のかぎ括弧です。
cvt … \(\lceil x \mapsto X \rfloor ( t )\) ≃ substitution(\(X\), \(x\) ↦ \(t\))
例　 \(\lceil x \mapsto x + a \rfloor ( b )\) ≃ \(b + a\)

\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。
例　 \(\lceil \bullet + a \rfloor\) ≈ \(\lceil x \mapsto x + a \rfloor\)
\(\lceil \bullet \rfloor\) は恒等写像です。
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例　 \(\lceil \bullet + \lceil \bullet + a \rfloor ( x ) \rfloor\) ≈ \(\lceil \bullet + ( x + a ) \rfloor\)

1.4 cvt変換

Book内の自動変数 \(\mathbb{W}_\mathrm{c}.\) は「〇. （〇 は gram に c を含む）という形の prop すべての列」です。この時点では \(\mathbb{W}_\mathrm{c}.\) は =_. のみです。
|cvt が「cvt(〇.) (〇は\(\mathbb{W}_\mathrm{c}.\), cls., fn.) を最大限繰り返し適用したもの」として定義されています。
例　 \(X = \{ x \mid x \in X \}\) |cvt … \(\forall x \, ( x \in X \Leftrightarrow x \in X )\)