Partiality and recursion in higher-order logic

DOI10.1007/978-3-642-37075-5_12MaRDI QIDQ4910419zbMATH OpenOpenAlexFDO

Authors Łukasz Czajka

Publication date 18 March 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Abstract: We present an illative system I_s of classical higher-order logic with subtyping and basic inductive types. The system I_s allows for direct definitions of partial and general recursive functions, and provides means for handling functions whose termination has not been proven. We give examples of how properties of some recursive functions may be established in our system. In a technical appendix to the paper we prove consistency of I_s. The proof is by model construction. We then use this construction to show conservativity of I_s over classical first-order logic. Conservativity over higher-order logic is conjectured, but not proven.

Recommendations

• Partial Recursive Functions in Higher-Order Logic
• Partial and nested recursive function definitions in higher-order logic
• Partial functions in a total setting
• scientific article; zbMATH DE number 515734
• scientific article; zbMATH DE number 4210120

Cited in

(8)

• Partial Recursive Functions in Higher-Order Logic
• scientific article; zbMATH DE number 515734 (Why is no real title available?)
• HYBRID PARTIAL-TOTAL TYPE THEORY
• An untyped higher order logic with Y combinator
• Function definition in higher-order logic
• Types, Tableaus and Gödel’s God in Isabelle/HOL
• On modal logics of partial recursive functions
• Partial and nested recursive function definitions in higher-order logic

This page was built for publication: Partiality and recursion in higher-order logic

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