Tarski's Fixed-Point Theorem And Lambda Calculi With Monotone Inductive Types

Author: Matthes R.

Source: Synthese, Volume 133, Numbers 1-2, October 2002 , pp. 107-129(23)

Publisher: Springer

Buy & download fulltext article:

Price: $47.00 plus tax (Refund Policy)

Abstract:

The new concept of lambda calculi with monotone inductive types is introduced by help of motivations drawn from Tarski's fixed-point theorem (in preorder theory) and initial algebras and initial recursive algebras from category theory. They are intended to serve as formalisms for studying iteration and primitive recursion on general inductively given structures. Special accent is put on the behaviour of the rewrite rules motivated by the categorical approach, most notably on the question of strong normalization (i.e., the impossibility of an infinite sequence of successive rewrite steps). It is shown that this key property hinges on the concrete formulation. The canonical system of monotone inductive types, where monotonicity is expressed by a monotonicity witness being a term expressing monotonicity through its type, enjoys strong normalization shown by an embedding into the traditional system of non-interleaving positive inductive types which, however, has to be enriched by the parametric polymorphism of system F. Restrictions to iteration on monotone inductive types already embed into system F alone, hence clearly displaying the difference between iteration and primitive recursion with respect to algorithms despite the fact that, classically, recursion is only a concept derived from iteration.

Language: English

Document Type: Research article

Affiliations: 1: Lehr- und Forschungseinheit für theoretische Informatik Institut für Informatik der Universität München Germany E-mail: matthes@informatik.uni-muenchen.de

Publication date: 2002-10-01