Proof relevant corecursive resolution

DOI10.1007/978-3-319-29604-3_9MaRDI QIDQ2798268zbMATH OpenOpenAlexFDO

Authors Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond

Publication date 4 April 2016

Published in Functional and Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1511.09394, https://lirias.kuleuven.be/handle/123456789/525900

zbMATH Keywords

coinductive proofscorecursionHaskell-type class inferenceHorn clause logicresolution

Mathematics Subject Classification ID

Logic in computer science (03B70) Logic programming (68N17) Functional programming and lambda calculus (68N18)

Abstract: Resolution lies at the foundation of both logic programming and type class context reduction in functional languages. Terminating derivations by resolution have well-defined inductive meaning, whereas some non-terminating derivations can be understood coinductively. Cycle detection is a popular method to capture a small subset of such derivations. We show that in fact cycle detection is a restricted form of coinductive proof, in which the atomic formula forming the cycle plays the role of coinductive hypothesis. This paper introduces a heuristic method for obtaining richer coinductive hypotheses in the form of Horn formulas. Our approach subsumes cycle detection and gives coinductive meaning to a larger class of derivations. For this purpose we extend resolution with Horn formula resolvents and corecursive evidence generation. We illustrate our method on non-terminating type class resolution problems.

Recommendations

• Coinductive soundness of corecursive type class resolution
• A type-theoretic approach to resolution
• A coinductive approach to proof search
• Proof-relevant Horn clauses for dependent type inference and term synthesis
• scientific article; zbMATH DE number 475191

Cites work

• A principled approach to programming with nested types in Haskell
• A type-theoretic approach to resolution
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Derivable type classes
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 733401 (Why is no real title available?)
• scientific article; zbMATH DE number 3349329 (Why is no real title available?)
• Idealized coinductive type systems for imperative object-oriented programs
• Non-Looping String Rewriting
• On the Foundations of Corecursion
• Proof methods for corecursive programs
• Qualified Types
• Scrap your boilerplate with class: extensible generic functions
• Termination of rewriting
• Understanding functional dependencies via constraint handling rules
• Uniform proofs as a foundation for logic programming

Cited in

(11)

• Logic programming: laxness and saturation
• A coinductive approach to proof search through typed lambda-calculi
• Coinductive soundness of corecursive type class resolution
• Operational semantics of resolution and productivity in Horn clause logic
• Proof-Relevant Parametricity
• Towards coinductive theory exploration in Horn clause logic: position paper
• Productive corecursion in logic programming
• The new normal: we cannot eliminate cuts in coinductive calculi, but we can explore them
• Category theoretic semantics for theorem proving in logic programming: embracing the laxness
• A type-theoretic approach to resolution
• Into the Infinite - Theory Exploration for Coinduction

This page was built for publication: Proof relevant corecursive resolution

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