Monotone (co)inductive types and positive fixed-point types
LFE für Theoretische Informatik,
Institut für Informatik der Universität München,
Oettingenstraße 67, 80538 München, Germany;
Revised: 2 June 1999
We study five extensions of the polymorphically typed lambda-calculus (system F) by type constructs intended to model fixed-points of monotone operators. Building on work by Geuvers concerning the relation between term rewrite systems for least pre-fixed-points and greatest post-fixed-points of positive type schemes (i.e., non-nested positive inductive and coinductive types) and so-called retract types, we show that there are reduction-preserving embeddings even between systems of monotone (co)inductive types and non-inter leav ing positive fixed-point types (which are essentially those retract types). The reduction relation considered is β- and η-reduction for system FF plus either (full) primitive recursion on the inductive types or (full) primitive corecursion on the coinductive types or an extremely simple rule for the fixed-point types. Monotonicity is not confined to the syntactic restriction on type formation of having only positive occurrences of the type variable α in ρ for the inductive type µαρ or the coinductive type ναρ. Instead of that only a “monotonicity witness” which is a term of type ∀α∀β.(α → β) → ρ → ρ[α:=β] is required. This term may already use (co)recursion such that our monotone (co)inductive types may even be “interleaved” and not only nested.
Mathematics Subject Classification: 03B40 / 68Q42 / 68Q65
Key words: System F / monotonicity witness / monotone inductive type monotone coinductive type / retract type / primitive recursion / primitive corecursion / iteration / coiteration.
© EDP Sciences, 1999