CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Fixed Points of Type Constructors and Primitive Recursion

Andreas Abel (Institutionen för datavetenskap) ; Ralph Matthes
Lecture Notes in Computer Science (0302-9743). Vol. 3210 (2004), p. 190-204.
[Artikel, refereegranskad vetenskaplig]

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 non-strictly positive type constructors of arbitrary finite kinds, where fixed-point 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.



Denna post skapades 2013-06-18. Senast ändrad 2016-10-18.
CPL Pubid: 178801

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap (2002-2004)

Ämnesområden

Data- och informationsvetenskap

Chalmers infrastruktur