Conference contribution 129 views 3 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 ManuscriptDownload (402.65KB)
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|
Check full text
No Tags, Be the first to tag this record!
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.
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
College of Science