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
In a PCF-like call-by-name typed λ-calculus with a minimal fixpoint operator, ‘parallelor’, Plotkin's ‘continuous existential quantifier’ 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 → , where and are the flat domains of natural numbers and boolean values, respectively.
(Received October 24 1991)
(Revised June 17 1993)