为什么循环引用和递归会使我的程序失败？
我写了这个简单的 Prolog 程序。
man(socrates).
mortal(X) :- man(X).
immortal(X) :- immortal(X).
我问了它一些常见的问题，比如苏格拉底是不是一个人，或者苏格拉底是否是一个凡人。
?- man(socrates).
true. //we know for a fact that Socrates is a man
?- mortal(socrates).
true. //and it can logically be inferred that Socrates is mortal
?- immortal(socrates).
//but we can't seem to figure out if he's immortal
由于 immortal 的递归定义，它崩溃了。循环引用也会导致崩溃或出现栈空间不足的错误。
在我看来，至少在这种情况下，Prolog 先生根据 中的规则得出这样的结论是相当简单的：程序中，不能推断苏格拉底是不朽的。如何？我想它可以检查堆栈并查看它是否正在遍历已经遍历过的规则。
是否有原因尚未实施？这样做是否会出现一些我忽略的问题，或者是否有 Prolog 的实现已经执行此类分析？
I wrote this simple Prolog program.
man(socrates).
mortal(X) :- man(X).
immortal(X) :- immortal(X).
I asked it the usual questions, such as whether Socrates is a man or if Socrates is a mortal.
?- man(socrates).
true. //we know for a fact that Socrates is a man
?- mortal(socrates).
true. //and it can logically be inferred that Socrates is mortal
?- immortal(socrates).
//but we can't seem to figure out if he's immortal
It crashed because of the recursive definition of immortal. Circular references also make it crash or error with Out of stack space.
It seems to me that, at least in this case, it would be fairly trivial for Mr. Prolog to conclude that from the rules in the program, it cannot be inferred that Socrates is immortal. How? I imagine it could examine the stack and see if it is traversing a rule that has already been traversed.
Is there a reason why this isn't already implemented? Would there be some problem with doing so that I am overlooking, or are there implementations of Prolog that already perform such analysis?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（4）
Prolog 使用不完全推理算法来提高效率。它旨在成为一种编程语言，其中程序除了程序意义之外还具有逻辑意义，而不是成熟的定理证明者。你必须小心编写子句的顺序，防止循环定义等。
至于你的谓词
immortal的逻辑含义，它是一个同义反复，可以从你的程序中删除/理论不改变其逻辑含义。这意味着如果它有助于改善程序意义（摆脱无限循环），您应该将其删除。
Prolog uses an incomplete inference algorithm for efficiency. It's meant to be a programming language where programs have a logical meaning in addition to a procedural one, not a full-blown theorem prover. You have to be careful with the order in which you write the clauses, prevent circular definitions, etc.
As for the logical meaning of your predicate
immortal, it'swhich is a tautology and can be removed from your program/theory without changing its logical meaning. This means you should remove it if that helps to improve the procedural meaning (gets rid of an infinite loop).
使用 XSB 进行制表：
然后：
Using tabling with XSB:
and then:
你的定义——以及你如何解释它们：
苏格拉底是一个人。
每个人都是凡人。
每个不朽者都是不朽的。
你的定义——以及 Prolog 如何解释它们：
如果你问苏格拉底的男子气概，我知道这是真的。
如果你问我关于某人的死亡率，我会检查他的男子气概（如果这是真的，那么死亡率也是如此）。
如果你问我一个人的不朽，我会检查他的不朽。
（你仍然想知道这如何导致无限循环吗？）
如果你想声明某人是不朽的，如果他不能被证明是凡人，那么你可以使用：
Your definitions - and how you interpret them:
Socrates is a man.
Every man is a mortal.
Every immortal is immortal.
Your definitions - and how Prolog interprets them:
If you ask about the manhood of Socrates, I know it's true.
If you ask me about the mortality of someone, I'll check his manhood (and if that's true, so is the mortality).
If you ask me about the immortality of someone, I'll check his immortality.
(Do you still wonder how that leads to an infinite loop?)
If you want to state that someone is immortal if he can't be proven mortal, then you can use:
这个小程序怎么样：
你的 Prolog 先生会推断，loopy(Y) 已经被调用并且会失败。
How about this little program:
Your Mr. Prolog would infer, that loopy(Y) has already been called and would fail.