Theory Morphisms in Church's Type Theory with Quotation and Evaluation
Abstrak
${\rm CTT}_{\rm 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. ${\rm CTT}_{\rm uqe}$ is a variant of ${\rm CTT}_{\rm qe}$ that admits undefined expressions, partial functions, and multiple base types of individuals. It is better suited than ${\rm CTT}_{\rm qe}$ as a logic for building networks of theories connected by theory morphisms. This paper presents the syntax and semantics of ${\rm CTT}_{\rm uqe}$, defines a notion of a theory morphism from one ${\rm CTT}_{\rm uqe}$ theory to another, and gives two simple examples that illustrate the use of theory morphisms in ${\rm CTT}_{\rm uqe}$.
Topik & Kata Kunci
Penulis (1)
William M. Farmer
Akses Cepat
- Tahun Terbit
- 2017
- Bahasa
- en
- Sumber Database
- arXiv
- Akses
- Open Access ✓