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

Posted

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了在Python中实现Prolog统一算法?回溯相关的知识,希望对你有一定的参考价值。

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

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

How can I implement the unification algorithm in a language like Java or 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上的统一。我想我已经回归平方,但我知道在回溯时替换帧会发生一些事情。


添加了当前代码的答案。

http://www.igrok.site/bi/Bi_language.html

http://www.igrok.site/bi/TOC.html

https://github.com/vsraptor/bi/blob/master/lib/bi_engine.py

答案

我将很快总结一下来自Unification Theory的Baader和Snyder关于Handbook of Automated Reasoning的章节:

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

  • 没有参数的常数是一个术语:例如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))

给定两个术语st,一个unifier是一个替换,使st相等。例如。如果我们将替换{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)可以通过应用unifier {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=sv=t取代。
  • 符号冲突:相等的a=bf(X) = g(X)终止失败的过程。
  • 东方:t=X形式的相等,其中t不是另一个变量被翻转到X=t,使得变量在左侧。
  • 发生检查:如果方程的形式为X=tt本身不是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应用小于右侧,所以只要我们看到一个术语为有限结构,它们就不能相等。

另一答案

我比开明更困惑

去过也做过。

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

第一:如果您使用正确的术语,您将获得更好的搜索结果,使用backward chaining而不是Backtracking。例如backward-chaining/inference.py

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

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

第三:实现统一算法的方法不止一种。 一个。您注意到使用转换规则的那个,或者由Baader和Snyder在Unification Theory中记为基于规则的方法,例如:删除分解等 湾我更喜欢通过在这个OCaml Unification Theory或Python example中给出的Baader和Snyder在example中的递归下降统一的算法 C。我见过一些使用排列但目前找不到好的参考。

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

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

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

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

当我想学习如何用函数式语言编写这本书时,有关AI 1 2 3The Programming Languages Zoo的书籍非常宝贵。不得不为LispOCaml安装环境,但值得付出努力。

另一答案

到目前为止,这适用于我提出的所有情况(除了一个需要进行检查的情况,我尚未完成):

def unify_var(self, var, val, subst):
#   print "var> ", var, val, subst

    if var in subst :   
        return self.unify(subst[var], val, subst)
    elif isinstance(val, str) and val in subst : 
        return self.unify(var, subst[val], subst)
    #elif (var occurs anywhere in x) then return failure
    else :
        #print "%s := %s" % (var, val)
        subst[var] = val ; return subst

def unify(self, sym1, sym2, subst):
    #print 'unify>', sym1, sym2, subst

    if subst is False : return False
    #when both symbols match
    elif isinstance(sym1, str) and isinstance(sym2, str) and sym1 == sym2 : return subst
    #variable cases
    elif isinstance(sym1, str) and is_var(sym1) : return self.unify_var(sym1, sym2, subst)
    elif isinstance(sym2, str) and is_var(sym2) : return self.unify_var(sym2, sym1, subst)
    elif isinstance(sym1, tuple) and isinstance(sym2, tuple) : #predicate case
        if len(sym1) == 0 and len(sym2) == 0 : return subst
        #Functors of structures have to match
        if isinstance(sym1[0], str) and  isinstance(sym2[0],str) and not (is_var(sym1[0]) or is_var(sym2[0])) and sym1[0] != sym2[0] : return False
        return self.unify(sym1[1:],sym2[1:], self.unify(sym1[0], sym2[0], subst))
    elif isinstance(sym1, list) and isinstance(sym2, list) : #list-case
        if len(sym1) == 0 and len(sym2) == 0 : return subst
        return self.unify(sym1[1:],sym2[1:], self.unify(sym1[0], sym2[0], subst))

    else: return False

FAIL案件应该失败:

OK: a <=> a : {}
OK: X <=> a : {'X': 'a'}
OK: ['a'] <=> ['a'] : {}
OK: ['X'] <=> ['a'] : {'X': 'a'}
OK: ['a'] <=> ['X'] : {'X': 'a'}
OK: ['X'] <=> ['X'] : {}
OK: ['X'] <=> ['Z'] : {'X': 'Z'}
OK: ['p', 'a'] <=> ['p', 'a'] : {}
OK: ['p', 'X'] <=> ['p', 'a'] : {'X': 'a'}
OK: ['p', 'X'] <=> ['p', 'X'] : {}
OK: ['p', 'X'] <=> ['p', 'Z'] : {'X': 'Z'}
OK: ['X', 'X'] <=> ['p', 'X'] : {'X': 'p'}
OK: ['p', 'X', 'Y'] <=> ['p', 'Y', 'X'] : {'X': 'Y'}
OK: ['p', 'X', 'Y', 'a'] <=> ['p', 'Y', 'X', 'X'] : {'Y': 'a', 'X': 'Y'}
 ================= STRUCT cases ===================
OK: ['e', 'X', ('p', 'a')] <=> ['e', 'Y', ('p', 'a')] : {'X': 'Y'}
OK: ['e', 'X', ('p', 'a')] <=> ['e', 'Y', ('p', 'Z')] : {'X': 'Y', 'Z': 'a'}
OK: ['e', 'X', ('p', 'a')] <=> ['e', 'Y', ('P', 'Z')] : {'X': 'Y', 'Z': 'a', 'P': 'p'}
OK: [('p', 'a', 'X')] <=> [('p', 'Y', 'b')] : {'Y': 'a', 'X': 'b'}
OK: ['X', 'Y'] <=> [('p', 'a'), 'X'] : {'Y': ('p', 'a'), 'X': ('p', 'a')}
OK: [('p', 'a')] <=> ['X'] : {'X': ('p', 'a')}
-----
FAIL: ['e', 'X', ('p1', 'a')] <=> ['e', 'Y', ('p2', 

以上是关于在Python中实现Prolog统一算法?回溯的主要内容,如果未能解决你的问题,请参考以下文章

Prolog中具有单面统一的Quine算法

我怎样才能在Prolog中实现“我是我自己的爷爷”?

如何具体化 Prolog 的回溯状态以执行与 Clojure 中的“lazy seq”相同的任务?

JS 最小到目前为止回溯算法错误

如何在 Prolog 回溯期间获取值列表?

Prolog中的双向链表