Inductive, coinductive, and pointed types
Inductive, coinductive, and pointed types
复制标题
感应式、共感应式和尖头式
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
Brian T. Howard
中科院分区：
文献类型：
--
作者：
Brian T. Howard
简单类型的lambda演算的一个扩展，其中包含结构良好的归纳和共归纳类型，并确定了一类类型的一般递归是可能的。这项工作的动机是某些自然结构的范畴论，特别是概念的代数有界函子，由于弗洛伊德。我们建议，这是一个特别优雅的核心语言，在与递归对象的工作，因为潜在的一般递归包含在一个单一的运营商，互动以及有界迭代和coiteration的设施。
An extension of the simply-typed lambda calculus is presented which contains both well-structured inductive and coinductive types, and which also identifies a class of types for which general recursion is possible. The motivations for this work are certain natural constructions in category theory, in particular the notion of an algebraically bounded functor, due to Freyd. We propose that this is a particularly elegant core language in which to work with recursive objects, since the potential for general recursion is contained in a single operator which interacts well with the facilities for bounded iteration and coiteration.