Theory morphisms in Church's type theory with quotation and evaluation

DOI10.1007/978-3-319-62075-6_11zbMATH Open1367.68302arXiv1703.02117OpenAlexW2605359050MaRDI QIDQ2364672FDOQ2364672

Authors: William M. Farmer 

Publication date: 21 July 2017

Abstract: ${mCTT}_{mqe}$ 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. ${mCTT}_{muqe}$ is a variant of ${mCTT}_{mqe}$ that admits undefined expressions, partial functions, and multiple base types of individuals. It is better suited than ${mCTT}_{mqe}$ as a logic for building networks of theories connected by theory morphisms. This paper presents the syntax and semantics of ${mCTT}_{muqe}$, defines a notion of a theory morphism from one ${mCTT}_{muqe}$ theory to another, and gives two simple examples that illustrate the use of theory morphisms in ${mCTT}_{muqe}$.

Full work available at URL: https://arxiv.org/abs/1703.02117

Recommendations

• Incorporating quotation and evaluation into Church's type theory
• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• Ratio and Product Type Exponential Estimators of Population Mean in Double Sampling for Stratification
• Andrews' type theory with undefinedness
• HOL Light QE

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Knowledge representation (68T30)

Cites Work

• An introduction to mathematical logic and type theory: To truth through proof.
• Title not available (Why is that?)
• HOL Light: An Overview
• Automated Reasoning
• Mathematical knowledge management: transcending the one-brain-barrier with theory graphs
• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• The formalization of syntax-based mathematical algorithms using quotation and evaluation
• Andrews' type theory with undefinedness
• High-Level Theories

Cited In (5)

• Ratio and Product Type Exponential Estimators of Population Mean in Double Sampling for Stratification
• Incorporating quotation and evaluation into Church's type theory
• Andrews' type theory with undefinedness
• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• Formalizing mathematical knowledge as a biform theory graph: a case study

Uses Software

• ML
• HOL
• ETPS
• HOL Light

This page was built for publication: Theory morphisms in Church's type theory with quotation and evaluation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2364672)