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

Issue		RAIRO-Theor. Inf. 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?

The OpenURL standard is a protocol for transmission of metadata describing the resource that you wish to access. An OpenURL link contains article metadata and directs it to the OpenURL server of your choice. The OpenURL server can provide access to the resource and also offer complementary services (specific search engine, export of references...). The OpenURL link can be generated by different means.

If your librarian has set up your subscription with an OpenURL resolver, OpenURL links appear automatically on the abstract pages.
You can define your own OpenURL resolver with your EDPS Account. In this case your choice will be given priority over that of your library.
You can use an add-on for your browser (Firefox or I.E.) to display OpenURL links on a page (see http://www.openly.com/openurlref/). You should disable this module if you wish to use the OpenURL server that you or your library have defined.