[Prev][Next][Index][Thread]

Results about F^omega with type fixed-points ?!



Currently I am studying extensions of System F^omega by positive
fixed-points of type operators.  These fixed-points are useful to
formalize so-called heterogeneous or nested datatypes.  An example of
such a fixed-point would be

     PList : * -> *
     PList = \A. A + PList (A x A)

which denotes powerlists resp. perfectly balanced leaf-labelled trees.

My question: Is something known about extensions of F^omega by
higher-order fixed-points like "PList"?  Does a proof of normalization
exist?

The literature I came across only deals with positive fixed-points of
kind "*" (lists, trees ...) or with fixed-points that are not positive
and hence destroy normalization.

Any hints very much appreciated.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/