HAL CCSD
Undecidability of Equality for Codata Types
Berger, Ulrich
Setzer, Anton
Department of Computer Science [Swansea] ; Swansea University
International audience
Lecture Notes in Computer Science
14th International Workshop on Coalgebraic Methods in Computer Science (CMCS)
Thessaloniki, Greece
Corina Cîrstea
Springer International Publishing
hal-02044645
https://inria.hal.science/hal-02044645
https://inria.hal.science/hal-02044645/document
https://inria.hal.science/hal-02044645/file/473364_1_En_4_Chapter.pdf
https://inria.hal.science/hal-02044645
14th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2018, Thessaloniki, Greece. pp.34-55, ⟨10.1007/978-3-030-00389-0_4⟩
DOI: 10.1007/978-3-030-00389-0_4
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-030-00389-0_4
en
Copattern matching
Intensional equality
Martin-Löf type theory
Decidable type checking
Weakly final coalgebras
Codata
Coalgebra
Intensional type theory
Dependent type theory
Undecidability results
Inseparability
Pattern matching
[INFO]Computer Science [cs]
info:eu-repo/semantics/conferenceObject
Conference papers
Decidability of type checking for dependently typed languages usually requires a decidable equality on types. Since bisimilarity on (weakly final) coalgebras such as streams is undecidable, one cannot use it as the equality in type checking. Instead, languages based on dependent types with decidable type checking such as Coq or Agda use intensional equality for type checking. Two streams are definitionally equal if the underlying terms reduce to the same normal form, i.e. if the underlying programs are syntactically equivalent. For reasoning about equality of streams one introduces bisimilarity as a propositional rather than judgemental equality.In this paper we show that it is not possible to strengthen intensional equality in a decidable way while having the property that equality respects one step expansion, which means that a stream with head n and tail s is equal to $\mathrm {cons}(n,s)$ 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 do not coincide with bisimilarity. Whereas 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.Therefore, pattern matching on streams is, understood literally, not a valid principle, since it assumes that every stream is equal to a stream of the form $\mathrm {cons}(n,s)$ 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, i.e. the so called “musical notation” for codata types.
TC 1
WG 1.3
http://creativecommons.org/licenses/by/
2018-04-14
info:eu-repo/semantics/OpenAccess