Quotienting the delay monad by weak bisimilarity
Quotienting the delay monad by weak bisimilarity
复制标题
通过弱双相似性对延迟单子进行引用
DOI：
10.1017/s0960129517000184
复制
发表时间：
2015
影响因子：
0.5
通讯作者：
Niccolò Veltri
中科院分区：
文献类型：
--
作者：
James Chapman;Tarmo Uustalu;Niccolò Veltri
延迟数据类型是由Capretta（计算机科学中的逻辑方法，1(2)，2005年第1篇）在Martin-Löf类型理论中作为处理部分函数（如可计算性理论）的一种手段引入的。延迟数据类型是单子。如果两个延迟的计算在其中一个终止时以相等的值终止，则通常认为它们是相等的。这种识别背后的等价关系称为弱双相似性。在类型理论中，通常用集类代替商。在这种方法中，由弱双相似度组成的延迟数据类型仍然是一个单子——一个可能单子的建设性替代方案。在本文中，我们考虑了Hofmann （extensionconstructs In intensiontype Theory，施普林格，London, 1997）用类归纳商类型扩展类型论的替代方法。在这种设置中，很难为有商数据类型定义预期的单子乘法。我们给出了一个解，其中我们假设了一些原理，关键命题的可拓性和可数选择公理。利用这些原理，我们还证明了商延迟数据类型提供自由ω-完全点偏阶（ωcppos）。Altenkirch et al. （Lecture Notes in Computer Science, vol. 10203，施普林格，Heidelberg, 534-549, 2017）证明了在同勒型理论中，某一高电感-电感型本质上是由定义的X型上的自由λ cppo；这使他们能够在不依赖选择原则的情况下获得一组免费ωcppos。我们注意到，通过类似的构造，一个更简单的普通高归纳类型给出了单位类型1上的自由可数完全连接半格。这种类型足以构造一个单子，它与Altenkirch等人的单子是同构的。我们已经在Agda依赖类型编程语言中完全形式化了我们的结果。
The delay datatype was introduced by Capretta (Logical Methods in Computer Science, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad–a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (Extensional Constructs in Intensional Type Theory, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωcppos). Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534–549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive–inductive type is the free ωcppo on a type X essentially by definition; this allowed them to obtain a monad of free ωcppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.
重温偏爱：作为商归纳-归纳类型的偏爱 Monad
DOI：
10.48550/arxiv.1610.09254
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Altenkirch T
通讯作者：
Altenkirch T