Proof relevant corecursive resolution

Peng Fu; Ekaterina Komendantskaya; Tom Schrijvers; Andrew Pond

doi:10.1007/978-3-319-29604-3_9

Proof relevant corecursive resolution

Peng Fu (Lead / Corresponding author)
, Ekaterina Komendantskaya
, Tom Schrijvers
, Andrew Pond

Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

20 Citations (Scopus)

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 rôle 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.

Original language	English
Title of host publication	FLOPS 2016
Subtitle of host publication	Functional and Logic Programming
Editors	Oleg Kiselyov, Andy King
Place of Publication	Switzerland
Publisher	Springer Verlag
Pages	126-143
Number of pages	18
ISBN (Electronic)	9783319296043
ISBN (Print)	9783319296036
DOIs	https://doi.org/10.1007/978-3-319-29604-3_9
Publication status	Published - 2016
Event	13th International Symposium on Functional and Logic Programming, FLOPS 2016 - Kochi, Japan Duration: 4 Mar 2016 → 6 Mar 2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	9613
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	13th International Symposium on Functional and Logic Programming, FLOPS 2016
Country/Territory	Japan
City	Kochi
Period	4/03/16 → 6/03/16

Keywords

Coinductive proofs
Corecursion
Haskell type class inference
Horn clause logic
Resolution

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-29604-3_9

Cite this

@inproceedings{01b7c5f55ea14feba3e68f6fa9114526,

title = "Proof relevant corecursive resolution",

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 r{\^o}le 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.",

keywords = "Coinductive proofs, Corecursion, Haskell type class inference, Horn clause logic, Resolution",

author = "Peng Fu and Ekaterina Komendantskaya and Tom Schrijvers and Andrew Pond",

year = "2016",

doi = "10.1007/978-3-319-29604-3\_9",

language = "English",

isbn = "9783319296036",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "126--143",

editor = "Oleg Kiselyov and Andy King",

booktitle = "FLOPS 2016",

address = "Germany",

note = "13th International Symposium on Functional and Logic Programming, FLOPS 2016 ; Conference date: 04-03-2016 Through 06-03-2016",

}

Fu, P, Komendantskaya, E, Schrijvers, T & Pond, A 2016, Proof relevant corecursive resolution. in O Kiselyov & A King (eds), FLOPS 2016: Functional and Logic Programming. Lecture Notes in Computer Science, vol. 9613, Springer Verlag, Switzerland, pp. 126-143, 13th International Symposium on Functional and Logic Programming, FLOPS 2016, Kochi, Japan, 4/03/16. https://doi.org/10.1007/978-3-319-29604-3_9

Proof relevant corecursive resolution. / Fu, Peng (Lead / Corresponding author); Komendantskaya, Ekaterina; Schrijvers, Tom et al.
FLOPS 2016: Functional and Logic Programming. ed. / Oleg Kiselyov; Andy King. Switzerland: Springer Verlag, 2016. p. 126-143 (Lecture Notes in Computer Science; Vol. 9613).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Proof relevant corecursive resolution

AU - Fu, Peng

AU - Komendantskaya, Ekaterina

AU - Schrijvers, Tom

AU - Pond, Andrew

PY - 2016

Y1 - 2016

N2 - 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ôle 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.

AB - 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ôle 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.

KW - Coinductive proofs

KW - Corecursion

KW - Haskell type class inference

KW - Horn clause logic

KW - Resolution

UR - https://www.scopus.com/pages/publications/84961126357

U2 - 10.1007/978-3-319-29604-3_9

DO - 10.1007/978-3-319-29604-3_9

M3 - Conference contribution

AN - SCOPUS:84961126357

SN - 9783319296036

T3 - Lecture Notes in Computer Science

SP - 126

EP - 143

BT - FLOPS 2016

A2 - Kiselyov, Oleg

A2 - King, Andy

PB - Springer Verlag

CY - Switzerland

T2 - 13th International Symposium on Functional and Logic Programming, FLOPS 2016

Y2 - 4 March 2016 through 6 March 2016

ER -

Proof relevant corecursive resolution

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)

Cite this

Proof relevant corecursive resolution

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)

Cite this