RAIRO - Theoretical Informatics and Applications (RAIRO: ITA)

Issue		Theoret. Informatics Appl. Volume 33, Number 4/5, July-October 1999
Page(s)		309 - 328
DOI		10.1051/ita:1999120

DOI: 10.1051/ita:1999120
Theoret. Informatics Appl. 33 (1999) 309-328

Monotone (co)inductive types and positive fixed-point types

Ralph Matthes
LFE für Theoretische Informatik, Institut für Informatik der Universität München, Oettingenstraße 67, 80538 München, Germany; (matthes@informatik.uni-muenchen.de)

Received November 15, 1998. Revised June 2, 1999.

Abstract: 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-interleaving positive fixed-point types (which are essentially those retract types). The reduction relation considered is $\beta$ - and $\eta$ -reduction for system F 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 $\alpha$ in $\rho$ for the inductive type ${\mu\alpha\rho}$ or the coinductive type ${\nu\alpha\rho}$ . Instead of that only a "monotonicity witness'' which is a term of type ${\forall\alpha\forall\beta.(\alpha\to\beta)\to\rho\to\rho[\alpha:=\beta]}$ is required. This term may already use (co)recursion such that our monotone (co)inductive types may even be "interleaved'' and not only nested.

Keywords and phrases: System F, monotonicity witness, monotone inductive type,monotone coinductive type, retract type, primitive recursion, primitive corecursion, iteration, coiteration.

AMS Subject Classification: 03B40, 68Q42, 68Q65

What is OpenURL?