在Python中实现Prolog统一算法?回溯 [英] Implementing the Prolog Unification algorithm in Python? Backtracking

问题描述

我正在尝试实现统一，但是遇到问题..已经有很多示例，但是他们要做的只是弄混水.我比开悟更困惑:

I'm trying to implement Unification, but having problems.. already got dozen of examples,but all they do is to muddy the water. I get more confused than enlightened :

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

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

https://www.doc.ic.ac.uk/~sgc/teaching/pre2012/v231/lecture8.html [code below is based on this intro]

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

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

如何可以用Java或C#这样的语言实现统一算法吗?

Prolog的一门艺术……还有其他几门. 最大的问题是我无法清楚地说明问题.更多的数学或狡猾的解释让我更加困惑.

The art of Prolog one ...and several others. The biggest problem is that I could not figure clear statement of the problem. More mathy or lispy explanations are confusing me even more.

作为一个好的开始，遵循表示形式是基于列表的一个好主意(就像在lispy中一样):

As a good start it seems a good idea to follow the representation to be list based (like in the lispy cases) i.e. :

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

除了您如何表示列表本身！?即[H | T]

except how do you represent lists themselves !? i.e. [H|T]

如果您能向我展示Python伪代码和/或更详细的算法描述或指向它的指针，我将非常乐意.

I would love if you can show me a Python pseudo code and/or more detailed algorithm description or a pointer to one.

我掌握的一些要点是需要将通用统一代码和var统一代码分开，但随后我看不到相互影响的情况！ ...等等.

Some points I grasp is the need to separate the code in general-unifier and var-unification, but then I cant see the mutual-recusive case ! ... and so on.

作为旁注:我也很想提您如何处理回溯统一.我想我已经回溯了平方根，但是我知道回溯中的替代帧必须发生一些事情.

As a side note : I would also love for you to mention how would you handle Unification on Backtracking. I think I have backtracking squared-away, but I know something has to happen to substitution-frame on backtracking.

使用当前代码添加了答案.

Added an answer with the current code.

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

推荐答案

我将快速总结有关自动推理手册:

术语由常量(以小写字母开头)和变量(以大写字母开头)构建而成:

Terms are built from constants (starting with a lower case letter) and variables (starting with an upper case letter):

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

• a constant without arguments is a term: e.g. car
• a constant with terms as arguments, a so called function application, is a term. e.g. date(1,10,2000)
• a variable is a term, e.g. Date (variables never have arguments)

替代是将术语分配给变量的映射.在文献中，这通常写为{f(Y)/X, g(X)/Y}或带有箭头{X→f(Y), Y→g(X)}.对术语应用替换将用列表中的相应术语替换每个变量.例如.上面对tuple(X,Y)的替换产生了tuple(f(Y),g(X))项.

A substitution is a map assigning terms to variables. In the literature, this is often written as {f(Y)/X, g(X)/Y} or with arrows {X→f(Y), Y→g(X)}. Applying a substitution to a term replaces each variable by the corresponding term in the list. E.g. the substitution above applied to tuple(X,Y) results in the term tuple(f(Y),g(X)).

给出两个术语s和t， unifier 是使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.最简单的此类统一符称为最通用的统一符.就我们的目的而言，足以知道我们可以将自己限制在这种最通用的统一符的搜索上，并且如果存在，它是唯一的(最多包含某些变量的名称).

Given two terms s and t, a unifier is a substitution that makes s and t equal. E.g. if we apply the substitution {a/X, a/Y} to the term date(X,1,2000), we get date(a,1,2000) and if we apply it to date(Y,1,2000) we also get date(a,1,2000). In other words, the (syntactic) equality date(X,1,2000) = date(Y,1,2000) can be solved by applying the unifier {a/X,a/Y}. Another, simpler unifier would be X/Y. The simplest such unifier is called the most general unifier. For our purposes it's enough to know that we can restrict ourselves to the search of such a most general unifier and that, if it exists, it is unique (up to the names of some variables).

Mortelli和Montanari(请参阅本文的2.2节及其中的参考文献)给出了一组规则，用于计算这种最通用的统一符(如果存在).输入是一组术语对(例如{f(X，b)= f(a，Y)，X = Y})，输出是最通用的统一符(如果存在)或失败(如果不存在).在此示例中，替换{a/X，b/Y}将使第一对相等(f(a,b) = f(a,b))，但是第二对将不同(a = b不正确).

Mortelli and Montanari (see section 2.2. of the article and the references there) gave a set of rules to compute such a most general unifier, if it exists. The input is a set of term pairs (e.g. { f(X,b) = f(a,Y), X = Y } ) and the output is a most general unifier, if it exists or failure if it does not exist. In the example, the substitution {a/X, b/Y} would make the first pair equal (f(a,b) = f(a,b)), but then the second pair would be different (a = b is not true).

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

The algorithm nondeterministically picks one equality from the set and applies one of the following rules to it:

• 小数:等式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应用于所有其他问题.

• Trivial: an equation s = s (or X=X) is already equal and can be safely removed.
• Decomposition: an equality f(u,v) = f(s,t) is replaced by the equalities u=s and v=t.
• Symbol Clash: an equality a=b or f(X) = g(X) terminates the process with failure.
• Orient: an equality of the form t=X where t is not another variable is flipped to X=t such that the variable is on the left side.
• Occurs check: if the equation is of the form X=t, t is not X itself and if X occurs somewhere within t, we fail. [1]
• Variable elimination: of we have an equation X=t where X does not occur in t, we can apply the substitution t/X to all other problems.

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

When there is no rule left to apply, we end up with a set of equations {X=s, Y=t, ...} that represents the substitution to apply.

还有更多示例:

• {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)}，失败并进行检查

• {f(a,X) = f(Y,b)} is unifiable: decompose to get {a=Y, X=b} and flip to get {Y=a, X=b}
• {f(a,X,X) = f(a,a,b)} is not unifiable: decompose to get {a=a,X=a, X=b}, eliminate a=a by triviality, then eliminate the variable X to get {a=b} and fail with symbol clash
• {f(X,X) = f(Y,g(Y))} is not unifiable: decompose to get {X=Y, X=g(Y)}, eliminate the variable X to get {Y=g(Y)}, fail with occurs check

即使该算法是不确定性的(因为我们需要选择一个等式进行处理)，顺序也不重要.因为您可以执行任何顺序，所以永远不必撤销工作并尝试使用其他方程式.这种技术通常称为回溯，是Prolog中的证明搜索所必需的，但不是统一本身所必需的.

Even though the algorithm is non-deterministic (because we need to pick a equality to work on), the order does not matter. Because you can commit to any order, it is never necessary to undo your work and try a different equation instead. This technique is usually called backtracking and is necessary for the proof search in Prolog, but not for unification itself.

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

Now you're only left to pick a suitable data-structure for terms and substitutions and implement the algorithms for applying a substitution to a term as well as the rule based unification algorithm.

[1]如果尝试求解X = f(X)，我们将看到X的形式必须为f(Y)才能应用分解.这导致解决问题f(Y) = f(f(Y))，随后又解决了Y = f(Y).由于左侧总是比右侧少应用f，因此只要我们将术语视为有限结构，它们就不能相等.

[1] If we try to solve X = f(X), we would see that X needs to be of the form f(Y) to apply decomposition. That leads to solving the problem f(Y) = f(f(Y)) and subsequently Y = f(Y). Since the left hand side always has one application of f less than the right hand side, they can not be equal as long we see a term as a finite structure.

这篇关于在Python中实现Prolog统一算法?回溯的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！