prolog - 二叉树的 Herbrand 宇宙、Herbrand 基础和 Herbrand 模型(序言)

Question

什么是二叉树的 Herbrand 宇宙、Herbrand 基础和 Herbrand 模型:

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

Answer 1

Herbrand 宇宙是给定签名的基本术语。许多序言系统有一个谓词ground/1，你可以用它来检查一个术语是否是实际上是接地的。 ground/1 的定义是它不包含变量:

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

赫布兰德基础是给定签名的基本素数公式。 A素数公式是谓词或等式。您还可以使用地面/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 模型。

Horn Clauses 始终具有 Herbrand 模型，特别是完整的 Herbrand 模型Herbrand 基地本身始终是一个典范。喇叭条款连同克拉克方程理论还有一个独特的最小赫布兰德模型。这是Herbrand 程序算子的固定点。程序的某些属性运算符允许声明可以在 omega 阶段达到固定点。

但是使用 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 ，即上述递推关系的最小不动点。好像什么也没说。