Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Fixed Points of Type Cons… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Fixed Points of Type Constructors and Primitive Recursion

Artikel i vetenskaplig tidskrift
Författare Andreas Abel
Ralph Matthes
Publicerad i Lecture Notes in Computer Science
Volym 3210
Sidor 190-204
ISSN 0302-9743
Publiceringsår 2004
Publicerad vid
Sidor 190-204
Språk en
Ämneskategorier Data- och informationsvetenskap

Sammanfattning

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.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?