问题标签 [prolog-abstract-interpretation]

问问题

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

1 问题
Newest
Active
Bountied
318
Unanswered
0 投票
6 回答
996 浏览

prolog - Prolog中的双重否定和执行模型

我试图理解为什么 Prolog 实现不按照教科书中的执行模型运行——例如，Sterling 和 Shapiro 的“Prolog 的艺术”书中的那个（第 6 章，“Pure Prolog”，第 6.1 节， “Prolog 的执行模型”）。

我所指的执行模型是这样的（Sterling & Shapiro 的第 93 页）：

输入：一个目标 G 和一个程序 P

输出： G 的一个实例，它是 P 的逻辑结果，否则不是

算法：

此外（同一本书的第 120 页），Prologchoose goal A以从左到右的顺序选择目标 ( )，并choose renamed clause ...按照它们在程序中出现的顺序搜索子句 ( )。

下面的程序有一个定义not（n在程序中调用）和一个单一的事实。

如果我尝试证明n(n(f(X)))，它会成功（根据两本教科书以及 SWI Prolog、GNU Prolog 和 Yap）。但这不是有点奇怪吗？根据几本书公开的执行模型，这是我期望发生的（跳过变量重命名以保持简单，因为无论如何都不会有冲突）：

  • 解决方案：n(n(f(Z)))

  • 统一X在第一个子句中与n(f(Z)), 匹配，并用该子句的尾部替换目标。

  • 解决方案：n(f(Z)), !, fail。

  • 统一X在第一个子句中再次匹配f(Z), 并用子句的尾部替换解析器中的第一个目标

  • 解决方案：f(Z), !, fail, !, fail。

  • 统一匹配f(Z)-> 成功！现在，这已从解决方案中消除。

  • 解决方案：!, fail, !, fail。

而“ !, fail, !, fail”应该不会成功！切割后有一个失败。故事结局。（事实上​​，!,fail,!,fail在我有权访问的所有 Prolog 系统中，作为查询输入都会失败）。

那么我可以假设教科书中的执行模型并不是Prolog使用的吗？

编辑：将第一个子句更改为对n(X) :- call(X), !, fail我尝试过的所有 Prolog 都没有影响。


12345678910