支持代数多态类型的惰性函数逻辑编程通用框架
编程语言
2007-05-23 v1
摘要
我们提出了一个支持一阶函数逻辑编程的通用框架,该框架支持惰性函数、非确定性和数据构造子遵循等式公理集 C 的多态数据类型。在给定的 C 之上,我们将程序规约为定义函数的一组基于 C 的条件重写规则集 R。我们论证了等式逻辑不能为这类程序提供合适的语义。因此,我们提出了一种替代逻辑,其中包含基于 C 的重写演算和模型的概念。我们获得了基于 C 的重写相对于模型的可靠性与完备性、所有程序的自由模型存在性,以及类型保持性结果。作为操作语义,我们开发了一个可靠且完备的目标求解过程,该过程基于惰性窄化与模 C 的合一的结合。我们的框架在许多用途上具有很强的表达能力,例如解决动作与变化问题,或实现 GAMMA 计算模型。
引用
@article{arxiv.cs/0404050,
title = {A General Framework For Lazy Functional Logic Programming With Algebraic Polymorphic Types},
author = {Puri Arenas-Sanchez and Mario Rodriguez-Artalejo},
journal= {arXiv preprint arXiv:cs/0404050},
year = {2007}
}
备注
Appeared in Theory and Practice of Logic Programming, vol. 1, no. 2, 2001