概要
プログラミング言語上で 1階述語論理の言語を実装したい。具体的には「論理式を 冠頭標準形 に変形し スコーレム標準形 を求め、節形式にする手順を実装に落とし込みたい」。そのために必要な 各種検討項目をまとめた。要するに 本稿は 論理プログラミング一歩手前までの数理論理学をプログラムに落とし込むための設計ドキュメントだといってよい。コードは未記載(分量が多いのでQiitaじゃないところに公開するかも)。
想定動作環境: Node上でのJavaScript で動作。依存パッケージは moo(字句解析), nearley (構文解析) のみ。npm i --save moo nearley で環境構築完了。
0. 表記 ～言語の記号～
- 変数は以下が使える:
x,y,z,w,x1,x2, ...x99 - 定数は以下が使える:
a,b,c,a1,a2, ...a99 - 関数は以下が使える:
f,g,h,f1,f2, ....f99 - 述語は以下が使える:
F,G,H,F1,F2, ...,F99 - 括弧とカンマが使える:
(,),, - 論理記号は以下が使える:
- ¬として
!, ⋀として&, ⋁として|, →として->, ↔として:: - ∀xとして
Ax., ∃xとしてEx. - = として
=
- ¬として
論理式の例をいくつか挙げる
- 原子論理式(コードでは prime と呼ぶ)
-
F(a),G(a13),F(a,x),G(f(a),b) -
a=b,x=f(a,g(b)),f(a1,b)=g(a,b,c)
-
- 複合論理式(コードでは compound と呼ぶ)
-
F(a)->G(b)->F(a),F(a)&G(f(b,c)),!F(a)&G(f(b)), Ax.Ey.(x=y -> f(x)=f(y))
-
1. 内部表現
- 構文木は S式を模した Array で表現する
-
f(a, b, c)は[f, a, b, c] -
a=b->F(a)は[->, [=, a, b], [F, a]]
-
- 言語の記号は文字列ではなく Object で表現する
-
xは{ type: 'variable', value: 'x' } -
aは{ type: 'constant', value: 'a' } -
fは{ type: 'function', value: 'f' } -
Fは{ type: 'predicate', value: 'F' } -
=は{ type: 'predicate', value: '=', infix: true } -
!は{ type: 'connective', value: 'not' } -
&は{ type: 'connective', value: 'and', infix: true } -
|は{ type: 'connective', value: 'or', infix: true } -
->は{ type: 'connective', value: 'then', infix: true } -
Ax.は{ type: 'connective', value: 'forAll', boundID: 'x' } -
Ex.は{ type: 'connective', value: 'exists', boundID: 'x' }
-
幾つかの特記事項:
- infix属性で中間記法であることを明示する。構文木を文字列にする際にのみ必要なので内部表現として保持しないという選択肢もあるが、この方式の方が論理記号の追加に対して対応しやすい（ファクトリ関数の修正だけで済む）。
- 量化子は、束縛する変数名を文字列で持つ(boundID)。Objectで持たないということを明示するために属性名にIDを付けている。
- 言語に追加論理記号を足す(例えば
+,-,<,e,0, ...)のは簡単。どうすればよいかを考えてみるとよい。
よって以下を実装すること:
-
toObj: 文字列を受け取り上述のオブジェクトを返す関数
2. 統語的な基本操作
一番最初に必要な 統語的な操作を記載:
-
parse: 文字列を構文木に変更する。moo, nearley, 文法ファイル, toObj を組み合わせて作る -
repr: (人間のために)構文木を文字列にする -
createNode: 構文木を入力として少し変形した構文木を作成する（例: 論理式の否定を作りたい, 二つの論理式の ⋀ をとった論理式を作りたい)。色々な場面で必要な操作なので まとめておくと読みやすいしコードの重複削減に貢献する。
加えて記号, 変数についての操作が必要
-
occurenceOf: 論理式の集合を渡し, 利用されている変数・定数・関数・述語の一覧を取得する。一覧が欲しいというよりも 未使用の記号が知りたいというニーズに応えることが多い。束縛変数をリネームしたい時や スコーレム関数に利用する記号を選択するなど。 -
freeOf,bndOf: 論理式における自由変数と束縛変数の一覧を求める。 -
rearrange: (人間のために) 論理式に登場する非自由な変数を機械的に一括して変更する。(例:Ax12.Ez.x12=f(x23,a, z)をAx.Ey.x=f(x23,a,y)に変更)。純統語的な操作ではないが正当化できる。自由変数をリネームしないのは、他の論理式との兼ね合いがあるため。注: 後述の束縛変数のリネームとは本質的に異なる操作 (例:F(z)->Az.F(z)を考えてみよ)
再帰・帰納の時によく使う操作:
-
isPrimeFormula: 与えられた論理式が原子論理式であることを判定。再帰の終了条件の判定に頻出。 -
isOpenFormula: 与えられた論理式に量化子が入っていないことを判定。再帰の終了条件の判定に頻出（特にPNF, SNFまわり)。
3. 統語的な応用操作
統語的な操作ではあるが、その定義に意味論的・証明論的なバックグラウンドを持つ各種操作をまとめる。
-
boundRename: 指定した束縛変数名を変更する操作。α同値性がバックグラウンドになっている（例:F(z) -> Az.F(z)はF(z) -> Ax.F(x)）。 -
substitiute: 代入操作。t/x と表記され 1つの変数x を1つの項t に置き換える帰納的操作。帰納的に定義されるが (∀xφ)[t/x] = ∀xφ, (∀yφ)[t/x] = ∀y(φ[t/x]) となることには注意。代入は 完全に統語的な操作であるが 無制限に代入操作をすることは(統語論的ではなく)意味論的・証明論的に許されない (例: y/x を ∃y¬(x=y) に施すと ∃y¬(y=y) になる。統語的には正しい挙動であるが、意味論的・証明論的には許容できない）。代入はスコーレム化の際に使う。 -
isCollisionFree: 上述のように 代入結果が変にならないための判定関数。「変になる」とは完全に意味論的・証明論的な概念だが、その判定自身は統語的に定義可能である。isCollisionFree(formula, term, variableName) というシグネチャを持つ。「論理式φが代入t/xに対してcollision-freeな場合t/xを行うと・・・・」というような意味論的・証明論的な規則を作るために利用。
4. 意味論的操作
意味論的同値関係を用いて論理式を変形する操作をまとめる
-
toPNF: 冠頭標準形への変形。意味論的同値性を再帰的に適用することで、量化子が論理式の先頭にのみ存在するように変形できる。同値変形の際に衝突判定を回避する変数を選ぶ必要があるが、もっと緩く未使用の変数を採用すればよい。利用する同値性:- ¬∀xφ = ∃x¬φ
- 未使用の変数y で ∀xφ⋀ψ = ∀y(φ[y/x]⋀ψ), ∀xφ⋀ψ = ∀y(φ[y/x]⋀ψ)
- 未使用の変数y で ∀xφ⋁ψ = ∀y(φ[y/x]⋁ψ), ∃xφ⋁ψ = ∃y(φ[y/x]⋁ψ)
- 未使用の変数y で ∀xφ→ψ = ∃y(φ[y/x]→ψ), ∃xφ→ψ = ∀y(φ[y/x]→ψ)
- 未使用の変数y で φ→∀xψ = ∀y(φ→ψ[y/x]), φ→∃xψ = ∃y(φ→ψ[y/x])
-
toSNF: スコーレム標準形への変形。意味論的同値性ではなく充足的同値性による式変形により、∀論理式に変形する。内部的には一度 toPNF を呼び出して冠頭標準形にしたのち、 occurenceOf で未使用の定数や変数の一覧を取得して帰納的に変形する。∀式にしたら、それを節形式にする(つまりCNFにする）のだが、ここまでくれば命題論理の方法が使える。
5. 最短ルート
目的が「任意の論理式を節形式にする」のであれば、前述したいくつかの操作は不要で、最低限必要な以下の操作を実装すればOK。parse, occurenceOf, substitiute, toPNF, toSNF。補助的に createNode, isPrimeFormula, isOpenFormula。あと確認用に repr, rearrange。何が言いたいかというと、自由変数/束縛変数/非衝突判定/束縛変数のリネームといった数理論理学で必要な概念は節形式にする上では不要だということ。言語で使用していない記号の一覧が occurenceOf で得られるので、衝突回避な代入は簡単に求まるという事情による。
最後に
議論・コメント・要望・指摘なんでも歓迎です。