论文部分内容阅读
几十年来，软件重用一直是计算机软件科学重要的研究工作之一。从面向过程的结构化方法到面向对象方法都是在提高软件的重用程度，但迄今为止，并没有取得满意的结果。泛型程序设计(GP，Generic Programming)提出了参数化的抽象方法：将软件分解为一系列组件，一个组件和其它组件之间只需最少的前提假设；组件的组合有最大的灵活性。
以C++的STL程序库为代表的命令式泛型程序设计方法，可定义适用与多种数据结构的抽象算法过程；以Haskell为代表的函数式泛型程序设计方法，在递归数据类型结构上定义泛型函数。在某种意义上类似于自底向上和自顶向下两种设计方法。无论是在程序设计技术还是在语言机制方面，都希望为程序设计者提供一种能力，设计出对多种数据结构都能有效计算的算法，提高算法的重用性。
类型系统在知识的表示、程序语言技术和程序验证等方面均起到了支撑作用，使得程序语言的设计，编译器的构造，语言学习和程序理解都更为清晰。类型化在程序设计和定理证明方面都是重要的手段，而且在程序的构造和证明的构造之间找到了明显的结构对应关系(同构)。
本文的主要研究工作可分为三个方面。第一，在类型系统下命令式程序的语义(IMP语言的指称语义和操作语义)描述问题；第二，函数式语言中数据类型的有效定义和表示；第三，模板化元程序设计和函数式泛型程序设计之间存在的相似性和对应关系，在同一个数学框架中刻画命令式和函数式泛型程序的特征。论文还讨论了刻画循环和递归程序指称语义的不动点理论并对其计算意义作出了一个直观的介绍；阐述了类型系统的一些理论基础和逻辑问题。取得了以下具体结果和结论：
(1)基于谓词转换器给出了IMP的指称语义，并证明与状态转换器形式的指称语义是等价的。通过状态转换器和谓词转换器之间的一种对应关系，将其公理语义和指称语义紧密关联起来，方便于在类型系统中对程序语义的刻画及程序验证。
(2)利用纯类型系统的计算完全性和表达能力，重述IMP命令操作语义的推导规则，将其表示成归纳关系，直接刻画了命令的操作语义。表明类型理论不仅适合于函数式程序的证明，也是刻画和证明命令式程序的合理框架。
(3)给出了函数式程序的一种构造多型值的方法。以等式函数为例，利用直积和直和给出了构造多型值的方法。利用这一结果能够定义各种数据类型的相等性，同时，定义相等性的方法也可以借鉴到其它函数的定义上。
(4)给出泛型数据类型存在的一种不动点的表示。使泛型参数的构造更为简洁和有效，将不同的泛型数据类型构造方法统一在一个单一的框架中。
(5)分析命令式和函数式两种典型泛型程序设计方法的共性，考察了二者的方法论基础。应用范畴论方法得到了描述它们共性的一般代数结构，即STL的概念分析是以F共代数为理论基础的，通过定义泛型函数可以映射到这个基本代数上；函数式程序是在初始代数上的运算，即在结构上归纳定义的抽象数据类型以初始代数为基础。二者在范畴的同一框架下，是以内函子对偶联系起来的，本质上相通，可以表示在同一个数学框架中。