Theory Morphisms in Church's Type Theory with Quotation and Evaluation

摘要

CTT_(qe) is a version of Church's type theory with global quotation and evaluation operators that is engineered to reason about the interplay of syntax and semantics and to formalize syntax-based mathematical algorithms. CTT_(uqe) is a variant of CTT_(qe) that admits undefined expressions, partial functions, and multiple base types of individuals. It is better suited than CTT_(qe) as a logic for building networks of theories connected by theory morphisms. This paper presents the syntax and semantics of CTT_(uqe), defines a notion of a theory morphism from one CTT_(uqe) theory to another, and gives two simple examples involving monoids that illustrate the use of theory morphisms in CTT_(uqe).