在Python中实现Prolog统一算法？回溯

Question

我正在尝试实施统一,但遇到问题......已经有很多例子,但他们所做的只是浑水.我比开明更困惑:

http://www.cs.trincoll.edu/~ram/cpsc352/notes/unification.html

https://www.doc.ic.ac.uk/~sgc/teaching/pre2012/v231/lecture8.html [以下代码基于此介绍]

http://www.cs.bham.ac.uk/research/projects/poplog/paradigms_lectures/lecture20.html#representing

https://norvig.com/unify-bug.pdf

如何在Java或C#等语言中实现统一算法？

Prolog的艺术......还有其他几个.最大的问题是我无法清楚地说明问题所在.更多的肮脏或lispy解释让我更加困惑.

作为一个良好的开端,遵循基于列表的表示似乎是个好主意(例如在lispy情况下),即:

pred(Var, val)  =becomes=> [pred, Var, val] 
p1(val1, p2(val2, Var1)) ==> [p1, val1, [p2, val2, Var1]]

除了你如何表示自己的名单!即[H | T]

我很乐意,如果你能告诉我一个Python伪代码和/或更详细的算法描述或指向一个.

我掌握的一些要点是需要在通用 - 统一和变量统一中分离代码,但后来我无法看到相互背叛的情况!... 等等.

---

作为旁注:我也很乐意提到你如何处理Backtracking上的统一.我认为我已经回归平方,但我知道在回溯时替换帧会发生一些事情.

---

添加了当前代码的答案.

Answer 1

我将从"自动推理手册"中快速总结Baader和Snyder 关于统一理论的章节:

术语是从常量(以小写字母开头)和变量(以大写字母开头)构建的:

• 没有参数的常数是一个术语:例如 car
• 一个带有术语作为参数的常量,一个所谓的函数应用程序,是一个术语.例如date(1,10,2000)
• 变量是一个术语,例如Date(变量永远不会有参数)

一个替代是一个地图分配方面的变量.在文献中,这通常{f(Y)/X, g(X)/Y}用箭头写成或用箭头写成{X?f(Y), Y?g(X)}.将替换应用于术语会将每个变量替换为列表中的相应术语.例如,上面的替换适用tuple(X,Y)于该术语的结果tuple(f(Y),g(X)).

鉴于两个术语s和t,一个统一者是一种替代,使得s和t相等.例如,如果我们将替换{a/X, a/Y}应用于该术语date(X,1,2000),我们就会得到date(a,1,2000),如果我们应用它,date(Y,1,2000)我们也会得到date(a,1,2000).换句话说,(语法)相等date(X,1,2000) = date(Y,1,2000) 可以通过应用统一器来解决{a/X,a/Y}.另一个更简单的统一者将是X/Y.最简单的这种统一者称为最通用的统一者.出于我们的目的,我们可以将自己局限于搜索这样一个最通用的统一者,并且如果它存在,它就是唯一的(取决于某些变量的名称).

Mortelli和Montanari(参见文章的第2.2节和那里的参考文献)提供了一组规则来计算这种最通用的统一者(如果存在的话).输入是一组术语对(例如{f(X,b)= f(a,Y),X = Y})并且输出是最通用的统一者(如果存在)或失败(如果它不存在).在该示例中,替换{a/X,b/Y}将使第一对等于(f(a,b) = f(a,b)),但是第二对将是不同的(a = b不是真的).

该算法不确定地从集合中选择一个等式并对其应用以下规则之一:

• 琐碎:方程s = s(或X=X)已经相等,可以安全地删除.
• 分解:一个平等f(u,v) = f(s,t)是由平等更换u=s和v=t.
• 符号冲突:相等a=b或f(X) = g(X)终止进程失败.
• 东方:以下形式的等式t=X,其中t不另一个变量被翻转到X=t使得可变是在左侧.
• 发生检查:如果等式是形式X=t,t不是X自身,如果X发生在某个地方t,我们就会失败.[1]
• 变量消除:我们有一个公式X=t,其中X不发生t,我们就可以替代适用t/X于所有其他问题.

当没有规则要申请时,我们最终得到一组{X=s, Y=t, ...}表示要应用的替代的方程式.

以下是一些例子:

• {f(a,X) = f(Y,b)} 是统一的:分解得到{a = Y,X = b}并翻转得到{Y = a,X = b}
• {f(a,X,X) = f(a,a,b)}是不可统一的:分解得到{a = a,X = a,X = b},a=a通过无关紧要的消除,然后消除变量X得到{a=b}和失败与符号冲突
• {f(X,X) = f(Y,g(Y))}是不可统一的:分解得到{X=Y, X=g(Y)},消除变量X得到{Y=g(Y)},失败与发生检查

即使算法是非确定性的(因为我们需要选择相等的工作),顺序无关紧要.因为您可以承诺任何订单,所以无需撤消您的工作并尝试使用其他等式.这种技术通常称为回溯,对于Prolog中的证明搜索是必需的,但对于统一本身则不然.

现在,您只需为术语和替换选择合适的数据结构,并实现将替换应用于术语的算法以及基于规则的统一算法.

[1]如果我们试图解决X = f(X),我们会看到X需要f(Y)采用分解的形式.这导致解决问题f(Y) = f(f(Y))并随后解决Y = f(Y).由于左侧总是有一个f小于右侧的应用,所以只要我们将术语看作有限结构,它们就不能相等.

Answer 2

我比开明更困惑

去过也做过.

注意:对于引用的任何源代码,我没有测试代码并且不能说它是有效的,它们是作为示例给出的,并且看起来足够正确,我将加载它们并针对它们运行测试用例以确定它们的有效性.

第一:如果您使用正确的术语,使用反向链接而不是回溯,您将获得更好的搜索结果.例如,后向链接/ inference.py

第二:了解您的问题列出了三个单独的阶段.
1.统一算法
2.使用统一的后向链接
3.列表的数据结构.您不会将其实现为Python源代码,而是将其作为要传递给函数的文本.见:缺点

在进行反向链接之前,您应首先开发并完全测试统一.然后在创建列表数据结构之前完全开发并测试反向链接.然后完全测试您的列表数据结构.

第三:实现统一算法的方法不止一种.
一个.您注意到使用转换规则的那个,或者Baader和Snyder 在统一理论中记为基于规则的方法,例如删除分解等 .我喜欢所指出的算法统一由递归下降的统一理论的巴德尔和斯奈德在这个OCaml中给出的例子或Python的例子 ℃.我见过一些使用排列但目前找不到好的参考.

第四:根据个人经验,首先使用笔和纸了解每个阶段的工作原理,然后在代码中实现它.

第五:同样从个人经验来看,有很多关于如何做到这一点的信息,但是数学和技术论文可能会让人感到困惑,因为许多人对自学者至关重要的东西有所掩盖.我建议您专注于查找源代码/数据结构的实现并使用它来学习.

第六:将您的结果与实际工作代码进行比较,例如SWI-Prolog.

在进入下一阶段之前,我不能强调你需要多少测试每个阶段,并确保你拥有一套完整的测试用例.

当我想学习如何用函数式语言编写这本书时,关于AI 1 2 3和编程语言动物园的书籍是非常宝贵的.不得不为Lisp和OCaml安装环境,但值得付出努力.