逻辑程序设计语言Godel的形式化过程性语义

摘要

Godel语言是继Prolog语言之后出现的逻辑程序设计语言，它建立在多态多类的一阶逻辑基础之上，摒弃了Prolog语言中的非逻辑成分，集成了许多语言的有效成分和优点，引入了类型系统，这使得它成为一种高效的说明性逻辑程序设计语言。然而，时至今日，Godel语言编译系统的开发研究仍然进展缓慢，主要原因是多态多类的类型系统、模块化结构、延迟计算、剪枝操作等多种新语言成分和机制的引入，使逻辑程序设计语言Godel的复杂程度大大提高，而面向过程程序设计语言的编译方法和技术完全不同于具有递归性、说明性特点的逻辑程序设计语言，先前关于Prolog语言的编译方法和技术不能简单移植和照搬，而理论基础研究的滞后直接导致系统研究和开发进展缓慢，迄今尚无新的进展和系统开发成果报道。 为了促进Godel语言的推广以及深入研究，本人所在的课题组基于类型一阶逻辑Horn子集提出了Godel语言一整套理论基础，本文在Godel语言的语法和形式化说明性语义基础上，着眼于编译系统的设计与实现，为Godel语言建立了严格的形式化过程性语义。 本文首先介绍了Godel语言的语法基础，接着详细阐述了基于类型一阶逻辑Horn子集的过程性语义，引入了较为完整的基类型，构造类型，结构类型间的偏序关系，讨论了类型相容性关系，类型推断与类型约束算法，以及基于类型约束的合一算法和SLD反驳消解法。然后，全面介绍了Godel语言程序设计的各个模块。最后，在原Godel语言系统模型的基础上完善了该系统的设计思想。相信在相关理论的支持和指导下，随着后续工作的逐步开展，以及Godel语言编译系统实现技术的逐步成熟，Godel语言将会受到更多的关注。

目录

文摘

英文文摘

声明

第一章绪论

1.1 G(o)del语言简介

1.2 G(o)del语言的理论基础

1.3 G(o)del语言理论研究及系统实现现状

1.4本文的主要工作及篇章结构

第二章G(o)del语言的语法

2.1类型符号

2.2类型一阶语言

2.3 G(o)del语言的语法

第三章G(o)del语言的形式化过程性语义

3.1类型系统

3.1.1类型序关系

3.1.2类型偏序集

3.1.3结构类型序关系

3.1.4类型兼容

3.2类型推断与类型检查

3.2.1类型推断算法

3.2.2类型约束算法

3.2.3类型运算规则

3.3变量置换和合一算法

3.3.1 变量置换

3.3.2合一算法

3.4 SLD反驳-消解法

3.5 SLD反驳消解法的正确性与完备性

3.5.1 SLD反驳消解法的正确性

3.5.2 SLD反驳消解法的完备性

第四章 G(o)del语言程序设计

4.1 G(o)del语言类型系统

4.2 G(o)del语言控制机制

4.2.1 计算规则

4.2.2延迟计算

4.2.3剪枝机制

4.3 G(o)del语言模块系统

4.4 G(o)del语言中元程序设计及应用

4.4.1 目标程序表示

4.4.2动态元程序设计

第五章 G(o)del语言编译系统的实现原理

第六章 总结与展望

参考文献

致谢