问题标签 [unification]

我有一个简单的知识库，可以对家谱进行编码。此表示中的一些重要规则如下：

我试图找到两个人之间最近的长者（谓词ne(X,Y,Z)）。这个人Z是两个X和的长辈Y，没有一个小辈也是两个和Z的长辈。XY

我的尝试如下所示：

但这在某种程度上是不正确的，因为每当我跑步时，?- ne(stephanie,cathy,Z).我都会得到

但我只应该得到一个答案，我不知道出了什么问题。谢谢！

作为我最后一个问题的后续问题（感谢帕特里克），

我有一个像这样的变量列表，它是谓词的输出to_var_list(InputList, X)：

现在我想将列表拆分为“9”，所以结果应该是这样的：

我正在使用这样的谓词：

但这仅适用于不是变量列表的列表，例如：

如果将枢轴设置为“9”，则列表将被拆分为

但是对于上面的变量列表，应用此谓词将自动将每个无界变量绑定到枢轴，输出列表如下：

我知道我可以先拆分它们然后应用to_var_list，但是原始列表中保留的关系X丢失了。我需要建立一个约束模型，以便稍后我可以处理列表中的每个变量（比如设置每个变量的范围），最后能够给出 list 的修复结果X。

有没有办法在拆分时避免将枢轴绑定到变量？

我正在尝试使用 Z3 来求解涉及未知投影函数的方程，以找到满足方程的函数的有效解释。例如，对于等式：snd . f = g . fst一个有效的解释是f = \(x,y) -> (y,x)和g = id。我知道 Z3 不是更高阶的，所以我一直在尝试以一阶形式对问题进行编码。因此，例如对于f = g.fst我使用：

返回的作品类型：

但是对于snd . f = g . fst（我已经将树简化为对尝试和帮助）：

我明白了unknown。

我还尝试在不使用 ADT 的情况下仅使用布尔值或整数作为参数来编码类似的问题，但是模型只是将常量值分配给函数。我还尝试为函数常量、恒等函数以及成对和顺序组合定义一个简单的 ADT，然后定义一个可以简化表达式的“等于”函数，例如f.id = f，但这要么涉及递归函数，例如：

这显然是无效的。或者，如果我使用未解释的函数，它会使“eq”成为常量函数，即

与涉及 Int -> Int 类型函数的方程类似，这将返回 f 和 g 的常数函数：

并添加这些时间：

有什么想法可以让这种事情发挥作用吗？

非常感谢！

我对 Prolog 完全陌生，很难理解它的统一系统。我的问题如下：

我有一个约束整数、一个源数组和一个目标数组（它们都是整数数组）。我想过滤源数组中的元素，以便剩余元素在目标数组中具有对应的元素，以便源数组中的元素和目标数组中的元素之间的差异正好是约束。

示例：约束 = 1，源 = [1, 5, 7]，目标 = [2, 3, 4]。FilteredSource 应该是 [1, 5]，因为 abs(1 - 2) = 1 和 abs(5 - 4) = 1。Target 中没有 6 或 8，所以 7 不好。

根据我使用的参数，我要么得到错误的结果，要么查询进入无限循环。

到目前为止，我想出了这个：

passDistanceConstraint 部分似乎工作正常，但我将在此处包含它以供参考：

我很确定这是一个微不足道的问题，但我无法弄清楚，我正在拔掉头发。谢谢你的帮助！

I have learned loves(bob,Y) and loves(X,santa) can unify because {Y\santa,X\bob}. However, I'm not sure if the following can be unified:

I'm trying to make what one might call a decidable parser in Idris. At first I am just looking at parsing natural numbers, but have ran into an unexpected problem. A minimum example of the code that produces it is this:

I would expect this to compile, but instead I get

But natToChar 0 clearly equals '0', so I don't understand what the problem here is.

Update

I have also asked a question more directly related to what I am trying to do here.

我正在使用这种类型来推断可以执行可判定解析的字符串：

例如，像这样定义数字 [0-9]：

那么我们可以有以下功能：

这个s2n函数现在可以在编译时正常工作，但它本身并不是很有用。要在运行时使用它，我们必须先构造证明Every Digit (unpack s)，然后才能使用该函数。

所以我想我现在想写这样的函数：

或者我们想要返回成员资格证明或非成员资格证明，但我不完全确定如何以一般方式执行这些操作。因此，我尝试Maybe只为字符制作版本：

但后来我得到这个统一错误：

但p 属于类型Char -> Type。我不确定是什么导致了这个统一失败，但认为这个问题可能与我之前的问题有关。

这是我想要做的事情的明智方法吗？我觉得目前的工作有点多，这些功能的更通用版本应该是可能的。auto如果关键字可以用于编写一个函数给你一个Maybe proof或一个，这将是很好的Either proof proofThatItIsNot，就像DecEq类的工作方式一样。

我正在尝试简化复合数据类型，但不知道最好的方法。到目前为止，这是我的代码：

我一直看到的问题可能很明显 - 我无法将预期结果类型的类型变量与封装的类型变量统一起来：

我听说过-XExistentialQuantification作为一种可能的解决方案，但我无法得到任何工作。除了将类型参数浮动到 ，有谁知道在这里做什么Wrap？

我正在努力加深对 Prolog 的理解，以及它如何处理统一。在这种情况下，它如何处理与列表的统一。

这是我的知识库；

如果我正确理解了这个过程。如果member(X, [X|_])不为真，则进入递归规则，如果X在列表中T，则[_|T]与 统一T。

那么我的递归谓词中的匿名变量会发生什么？它会被丢弃吗？我很难理解列表的确切统一过程，因为[_|T]是两个变量，而不是一个。我只是想弄清楚统一过程如何与列表精确配合。

假设给定N个符号表达式，例如：

为简单起见，假设所有同名函数具有相同的数量（如，没有重载）。

我的目标是使用内存中最少数量的join、union和list表达式来表示这组N项：

• 列表表达式只是一个有限集。我们在问题中的输入集是一个列表表达式。例如：

  /li>

• 联合表达式是多个集合的联合：

  /li>

• 函数的连接表达式f表示一个集合，该集合是其参数集与f应用于每个参数组合的函数的笛卡尔积。例如：

  /li>

给定输入集，有许多可能的方法来用这些运算符表示它。简单地将所有N个表达式合并到一个列表中是一种方法。其他两种可能如下所示：

直观地说，这些表示中的每一个都将给定表达式的一些公共部分统一为一个共享组件。显然，对于足够大的N而言，存在比仅包含N个表达式的显式列表占用更少内存的表示。我这里将“占用内存”定义为集合中所有项的总数（包括中间项，例如函数应用程序）加上集合表达式（连接和联合）的总数。直观地说，它只是表示中运算符和操作数的总数。例如：

• f我们的输入集用 19 个术语表示，这是所有 5 个表达式（5秒、2g秒、...）中的术语总数。
• 上面的第一个替代表示有 14 个术语：1 个union，2 f- joins，以及所有列表元素的 11 个术语。
• 上面的第二种替代表示具有 13 个术语：2 个unions、 2 f- joins、 1 g- join和所有列表元素的 8 个术语。

在这些选项中，最后一个是最优化的。可能还有更好的，我不知道。最终，选择最佳表示是要弄清楚哪些部分应该共享，哪些应该明确列出。有没有办法通过算法解决这个问题？对我来说，它看起来像是对所有表达式形状的某种自上而下的动态编程，但我还没有找到确切的解决方案。

谢谢！