标签: unification

我对统一的理解有点不完整.我理解基本的统一,但是我遇到了一些问题,但是我的问题并非一致.

我正在观看关于统一的youtube教程,该教程说明如果变量试图与包含该变量的术语进行统一,那么它就不是统一的.

然而,当我输入?- f(X) = Xprolog时,它返回的内容符合......f(f(f(f(f(f(...)))))) ?

我明白为什么会这样......但是我不明白这是否意味着它是不可统一的,正如我所预料的那样,如果它不是可以统一的话,它就会返回'不'.我是否正确地认为尝试统一f(X)= X会失败发生检查,从而使它们不能统一？

我想了解 SICStus 风格的可扩展统一。在用户手册上的library(atts)规定：

Module:verify_attributes(-Var, +Value, -Goals) 钩

...
verify_attributes/3可能会调用任意的 Prolog 目标，但Var不应受其约束。绑定Var将导致未定义的行为。
...
在单个统一绑定多个属性变量的情况下，首先撤消所有此类绑定，然后对每个相关变量执行以下操作：

1. 对于每个相关模块M，都会M:verify_attributes/3被调用，收集返回的Goals.
2. 重做变量绑定。
3. 任何Goals被称为。
4. 任何在变量上阻塞的目标，现在已经解除阻塞，都会被调用。

到目前为止，我想出了对上述内容的以下解释：

• 不同的verify_attribute/3处理程序挂钩Var，看到相同的状态Var：所有看到它“pre_unify”。

• verify_attribute/3不能绑定Var，但可以绑定其他属性变量。

• 这些绑定也将被延迟，以便处理程序不仅看到 的相同状态Var，而且看到所有涉及的属性变量。

  上面的操作列表需要“5. 强制对属性变量进行任何延迟绑定”。

我是否朝着正确的方向前进 -这就是“完成，然后撤消，然后重做”的全部内容吗？  请帮忙！

假设我有以下规则:

unify('test', 'this is a test').
run :- write('Enter something: '), 
       read(X), 
       unify(X, Y), 
       write('The answer is '), write(Y).

然后我运行如下:

?- ['unify.pl'].
% unify.pl compiled 0.00 sec, -48 bytes
true.

?- run.
Enter something: test.
The answer is this is a test
true.

?- run.
Enter something: 'test'.
The answer is this is a test
true.

为什么SWI-Prolog的统一都test和'test'来unify('test', 'this is a test').？我在回答关于SO的Prolog问题时遇到了这个问题.虽然我能够回答这个人的问题,但我无法解释这个特殊的行为,我想知道是否有其他人可以.

我正在尝试创建自己的WAM实现,我坚持练习2.4

我无法理解如何执行unify_value X4图2.4中的指令.

据我所知,该指令应该从查询中用程序中的f(W)统一Y.

unify_value X4调用unify (X4,S)S = 2(见图2.1),相应的堆单元格为"REF 2",X4为"STR 5".

Unify(图2.7)应该bind是那些值,但我不明白如何deref注册.

"REF 2"在堆中,"STR 5"在寄存器中.你怎么bind去登记册？

这是第一个观察:

?- is_list([]), is_list([_,_,_]).
true.

这是另一个观察:

?- [] = _, [_,_,_] = _.
true.

因此,为什么会is_list/1这样实施

?- is_list(_).
false.

要么

?- is_list([_|_]).
false.

何时_可以清楚地统一列表？这不是逻辑上更健全的true吗？

在SWI-Prolog的文档中is_list/1,注释说: 

在5.0.1之前的版本中,is_list/1只检查[]或[_|_]与proper_list/1有电流的作用is_list/1.目前的定义符合事实上的标准.

为什么这是事实上的标准？

在 Prolog 中，集合似乎是使用列表来表示的。

例如，以下是union/3SWI-Prolog 的实现：

union([], L, L) :- !.
union([H|T], L, R) :-
    memberchk(H, L), !,
    union(T, L, R).
union([H|T], L, [H|R]) :-
union(T, L, R).

然而这个谓词不是很有声明性，例如：

?- union([1,2,3],X,[1,2,3,4]).
X = [1, 2, 3, 4].

这应该留下一些选择点，或者：

