Proof Relevant Corecursive Resolution

5 years 2 months ago
Proof Relevant Corecursive Resolution
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 rˆole 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 nonterminating type class resolution problems.
Peng Fu 0001, Ekaterina Komendantskaya, Tom Schrij
Added 03 Apr 2016
Updated 03 Apr 2016
Type Journal
Year 2016
Authors Peng Fu 0001, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond
Comments (0)