No Cover Image

Conference contribution 145 views 9 downloads

Undecidability of Equality for Codata Types / Ulrich Berger; Anton Setzer

Coalgebraic Methods in Computer Science, Volume: 11202

Swansea University Author: Berger, Ulrich

Abstract

Decidability of type checking for dependently typed systems such as Coq or Agda requires a decidable equality on types. Since bisimilarity on (weakly final) coalgebras such as streams is undecidable, one is forced to use an intensional or definitional form of equality instead which equates two terms...

Full description

Published in: Coalgebraic Methods in Computer Science
ISBN: 978-3-030-00388-3 978-3-030-00389-0
ISSN: 0302-9743 1611-3349
Published:
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa39954
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2018-12-13T13:56:40Z
last_indexed 2019-06-28T14:32:17Z
id cronfa39954
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-06-28T13:18:47Z</datestamp><bib-version>v2</bib-version><id>39954</id><entry>2018-05-03</entry><title>Undecidability of Equality for Codata Types</title><alternativeTitle></alternativeTitle><author>Ulrich Berger</author><firstname>Ulrich</firstname><surname>Berger</surname><active>true</active><ORCID>0000-0002-7677-3582</ORCID><ethesisStudent>false</ethesisStudent><sid>61199ae25042a5e629c5398c4a40a4f5</sid><email>1033ad124f5b3817f154c6a412b415fb</email><emailaddr>CKinmB6DN60fV15NUChxf9yvqZQRJmUl2lxhnzSZE7o=</emailaddr><date>2018-05-03</date><deptcode>SCS</deptcode><abstract>Decidability of type checking for dependently typed systems such as Coq or Agda requires a decidable equality on types. Since bisimilarity on (weakly final) coalgebras such as streams is undecidable, one is forced to use an intensional or definitional form of equality instead which equates two terms if they reduce to the same normal form. For reasoning about equalityof streams one introduces bisimilarity as a propositional rather than judgemental equality.This paper shows that it is not possible to strengthen intensional equality in a decidable way while having the property that the equality respects one step expansion, which means that a stream with head n and tail s is equal to cons(n,s). This property, which would be very useful in type checking, would not necessarily imply that bisimilar streams are equal, and we prove that there exist equalities with this properties which are not bisimilarity. While a proof that bisimilarity on streams is undecidable is straightforward, proving that respecting one step expansion makes equality undecidable is much more involved and relies on an inseparability result for sets of codes for Turing machines. We prove this theorem both for streams with primitive corecursion and with coiteration as introduction rule.It follows that pattern matching on streams, understood literally, is not a valid principle, since it assumes that every stream is equal to a stream of the form cons(n,s). We relate this problem to the subject reduction problem found when adding pattern matching on coalgebras to Coq and Agda. We discuss how this was solved in Agda by defining coalgebras by their elimination rule and replacing pattern matching on coalgebras by copattern matching, and how this relates to the approach in Agda which uses the type of delayed computations.</abstract><type>Conference contribution</type><journal>Coalgebraic Methods in Computer Science</journal><volume>11202</volume><journalNumber/><paginationStart/><paginationEnd>55</paginationEnd><publisher></publisher><placeOfPublication/><isbnPrint>978-3-030-00388-3</isbnPrint><isbnElectronic>978-3-030-00389-0</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords>Coalgebra, weakly final coalgebras, codata, decidable type checking, Martin-Lof type theory, intensional equality, intensional type theory, dependent type theory, undecidability results, inseparability, pattern matching, copattern matching</keywords><publishedDay>0</publishedDay><publishedMonth>0</publishedMonth><publishedYear>0</publishedYear><publishedDate>0001-01-01</publishedDate><doi>10.1007/978-3-030-00389-0_4</doi><url></url><notes></notes><college>College of Science</college><department>Computer Science</department><CollegeCode>CSCI</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution/><researchGroup>Theoretical Computer Science</researchGroup><supervisor/><sponsorsfunders/><grantnumber/><degreelevel/><degreename>None</degreename><lastEdited>2019-06-28T13:18:47Z</lastEdited><Created>2018-05-03T23:21:10Z</Created><path><level id="1">College of Science</level><level id="2">Computer Science</level></path><authors><author><firstname>Ulrich</firstname><surname>Berger</surname><orcid/><order>1</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid/><order>2</order></author></authors><documents><document><filename>0039954-13122018102927.pdf</filename><originalFilename>39954.pdf</originalFilename><uploaded>2018-12-13T10:29:27Z</uploaded><type>Output</type><contentLength>354764</contentLength><contentType>application/pdf</contentType><version>AM</version><cronfaStatus>true</cronfaStatus><action>Published to Cronfa</action><actionDate>13/12/2018</actionDate><embargoDate>2019-09-20T00:00:00</embargoDate><documentNotes/><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents></rfc1807>
spelling 2019-06-28T13:18:47Z v2 39954 2018-05-03 Undecidability of Equality for Codata Types Ulrich Berger Ulrich Berger true 0000-0002-7677-3582 false 61199ae25042a5e629c5398c4a40a4f5 1033ad124f5b3817f154c6a412b415fb CKinmB6DN60fV15NUChxf9yvqZQRJmUl2lxhnzSZE7o= 2018-05-03 SCS Decidability of type checking for dependently typed systems such as Coq or Agda requires a decidable equality on types. Since bisimilarity on (weakly final) coalgebras such as streams is undecidable, one is forced to use an intensional or definitional form of equality instead which equates two terms if they reduce to the same normal form. For reasoning about equalityof streams one introduces bisimilarity as a propositional rather than judgemental equality.This paper shows that it is not possible to strengthen intensional equality in a decidable way while having the property that the equality respects one step expansion, which means that a stream with head n and tail s is equal to cons(n,s). This property, which would be very useful in type checking, would not necessarily imply that bisimilar streams are equal, and we prove that there exist equalities with this properties which are not bisimilarity. While a proof that bisimilarity on streams is undecidable is straightforward, proving that respecting one step expansion makes equality undecidable is much more involved and relies on an inseparability result for sets of codes for Turing machines. We prove this theorem both for streams with primitive corecursion and with coiteration as introduction rule.It follows that pattern matching on streams, understood literally, is not a valid principle, since it assumes that every stream is equal to a stream of the form cons(n,s). We relate this problem to the subject reduction problem found when adding pattern matching on coalgebras to Coq and Agda. We discuss how this was solved in Agda by defining coalgebras by their elimination rule and replacing pattern matching on coalgebras by copattern matching, and how this relates to the approach in Agda which uses the type of delayed computations. Conference contribution Coalgebraic Methods in Computer Science 11202 55 978-3-030-00388-3 978-3-030-00389-0 0302-9743 1611-3349 Coalgebra, weakly final coalgebras, codata, decidable type checking, Martin-Lof type theory, intensional equality, intensional type theory, dependent type theory, undecidability results, inseparability, pattern matching, copattern matching 0 0 0 0001-01-01 10.1007/978-3-030-00389-0_4 College of Science Computer Science CSCI SCS Theoretical Computer Science None 2019-06-28T13:18:47Z 2018-05-03T23:21:10Z College of Science Computer Science Ulrich Berger 1 Anton Setzer 2 0039954-13122018102927.pdf 39954.pdf 2018-12-13T10:29:27Z Output 354764 application/pdf AM true Published to Cronfa 13/12/2018 2019-09-20T00:00:00 true eng
title Undecidability of Equality for Codata Types
spellingShingle Undecidability of Equality for Codata Types
Berger, Ulrich
title_short Undecidability of Equality for Codata Types
title_full Undecidability of Equality for Codata Types
title_fullStr Undecidability of Equality for Codata Types
title_full_unstemmed Undecidability of Equality for Codata Types
title_sort Undecidability of Equality for Codata Types
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Berger, Ulrich
author Berger, Ulrich
author2 Ulrich Berger
Anton Setzer
format Conference contribution
container_title Coalgebraic Methods in Computer Science
container_volume 11202
institution Swansea University
isbn 978-3-030-00388-3
978-3-030-00389-0
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-030-00389-0_4
college_str College of Science
hierarchytype
hierarchy_top_id collegeofscience
hierarchy_top_title College of Science
hierarchy_parent_id collegeofscience
hierarchy_parent_title College of Science
department_str Computer Science{{{_:::_}}}College of Science{{{_:::_}}}Computer Science
document_store_str 1
active_str 1
researchgroup_str Theoretical Computer Science
description Decidability of type checking for dependently typed systems such as Coq or Agda requires a decidable equality on types. Since bisimilarity on (weakly final) coalgebras such as streams is undecidable, one is forced to use an intensional or definitional form of equality instead which equates two terms if they reduce to the same normal form. For reasoning about equalityof streams one introduces bisimilarity as a propositional rather than judgemental equality.This paper shows that it is not possible to strengthen intensional equality in a decidable way while having the property that the equality respects one step expansion, which means that a stream with head n and tail s is equal to cons(n,s). This property, which would be very useful in type checking, would not necessarily imply that bisimilar streams are equal, and we prove that there exist equalities with this properties which are not bisimilarity. While a proof that bisimilarity on streams is undecidable is straightforward, proving that respecting one step expansion makes equality undecidable is much more involved and relies on an inseparability result for sets of codes for Turing machines. We prove this theorem both for streams with primitive corecursion and with coiteration as introduction rule.It follows that pattern matching on streams, understood literally, is not a valid principle, since it assumes that every stream is equal to a stream of the form cons(n,s). We relate this problem to the subject reduction problem found when adding pattern matching on coalgebras to Coq and Agda. We discuss how this was solved in Agda by defining coalgebras by their elimination rule and replacing pattern matching on coalgebras by copattern matching, and how this relates to the approach in Agda which uses the type of delayed computations.
published_date 0001-01-01T05:03:43Z
_version_ 1647974152761507840
score 10.901736