The D-Calculus: A System to Describe the Semantics of Programs Involving Complex Data Types

Abstract

Variants of the λ-calculus together with D. Scott’s lattice-theoretic models have turned out to be a basic tool for describing the semantics of programming languages (e.g. [LANDIN 66], [REYNOLDS 72, 74], [SCOTT 74], [SCOTT-STRACHEY 71]). Based upon these approaches, in LCF [WEYHRAUCH-MILNER 72] a typed λ-calculus has been imbedded into a type theory providing a system in which properties about programs can be proven and programs can be constructed according to the properties being specified. The D-calculus presented in this paper contains essentially three new concepts that extend and refine the above systems:

• (1) The D-calculus is an overtyped system combining the advantages of both typed and untyped systems without having the restrictions brought about by types. Hence, e.g. the semantics of programming language constructs having side effects and procedures taking arbitrary procedures as arguments as well as the intricacies of modes in ALGOL 68 can be adequately described in overtyped systems. A detailed account of overtyping the λ-calculus and such examples of applications is given in [RAULEFS 74].

• (2) Abstract data types are introduced in terms of inverse systems of complete partially ordered sets (cpo-sets) that are refinements of the lattices developed by Scott and reflect the structure of data types more closely.

• (3) The β-reduction mechanism of the λ-calculus is generalized to matching the binder to the argument — i.e. computing a substitution that makes the binder equal to the argument — and applying this substitution to the body of the λ-term. The control structure of “sugared” λ-calculi is generalized by using a pattern matching mechanism.