Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, Colocated with ETAPS 2018, Thessaloniki, Greece, April 14-15, 2018, Revised Selected Papers
Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, Colocated with ETAPS 2018, Thessaloniki, Greece, April 14-15, 2018, Revised Selected Papers
复制标题
计算机科学中的代数方法 - 第 14 届 IFIP WG 1.3 国际研讨会，CMCS 2018，与 ETAPS 2018 同期举办，希腊塞萨洛尼基，2018 年 4 月 14-15 日，修订后的精选论文
DOI：
10.1007/978-3-030-00389-0_4
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Berger U
中科院分区：
文献类型：
--
作者：
Berger U
依赖类型语言的类型检查的可判定性通常需要类型上的可判定等式。由于（弱最终）余代数（如流）上的双相似性是不可判定的，因此不能将其用作类型检查中的相等性。相反，基于依赖类型并带有可判定类型检查的语言，如Coq或Agda，使用内涵相等进行类型检查。两个流定义上相等，如果底层项简化为相同的范式，即如果底层程序在语法上是等价的。对于流的相等性的推理，我们引入了双相似性作为一个命题而不是判断的相等性，本文证明了在具有相等性尊重一步扩展的性质的同时，不可能以可判定的方式加强内涵的相等性，这意味着具有头尾的流等于。这个属性，这将是非常有用的类型检查，并不一定意味着bisilimeric流是平等的，我们证明了存在与此属性不符合bisilimidity的等式。虽然证明流上的双相似性是不可判定的是简单的，但证明尊重一步扩展使等式不可判定则要复杂得多，并且依赖于图灵机的代码集的不可分离性结果。我们证明了这一定理的流与原始corecursion和coiteration作为引进规则.因此，流上的模式匹配，从字面上理解，不是一个有效的原则，因为它假设每个流都等于流的形式.我们将这个问题的主题减少问题时，发现添加模式匹配coalgebras Coq和Agda。我们讨论如何解决这是在Agda定义coalgebras由其消除规则和替换模式匹配coalgebras的copattern匹配，以及如何这涉及到的方法在Agda使用的类型的延迟计算，即所谓的“乐谱”的codata类型。
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 headnand tailsis equal to. 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. 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.