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

Iteration and coiteration schemes for higher-order and nested datatypes

Andreas Abel (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; R. Matthes ; T. Uustalu
Theoretical Computer Science (03043975). Vol. 333 (2005), 1-2, p. 3-66.
[Artikel, refereegranskad vetenskaplig]

This article studies the implementation of inductive and coinductive constructors of higher kinds (higher-order nested datatypes) in typed term rewriting, with emphasis on the choice of the iteration and coiteration constructions to support as primitive. We propose and compare several well-behaved extensions of System Fω with some form of iteration and coiteration uniform in all kinds. In what we call Mendler-style systems, the iterator and coiterator have a computational behavior similar to the general recursor, but their types guarantee termination. In conventional-style systems, monotonicity witnesses are used for a notion of monotonicity defined uniformly for all kinds. Our most expressive systems GMItω and GItω of generalized Mendler, resp. conventional (co)iteration encompass Martin, Gibbons and Bailey's efficient folds for rank-2 inductive types. Strong normalization of all systems considered is proved by providing an embedding of the basic Mendler-style system MItω into System Fω.



Denna post skapades 2010-01-25. Senast ändrad 2016-10-18.
CPL Pubid: 110804

 

Läs direkt!


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