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?

Denna text är utskriven från följande webbsida:
http://gu.se/forskning/publikation/?publicationId=178801
Utskriftsdatum: 2020-02-28