主要特點

我最近一直在尋找具有特定功能集的 Prolog 元解釋器，但我開始發現我沒有理論知識來處理它。

特點如下：

1. 深度優先搜索。
2. 以與經典解釋器相同的方式解釋任何非遞回 Prolog 程式。
3. 保證突破任何無限遞回。這很可能意味著破壞圖靈完備性，我對此表示同意。
4. 只要遞回的每一步都降低了運算式的復雜性，就繼續評估它。更具體地說，我希望允許謂詞呼叫自己，但我想防止子句能夠呼叫自己的類似或更復雜的版本。

顯然，（3）和（4）是我遇到的問題。我不確定這兩個功能是否兼容。我什至不確定是否有一種方法可以定義復雜性，使得 (4) 具有邏輯意義。

在我的研究中，我遇到了“不可避免的模式”的概念，我相信它提供了一種方法來確保特征（3），只要特征（4）有一個格式良好的定義。

我特別想知道這種解釋器是否已被證明是不可能的，如果沒有，過去是否已經對類似的解釋器進行了理論或具體的作業。

額外功能

如果上述功能可以實作，我還有一些額外的功能要添加，如果您也能告訴我這些功能的可行性，我將不勝感激：

5. 系統地描述和描述這些遞回，這樣，當檢測到一個遞回時，可以呼叫與這種特定形式的遞回匹配的用戶定義的謂詞或子句。
6. 檢測導致組合選擇呈指數級增長的模式，阻止評估，并以與步驟 (5) 相同的方式對它們進行表征，以便它們可以由內置或用戶定義的謂詞處理。

例子

這是一個簡單的謂詞，除了最簡單的情況外，它顯然會在普通 Prolog 解釋器中導致無限遞回。該解釋器最多應該能夠在 PSPACE 中對其進行評估（并且我相信，如果 (6) 可以實作，則最多 P），同時仍然給出相關結果。

eq(E, E).
eq(E, F):- eq(E,F0), eq(F0,F).

eq(A   B, AR   BR):- eq(A, AR), eq(B, BR).

eq(A   B, B   A).
eq(A * B, B * A).
eq((A * B) / B, A).

eq(E, R):- eq(R, E).

預期結果示例：

?- eq((a   c)   b, b   (c   a)).
true.

?- eq(a, (a * b) / C).
C = b.

The fact that this kind of interpreter might prove useful by the provided example hints me towards the fact that such an interpreter is probably impossible, but, if it is, I would like to be able to understand what makes it impossible (for example, does (3) (4) reduce to the halting problem? is (6) NP?).

uj5u.com熱心網友回復：

如果您想保證終止，您可以保守地假設任何輸入目標都是非終止的，除非另有證明，使用可判定的證明程式。基本上，定義一些你知道會停止的小目標，并隨著時間的推移用聰明的想法擴展它。

下面是三個示例，分別保證或強制執行三種不同的終止（另請參見 Prolog 的Power of Prolog 章節終止）：

• 存在-存在：在潛在分歧之前至少達到一個答案
• 普遍存在的：沒有分支分叉，但可能有無數個分支，因此目標可能不會普遍終止
• Universal-universal：經過有限數量的步驟后，每個答案都會得到，所以特別是必須有有限數量的答案

在下文中，halts(Goal)假設正確測驗存在-存在終止的目標。

存在-存在

這用于halts/1證明適度目標類別的存在終止。當前的評估器eval/1只是回退到底層引擎：

halts(halts(_)).

eval(Input) :- Input.

:- \  \  halts(halts(eval(_))).

safe_eval(Input) :-
    halts(eval(Input)),
    eval(Input).

?- eval((repeat, false)).
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted
?- safe_eval((repeat, false)).
false.

可選但強烈推薦的目標指令\ \ halts(halts(eval(_)))可確保halts在運行時始終停止eval應用于任何內容。

將問題拆分為終止檢查器和評估器的優點是兩者是解耦的：您可以使用任何您想要的評估策略。halts可以逐漸增加更高級的方法來擴展允許目標的類別，從而可以自由eval地做同樣的事情，例如基于靜態/運行時模式分析的子句重新排序、傳播失敗等。eval本身可以通過改進來擴展允許目標的類別可以理解的終止屬性halts。

一個警告 - 使用元邏輯謂詞的輸入var/1可能會破壞目標指令。也許一開始只是不允許這樣的謂詞，然后隨著時間的推移再次放寬限制，因為您發現了安全的使用模式。

普遍存在

This example uses a meta-interpreter, adapted from the Power of Prolog chapter on meta-interpreters, to prune off branches which can't be proven to existentially terminate:

eval(true).
eval((A,B)) :- eval(A), eval(B).
eval((A;_)) :- halts(eval(A)), eval(A).
eval((_;B)) :- halts(eval(B)), eval(B).
eval(g(Head)) :-
    clause(Head, Body),
    halts(eval(Body)),
    eval(Body).

So here we're destroying branches, rather than refusing to evaluate the goal.

For improved efficiency, you could start by naively evaluating the input goal and building up per-branch sets of visited clause bodies (using e.g. clause/3), and only invoke halts when you are about to revisit a clause in the same branch.

Universal-Universal

The above meta-interpreter rules out at least all the diverging branches, but may still have an infinite number of individually terminating branches. If we want to ensure universal termination we can again do everything before entering eval, as in the existential-existential variation:

...

:- \  \  halts(halts(\  \  eval(_))).

...

safe_eval(Input) :-
    halts(\  \  eval(Input)),
    eval(Input).

So we're just adding in universal quantification.

One interesting thing you could try is running halts itself using eval. This could yield speedups, better termination properties, or qualitatively new capabilities, but would of course require the goal directive and halts to be written according to eval's semantics. E.g. if you remove double negations then \ \ would not universally quantify, and if you propagate false or otherwise don't conform to the default left-to-right strategy then the (goal, false) test for universal termination (PoP chapter on termination) also would not work.

標籤：recursion prolog complexity-theory interpreter computation-theory

上一篇：無限遞回飛鏢生成器（yield*）堆疊溢位嗎？

下一篇：在javascript中使用filter()來實作curriable()是可行的，但是，uisngmap()是可行的，為什么？