云昴(Mao Yun)

[Learn Prolog Now 2] Unification and Proof Search

| Prolog

本文英文原文: http://www.learnprolognow.org/ 并会增加自己在Imperial学习中的一些想法,因为自己已经熟悉Prolog,并非完整翻译。

合一

  1. 如果term1和term2都是常量,那么term1和term2能够合一,当且仅当它们是相同的原子,或者相同的数字。

  2. 如果term1是变量并且term2是任意类型的语句,那么term1和term2能够合一,并且term1被初始化为term2;同理,如果term2是变量并且term1是任意类型的语句,那么term1和term2能够合一,并且term2被初始化为term1。(如果两个都是变量,他们都能够被互相初始化,即它们共享相同的值)

  3. 如果term1和term2都是复杂语句,那么它们能够合一当且仅当:

    3.1 它们有相同的函子和元数;

    3.2 所有对应的参数能够合一;

    3.3 变量的初始化能够匹配。(比如,如果两个复杂语句在进行合一,不可能在一个复杂语句中将X初始化为mia,在另外一个复杂语句中将X初始化为vincent)

  4. 两个语句能够合一当且仅当它们遵循上面三个定义之一。

特殊的例子1

?- X = Y.

Prolog会如何回答?这依赖不同的Prolog实现,在我的机器上,SWI-Prolog会回答:

X = Y

即简单地认为X和Y可以合一,因为变量可以和任意类型的语句合并,如果变量和变量合一,表示它们分享同样的值。另外,可能其他Prolog实现会这么回答:

X = _5071

Y = _5071

true

这里发生了什么?本质上,和之前的第一个回答是一致的。注意_5071是一个变量(以下划线开头),合一的定义子句2告诉我们,如果两个变量合一,它们会共享一个值,所以Prolog就创建了一个新的值(名字是_5071),X和Y都共享这个值。不必在意_5071的实际值,它仅仅是表示X和Y有相同的值,这个值可能是另外的变量,比如_5075,或者_6189。

特殊的例子2

?- X = mia, X = vincent.

Prolog会回答false。这个查询包含了两个目标,X = mia和 X = vincent,分开来看,Prolog会认为两个目标都成功,首先将X初始化为mia,然后是vincent。但是这里存在问题:一旦Prolog尝试满足第一个目标,X被初始化为mia,它就不能再和vincent合一了(变量只能初始化一次)。所以第二个目标会失败,一个已经初始化的变量不再是变量了,它已经变成了它初始化的值。

云昴(Mao Yun)