Prologish Boolos 好奇推理的计算机推理

Question

Boolo 的奇妙推理最初是用方程式 here 制定的。它是函数 f 和谓词 d 的递归定义，通过 N+ 的语法，即不为零的自然数，由 1 和 s(.) 生成。

但它也可以用喇叭子句来表述。逻辑内容不完全相同，谓词 f 只捕获函数的积极方面，但问题类型相同。采用以下 Prolog 程序：

f(_, 1, s(1)).
f(1, s(X), s(s(Y))) :- f(1, X, Y).
f(s(X), s(Y), T) :- f(s(X), Y, Z), f(X, Z, T).

d(1).
d(s(X)) :- d(X).

最后一个查询的理论上的逻辑结果是什么，你能否在我们的时空证明有一个计算机程序产生结果，即将程序发布在 gist 上，每个人都可以运行它？

?- f(X,X,Y).
X = 1,
Y = s(1) 
X = s(1),
Y = s(s(s(1))) 
X = s(s(1)),
Y = s(s(s(s(s(s(s(s(s(s(...)))))))))) 
ERROR: Out of global stack

?- f(s(s(s(s(1)))), s(s(s(s(1)))), X), d(X).

如果执行结果验证工作的程序不是像 here 这样的 Prolog 解释器本身，那么该工作将做什么特别适合这个 Prologish 问题表述？

Answer 1

一种解决方案：抽象解释

预赛

在这个答案中，我使用 解释器 来证明这一点成立。但是，它不是 Prolog 解释器，因为它解释程序的方式与 Prolog 解释程序的方式不同。

相反，它以更抽象的方式解释程序。因此，此类解释器被称为抽象解释器。

程序表示

重要的是，我直接使用源程序，只使用我们通过纯代数推理知道可以安全应用的修改。它对您的源程序在构造上完全纯这样的推理有很大帮助，因为它只使用纯谓词。

为了简化对程序的推理，我现在明确所有统一。很容易看出，这并没有改变程序的含义，并且可以很容易地实现自动化。我得到：

f（_，X，Y）：- X = 1, Y = s(1)。 f（Arg，X，Y）：- 精氨酸 = 1， X = s(X0), Y = s(s(Y0)), f(Arg, X0, Y0)。 f（X，Y，T）：- X = s(X0), Y = s(Y0), f(X, Y0, Z), f(X0, Z, T)。

我把它作为一个简单的练习来证明这在声明上等同于原始程序。

抽象

我使用的抽象如下：我没有对 具体 术语 1、s(1)、s(s(1)) 等进行推理，而是使用原子 d 对于我可以证明d(T) 成立的每个术语T。

让我向您展示我对统一的以下解释的意思：

解释（d = N）：- d（N）。

这说：

如果 d(N) 成立，那么 N 被视为与原子@相同987654330@，正如我们所说，它应表示d/1 持有的任何术语。

请注意，这与具体术语 d 和 N 之间的实际统一的含义显着不同！例如，我们得到：

?-解释(X = s(s(1)))。 X = d。

很奇怪，但我希望你能习惯。

扩展抽象

当然，解释一个单一的统一并不足以解释这个程序，因为它还包含额外的语言元素。

因此，我将抽象解释扩展为：

• 联结
• f/3的电话。

解释连词很容易，但是f/3呢？

增量推导

如果在抽象解释期间，我们遇到目标f(X, Y, Z)，那么我们知道以下内容：原则上，论据当然可以与目标成功的任何术语统一。因此，我们会跟踪那些我们知道查询原则上可以成功的参数。

因此，我们为谓词配备了一个附加参数：f/3 目标列表，这些目标是程序的逻辑结果。

此外，我们实施了以下非常重要的规定：如果我们遇到无法用抽象术语安全解释的统一，那么我们会抛出错误而不是失败默默。例如，如果统一在被视为抽象解释时会失败，尽管它会成功作为具体统一，或者如果我们不能完全确定论点是否属于预期的域。该规定的主要目的是避免由于抽象解释器的疏忽而无意中消除了实际解决方案。这是解释器中最关键的方面，任何证明理论的机制都会面临密切相关的问题（我们如何确保没有遗漏任何证明？）。

这里是：

