正则序类逻辑Institution的Lawvere定理及其初始与终结语义

主要考虑了以下3个问题:(1)通过将正则序类理论态射φ延拓为多类型理论态射,得到了模型函子()·和()#都与φ可交换的结论;(2)获得了正则序类逻辑Institution的Lawvere定理;(3)讨论了正则序类逻辑Institution中合并理论与各因子理论的初始和终结语义.

模块化程序设计的代数理论

文献[1]对程序开发中逐步求精过程予以形式化,提出求精实现的数学定义。本文在此基础上提出模块化实现的概念,作为模块化程序设计过程的形式化定义。本文证明了模块化实现具有水平合成与垂直合成性质,文[1]中的求精实现是本文定义的模块实观的一个特例。

Institution中自由理论态射的合成

本文在一定的条件下建立了Institution中理论态射的粘合与各因子态射的自由性之间的联系.并证明了自由理论态射的复合仍为自由的.