逻辑程序员的三值语义

本文描述了一种更简单的方式，让程序员推理其代码的正确性。对逻辑程序语义的研究已经显示出模型论语义（程序员对程序解释中原子的真与假）、过程语义（例如，SLD归结）和不动点语义（对程序分析和替代执行机制有用）之间的紧密联系。这些工作大多假设预期的解释是二值的：一个基原子是真的（并且应该根据过程语义成功）或假的（并且不应该成功）。实际上，预期的解释不那么精确。程序员认为某些原子“不应该出现”或“类型错误”或“不可接受”。程序员不知道也不关心这些原子是否成功。在本文中，我们为（本质上）纯Prolog程序提出了一种三值语义，该语义带有（基）否定即失败，反映了这一点。Fitting的语义类似，但只将第三个真值与非终止相关联。我们提供了工具来推理程序的正确性，而无需不自然的精度或对编程风格的不当限制。除了理论结果，我们还提供了一个面向程序员的概要。这项工作源于声明式调试的工作，其中已经认识到不可接受的调用很重要。本文已被《Theory and Practice of Logic Programming》接受发表。