Mathematical Structures in Computer Science

Table of Contents - 1994 - Volume 4, Issue 01  

Research Article

A universality theorem for PCF with recursive types, parallel-or and xs2203

Thomas Streichera1

a1 Fakultät für Mathematik und Informatik, c/o Lehrstuhl Prof. Wirsing, Ludwig Maximilian Universität, Leopoldstr. 11b, D-80802 München 40, Germany

Abstract

In a PCF-like call-by-name typed λ-calculus with a minimal fixpoint operator, ‘parallelor’, Plotkin's ‘continuous existential quantifier’ xs2203 and recursive types together with constructors and destructors, all computable objects can be denoted by terms of the programming language. According to A. Meyer's terminology (cf. Meyer (1988)), such a programming language is called universal in the sense that any extension of it must be conservative, as all computable objects can already be expressed by program terms.

As a byproduct, we get that, in principle, recursive types could be totally avoided, as they appear as syntactically expressible retracts of the non-recursive type S0960129500000384_xs1D4A9 → S0960129500000384_xs1D4D1, where S0960129500000384_xs1D4A9 and S0960129500000384_xs1D4D1 are the flat domains of natural numbers and boolean values, respectively.

(Received October 24 1991)

(Revised June 17 1993)