Positive recursive (fixpoint) type cna be added to the polymorphic (Chruch-style) lambda calculus #lambda#2(Ssytem F) in several different ways,depending on the choice of the elimination operator.We compare4 several such defintiions and we hsow that they fall inot two equivalence classes with respect to multual intepretaiblity by means of beta-eta reductions.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: type of iterators and recursors can be seen as imaes of induction axioms udner different dependency erasing maps.
展开▼
