基于类型一阶逻辑系统的逻辑程序设计语言语义描述方法的研究

摘要

逻辑程序设计是一种说明性程序设计方式，它将程序的逻辑和控制分开，程序员只需考虑逻辑描述部分，控制部分则完全交付语言的编译或解释系统完成，这使得人们能在较高的抽象层面上进行程序设计。这一思想需要借助合适的逻辑程序设计语言来展现其优势。Prolog是最具影响的逻辑程序设计语言，它以一阶谓词逻辑的Horn子句逻辑为基础，其简单的文法、独特的说明性适合用于表达人工智能领域中的问题求解，曾经受到了人工智能研究和应用开发者的重视。但Prolog设计相对简单，未能吸取程序设计语言研究中的诸多先进成果，在使用过程中暴露出了种种不足，尤其是缺乏类型、不支持模块等，难以适应现代大规模程序开发的需要。
　　 G(o)del是继Prolog之后出现的新型逻辑程序设计语言，它建立在多态多类的一阶逻辑基础之上，摒弃了Prolog语言中的非逻辑成分，引入多态多类、模块化、延迟计算、剪枝操作等诸多新语言成分，是一种高效、先进的说明性逻辑程序设计语言。着眼于G(o)del编译器的实现和促进该语言的推广以及深入研究，本文作者在研究小组的探索研究工作中，对基于类型一阶逻辑理论的逻辑程序设计语言G(o)del的语义描述方式进行了研究。本文的工作建立在一阶逻辑程序的语义模型基础上，对传统的一阶谓词逻辑语言进行扩展，引入多态类型，建立多态类型一阶语言系统的语法和语义理论基础，用于描述G(o)del程序的说明性和过程性语义，并用于指导G(o)del语言的编译实现和深入应用开发。
　　 论文的主要工作和贡献如下：
　　 首先，参与提出和发展了多态类型一阶语言，完整地给出了多态类型一阶语言的语法定义，建立了带类型的一阶逻辑理论及其推理规则；
　　 其次，独立针对类型一阶语言的Horn子集定义了G(o)del语言核心部分的语法，在此基础上，给出了解释（或称赋值）的一般定义，讨论了在合理的解释下类型合式公式的真值判别法，并由此建立带类型的一阶逻辑系统的模型；
　　 第三，利用类型一阶语言的Herbrand模型探讨了Godel程序的形式化说明性语义，最终得出结论为最小Herbrand模型MP可以作为程序P的形式语义，其理由是MP恰由作为P的逻辑推论的那些类型基原子组成；
　　 第四，定义由基类型、构造类型、结构类型和类型变元组成的类型系统的定型规则，讨论了类型的偏序关系、相容性关系，主要解决如何将逻辑程序中的个体符、约束变元符、谓词符、类型项、类型合式公式和类型命题形式等指派为不同的实体类型对象，给出了对不同类型的对象进行类型检查与类型推断的一组算法：
　　 第五，引入了一组定义描述G(o)del中的commt剪枝算子的过程语义，阐述了剪枝算子和支持延迟计算的计算规则之间的关系，并给出了剪枝算子的实现方法：
　　 最后，基于类型的合一算法和SLD反驳一消解法，设计逻辑程序求解目标的计算规则和搜索策略，也就是逻辑程序设计语言的控制机制，从而描述了G(o)del程序的过程性语义。
　　 类型一阶逻辑系统为描述逻辑程序的说明性和过程性语义奠定了理论基础，随着语言编译系统逐步完善，G(o)del语言将会受到更多的关注，在逻辑程序设计语言中体现其优势。