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

PDF  Accepted Manuscript
Download (402.65KB)
DOI (Published version): 10.1007/9783030003890_4
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...
Published in:  Coalgebraic Methods in Computer Science 

ISBN:  9783030003883 9783030003890 
ISSN:  03029743 16113349 
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 
20181213T13:56:40Z 

last_indexed 
20190628T14:32:17Z 
id 
cronfa39954 
recordtype 
SURis 
fullrecord 
<?xml version="1.0"?><rfc1807><datestamp>20190628T13:18:47Z</datestamp><bibversion>v2</bibversion><id>39954</id><entry>20180503</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>0000000276773582</ORCID><ethesisStudent>false</ethesisStudent><sid>61199ae25042a5e629c5398c4a40a4f5</sid><email>1033ad124f5b3817f154c6a412b415fb</email><emailaddr>CKinmB6DN60fV15NUChxf9yvqZQRJmUl2lxhnzSZE7o=</emailaddr><date>20180503</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>9783030003883</isbnPrint><isbnElectronic>9783030003890</isbnElectronic><issnPrint>03029743</issnPrint><issnElectronic>16113349</issnElectronic><keywords>Coalgebra, weakly final coalgebras, codata, decidable type checking, MartinLof 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>00010101</publishedDate><doi>10.1007/9783030003890_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>20190628T13:18:47Z</lastEdited><Created>20180503T23: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>003995413122018102927.pdf</filename><originalFilename>39954.pdf</originalFilename><uploaded>20181213T10: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>20190920T00:00:00</embargoDate><documentNotes/><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents></rfc1807> 
spelling 
20190628T13:18:47Z v2 39954 20180503 Undecidability of Equality for Codata Types Ulrich Berger Ulrich Berger true 0000000276773582 false 61199ae25042a5e629c5398c4a40a4f5 1033ad124f5b3817f154c6a412b415fb CKinmB6DN60fV15NUChxf9yvqZQRJmUl2lxhnzSZE7o= 20180503 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 9783030003883 9783030003890 03029743 16113349 Coalgebra, weakly final coalgebras, codata, decidable type checking, MartinLof type theory, intensional equality, intensional type theory, dependent type theory, undecidability results, inseparability, pattern matching, copattern matching 0 0 0 00010101 10.1007/9783030003890_4 College of Science Computer Science CSCI SCS Theoretical Computer Science None 20190628T13:18:47Z 20180503T23:21:10Z College of Science Computer Science Ulrich Berger 1 Anton Setzer 2 003995413122018102927.pdf 39954.pdf 20181213T10:29:27Z Output 354764 application/pdf AM true Published to Cronfa 13/12/2018 20190920T00: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 
9783030003883 9783030003890 
issn 
03029743 16113349 
doi_str_mv 
10.1007/9783030003890_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 
00010101T05:03:43Z 
_version_ 
1647974152761507840 
score 
10.901736 