Form
私たちは一階言語を拡張し、数学の土台である集合とクラスを平易に扱えるようにします。一階言語での項に当たるものをs-Form、式に当たるものをp-Formとし、さらにc-Formを扱います。
Formのtex表記は【 】内にされます。phpではform_texによりFormのtex commandが計算されます。
特別なwordにvarがあり、ローマ字およびそれらに自然数が付いたものになります。例 \(x_0\)
gram
wordはgramというデータを持ちます。gram は (gram0, gram1) という形になります。
・gram0 … s,c,p の列か vp (vsとかも？)
・gram1 … s,c,p のどれか
また、arity : gram0の長さ、ただし gram0がvsかvp ⇒ arity : q とされます。
varは word(,s) です。var以外のword[arity : 0]はconstと呼ばれます。
例えば word(c,s) や word(p,s) は使用できません。基準はまだわかっていません…
word(,c)とword(s,p)は等価で、後者はほとんど使用されません。
word(ss,p) … \(=\)
word(cc,p) … \(=\)
prefix Form
Formは、wordの列で帰納的に作成されます。
・\({\tt w}\)がword[arity : \(n\)], \({\tt F}_1,\cdots,{\tt F}_n\)がForm ⇒ \({\tt wF}_1\cdots{\tt F}_n\)がForm
・\({\tt w}\)がword[arity : q], \({\tt x}\)がvar, \({\tt F}\)がForm ⇒ \({\tt wxF}\)がForm
\([\;]\)を使うときは入れ子列としてみなされるので、例えば 【\(\neg \neg \top\)】\([1][0]\) = \(\neg\)
Formの中でもgramが正しく処理されているものには s-Form, c-Form, p-Form があります。それらの細かい規則として、例えば
・\({\tt w}\)がword(s,p)，\({\tt S}\)がs-Form ⇒ \({\tt wS}\)がp-Form
【\(\neg P\)】はp-Formにはなっていません…【\(P\)】はs-Formなので。
また正確には
・\({\tt w}\)がword(vp,p), \({\tt x}\)がvar, \({\tt F}\)がp-Form ⇒ \({\tt wxF}\)がp-Form
表記法
arityが0でないwordは表記法データも持ちます。それは次の3種類のどれかになります。
F ! 結合性(LかR)およびprecedの組
! は単独表記を持たないことを意味します。結合性は通常は L です。
word(vp,p)R … \(\forall\) \(\exists\) \(\exists!\)
precedは大小関係に意味があります。デフォルトでは次の値になります。
word[gram1 : sかc] … 300
word[gram0 : s,c以外を含まない、gram1 : p] … 700
word(vp,p) … 750
さらに
\(\neg\) … 730
\(\Rightarrow\) \(\Leftrightarrow\) … 770
\(,\) \(\mathbin{\rm o\!r}\) … 780
\(\Longrightarrow\) \(\Longleftrightarrow\) … 790
decent Form
wordと \((\) \(,\) \()\)の列で、読みやすい形を作ります。word[arity : 2] はinfixにされます。例 【\(P , Q\)】
表記法がFのword [arity : \(n\)] \({\tt w}\) は【\({\tt w}({\tt x}_1,\cdots,{\tt x}_n)\)】の形で使用されます。
後置もできます？
prefixへの変形によって等しくなることを ≈ で表します。
infixでは\((\;)\)が必要になりますが、precedの差を利用して略せることがあります。
例 【\(x = y \Rightarrow y = x\)】≈【\(( x = y ) \Rightarrow ( y = x )\)】
例 【\(P \Rightarrow Q \Longleftrightarrow \neg P \mathbin{\rm o\!r} Q\)】≈【\(( P \Rightarrow Q ) \Longleftrightarrow ( ( \neg P ) \mathbin{\rm o\!r} Q )\)】
内部ではdecent→post→prefixと計算されます。前の→は操車場アルゴリズムform_postにより計算されます。postの状態でparseしてから、post_preにより後の→を計算しています。
L結合性でprecedが等しいものは左から読まれます。例 【\(P , Q , R\)】≈【\(( P , Q ) , R\)】
\(\forall\) はR結合性で 【\(\forall x \forall y P\)】≈【\(\forall x ( \forall y P )\)】
なお、decentでは区別されますが、prefixでは次の同一視をして良いです。
\(\Rightarrow\) ≈ \(\Longrightarrow\)
\(\Leftrightarrow\) ≈ \(\Longleftrightarrow\)
優先順位はphpの記号にもあります。&& = and の順なので
$result = true && false;
var_dump($result); // bool(false)
$result = true and false;
var_dump($result); // bool(true) ←あれ？ってなる