关于元程序的终止性

术语“元编程”是指编写以其他程序为数据并利用其语义的程序的能力。本文的目的是提出一种方法，使我们能够对一大类实用的元解释器进行正确的终止性分析，包括在执行过程中处理否定和执行不同任务。它基于结合用于证明项重写系统和程序终止性的一般排序的能力，以及用于证明逻辑程序终止性的著名可接受性条件。该方法建立了证明被解释程序终止性所需的排序与证明元解释器连同该被解释程序终止性所需的排序之间的关系。如果建立了这种关系，其中一个的终止性即蕴含另一个的终止性，即元解释器保持终止性。被正确分析的元解释器包括构造证明树的元解释器、各种类型的跟踪器和推理器。本文（不含附录）将发表于 Theory and Practice of Logic Programming。