Results about F^omega with type fixed-points ?!
Subject: Results about F^omega with type fixed-points ?!
From: Andreas Abel <firstname.lastname@example.org>
Date: Tue, 23 Sep 2003 19:53:41 +0200
Organization: LMU Muenchen
User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.3) Gecko/20030312
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
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.
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich