问题标签 [lambda-prolog]

有这篇论文：

William E. Byrd、Eric Holk、Daniel P. Friedman，2012
miniKanren，
通过关系解释器实时和未标记的 Quines 生成
http://webyrd.net/quines/quines.pdf

它使用逻辑编程来查找 Scheme Quine。这里考虑的 Scheme 子集不仅包含 lambda 抽象和应用程序，还包含通过以下归约处理的小列表处理，已翻译为 Prolog：

因此，除了用于 lambda 抽象和绑定变量的 lembda 之外，唯一的符号是引号、[] 和 cons。我们将使用 Prolog 列表作为 Scheme 列表。目标是通过 Prolog 找到一个 Scheme 程序 Q，这样我们得到 Q ~~> Q，即对自身求值。

有一个复杂性，这使得努力变得不平凡，[lembda,X,Y] 不会在语法上对其自身进行评估，而是应该返回一个环境闭包。因此，评估器与此处的 Plotkin 评估器不同。

周围有任何 Prolog 解决方案吗？圣诞快乐

λProlog 以假设推理为特征。通过使用运算符 (=>)/2 我们可以临时断言一些子​​句。这可以用来 在 λProlog中实现对抗搜索吗？

正在考虑井字游戏。除了从填充为空白的 cell/3 事实开始，我们还可以简单地从根本没有 cell/3 事实开始。

然后每个玩家通过添加 cell/3 个事实来移动。周围有什么相应的实现吗？我想他们将是这里代码的改编。

两次移动后，数据库可能如下所示：

我正在阅读在高阶约束逻辑编程中实现类型理论的论文，在 p7 上我看到了以下 lambda-prolog 代码：

!我对第三条中cut的位置感到困惑。我对 cut 的理解是它总是成功的，但会阻止回溯到该成功之后，特别是会导致同一谓词的后续子句被忽略。特别是，在子句中首先出现的剪切应该意味着一旦与该子句的头部统一成功，所有后面的子句都将被忽略。

考虑到这一点，上面第一条和第二条开始的削减对我来说是有意义的：他们说如果被归约的术语是 anapp或 a lam，那么只有一个规则可以适用于它。但在我看来，第三个子句的开头似乎是完全一般的——所有的论点都是不同的变量——所以它不能不统一。因此，在我看来，总是会调用从第三个子句开始的剪切，因此永远不会到达第四个子句。我本来希望第三个子句写成类似

所以它只适用于他们所谓的“val-bound variables”；然后剪切将指示 ifX是这样一个变量，只有这个子句适用，而 if Xis not such a variable 那么我们将能够回溯并尝试第四个子句。

但是，我对 cut 的理解非常初级，所以我希望我遗漏了一些东西。有人可以解释吗？