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^*, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond

^*Corresponding author for this work

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	Functional and Logic Programming
Subtitle of host publication	13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings
Editors	Oleg Kiselyov, Andy King
Publisher	Springer
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 2016 - Kochi, Japan Duration: 4 Mar 2016 → 6 Mar 2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing
Volume	9613
ISSN (Print)	0302-9743

Conference

Conference	13th International Symposium on Functional and Logic Programming 2016
Abbreviated title	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

General Computer Science
Theoretical Computer Science

Access to Document

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

Cite this

Fu, P., Komendantskaya, E., Schrijvers, T., & Pond, A. (2016). Proof Relevant Corecursive Resolution. In O. Kiselyov, & A. King (Eds.), Functional and Logic Programming: 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings (pp. 126-143). (Lecture Notes in Computer Science; Vol. 9613). Springer. https://doi.org/10.1007/978-3-319-29604-3_9

@inproceedings{a689b0bc9d7e48cdb73a435debe802a6,

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",

pages = "126--143",

editor = "Oleg Kiselyov and Andy King",

booktitle = "Functional and Logic Programming",

address = "United States",

note = "13th International Symposium on Functional and Logic Programming 2016, 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), Functional and Logic Programming: 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9613, Springer, pp. 126-143, 13th International Symposium on Functional and Logic Programming 2016, Kochi, Japan, 4/03/16. https://doi.org/10.1007/978-3-319-29604-3_9

Proof Relevant Corecursive Resolution. / Fu, Peng; Komendantskaya, Ekaterina; Schrijvers, Tom et al.
Functional and Logic Programming: 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings. ed. / Oleg Kiselyov; Andy King. Springer, 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 - http://www.scopus.com/inward/record.url?scp=84961126357&partnerID=8YFLogxK

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 - Functional and Logic Programming

A2 - Kiselyov, Oleg

A2 - King, Andy

PB - Springer

T2 - 13th International Symposium on Functional and Logic Programming 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

Ekaterina Komendantskaya

Cite this

Proof Relevant Corecursive Resolution

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Profiles

Ekaterina Komendantskaya

Cite this