Theory Morphisms in Church's Type Theory with Quotation and Evaluation
William M. Farmer

TL;DR
This paper introduces ${\rm CTT}_{\rm uqe}$, an extension of Church's type theory with quotation and evaluation, enabling reasoning about syntax, semantics, and theory morphisms, including undefined expressions and multiple base types.
Contribution
It formalizes syntax and semantics for ${\rm CTT}_{\rm uqe}$ and defines theory morphisms within this framework, expanding the applicability of Church's type theory.
Findings
Defined syntax and semantics of ${\rm CTT}_{\rm uqe}$
Introduced theory morphisms for ${\rm CTT}_{\rm uqe}$
Provided illustrative examples of theory morphisms
Abstract
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. is a variant of that admits undefined expressions, partial functions, and multiple base types of individuals. It is better suited than as a logic for building networks of theories connected by theory morphisms. This paper presents the syntax and semantics of , defines a notion of a theory morphism from one theory to another, and gives two simple examples that illustrate the use of theory morphisms in .
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSemantic Web and Ontologies · Logic, programming, and type systems · Constraint Satisfaction and Optimization
