| 摘要: |
| 主要考虑了以下3个问题:(1) 通过将正则序类理论态射(延拓为多类型理论态射,得到了模型函子( )·和( )#都与(可交换的结论;(2) 获得了正则序类逻辑Institution的Lawvere定理;(3) 讨论了正则序类逻辑Institution中合并理论与各因子理论的初始和终结语义. |
| 关键词: 代数语义学 程序规范说明 抽象模型论 范畴论 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the Youth Foundation of Guangdong University of Technology under Grant No.042027 (广东工业大学青年基金) |
|
| Lawvere Theorem in Institution of Regular Order-Sorted Equational Logic and Initial (Terminal) Semantics for Its Glued Theories |
|
LIU Fu-Chun
|
| Abstract: |
| 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. |
| Key words: algebraic semantics programming specification abstract model theory category theory |
