基于 Prolog 控制策略的线性表格解析
计算机科学中的逻辑
2007-05-23 v1
摘要
无限循环和冗余计算是 Prolog 中长期存在的开放问题。已探索了两种解决这些问题的方法：循环检查和表格化。循环检查可以切断无限循环，但即使对于无函数的逻辑程序也不能同时保持 sound 与 complete。表格化似乎是解决无限循环和冗余计算的有效方法。然而，现有的表格化解析，如 OLDT-解析、SLG-解析和 Tabulated SLS-解析，都是非线性的，因为它们依赖于用于制定表格化的 solution-lookup 模式。非线性解析的主要劣势是它们不能像 Prolog 中的那样使用简单基于栈的内存结构来实现。此外，某些严格顺序运算符如 cut 在 Prolog 中处理起来也不那么容易。在本文中，我们提出了一种混合方法来解决无限循环和冗余计算问题。我们将循环检查和表格化的想法结合起来，建立一种称为 TP-解析的线性表格化解析。TP-解析有两个独特特征：(1) 它以与 Prolog 相同的线性方式进行表格化推导，除了无限循环被切断和冗余计算被减少。它以与 Prolog 相同的效果处理 cut。(2) 它对于具有有界术语大小属性的正逻辑程序是 sound 与 complete 的。其底层算法可通过扩展任何现有的 Prolog 抽象机（如 WAM 或 ATOAM）来实现。
引用
@article{arxiv.cs/0003045,
title = {Termination Proofs for Logic Programs with Tabling},
author = {Sofie Verbaeten and Danny De Schreye and Konstantinos Sagonas},
journal= {arXiv preprint arXiv:cs/0003045},
year = {2007}
}
备注
48 pages, 6 figures, submitted to ACM Transactions on Computational Logic (TOCL)