检测是否证明谓词统一了某些东西答案

【问题标题】：Detecting whether proving a predicate unified something检测是否证明谓词统一了某些东西
【发布时间】：2016-04-18 18:04:37
【问题描述】：

我有一个谓词可以统一它的参数，例如：

foo(X) :- X = 42.

在证明foo(X) 时，我如何判断统一是否改变了 X？例如，我想知道writeln(X), foo(X), writeln(X) 是否会为 X 打印两次相同的值，而无需实际进行打印。

我对@987654324@ 的实际实现实际上要复杂得多，所以请不要针对上面的简化版本提出具体建议。在我的程序中，foo(X) 使用统一化简化了X，但foo(X) 可能需要多次证明，直到所有简化都执行完毕。我希望能够编写一个调用foo(X) 的foohelper(X) 谓词，直到X 停止统一。

【问题讨论】：

什么时候你想知道X是否已经被实例化了？（我们不改变X，我们实例化它）
我想知道X 是否在证明foo(X) 时被实例化，在我的示例中位于第二个writeln(X) 的位置。

标签： prolog unification

【解决方案1】：

假设我们只有句法统一——也就是说，没有约束：

:- meta_predicate(call_instantiated(0,?)).

call_instantiated(Goal_0, Instantiated) :-
    copy_term(Goal_0, Copy_0),
    Goal_0,
    (  subsumes_term(Goal_0, Copy_0) ->  % succeeds iff equal u.t.r.
       Instantiated = false
    ;  Instantiated = true
    ).

请注意，Goal_0 将或不会被进一步实例化。上面的subsumes_term/2 测试Goal_0 现在是否比Copy_0“更通用”。当然，它不能更笼统，如此有效，以至于 test 测试术语是否与重命名变量相同。

与使用term_variables/2 相比，正如@PauloMoura 所指出的，这可能不是更有效。主要看subsumes_term/2的效率。

【讨论】：

Goal_0 应该是 call(Goal_0)。使用裸（元）变量的不良编程风格。此外，它们的语义可能等同于也可能不等同于 call/1，具体取决于 Prolog 系统（w.r.t. 对剪辑不透明或透明）。
@PauloMoura ??这是定义明确的行为。哪个 Prolog 系统不能正确处理这个问题？
不是正确性的问题，而是裸元变量的语义选择问题。 ECLiPSe 是一个系统示例，其中裸元变量对切割是透明的。
@PauloMoura：有时可能会有一些不同。但是这种情况没有区别。说：mynot(X) :- X, !, fail. mynot(_)。在 Eclipse 中使用 mynot((!,fail)) 正确成功（默认模式）。
在这种情况下（裸元变量），好的编程风格也是防御性编程。

【解决方案2】：

也许您可以使用标准的term_variables/2 谓词？您可以在调用目标之前和之后使用您的目标调用它，并检查返回的变量列表是否不同。比如：

...,
term_variables(foo(X), Vars0),
foo(X),
term_variables(foo(X), Vars),
(  Vars0 == Vars ->
   write(simplified)
;  write(not_simplified)
),
...

【讨论】：

“简化”应该是“相同的”
@false 阅读问题。在那里你会发现我为什么使用“简化”这个词。
我认为这应该可行——谢谢！我很好奇是否有更好的方法来拍摄一个术语的“快照”。
@EdMcMan 您可以使用标准的copy_term/2 谓词来获取您所谓的术语快照，然后将此快照与标准的subsumes_term/2 谓词一起使用，但这会更冗长而昂贵的解决方案。