[Prev][Next][Index][Thread]
Type Fixpoints: Iteration vs. Recursion
I have the pleasure to announce the availability of the following paper:
Type Fixpoints: Iteration vs. Recursion
---------------------------------------
(To appear in Proc. 4th ICFP, Paris, France, September 1999.)
Authors: Zdzislaw Splawski, Faculty of Informatics and Management,
Wroc\l aw University of Technology, Poland
zs@pwr.wroc.pl
Pawel Urzyczyn, Institute of Informatics, Warsaw University, Poland
urzy@mimuw.edu.pl
The paper can be downloaded from http://zls.mimuw.edu.pl/~urzy/ftp.html
Abstract
--------
Positive recursive (fixpoint) types can be added to the polymorphic
(Church-style) lambda calculus \lambda 2 (System {\bf F}) in several different
ways, depending on the choice of the elimination operator. We compare several
such definitions and we show that they fall into two equivalence classes with
respect to mutual interpretability. Elimination operators for fixpoint types
are thus classified as either ``iterators'' or ``recursors''. This
classification has an interpretation in terms of the Curry-Howard
correspondence: types of iterators and recursors can be seen as images
of induction axioms under different dependency-erasing maps.
Systems with recursors are equivalent to a calculus of recursive types
with the operators Fold :
sigma[mu alpha.sigma/alpha] -> mu alpha.sigma and
Unfold: mu alpha.sigma -> sigma[mu alpha.sigma/alpha], where
Unfold circ Fold =_beta I.
It is known that systems with iterators can be defined within lambda 2.
We show that systems with recursors can not. For this we study the notion
of polymorphic type embeddability (via (beta) left-invertible terms) and
we show that if a type sigma is embedded into another type tau
then sigma can not be longer than tau.
=============================================================================
Pawel Urzyczyn urzy@mimuw.edu.pl
Institute of Informatics http://zls.mimuw.edu.pl/~urzy/home.html
University of Warsaw direct phone: +48-22-658-43-77
Banacha 2, room #4280 main office: +48-22-658-31-65
02-097 Warszawa, Poland fax: +48-22-658-31-64
=============================================================================