逻辑程序设计中的作用域构造:实现问题及其解决
编程语言
2007-05-23 v1
摘要
本文考虑在逻辑程序设计的子目标中加入全称量词与一种蕴涵形式。这些扩充为作用域提供了逻辑基础,但也带来了新的实现问题。当允许全称量词与存在量词以混合次序出现在子目标中时,用于求解存在性目标的逻辑变量与合一(unification)机制必须被修改,以确保尊重由量词次序所产生的约束。文中描述了基于为常元和变量附加数值标记并在合一中使用这些标记所作的适当修改。所得机制适于高效实现,并且事实上可轻易融入 Warren 抽象机(WAM)的常规装置中。在子目标中提供蕴涵会导致为求解特定子目标而向程序添加程序子句的可能性。一种基于断言与收回程序子句的朴素方案不足以实现此类添加,原因有二。首先,面对回溯时必须支持早先存在的程序的恢复。其次,蕴涵目标被量词包围的可能性要求考虑程序子句按其自由变量的绑定进行参数化。文中描述了支持这些附加需求的机制,以及将这些机制集成进 WAM 的方法。还概述了针对语言中高阶扩充的机器进一步扩展。此处给出的思想与高阶逻辑程序设计语言 lambda Prolog 的实现相关。
引用
@article{arxiv.cs/9809016,
title = {Scoping Constructs in Logic Programming: Implementation Problems and their Solution},
author = {Gopalan Nadathur and Bharat Jayaraman and Keehang Kwon},
journal= {arXiv preprint arXiv:cs/9809016},
year = {2007}
}
备注
46 pages