问题标签 [unification]

在对描述对话表达式语义的谓词执行引用解析时，由于在开放世界中工作，我需要能够允许部分统一。

例如，考虑以下场景：

你面前有一个蓝色的盒子。我们使用 id 来引用这个蓝色框3。

一组谓词box(x)^blue(x)可以轻松解析为您所知道的蓝色框。进行此查询将返回3

一组谓词ball(x)^yellow(x)不会解决任何问题。这可以。

但现在考虑ball(x)^yellow(x)^box(y)^blue(y)^behind(x,y) 的是，蓝色盒子后面的黄色球。

我们不知道黄球，但我们知道蓝盒子！当然，有可能已知盒子后面没有球，而另一个盒子正在被提及。但我们很确定我们知道正在谈论什么盒子。

我在一个概率框架内工作，在这个框架中我计算每组绑定满足一组命题的概率；然后，引用解析过程返回最可能的统一器/绑定集。不幸的是，在考虑 时behind(x,y)，我的系统消除了3被绑定到的可能性，y因为它不知道带有 id 的框后面有任何黄球3。

有没有办法对谓词进行部分统一，以便系统确定该语句最可能的解析是，y/3 x/?即 y 绑定到 3 并且 x 的身份是未知的？

我有这个特殊的问题，我还没有解决方案。我认为如果我知道它存在相关算法会有所帮助。

我正在寻找的算法是一种有助于找到满足函数返回目标的参数的算法。

例如，a works for b表示为(a,b)

函数works将确保它们与布尔值的关系

现在给了我

如果我希望这两个绑定是真的，那么这个函数必须是真的

现在我正在尝试编写一个函数/算法来帮助我实现这样的"x" = b

我正在考虑回溯，但还不知道如何实现它。如果有人能给我一个提示，我将不胜感激。

作为旁注，我正在使用函数式编程范例在 F# 中实现该算法。

假设我有以下理论：

它只是说真的，这当然a(X)是正确的，因为不存在b(X)（否定作为有限失败）是真的。因为只有 ab(X)如果没有c(X)，而我们有c(a)，所以可以说这是真的。但是我想知道为什么 Prolog 不提供答案X = a？比如说我介绍了一些语义：

当然，如果我查询noOrphan(michael)，这将导致trueand noOrphan(david)in false（因为我没有为 定义父david级）。但是我想知道为什么没有主动方法来检测哪些人（michael，david，...）属于该noOrphan/1关系?

这可能是 Prolog 的回溯机制的结果，但 Prolog 可以保持一种状态，该状态可以验证一个人是在以积极的方式（0,2,4,...）深度否定，还是以消极的方式（1,3 ,5,...) 深度否定。

Warren 的抽象机器中的练习 2.2 ：教程重构

要求对术语 f(X, g(X, a)) 和 f(b, Y) 进行表示，然后对这些术语的地址进行统一（分别表示为 a1 和 a2）。

我已经为这些术语构建了堆表示，它们如下：

现在我被要求跟踪统一（a1，a2），但是按照第 20 页的算法，我得到：

我的错误在哪里？

我需要引入一个谓词来否定原子。到目前为止，我有neg(Premise) :- \+ Premise.，这给了我以下结果：

这是有道理的，一切都是花花公子，直到我尝试统一。例如

[a,_] = [a,123].返回true.

尽管

[a,_] = [neg(neg(a)),123].返回false.。

我该如何解决这个问题，以便对neg(neg(X))零件进行评估或以其他方式统一X（因为它们在逻辑上都是等效的）？所以基本上，我需要X=neg(a), a=neg(X).成功。

编辑我找到了一个解释，为什么 not(not(<expression>))不等同<expression>于序言。既然<expression>成功了，not(<expression>)就失败了。当目标失败时，它实例化的变量将无法实例化。（来源，幻灯片 14）。

我仍然不确定如何解决这个问题。

我正在为自然推论编写一个证明检查器，但我对在列表中“更进一步”的部分证明存在问题。

首先我读取一个文件等，然后调用导致问题的函数：

通过跟踪检查，我知道下面的调用是失败的：

这些是程序的相关部分：

鉴于这对表达式，是否有可能为它找到一个 MGU？

1. f(x,y)
2. f(y,x)

我想说这是可能的，当 x/y 时，但我不确定这是否合法。你们怎么说？

谢谢！

我正在制作一个编译器（用于一种新语言），它通过模式匹配支持 AC 统一。匹配算法已经有效，但是我在函数的逻辑和数学方面以及它的属性方面遇到了麻烦，这将以很好的方式定义语言的设计。我有几个关于函数属性的问题：

关联和交换属性仅适用于二元函数？

例如，如果我声明一个函数 max(a,b)，这将是可交换的，因为 max(a,b) = max(b,a) 并且是关联的，因为 max(a,max(b,c)) = max(max （a，b），c），但我想不出任何具有两个以上满足该公理的参数的函数。例如，我可以定义 max(a,b,c) = max(a,max(b,c)) 这将是一个三元函数，但该语言将能够将它与符合它的二进制操作统一起来。

统一通过将诸如 max(a,max(b,c)) 之类的关联函数简化为可变和规范形式 max(a,b,c) 然后在此规范形式上执行模式匹配，所以所有（我认为) 具有超过 3 个参数的此属性的可能函数实际上是相同二元函数的复合

标识元素是否仅适用于二元函数？

解释：可以有一个可变函数 f(a,b,...)（超过 2 个参数），使得存在满足 f(a,b,c,e) = f(a,b,c) 的元素 e ) 对于没有直接二进制父级的函数（例如加法是二进制的，但编译器将加法管理为内部表示的可变函数）

诸如零之类的统一元素仅在语言中通过删除其对函数的 aparences 进行管理，例如 add(1,2,x,0) ，它表示表达式 1+2+x+0 减少为 1+2+x

这些问题对于在定义规则（例如 a+b = b+a）时自动识别函数的此属性的算法设计以及语言设计和将强加于函数声明的约束（可以是，如果这些问题中的任何一个为假，则不合逻辑

当你调用member(Item, List)一个未实例化的列表时，Prolog 会统一并返回一个包含项目的列表。我想要一个返回true/false并且不尝试统一的规则。有这样的规定吗？

我试图理解为什么函数

有类型

如果过滤器必须接收一个返回 Bool-Type 的函数并且 fst 只返回元组的第一个元素，“过滤器 fst”如何工作？

谁能解释我？谢谢 ;）