2 高レベルの表現
2.1 穴
数学は記号列を変形していくゲームです。「記号列の変形の規則」もまた表現されます。
「規則が使用される際にFormが代入されるもの」を「Formの穴」と言い、次が使用されます。
Formの穴 …
$[lDP]例えば「
\(\mathbin{\rm o\!r}\) の前後をひっくり返す」という規則は
\(P \mathbin{\rm o\!r} Q\) →
\(Q \mathbin{\rm o\!r} P\) と表現できます。(規則としては)
\(X \mathbin{\rm o\!r} Y\) →
\(Y \mathbin{\rm o\!r} X\) でも同じです。
wordの列の穴 …
$_[lDP]以下に出てくる
[ｌDP] は「全角英字1文字の後に数字と ' が0個以上」（
ｘ など）です。
v-Formの穴 …
[ｌDP]v_-Formの穴 …
[ｌDP]_2.2 word alias
一般に
word+として紹介されるwordは高度な表現の為にあり、
FCL変換では
lowerという規則で処理されます。
最も簡単な例に
alias wordがあります。何らかの目的で作られた「
FCL変換では同一視されるword」です。
例えばtex表記だけが違う
\(,\) のaliasがあります。★現状ではまだ
word+(pp,p) …
\(\text{and}\)結合力が異なるだけの論理記号 alias もあります。
word+(pp,p) …
\({\bf ,}\,\) \(\Longrightarrow\) \(\Longleftrightarrow\)lower …
\(P {\bf ,}\, Q\) ≃
\(P , Q\) lower …
\(P \Longrightarrow Q\) ≃
\(P \Rightarrow Q\) lower …
\(P \Longleftrightarrow Q\) ≃
\(P \Leftrightarrow Q\) precedは
\(\neg\) <
\(\forall\) \(\exists\) <
\(\Rightarrow\) \(\Leftrightarrow\) <
\(,\) \(\mathbin{\rm o\!r}\) <
\(\Longrightarrow\) \(\Longleftrightarrow\) <
\({\bf ,}\,\) となっています。
例
\(P \Rightarrow Q \Longleftrightarrow \neg P \mathbin{\rm o\!r} Q\) ≈
\(( P \Rightarrow Q ) \Leftrightarrow ( \neg P \mathbin{\rm o\!r} Q )\) 次の例には注意しましょう。
\(P , Q \Rightarrow R\) ≈
\(P , ( Q \Rightarrow R )\) \(P , Q \mathbin{\rm o\!r} R\) ≈
\(( P , Q ) \mathbin{\rm o\!r} R\) 2.3 word関数
次のwordも良く使用されます。gramの \({\tt x}\),\({\tt y}\),\({\tt z}\) には s,c,p が入ります。
word(p,p) …
\(\neg\)word+(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) …
\({\tt /}\)lower …
\(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃
\(\neg ( A \mathbin{{\sf p}} B )\) \(x \neq y\) の
FCL変換は
\(\neg ( x = y )\) です。式の中では{/}と=の間に
スペースを入れません。
なお
\(\mathbin{{\sf p}}\) は2項記号の穴です。★今後、穴の綴りを整備する予定
2.4 省略表現
省略表現も使用可能です。
FCL変換では
abbrという規則で処理されます（abbr処理はlower処理の前です。）。
abbr …
\(X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈
\(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\) \({\tt n}\) は自然数が代入されるものです。
\({\tt n\,{\text -}\,1}\)なども利用できます。このようなものを処理するのも
formel です。
例
\(x , y \in A\) ≈
\(x \in A , y \in A\) 他にも次のものなどがよく使用され、端的な記述に役立ちます。
\(X \subset Y \subset X\) ≈
\(X \subset Y , Y \subset X\) \(\forall x \in X . x \in Y\) ≈
\(\forall x ( x \in X \Rightarrow x \in Y )\)