?- union(X,[1,2],[1,2,3,4]).
<infinite loop>

这甚至不起作用！

除此之外，我们还发现以下问题：

?- union([1,2,3],[4,5],[1,2,3,5,4]).
false.

?- union([1,1,1],[4,5],[1,1,1,4,5]).
true.

如果我们真的谈论集合，这显然是错误的。

我们可以清楚地看到，使用列表来讨论集合并不简单，因为：

• 集合没有排序，而列表则有；
• 集合不包含重复值，而列表可以。

因此，我们要么发现作用于集合的谓词可以削减可能的解决方案（例如，联合的实现仅在集合有序的情况下才起作用），要么找到根据变量的实例化提供无用选择点的谓词（例如，联合谓词将具有作为许多选择点作为结果集的排列数）。

在 Prolog 中应该如何正确实现适用于集合的谓词？

这个问题非常笼统，并不特定于此处使用的示例union/3。

我在haskell中具有以下结构，该结构实现了一些用于打印的机制并调用了统一器。我从main收到以下错误：

0 =/= int

似乎认为0是数字而不是变量。以下是完整的实现。

 data CType 
      = CVar Int 
      | CArr CType CType
      | CInt
      | CBool
      deriving (Eq, Data)

data Constraint 
  = Equality CType CType
    deriving (Eq, Data)

我有一些基本类型（int和bool），箭头类型和类型变量。然后，我运行一些生成相等约束的算法，这些约束以上述方式表示。

我的目标是给定约束列表，我想找到最通用的统一器。

我遇到了这个库：http : //hackage.haskell.org/package/compdata-0.1/docs/Data-Comp-Unification.html

由于我是Haskell的新手，所以我无法立即弄清楚是否可以直接应用它。我可以使用该库还是建议从头开始编写统一器？

更新

我目前正在对代码进行以下更改，但方程式出现统一错误

f =克

module SolveEq where
import Data.Data
import Data.Void
import Data.List as List
import Data.Map as Map
import Data.Set as Set
import Data.Maybe (fromJust)
import Data.Maybe (isJust)
import Control.Monad
import TypeCheck
import Data.Comp.Variables
import Data.Comp.Unification
import Data.Comp.Term
import Data.Comp.Derive
import Constraint …

我正在阅读的一篇论文如下：

Plaisted [3] 表明，可以使用一阶谓词演算语义编写形式上正确的 PROLOG 程序，并导出无意义的结果，例如 3 < 2。

它指的是 Prologs 在当时（1980 年代）没有使用发生检查的事实。

不幸的是，它引用的论文是在付费墙后面。我仍然希望看到这样的例子。直觉上，感觉就像省略发生检查只是将结构的范围扩大到包括循环结构（但根据作者的说法，这种直觉一定是错误的）。

我希望这个例子不是

smaller(3, 2) :- X = f(X).

那会令人失望。

如果量词出现在逆变位置，则函数类型具有更高的等级： f :: (forall a. [a] -> b) -> Bool

关于这种类型的统一，类型变量a比 更严格b，因为以下实例化规则适用：

• a可以使用灵活的类型变量实例化，前提是这不允许a超出其范围
• 或使用另一个刚性类型变量
• 但不是非抽象类型，因为不是调用者foo而是foo自己决定是什么a，而b已经由调用者决定

然而，一旦包容开始发挥作用，事情就会变得更加复杂：

{-# LANGUAGE RankNTypes #-}

f :: (forall a. [a] -> [a]) -> Int -- rank-2
f _ = undefined

arg1a :: a -> a
arg1a x = x

arg1b :: [Int] -> [Int]
arg1b x = x

f arg1a -- type checks
f arg1b -- rejected

g :: ((forall …

{-# LANGUAGE RankNTypes #-}

newtype Coyoneda f a = Coyoneda {
  uncoyo :: forall b r. ((b -> a) -> f b -> r) -> r
}

coyoneda f tx = Coyoneda (\k -> k f tx)

我认为Coyoneda应该通过模拟具有更高等级类型的存在来工作，但我无法构造这种类型的值。在coyoneda辅助功能不类型检查，因为对于术语k f tx中较高等级类型变量b将难逃其范围。

但是，我无法想出另一种实现coyoneda. 有可能吗？