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

DOI10.1007/978-3-319-62075-6_11MaRDI QIDQ2364672zbMATH OpenOpenAlexFDO

Authors William M. Farmer

Publication date 21 July 2017

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

Mathematics Subject Classification ID

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

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}$.

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

Cites work

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

Cited in

(6)

• Incorporating quotation and evaluation into Church's type theory
• Formalizing mathematical knowledge as a biform theory graph: a case study
• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• Andrews' type theory with undefinedness
• Ratio and Product Type Exponential Estimators of Population Mean in Double Sampling for Stratification
• A natural language formalization of perfectoid rings in \(\mathbb{N}\)aproche

Describes a project that uses

Uses Software

• HOL Light
• HOL
• ML
• ETPS

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)