惰性函数逻辑编程的一般框架与代数多态类型
摘要：对于首阶函数逻辑编程，我们提出了一个通用框架，支持惰性函数、非确定性和多态数据类型。这些数据类型的构造函数服从一组等式公理C。在给定C的基础上，我们将程序规定为一组基于C的有条件重写规则，用于定义函数。我们认为等式逻辑不能为这种程序提供适当的语义。因此，我们提出了一种替代逻辑，包括基于C的重写演算和模型的概念。我们在模型方面得到了基于C的重写的音准和完备性，对于所有程序都存在自由模型，并且得到了类型保护的结果。作为操作语义，我们开发了一种基于惰性缩小和基于C的合一的目标求解的有声完全过程。我们的框架对于解决行动和变化问题，或实现GAMMA计算模型等多种目的都非常灵活。
作者：Puri Arenas-Sanchez, Mario Rodriguez-Artalejo
论文ID：cs/0404050
分类：Programming Languages
分类简称：cs.PL
提交时间：2007-05-23