RAIRO-Theor. Inf. Appl.
Volume 33, Number 4-5, July October 1999
|Page(s)||309 - 328|
|Published online||15 August 2002|
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
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.