GENERAL RECURSION VIA COINDUCTIVE TYPES
GENERAL RECURSION VIA COINDUCTIVE TYPES
复制标题
DOI：
10.2168/lmcs-1(2:1)2005
复制
发表时间：
2005-01-01
影响因子：
0.6
通讯作者：
Capretta, Venanzio
中科院分区：
文献类型：
--
作者：
Capretta, Venanzio
理论计算机科学研究的肥沃领域研究了强化类型理论中一般递归功能的表示。最成功的方法之一是：使用良好的关系，实施操作语义，领域理论的形式化以及域谓词的归纳定义。在这里，提出了一种不同的解决方案：利用共同体类型来建模无限计算。对于每种类型A，我们将某种类型的部分元素与两个构造函数共同生成的部分元素A（）（nu）：第一个，[a]只是返回一个元素a：a：a;第二个（SIC）X，将计算步骤添加到递归元素x：a（nu）中。我们展示了这种简单的设备如何足以使两种给定类型之间的所有递归功能形式化。它允许定义固定点，即连续的操作员。我们将将这种方法与文献中的不同方法进行比较。最后，我们提到的是，具有适当的结构图的形式化定义了一个强大的单调。
A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations, implementation of operational semantics, formalization of domain theory, and inductive definition of domain predicates. Here, a different solution is proposed: exploiting coinductive types to model infinite computations. To every type A we associate a type of partial elements A(,)(nu) coinductively generated by two constructors: the first, [a] just returns an element a: A; the second, (sic)x, adds a computation step to a recursive element x: A(nu). We show how this simple device is sufficient to formalize all recursive functions between two given types. It allows the definition of fixed points of finitary, that is, continuous, operators. We will compare this approach to different ones from the literature. Finally, we mention that the formalization, with appropriate structural maps, defines a strong monad.