Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings
Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings
复制标题
软件科学与计算结构基础 - 第 20 届国际会议，FOSSACS 2017，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2017，瑞典乌普萨拉，2017 年 4 月 22-29 日，会议记录
DOI：
10.1007/978-3-662-54458-7_31
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Altenkirch T
中科院分区：
文献类型：
--
作者：
Altenkirch T
Capretta的延迟Monad可以用来模拟部分计算，但它具有内置的相等、很强的双向相似性的“错误”概念。另一种选择是用平等、弱相似的“正确”概念来计算延迟单数的商。然而，查普曼等人最近的工作。指出如果不假定可数选择的公理(实例)，就不可能在类型理论的常见形式的结果结构上定义单数结构。利用同伦类型理论的思想--更高的归纳-归纳类型--我们不依赖于可数选择来构造偏好单数。我们证明了在存在可数选择的情况下，我们的偏好单子等价于弱互相似商的延迟单子。此外，我们还概述了几种应用。
Capretta’s delay monad can be used to model partial computations, but it has the “wrong” notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the “right” notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice.Using an idea from homotopy type theory—a higher inductive-inductive type—we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications.