Coinductive soundness of corecursive type class resolution

František Farka; Ekaterina Komendantskaya; Kevin Hammond

doi:10.1007/978-3-319-63139-4_18

Coinductive soundness of corecursive type class resolution

František Farka, Ekaterina Komendantskaya, Kevin Hammond

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

4 Citations (Scopus)

16 Downloads (Pure)

Abstract

Horn clauses and first-order resolution are commonly used to implement type classes in Haskell. Several corecursive extensions to type class resolution have recently been proposed, with the goal of allowing (co)recursive dictionary construction where resolution does not terminate. This paper shows, for the first time, that corecursive type class resolution and its extensions are coinductively sound with respect to the greatest Herbrand models of logic programs and that they are inductively unsound with respect to the least Herbrand models. We establish incompleteness results for various fragments of the proof system.

Original language	English
Title of host publication	Logic-Based Program Synthesis and Transformation
Subtitle of host publication	LOPSTR 2016
Publisher	Springer
Pages	311-327
Number of pages	17
ISBN (Electronic)	9783319631394
ISBN (Print)	9783319631387
DOIs	https://doi.org/10.1007/978-3-319-63139-4_18
Publication status	Published - 25 Jul 2017

Publication series

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

Keywords

Coinduction
Haskell
Herbrand models
Horn clauses
Resolution
Type classes

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-319-63139-4_18

Download pdf
© 2017, Springer International Publishing AG 2017. This work has been made available online in accordance with the publisher’s policies. This is the author created, accepted version manuscript following peer review and may differ slightly from the final published version. The final published version of this work is available at link.springer.com / http://doi.org/10.1007/978-3-319-63139-4_18
Accepted author manuscript, 440 KBLicence: Copyright Publisher

http://hdl.handle.net/10023/11356Licence: Copyright Publisher
Link to publication in Scopus

Fingerprint Dive into the research topics of 'Coinductive soundness of corecursive type class resolution'. Together they form a unique fingerprint.

Cite this

@inproceedings{15c368eecc0d4db299d3b3f34404b602,

title = "Coinductive soundness of corecursive type class resolution",

abstract = "Horn clauses and first-order resolution are commonly used to implement type classes in Haskell. Several corecursive extensions to type class resolution have recently been proposed, with the goal of allowing (co)recursive dictionary construction where resolution does not terminate. This paper shows, for the first time, that corecursive type class resolution and its extensions are coinductively sound with respect to the greatest Herbrand models of logic programs and that they are inductively unsound with respect to the least Herbrand models. We establish incompleteness results for various fragments of the proof system.",

keywords = "Coinduction, Haskell, Herbrand models, Horn clauses, Resolution, Type classes",

author = "Franti{\v s}ek Farka and Ekaterina Komendantskaya and Kevin Hammond",

year = "2017",

month = jul,

day = "25",

doi = "10.1007/978-3-319-63139-4_18",

language = "English",

isbn = "9783319631387",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "311--327",

booktitle = "Logic-Based Program Synthesis and Transformation",

}

TY - GEN

T1 - Coinductive soundness of corecursive type class resolution

AU - Farka, František

AU - Komendantskaya, Ekaterina

AU - Hammond, Kevin

PY - 2017/7/25

Y1 - 2017/7/25

N2 - Horn clauses and first-order resolution are commonly used to implement type classes in Haskell. Several corecursive extensions to type class resolution have recently been proposed, with the goal of allowing (co)recursive dictionary construction where resolution does not terminate. This paper shows, for the first time, that corecursive type class resolution and its extensions are coinductively sound with respect to the greatest Herbrand models of logic programs and that they are inductively unsound with respect to the least Herbrand models. We establish incompleteness results for various fragments of the proof system.

AB - Horn clauses and first-order resolution are commonly used to implement type classes in Haskell. Several corecursive extensions to type class resolution have recently been proposed, with the goal of allowing (co)recursive dictionary construction where resolution does not terminate. This paper shows, for the first time, that corecursive type class resolution and its extensions are coinductively sound with respect to the greatest Herbrand models of logic programs and that they are inductively unsound with respect to the least Herbrand models. We establish incompleteness results for various fragments of the proof system.

KW - Coinduction

KW - Haskell

KW - Herbrand models

KW - Horn clauses

KW - Resolution

KW - Type classes

UR - http://www.scopus.com/inward/record.url?scp=85028345150&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-63139-4_18

DO - 10.1007/978-3-319-63139-4_18

M3 - Conference contribution

AN - SCOPUS:85028345150

SN - 9783319631387

T3 - Lecture Notes in Computer Science

SP - 311

EP - 327

BT - Logic-Based Program Synthesis and Transformation

PB - Springer

ER -