[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
=============================================================================