prolog - 二分木のHerbrandユニバース、HerbrandベースおよびHerbrandモデル（プロローグ）

Question

二分木のHerbrandユニバース、Herbrand Base、Herbrand Modelとは何ですか？

binary_tree(empty). 
binary_tree(tree(Left,Element,Right)) :- 
     binary_tree(Left), 
     binary_tree(Right). 

Answer 1

Herbrand ユニバースは、特定の署名の基本用語です。多くの Prolog システムには述語 Ground/1 があり、これを使用して項が実際に Ground であるかどうかを確認できます。Ground/1 の定義は、変数を含まないということです:

?- ground(empty).
Yes
?- ground(tree(X,Y,Z)).
No

Herbrand base は、与えられた署名の素数公式です。素数式は、述語または等式です。また、ground/1 を使用して、素数式がグラウンドかどうかを確認することもできます。

?- ground(a = X).
No
?- ground(a = b).
Yes
?- ground(binary_tree(X)).
No
?- ground(binary_tree(tree(empty,n,empty))).
Yes

Herbrand モデルは、宇宙が Herbrand 宇宙であるモデルです。図で見ると、Herbrand モデルは Herbrand ベースのサブセットです。理論には Herbrand モデルがないか、1 つまたは多数の Herbrand モデルがあります。

Horn Clauses には常に Herbrand モデルがあり、特に Herbrand ベース自体である完全な Herbrand モデルは常にモデルです。ホーン節とクラークの等式理論は、独自の最小ヘルブランド モデルも持っています。Herbrand プログラム オペレータの固定点です。プログラム オペレータの特定のプロパティにより、ステージ オメガで固定点に到達できることを示すことができます。

しかし、Herbrand モデルの操作は、ソートされていないため扱いにくいものです。多くのソートされた署名と対応する地上モデルは、より便利です。簡単にするために、また現在のケースで多くのソートされたロジックを避けるために、プログラムが読み取る、つまりツリー要素がペアノ数であると仮定できます。

binary_tree(empty). 
binary_tree(tree(Left,Element,Right)) :- 
    binary_tree(Left),
    tree_element(Element), 
    binary_tree(Right).
tree_element(n).
tree_element(s(X)) :-
    tree_element(X).

次に、バイナリ ツリーの定義は、次の再帰関係につながります。

T_0 = {}
T_n+1 = {binary_tree(empty)} u {binary_tree(tree(s,e,t)) | 
       binary_tree(s) in T_n, 
       tree_element(e) in T_n, 
       binary_tree(t) in T_n } u 
        {tree_element(n)} u {tree_element(s(e)) |
       tree_element(e) in T_n} u T_n

固有の最小 Herbrand モデルは T = union_n T_n となり、これは上記の再帰関係の最小不動点です。何も言われていないようです。