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

Lawvere Theorem in Institution of Regular Order-Sorted Equational Logic and Initial (Terminal) Semantics for Its Glued Theories

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

The following three conclusions are found: (1) By regular order-sorted theory morphism being deduced to many-sorted theory morphism, both model functors (). and ()# being commutative with φ have been proved; (2) Lawvere theorem in Institution of regular order-sorted equational logic is presented; (3) The correspondence among initial (terminal) semantics of glued theories and factor theories in Institution of regular order-sorted equational logic is clarified.