解释（Var = N，_）：- must_be(var, Var), must_be（地面，N）， d(N), 变量 = d。 解释（（A，B），Ds）： - 解释（A，Ds）， 解释（B，Ds）。 解释（f（A，B，C），Ds）：- 成员（f（A，B，C），Ds）。

Quis custodiet ipsos custodes？

我们如何判断这是否真的正确？这是困难部分！事实上，事实证明上述方法不足以确定捕获所有情况，因为如果d(N) 不成立，它可能只是失败。抽象解释器在无法处理的情况下静默失败显然是不可接受的。所以我们至少还需要一个子句：

解释（Var = N，_）：- must_be(var, Var), must_be（地面，N）， \+ d(N), 域错误（d，N）。

事实上，当我们推理基本术语时，抽象解释器变得更不容易出错，因此我将使用原子any 来表示派生中的“任何术语”答案。

在这个域上，统一的解释变成：

解释（Var = N，_）：- must_be（地面，N）， ( var(Var) -> ( d(N) -> Var = d ; N = s(d) -> Var = d ; N = s(s(d)) -> Var = d ; domain_error(d, N) ) ; Var == 任何 -> 真 ;域错误（任何，变量） )。

此外，我已经在这个抽象域上实现了进一步的统一案例。我把它作为一个练习来思考这是否正确地模拟了预期的语义，并实现了更多的案例。

事实证明，这个定义足以回答发布的问题。然而，它显然还有很多不足之处：它比我们想要的更复杂，而且越来越难以判断我们是否涵盖了所有案例。但请注意，任何证明理论的方法都将面临密切相关的问题：它变得越复杂和强大，就越难判断它是否仍然正确。

所有推导：定点见！

现在剩下的就是从原始程序中推断出所有内容。

这是一个简单的fixpoint计算：

衍生品（Ds）：- 函子（头，f，3）， findall(Head-Body, Clause(Head, Body), Clauses), derivables_fixpoint（子句，[]，Ds）。 derivables_fixpoint（子句，Ds0，Ds）：- findall（D，clauses_derivable（子句，Ds0，D），Ds1，Ds0）， term_variables(Ds1, Vs), 地图列表（=（任何），Vs）， 排序（Ds1，Ds2）， （相同长度（Ds2，Ds0）-> Ds = Ds0 ; derivables_fixpoint（子句，Ds2，Ds） )。 Clauses_derivable(Clauses, Ds0, Head) :- 成员（头体，子句）， 解释（正文，Ds0）。

由于我们正在导出基本术语，sort/2 会删除重复项。

查询示例：

?- 导数（Ds）。 错误：参数没有充分实例化

有点虎头蛇尾，抽象解释器无法处理这个程序！

拯救的交换性

在证明理论的方法中，我们搜索，嗯，证明。在基于解释器的方法中，我们可以改进解释器或应用代数定律以保留基本属性的方式转换源程序。

在这种情况下，我将做后者，而将前者留作练习。我们不是搜索证明，而是搜索等效方法来编写程序，以便我们的解释器可以推导出所需的属性。比如我现在用commutativity的连词来获得：

f（_，X，Y）：- X = 1, Y = s(1)。 f（Arg，X，Y）：- 精氨酸 = 1， f(Arg, X0, Y0), X = s(X0), Y = s(s(Y0))。 f（X，Y，T）：- f(X, Y0, Z), f(X0, Z, T), X = s(X0), Y = s(Y0)。

再次，我把它作为一个练习来仔细检查这个程序是否声明性地等效到您的原始程序。

iamque opus exegi，因为：

?- 导数（Ds）。 Ds = [f(any, d, d)]。

这表明在f/3 的每个 解中，最后两个参数是d/1 成立的始终 项！特别是，它也适用于您发布的示例参数，即使没有希望实际计算具体项！

结论

通过抽象解释，我们已经表明：

• 对于所有X，其中f(_, _, X) 成立，d(X) 也 成立
• 除此之外，对于所有Y，f(_, Y, _) 成立，d(Y) 也成立。

该问题只要求 first 属性的 特殊情况。我们已经展示了更多！

总结：

如果 f(_, Y, X) 成立，那么 d(X) 成立并且 d(Y) 成立。

Prolog 使推理 Prolog 程序变得相对容易和方便。这通常使我们能够导出 Prolog 程序的有趣属性，例如终止属性和类型信息。

请参阅Reasoning about programs 以获取参考资料和更多说明。

+1 提出一个很好的问题和参考。