×

Monotone inductive and coinductive constructors of rank 2. (English) Zbl 0999.68037

Fribourg, Laurent (ed.), Computer science logic. 15th international workshop, CSL 2001, 10th annual conference of the EACSL, Paris, France, September 10-13, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2142, 600-614 (2001).
Summary: A generalization of positive inductive and coinductive types to monotone inductive and coinductive constructors of rank 1 and rank 2 is described. The motivation is taken from initial algebras and final coalgebras in a functor category and the Curry-Howard-correspondence. The definition of the system as a \(\lambda\)-calculus requires an appropriate definition of monotonicity to overcome subtle problems, most notably to ensure that the (co-)inductive constructors introduced via monotonicity of the underlying constructor of rank 2 are also monotone as constructors of rank 1. The problem is solved, strong normalization shown, and the notion proven to be wide enough to cover even highly complex datatypes.
For the entire collection see [Zbl 0971.00033].

MSC:

68N18 Functional programming and lambda calculus
03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite
Full Text: Link