Hostname: page-component-745bb68f8f-kw2vx Total loading time: 0 Render date: 2025-01-09T13:05:04.208Z Has data issue: false hasContentIssue false
  • English
  • Français

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

Published online by Cambridge University Press:  04 March 2009

Thomas Streicher
Thomas Streicher
Affiliation:
Fakultät für Mathematik und Informatik, c/o Lehrstuhl Prof. Wirsing, Ludwig Maximilian Universität, Leopoldstr. 11b, D-80802 München 40, Germany
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 4 , Issue 1 , March 1994 , pp. 111 - 115
Copyright
Copyright © Cambridge University Press 1994

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Kanda, A. (1980) Fully Effective Solutions of Recursive Domain Equations, Ph.D. Thesis, Univ. Warwick.CrossRefGoogle Scholar
Meyer, A. R. (1988) Semantical paradigms: notes on an invited lecture, with two appendices by S. Cosmadakis. In: Proc. LICS'88, IEEE Press.Google Scholar
Plotkin, G. (1977) LCF considered as a programming language. Theor. Comp. Sci. 5.CrossRefGoogle Scholar
Plotkin, G. (1978) Tw as a universal domain. JCSS 17(2).Google Scholar
Plotkin, G. (1983) Domain Theory. Lecture Notes. Univ. Edinburgh.Google Scholar
Rogers, H. (1967) Theory of Recursive Functions and Effective Computability, McGraw-Hill.Google Scholar
Sazonov, V. (1976) Expressability of functions in D. Scott's LCF language. Algebra i Logika 15 308–330.Google Scholar
Smyth, M. B. (1977) Effectively Given Domains. Theor. Comp. Sci. 5.Google Scholar
Streicher, T. (1982) Scott Domains, Computability and the Definability Problem, Diplomarbeit, Kepler Univ. Linz.Google Scholar
Streicher, T. (1983) Definability in Scott Domains. In: Informal Proceedings of Workshop on Semantics of Programming Languages, Chalmers Univ., Gotenburg.Google Scholar