适用于程序规范说明的Institution范畴的完备性研究

A Study on the Completeness of Institution Category for Programming Specification

Institution作为一般框架下的逻辑系统,在数据库理论、程序设计语言、模块化技术和人工智能等方面有着重要的应用。论文主要研究了Institution范畴的完备性,它直观上表明如果基调类可分解,那么它们对应的Institution也可分解。这为大规模程序设计中模块化程序的安全分解和调用提供了一定的逻辑支持。首先,根据基调类范畴中的极限r:SignD',构造了一个Institution&,讨论了&中的一些性质,特别是闭包引理和表示定理;然后又建立了Institution范畴Ins中相应的极限r:&D,得到了遗忘函子U:Ins→Sig反射极限的重要结论,从而推广了Sign:Th→Sign反射余极限的关键性结果;最后给出了Ins的完备性定理。

Institution is a kind of formalized logical system which has been widely applied in database theory,programming languages,modularized program and artificial intelligence.In this paper,the completeness of institution category is presented,which shows that the corresponding institutions are resoluble if the signature classes are resoluble.Firstly,the limit r:&D of Institution category Ins is skillfully constructed from the limit r:SignD′ of signature category.Some of the main results of Institution &,especially Closure Lemma and Presentation Theorem are generalized.Then the conclusion of forgetful functor U:Ins→Sig reflecting limits is obtained.It shows that Institution category Ins is complete.