Fixed Points of Type Constructors and Primitive Recursion

13 years 11 months ago
Fixed Points of Type Constructors and Primitive Recursion
Abstract. For nested or heterogeneous datatypes, terminating recursion schemes considered so far have been instances of iteration, excluding efficient definitions of fixed-point unfolding. Two solutions of this problem are proposed: The first one is a system with equi-recursive nonstrictly positive type constructors of arbitrary finite kinds, where fixedpoint unfolding is computationally invisible due to its treatment on the level of type equality. Positivity is ensured by a polarized kinding system, and strong normalization is proven by a model construction based on saturated sets. The second solution is a formulation of primitive recursion for arbitrary type constructors of any rank. Although without positivity restriction, the second system embeds—even operationally—into the first one.
Andreas Abel, Ralph Matthes
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CSL
Authors Andreas Abel, Ralph Matthes
Comments (0)