Domain-Theoretic Foundations of Functional Programming

The following sections are included:

• Contents

• Preface

The following sections are included:

• Correctness

• Completeness

• Computational Adequacy

• Full Abstraction

• Universality

The following sections are included:

• Typing Rules for PCF

• Bigstep Semantics for PCF

• Smallstep Semantics for PCF
  • The syntactic preorders and ≲
  • An Abstract Environment Machine for PCF

• Transition Rules of the Abstract Environment Machine

The following sections are included:

• Basic Domain Theory

• Domain Model of PCF

• LCF – A Logic of Computable Functionals

One easily verifies by induction on the structure of derivations that in the Scott model we have whenever M ⇓ V. Thus, the Scott model is correct w.r.t. the operational semantics. This holds in particular for programs, i.e. closed terms of type nat. In this chapter we will show that the Scott model is also computationally adequate for the operational semantics, i.e. that whenever …

We now will use the logical relation R of the previous chapter to cook up a slick proof of Milner's Context Lemma saying that and ≲ coincide at all types. Whereas older proofs were fairly syntactical and combinatorial in character the current proof (due to A. Jung) is fairly abstract and, accordingly, more transparent…

In the previous chapter we have seen that entails M ≲ N as from and it follows that and thus M ≲ N. In this chapter we will show that the reverse implication is not valid for the Scott model. Even more we will show that need not hold even if M and N are observationally equal. This phenomenon occurs already at type (i→i→i)→i and the reason is that there are not enough PCF-definable objects within D_i→i→i…

In this chapter we will discuss logical relations on the Scott model for PCF. These will allow us to express invariance properties of syntactic definability without any reference to syntax and use these to prove in a mathematically precise way that certain elements of the Scott model are not PCF definable…

Up to now we know about the Dσ arising in the Scott model of PCF just that they are domains, i.e. have suprema of directed subsets and a least element. Actually, they have much more properties which will be investigated in this chapter…

Unlike PCF “real” functional programming languages like ML or Haskell provide the facility of defining types recursively. A recursive definition of type A takes the form of a “domain equation” A = E[A] where the right hand side is a type expression typically involving the recursively denned type A. Typical examples of such domain equations are

The aim of this chapter is to show that extensionally fully abstract models of PCF ar unique up to isomorphism. For this purpose we first fix an appropriate notion of model…

In this chapter, based on previous work by K. Sieber, P. O'Hearn, J. Riecke and A. Sandholm (see [Sieber 1992; O'Hearn and Riecke 1995; Riecke and Sandholm 2002]), we define a category S of sequential domains which hosts a model of PCF which in the next chapter will be shown to be fully abstract…

From the main result of Chapter 10 we know that for order extensional models full abstraction is equivalent to PCF definability of all compact elements of all PCF types. For showing that all compact elements of interpretations of PCF types in the model S are actually definable in PCF we will examine the Kripke logical relations at certain varying arities A_n which will be defined subsequently after first fixing some notation in the following definition…

The intention of Domain Theory is to provide a mathematical semantics of computation. However, in the Scott model D for PCF (and also in the sequential domains model S) the type D_i→i does contain (strict) functions that are not computable. The aim of this chapter is to remedy this shortcoming by defining domain endowed with a notion of computability, the so-called effectively given domains.¹ As a byproduct we will arrive at a notion of higher type computability which is usually neglected² in the main stream of recursion-theoretic literature…

The following sections are included:

• Bibliography

• Index