24th July 2006 16:19  WSPC/Book Trim Size for 9in x 6in  MGFP

Publishers’ page

24th July 2006 16:19  WSPC/Book Trim Size for 9in x 6in  MGFP

Publishers’ page

24th July 2006 16:19  WSPC/Book Trim Size for 9in x 6in  MGFP

Publishers’ page

24th July 2006 16:19  WSPC/Book Trim Size for 9in x 6in  MGFP

Publishers’ page

24th July 2006 16:19  WSPC/Book Trim Size for 9in x 6in  MGFP

Contents

Preface vii 1. Introduction 9 2. PCF and its Operational Semantics 21 3. The Scott Model of PCF 31

3.1 Basic Domain Theory . . . . . . . . . . . . . . . . . . . . . 33 3.2 Domain Model of PCF . . . . . . . . . . . . . . . . . . . . . 40 3.3 LCF – A Logic of Computable Functionals . . . . . . . . . 42

4. Computational Adequacy 45 5. Milner’s Context Lemma 51 6. The Full Abstraction Problem 53 7. Logical Relations 59 8. Some Structural Properties of the D_{σ} 65 9. Solutions of Recursive Domain Equations 73 10. Characterisation of Fully Abstract Models 85

vi Book Title

11. Sequential Domains as a Model of PCF 95 12. The Model of PCF in S is Fully Abstract 103 13. Computability in Domains 107 Bibliography 125 Index 127

Preface

This little book is the outcome of a course I have given over the last ten years at the Technical University Darmstadt for students of Mathematics and Computer Science. The aim of this course is to provide a solid basis for students who want to write their Masters Thesis in the field of Denotational Semantics or want to start a PhD in this field. For the latter purpose it has been used successfully also at the Univ. of Birmingham (UK) by the students of Martin Escardó.

Thus I think this booklet serves well the purpose of filling the gap between introductory textbooks like e.g. [Winskel 1993] and the many research articles in the area of Denotational Semantics. Intentionally I have concentrated on denotational semantics based on Domain Theory and neglected the more recent and flourishing field of Game Semantics (see [Hyland and Ong 2000; Abramsky et.al. 2000]) which in a sense is located in between Operational and Denotational Semantics. The reason for this choice is that on the one hand Game Semantics is covered well in [McCusker 1998] and on the other hand I find domain based semantics mathematically simpler than competing approaches since its nature is more abstract and less combinatorial. Certainly this preference is somewhat subjective but my excuse is that I think one should write books rather about subjects which one knows quite well than about subjects with which one is less familiar.

We develop our subject by studying the properties of the well known functional kernel language PCF introduced by D. Scott in the late 1960ies. The scene is set in Chapters 2 and 3 where we introduce the operational and domain semantics of PCF, respectively. Subsequently we concentrate on studying the relation between operational and domain semantics employing more and more refined logical relation techniques culminating in the construction of the fully abstract model for PCF in Chapters 11 and

viii Preface

12. I think that our construction of the fully abstract model is more elegant and more concise than the accounts which can be found in the literature though, of course, heavily based on them. Somewhat off this main thread we show also how to interpret recursive types (Chapter 9) and give a self contained account of computability in Scott domains (Chapter 13) where we prove the classical theorem of [Plotkin 1977] characterizing the computable elements of the Scott model of PCF as those elements definable in PCF extended by two parallel constructs por (“parallel or”) and ∃ (Plotkin’s “continuous existential quantifier”) providing an extensional variant of the dove tailing technique known from basic recursion theory.

Besides basic techniques like naive set theory, induction and recursion (as covered e.g. by [Winskel 1993]) we assume knowledge of basic category theory (as covered by [Barr and Wells 1990] or the first chapters of [MacLane 1998]) from Chapter 9 onwards and knowledge of basic recursion theory only in the final Chapter 13. Except these few prerequisits this little book is essentially self contained. However, the pace of exposition is not very slow and most straightforward verifications—in particular at the beginning—are left to the reader. We recommend the reader to solve the many exercises indicated in the text whenever they show up. Most of them are straightforward and in case they are not we give some hints.

I want to express my gratitude to all the colleagues who over the years have helped me a lot by countless discussions, providing preprints etc. Obviously, this little book would have been impossible without the seminal work of Dana Scott and Gordon Plotkin. The many other researchers in the field of domain theoretic semantics who have helped me are too numerous to be listed here. I mention explicitly just Klaus Keimel and Martin Escardó, the former because he was and still is the soul of our little working group on domain theory in Darmstadt, the latter because his successful use of my course notes for his own teaching brought me to think that it might be worthwhile to publish them. Besides for many comments on the text I am grateful to Martin also for helping me a lot with TEXnical matters. I acknowledge the use of Paul Taylor’s diagram and prooftree macros which were essential for type setting.

Finally I want to thank the staff of IC press for continuous aid and patience with me during the process of preparing this book. I have experienced collaboration with them as most delightful in all phases of the work.

Chapter 1

Introduction

Functional programming languages are essentially as old as the more wellknown imperative programming languges like FORTRAN, PASCAL, C etc. The oldest functional programming language is LISP which was developed by John McCarthy in the 1950ies, i.e. essentially in parallel with FOR-TRAN. Whereas imperative or state-oriented languages like FORTRAN were developed mainly for the purpose of numerical computation the intended area of application for functional languages like LISP was (and still is) the algorithmic manipulation of symbolic data like lists, trees etc.

The basic constructs of imperative languages are commands which modify state (e.g. by an assignment x:=E) and conditional iteration of commands (typically by while-loops). Moreover, imperative languages strongly support random access data structures like arrays which are most important in numerical computation.

In purely functional languages, however, there is no notion of state or state-changing command. Their basic concepts are

• application of a function to an argument

• definition of functions either explicitly (e.g. f(x) = x∗x+1) or recursively (e.g. f(x) = if x=0 then 1 else x∗f(x−1) fi).

These examples show that besides application and definition of functions one needs also basic operations on basic data types (like natural numbers or booleans) and a conditional for definition by cases. Moreover, all common functional programming languages like LISP, Scheme, (S)ML, Haskell etc. provide the facility of defining recursive data types by explicitly listing their constructors as e.g. in the following definition of the data type of binary trees

tree = empty() | mk tree(tree, tree)

10 Domain-theoretic foundations of functional programming

where empty is a 0–ary constructor for the empty tree with no sons and mk tree is a binary constructor taking two trees t_{1} and t_{2} and building a new tree where the left and right sons of its root are t_{1} and t_{2}, respectively. Thus functional languages support not only the recursive definition of functions but also the recursive definition of data types. The latter has to be considered as a great advantage compared to imperative languages like PASCAL where recursive data types have to be implemented via pointers which is known to be a delicate task and a source of subtle mistakes which are difficult to eliminate.

A typical approach to the development of imperative programs is to design a flow chart describing and visualising the dynamic behaviour of the program. Thus, when programming in an imperative language the main task is to organize complex dynamic behaviours, the so–called control flow.

In functional programming, however, the dynamic behaviour of programs need not be specified explicitly. Instead one just has to define the function to be implemented. Of course, in practice these function definitions are fairly hierarchical, i.e. are based on a whole cascade of previously defined auxiliary functions. Then a program (as opposed to a function definition) usually takes the form of an application f(e_{1}, …, e_{n}) which is evaluated by the interpreter^{1}. As programming in a functional language essentially consists of defining functions (explicitly or recursively) one need not worry about the dynamical aspects of execution as this task is taken over completely by the interpreter. Thus, one may concentrate on the what and forget about the how when programming in a functional language. However, when defining functions in a functional programming language one has to stick to the forms of definition as provided by the language and cannot use ordinary set-theoretic language as in everyday mathematics.

In the course of these lectures we will investigate functional (kernel) languages according to the following three aspects

Model  Interpreter

Logic

1But usually implementations of functional languages also provide the facility of compiling your programs.

Introduction 11

or

Denotational Semantics  Operational Semantics

Verification Calculus

respectively and, in particular, how these aspects interact.

First we will introduce a most simple functional programming language PCF (Programming Computable Functionals) with natural numbers as base type but no general recursive types.

The operational semantics of PCF will be given by an inductively defined evaluation relation

E⇓V

specifying which expressions E evaluate to which values V (where values are particular expressions which cannot be further evaluated). For example if E⇓V and E is a closed term of the type nat of natural numbers then V will be an expression of the form \underline{n}, i.e. a canonical expression for the natural number n (usually called numeral). It will turn out as a property of the evaluation relation ⇓ that V_{1} = V_{2} whenever E⇓V_{1} and E⇓V_{2}. That means that ⇓ is determinstic in the sense that ⇓ assigns to a given expression E at most one value. An operational semantics as given by an (inductively defined) evaluation relation ⇓ is commonly called a “Big Step Semantics” as it abstracts from intermediary steps of the computation (of V from E).^{2} Notice that in general there does not exists a value V with E⇓V for arbitrary expressions E, i.e. not every program terminates. This is due to the presence of general recursion in our language PCF guaranteeing that all computable functions on natural numbers can be expressed by PCF programs.

Based on the big step semantics for PCF as given by ⇓ we will introduce a notion of observational equality for closed PCF expressions of the same type where E_{1} and E_{2} are considerd as observationally equal iff for all contexts C[ ] of base type nat it holds that

C[E_{1}]⇓\underline{n} ⟺ C[E_{2}]⇓\underline{n}

2For sake of completeness we will also present a “Small Step Semantics” for PCF as well as an abstract machine serving as an interpreter for PCF.

12 Domain-theoretic foundations of functional programming

for all natural numbers n ∈ ℕ. Intuitively, expressions E_{1} and E_{2} are observationally equal iff the same observations can be made for E_{1} and E_{2} where an observation of E consists of observing that C[E]⇓\underline{n} for some context C[ ] of base type nat and some natural number n. This notion of observation is a mathematical formalisation of the common practice of testing of programs and the resulting view that programs are considered as (observationally) equal iff they pass the same tests.

However, this notion of observational equality is not very easy to use as it involves quantification over all contexts and these form a collection which is not so easy to grasp. Accordingly there arises the desire for more convenient criteria sufficient for observational equality which, in particular, avoid any reference to (the somewhat complex) syntactic notions of evaluation relation and context.

For this purpose we introduce a so-called Denotational Semantics for PCF which assigns to every closed expression E of type σ an element [[E]] ∈ D_{σ}, called the denotation or meaning or semantics of E, where D_{σ} is a previously defined structured set (called “semantic domain”) in which closed expressions of type σ will find their interpretation.

The idea of denotational semantics was introduced end of the 1960ies by Ch. Strachey and Dana S. Scott. Of course, there arises the question of what is the nature of the mathematical structure one should impose on semantical domains. Although the semantic domains which turn out as appropriate can be considered as particular topological spaces they are fairly different^{3} in flavour from the spaces arising in analysis or geometry. An appropriate notion of semantic domain was introduced by Dana S. Scott who also developed their basic mathematical theory to quite some extent of sophistication. From the early 1970ies onwards various research groups all over the world invested quite some energy into developing the theory of semantic domains—from now on simply referred to as Domain Theory— both from a purely mathematical point of view and from the point of view of Computer Science as (at least one) important theory of meaning (semantics) for programming languages.

Though discussed later into much greater detail we now give a preliminary account of how the domains D_{σ} are constructed in which closed terms of type σ find their denotation. For the type nat of natural numbers one puts D_{nat} = ℕ ∪ {⊥} where ⊥ (called “bottom”) stands for the denotation

3In particular, as we shall see they will not satisfy Hausdorff’s separation property requiring that for distinct points x and y there are disjoint open sets U and V containing x and y, respectively.

Introduction 13

of terms of type nat whose evaluation “diverges”, i.e. does not terminate. We think of D_{nat} as endowed with an “information ordering” ⊑ w.r.t. which ⊥ is the least element and all other elements are incomparable. The types of PCF are built up from the base type nat by the binary type forming operator → where D_{σ→τ} is thought of as the type of (computable or continuous) functionals from D_{σ} to D_{τ}, i.e. D_{σ→τ} ⊆ D_{τ}^{D_{σ}} = {f | f : D_{σ} → D_{τ} }. In particular, the domain D_{nat→nat} will consist of certain functions from D_{nat} to itself. It will turn out as appropriate to define D_{nat→nat} as consisting of those functions on ℕ ∪ {⊥} which are monotonic, i.e. preserve the information ordering ⊑. The clue of Domain Theory is that domains are not simply sets but sets endowed with some additional structure and D_{σ→τ} will then accordingly consist of all structure preserving maps from D_{σ} to D_{τ}. However, for higher types (i.e. types of the form σ→τ where σ is different form nat) it will turn out that it is not sufficient for maps in D_{σ→τ} to preserve the information ordering ⊑. One has to require in addition some form of continuity^{4} which can be expressed as the requirement that certain suprema are preserved by the functions. The information ordering on D_{σ→τ} will be defined pointwise, i.e. f ⊑ g iff f(x) ⊑ g(x) for all x ∈ D_{σ}.

Denotational semantics provides a purely extensional view of functional programs as closed expressions of type σ→τ will be interpreted as particular functions from D_{σ} to D_{τ} which are considered as equal when they deliver the same result for all arguments. In other words the meaning of such a program is fully determined by its input/output behaviour. Thus, denotational semantics just captures what is computed by a function (its extensional aspect) and abstracts from how the function is computed (its intensional aspect as e.g. time or space complexity).

When a programming language like PCF comes endowed with an operational and a denotational semantics there arises the question how good they fit together. We will now discuss a sequence of criteria for “goodness of fit” of increasing strength.

Correctness

Closed expressions P and Q of type σ are called semantically or denotationally equal iff [[P]] = [[Q]] ∈ D_{σ}. We call the operational semantics correct w.r.t. the denotational one iff P and V are denotationally equal whenever P ⇓V, i.e. when evaluation preserves semantical equality. In particular for

4which is in accordance with the usual topological notion of continuity when the domains D_{σ} and D_{τ} are endowed with the so-called Scott topology which is defined in terms of the information ordering

14 Domain-theoretic foundations of functional programming

programs, i.e. closed expressions P of base type nat, correctness ensures that [[P]] = n whenever P ⇓\underline{n}, i.e. the operational semantics evaluates a program in case of termination to the number which is prescribed by the denotational semantics.

Completeness

On the other hand it is also desirable that if a program denotes n then the operational semantics evaluates program P to the numeral \underline{n} or, more formally, P ⇓\underline{n} whenever [[P]] = n in which case we call the operational semantics complete w.r.t. the denotational semantics.

Computational Adequacy

In case the operational semantics is both correct and complete w.r.t. the denotational semantics, i.e.

P ⇓\underline{n} ⟺ [[P]]=n

for all programs P and natural numbers n, we say that the denotational semantics is computationally adequate^{5} w.r.t. the operational semantics.

Computational adequacy is sort of a minimal requirement for the relation between operational and denotational semantics and holds for (almost) all examples considered in the literature. Nevertheless, we shall see later that the proof of computational adequacy does indeed require some mathematical sophistication.

If the denotational semantics is computationally adequate w.r.t. the operational semantics then closed expressions P and Q are observationally equal if and only if [[C[P]]] = [[C[Q]]] for all contexts C[ ] of base type, i.e. observational equality can be reformulated without any reference to an operational semantics.

The denotational semantics considered in the sequel will be compositional in the sense that from [[P]] = [[Q]] it follows that [[C[P]]] = [[C[Q]]] for all contexts C[ ] (not only those of base type). Thus, for compositional computationally adequate denotational semantics from [[P]] = [[Q]] it follows that P and Q are observationally equal. Actually, this already entails

5One also might say that “the operational semantics is computationally adequate w.r.t. the denotational semantics” because the denotational semantics may be considered as conceptually prior to the operational semantics. One could enter an endless “philosophical” discussion on what comes first, the operational or the denotational semantics. The authors have a slight preference for the view that denotational semantics should be conceptually prior to operational semantics (the What comes before the How)

being, however, aware of the fact that in practice operational semantics often comes before the denotational semantics.

Introduction 15

completeness of the denotational semantics as if [[P]] = n = [[\underline{n}]] then P and \underline{n} are observationally equal from which it follows that P ⇓\underline{n} ⇔ \underline{n}⇓\underline{n} and, therefore, P ⇓\underline{n} as \underline{n}⇓\underline{n} does hold anyway. Thus, under the assumption of correctness for a compositional denotational semantics computational adequacy is equivalent to the requirement that denotational equality entails observational equality.

Full Abstraction

For those people who think that operational semantics is prior to denotational semantics the notion of observational equality is more basic than denotational equality because the former can be formulated without reference to denotational semantics. From this point of view computational adequacy is sort of a “correctness criterion” as it guarantees that semantic equality entails the “real” observational equality (besides the even more basic requirement that denotation is an invariant of evaluation).

However, one might also require that denotational semantics is complete w.r.t. operational semantics in the sense that observational equality entails denotational equality, in which case one says that the denotational semantics is fully abstract w.r.t. the operational semantics. At first sight this may seem a bit weird because in a sense denotational semantics is more abstract than operational semantics as due to its extensional character it abstracts from intensional aspects such as syntax. However, observational equivalence—though defined a priori in operational terms—is more abstract than denotational equality under the assumption of computational adequacy guaranteeing that denotational equality entails observational equality. Accordingly, a fully abstract semantics induces a notion of denotational equality which is “as abstract as reasonably possible” where “reasonable” here means that terms are not identified if they can be distinguished by observations.

Notice, moreover, that under the assumption of computational adequacy full abstraction can be formulated without reference to operational semantics as follows: closed expressions P and Q (of the same type) are denotationally equal already if C[P] and C[Q] are denotationally equal for all contexts C[ ] of base type. A denotational semantics satisfying this condition is fully abstract w.r.t. an operational semantics iff it is computationally adequate w.r.t. this operational semantics.

Whereas computational adequacy holds for almost all models of PCF this is not the case for full abstraction as exemplified by the (otherwise sort of canonical) Scott model. Though the Scott model (and, actually, also

16 Domain-theoretic foundations of functional programming

all other models considered in the literature) is fully abstract for closed expressions of first order types nat→nat→ … →nat→nat full abstraction fails already for the second order type (nat→nat→nat)→nat.

However, the Scott model is fully abstract for an extension of PCF by a parallel, though deterministic, language construct por : nat→nat→nat, called “parallel or”, which gives 0 as result if its first or its second argument equals 0, 1 if both arguments equal 1 and delivers ⊥ as result in all other cases. This example illustrates quite forcefully the relativity of the notion of full abstraction w.r.t. the language under consideration. The only reason why the Scott model fails to be fully abstract w.r.t. PCF is that it distinguishes closed expressions E_{1} and E_{2} of the type (nat→nat→nat)→nat although these cannot be distinguished by program contexts C[ ] expressible in the language of PCF. However, E_{1} and E_{2} can be distinguished by the context [ ](por). In other words whether a denotational semantics is fully abstract for a language strongly depends on the expressiveness of this very language. Accordingly, a lack of full abstraction can be repaired in two possible, but different ways

(1) keep the model under consideration but extend the language in a way such that the extension can be interpreted in the given model and denotationally different terms can be separated by program contexts expressible in the extended language (e.g. keep the Scott model but extend PCF by por) or

(2) keep the language and alter the model to one which is fully abstract for the given language.

Whether one prefers (1) or (2) depends on whether one gives preference to the model or to the syntax, i.e. the language under consideration. A mathematician’s typical attitude would be (1), i.e. to extend the language in a way that it can grasp more aspects of the model, simply because he is interested in the structure and the language is only a secondary means for communication. However, (even) a (theoretical) computer scientist’s attitude is more reflected by (2) because for him the language under consideration is the primary concern whereas the model is just regarded as a tool for analyzing the language. Of course, one could now enter an endless discussion on which attitude is the more correct or more adequate one. The authors’ opinion rather is that each single attitude when taken absolutely is somewhat disputable as (i) why shouldn’t one take into account various different models instead of stubbornly insisting on a particular “pet model” and (ii) why should one take the language under consideration as

Introduction 17

absolute because even if one wants to exclude por for reasons of efficiency why shouldn’t one allow^{6} the observer to use it?

Instead of giving a preference to (1) or (2) we will present both approaches. We will show that extending PCF by por will render the Scott model fully abstract and we will present a refinement of the Scott model, the so-called sequential domains, giving rise to a fully abstract model for PCF which we consider as a final solution to a—or possibly the—most influential open problem in semantic research in the period 1975–2000. The solution via sequential domains is mainly known under the name “relational approach” because domains are endowed with (a lot of) additional relational structure which functions between sequential domains are required to preserve in addition to the usual continuity requirements of Scott’s Domain Theory.

A competing and, actually, more influential approach is via game semantics where types are interpreted as games and programs as strategies. However, this kind of models is never extensional and, accordingly, not fully abstract for PCF as by Milner’s Context lemma extensional equality entails observational equality. However, the “extensional collapse” of games models turns out as fully abstract for PCF. But this also holds for the term model of PCF and in this respect the game semantic approach cannot really be considered as a genuine solution of the full abstraction problem at least according to its traditional understanding. However, certain variations of game semantics are most appropriate for constructing fully abstract models for non-functional extensions of PCF, e.g. by control operators or references, as for such extensions the term models obtained by factorisation w.r.t. observational equivalence are not extensional anymore and, therefore, the inherently extensional approach via domains is not applicable anymore.

Notice that there is also a more liberal notion of sequentiality, namely the strongly stable domains of T. Ehrhard and A. Bucciarelli where, however, the ordering on function spaces is not pointwise anymore.

Universality

In the Scott model one can distinguish for every type σ a subset C_{σ} ⊆ D_{σ} of computable elements without any reference to PCF-definability such that all PCF-definable elements of D_{σ} are already contained in C_{σ}. Now, if one has fixed such a semantic notion of computability for a model then there arises the question whether all computable elements of the model do

6as for example in cryptology where the attacker is usually assumed to employ as strong weapons as possible

18 Domain-theoretic foundations of functional programming

arise as denotations of closed PCF terms in which case the model is called universal.^{7}

A language universal for the Scott model can be obtained from PCF by adding por (“parallel or”) and Plotkin’s continuous existential quantifier ∃ of type (nat→nat)→nat which is defined as follows: ∃(f) = 0 if f(n) = 0 for some n ∈ ℕ, ∃(f) = 1 if f(⊥) = 1 and ∃(f) = ⊥ in all other cases.

Notice, however, that ∃ cannot be implemented within PCF+por from which it follows that universality is a stronger requirement than full abstraction. But universality entails full abstraction as there is a theorem saying that a model of PCF is fully abstract iff all its “finite” elements are PCF definable and as these “finite” elements are subsumed by any reasonable notion of computability.

We conclude this introductory chapter by discussing the relevance of denotational semantics for logics of programs, i.e. calculi where properties of programs can be expressed and verfied.

First of all denotational models of programming languages are needed for defining validity of assertions about programs as can be expressed in a logic for this programming language. In case of PCF the family (D_{σ})_{σ∈Type} provides the carriers for a many-sorted structure in which one can interpret the terms of the program logic LCF (Logic of Computable Functionals)^{8} whose terms are expressions of the programming language PCF and whose formulas are constructed via the connectives and quantifiers of first order logic from atomic formulas t_{1} ⊑ t_{2} stating that the meaning of t_{1} is below the meaning of t_{2} w.r.t. the information ordering as given by the denotational model. Notice, however, that the term language PCF is not first order as it contains a binding operator λ needed for explict definitions of functions. However, this does not cause any problems for the interpretation of LCF. Instead of first order logic one might equally well consider higher

7Calling this property “universal” is in accordance with the common terminology where a programming language L is called “Turing universal” iff all partial recursive functions on ℕ can be implemented by programs of L. The property “universal” as defined above is stronger since it requires that computable elements of all types can be implemented within the language under consideration. But in both cases “universal”

means that one has already got an implementation for all possible computable elements (of a certain kind).

8The calculus LCF was introduced by D. Scott in an unpublished, but widely circulated and most influential manuscript dating back to 1967. In the 1970ies a proof assistant for LCF was implemented by R. Milner who for this very purpose developed and implemented the functional programming language ML (standing for “Meta-Language”)

whose refined versions SML and OCAML today constitute the most prominent typed call-by-value functional programming languages.

Introduction 19

order logic over a model of PCF which has the advantage that higher order logic allows one to express inductively defined predicates which are most useful for the purposes of program verifiaction.

In principle one could interpret LCF also in the structure obtained by factorizing the closed PCF terms modulo observational equality. However, such a structure is not very easy to analyze as it is too concrete. Denotational models have the advantage that simple and strong proof principles like fixpoint induction, computational induction and Park induction, which are indispensible for reasoning about recursively defined functions and objects, can be easily verified for these models as they are actually derived from some obvious properties of these models.

Chapter 2

PCF and its Operational Semantics

In this chapter we introduce the prototypical functional programming language PCF together with its operational semantics.

The language PCF is a typed language whose set Type of types is defined inductively as follows

• the base type nat is a type and

• whenever σ and τ are types then (σ→τ) is a type, too.

We often write ι for base type nat and σ→τ instead of (σ→τ) where → is understood as a right associative binary operation on Type meaning that e.g. σ_{1}→σ_{2}→σ_{3} is understood as standing for σ_{1}→(σ_{2}→σ_{3}). Due to the inductive definition of Type every type σ is of the form σ_{1}→ … →σ_{n}→ι in a unique way.

As PCF terms may contain free variables we will define terms relative to type contexts where finitely many variables are declared together with their types, i.e. type contexts are expressions of the form

Γ ≡ x_{1}:σ_{1}, …, x_{n}:σ_{n}

where the σ_{i} are types and the x_{i} are pairwise distinct variables. As variables cannot occur in type expressions the order of the single variable declarations x_{i}:σ_{i} in Γ is irrelevant and, accordingly, we identify Γ with Γ′ if the latter arises from the former by a permutation of the x_{i}:σ_{i}.

The valid judgements of the form

Γ ⊢ M : σ (M is a term of type σ in context Γ)

are defined inductivly by the rules in Figure 2.1.

One easily shows by induction on the structure of derivations that whenever Γ ⊢ M : σ can be derived then π(Γ) ⊢ M : σ can be derived, too, for

22 Domain-theoretic foundations of functional programming

Typing Rules for PCF

Γ, x:σ, Δ ⊢ x : σ  {Γ, x:σ ⊢ M : τ \atop Γ ⊢ (λx:σ. M) : σ→τ}

{Γ ⊢ M : σ→τ Γ ⊢ N : σ \atop Γ ⊢ M(N) : τ}  {Γ ⊢ M : σ→σ \atop Γ ⊢ Y_{σ}(M) : σ}

Γ ⊢ zero : nat

Γ ⊢ M : nat

Γ ⊢ succ(M) : nat

Γ ⊢ M : nat

Γ ⊢ pred(M) : nat

Γ ⊢ M_{i} : nat (i=1, 2, 3)
Γ ⊢ ifz(M_{1}, M_{2}, M_{3}) : nat

Figure 2.1 Typing rules for PCF

every permutation π of Γ.

As for every language construct of PCF there is precisely one typing rule one easily shows (Exercise!) that the σ with Γ ⊢ M : σ is determined uniquely by Γ and M. Thus, applying these typing rules backwards gives rise to a recursive type checking algorithm which given M and Γ computes the type σ with Γ ⊢ M : σ provided it exists and reports failure otherwise. (We invite the reader to test this algorithm for some simple examples!)

In the sequel we will not always stick to the “official” syntax of PCF terms as given by the typing rules. Often we write MN or (MN) instead of M(N). In accordance with right-associativity of → we assume that application as given by juxtaposition is left-associative meaning that M_{1} … M_{n} is read as (… (M_{1}M_{2}) … M_{n}) or M_{1}(M_{2}) … (M_{n}), respectively.

For variables bound by λ’s we employ the usual convention of αconversion according to which terms are considered as equal if they can be obtained from each other by an appropriate renaming of bound variables. Furthermore, when substituting term N for variable x in term M we first rename the bound variables of M in such a way that free variables of N will not get bound by lambda-abstractions in M, i.e. we employ so–called capture-free substitution.^{1}

1These are the same conventions as usually employed for the quantifiers ∀ and ∃.

The only difference is that quantifiers turn formulas into formulas whereas λ-abstraction

PCF and its Operational Semantics 23

Before we define the operational semantics of PCF we introduce the notion of “raw terms” of PCF as given by the following grammar

M :: = x | (λx:σ.M) | M(M) | Y_{σ}(M) |
zero | succ(M) | pred(M) | ifz(M, M, M)

in BNF form. Of course, not every raw term is typable as for example λx:nat.x(x) where the first occurrence of x would have to be of functional type in order to render x(x) well-typed.

We now present a “big step” semantics for PCF by inductively defining a binary relation ⇓ on raw terms via the rules exhibited in Figure 2.2 where \underline{n} is the canonical numeral for the natural number n defined as \underline{0} ≡ zero and \underline{k+1} ≡ succ(\underline{k}) by recursion on k.^{2}

Bigstep Semantics for PCF

x ⇓ x  λx:σ.M ⇓ λx:σ.M

{M ⇓ λx:σ.E E[N/x] ⇓ V \atop M(N) ⇓ V}  {M(Y_{σ}(M)) ⇓ V \atop Y_{σ}(M) ⇓ V}

\underline{0} ⇓ \underline{0}  {M ⇓ \underline{n} \atop succ(M) ⇓ \underline{n+1}}

{M ⇓ \underline{0} \atop pred(M) ⇓ \underline{0}}  {M ⇓ \underline{n+1} \atop pred(M) ⇓ \underline{n}}

{M ⇓ \underline{0} M_{1} ⇓ V \atop ifz(M, M_{1}, M_{2}) ⇓ V}  {M ⇓ \underline{n+1} M_{2} ⇓ V \atop ifz(M, M_{1}, M_{2}) ⇓ V}

Figure 2.2 Bigstep Semantics for PCF

Whenever E⇓V then V is a variable, a numeral or a λ-abstraction. It follows by induction on the structure of derivations of E⇓V that the free

turns terms into terms.

2Notice that in the literature one finds variants of PCF where instead of zero there are constants \underline{n} for every natural number n. However, the same rules can be used for defining ⇓ inductively (albeit with a slightly different reading).

24 Domain-theoretic foundations of functional programming

variables of V are contained in the free variables of E. Thus, if E is a closed expression and E⇓V then V is either a numeral or a λ-abstraction without free variables. Such terms are called (syntactic) values and one can see easily that for every such value V it holds that V ⇓V. Thus syntactic values are those terms V such that M⇓V can be derived for some closed term M. Notice that λx:σ.M is a value even if M is not a value, i.e. evaluation stops as soon as it has arrived at a functional abstraction. In our investigations of PCF we are mainly interested in closed terms and will hardly ever need the evaluation rule for variables. This is also the reason why we have not included variables into our definition of syntactic values.

Notice that with the exception of pred and ifz for each construct of PCF there is precisely one evaluation rule. In case of pred and ifz there are two rules which, however, do not overlap (in the sense that for every term at most one of these two rules is applicable). This observation gives rise to the following lemma.

Lemma 2.1 The evaluation relation ⇓ is deterministic, i.e. whenever M⇓V and M⇓W then V ≡ W.

Proof. Straightforward induction on the structure of derivations of M⇓V. (Exercise!) □

Next we will show that evaluation preserves types, a property which is usually called Subject Reduction.

Theorem 2.2 (Subject Reduction) If ⊢ M : σ and M⇓V then ⊢ V : σ.

Proof. Straightforward induction (Exercise!) on the structure of derivations of M⇓V. □

Thus, if M is a closed term of type nat and M⇓V then V ≡ \underline{n} for some natural number n and if M is a closed term of type σ→τ and M⇓V then V ≡ λx:σ.E for some E with x:σ ⊢ E : τ.

Often in the literature one can find definitions of PCF with a base type bool of boolean values included. In this case one adds the following term formation rules

Γ ⊢ true : bool  Γ ⊢ false : bool
Γ ⊢ M : bool Γ ⊢ M_{1} : σ Γ ⊢ M_{2} : σ
(σ ∈ {nat, bool})
Γ ⊢ cond_{σ}(M, M_{1}, M_{2}) : σ

PCF and its Operational Semantics 25

together with the following evaluation rules

true ⇓ true  _{false ⇓ false}
M ⇓ true M_{1} ⇓ V
cond_{σ}(M, M_{1}, M_{2}) ⇓ V

M ⇓ false M_{2} ⇓ V
cond_{σ}(M, M_{1}, M_{2}) ⇓ V

Notice that in this case ifz can be replaced by a predicate isz, i.e. isz(M) is a term of type bool whenever M is a term of type nat and isz(M) evaluates to true iff M⇓\underline{0} and to false iff M⇓\underline{n+1} for some natural number n. Using isz we can implement ifz by putting ifz(M, M_{1}, M_{2}) ≡ cond_{nat}(isz(M), M_{1}, M_{2}).

However, this extension by boolean values is fairly redundant as we can simulate boolean values within nat coding, say, true by \underline{0} and false by \underline{1}.

Next we present a “single step” semantics for PCF and show that it coincides with the big step semantics. The single step semantics is given by specifying a relation ▷ between terms (of the same type) where M▷N reads as “M reduces in one step to N”. This reduction relation ▷ is defined inductively by the rules given in Figure 2.3.

Only the first six rules of Figure 2.3 specify proper computation steps. The purpose of the remaining four rules is to fix a leftmost outermost reduction strategy. These last four rules could be replaced by a single one, namely

{M_{1} ▷ M_{2} \atop E[M_{1}] ▷ E[M_{2}]}

where E ranges over evaluation contexts defined by the grammar

E := [ ] | E(M) | succ(E) | pred(E) | ifz(E, M_{1}, M_{2})

in BNF form. As for every term M there is at most one evaluation context E such that M ≡ E[N] and N is the left hand side of some valid reduction N ▷ N′ it follows that the reduction relation ▷ is deterministic.

Let us write ▷^{∗} for the reflexive transitive closure of ▷. One can show (Exercise!) that M⇓V iff M▷^{∗}V and V is a syntactic value^{3}. For this purpose one verifies (Exercise!) that

(a) if M⇓V then M ▷^{∗} V and

(b) if M ▷ N then for all values V, if N⇓V then M⇓V

3Notice that V is a value if there is no term N with V ▷ N.

26 Domain-theoretic foundations of functional programming

by induction on the structure of derivations of M⇓V and M ▷ N, respectively. Applying (b) iteratively it follows that

(c) if M ▷^{∗} N then for all values V, if N⇓V then M⇓V.

Then from (a) and (c) it follows immediately that M⇓V if and only if M ▷^{∗} V for all terms M and values V. Thus big step and small step semantics for PCF coincide. Of course, big step semantics is more abstract in the sense that it forgets about intermediary computation steps. That is the reason why we stick to big step semantics when studying the relation between operational and denotational semantics of PCF.

Smallstep Semantics for PCF

(λx:σ.M)(N) ▷ M[N/x]  Y_{σ}(M) ▷ M(Y_{σ}(M))

pred(\underline{0}) ▷ \underline{0}  pred(\underline{n+1}) ▷ \underline{n}

ifz(\underline{0}, M_{1}, M_{2}) ▷ M_{1}  ifz(\underline{n+1}, M_{1}, M_{2}) ▷ M_{2}

{M_{1} ▷ M_{2} \atop M_{1}(N) ▷ M_{2}(N)} M_{1} ▷ M_{2}

succ(M_{1}) ▷ succ(M_{2})

M_{1} ▷ M_{2}

pred(M_{1}) ▷ pred(M_{2})

{M_{1} ▷ M_{2} \atop ifz(M_{1}, N_{1}, N_{2}) ▷ ifz(M_{2}, N_{1}, N_{2})}

Figure 2.3 Small Step Semantics for PCF

The syntactic preorders ⊏ ∼ and < ∼

For every type σ we write Prg_{σ} for the set {M | ⊢M:σ} of closed PCF terms of type σ also called programs of type σ. Programs of base type will be simply called programs. By induction on the structure of σ we will now define preorders ⊏ ∼_{σ} and < ∼_{σ} on Prg_{σ}.

PCF and its Operational Semantics 27

For base type nat we define

M ⊏ ∼_{nat} N iff ∀n∈ℕ. M⇓\underline{n} ⇒ N⇓\underline{n}

and for functional types σ→τ we define

M ⊏ ∼_{σ→τ} N iff ∀P ∈Prg_{σ}. M(P) ⊏ ∼_{τ} N(P) .

The relation ⊏ ∼ will be called “applicative approximation” and we leave it as an exercise(!) to the reader to verify that ⊏ ∼_{σ} is actually a preorder on Prg_{σ}, i.e. that ⊏ ∼_{σ} is reflexive and transitive. One easily shows that for types σ ≡ σ_{1}→ … →σ_{n}→nat it holds that M ⊏ ∼_{σ} N iff MP⃗ ⊏ ∼_{nat} NP⃗ for all P⃗ ∈ Prg_{σ_{1}}× … ×Prg_{σ_{n}} (where we write MP⃗ for M(P_{1}) … (P_{n}) if P⃗ is the n–tuple ⟨P_{1}, …, P_{n}⟩).

The “observational approximation” ordering < ∼_{σ} at type σ is defined as

M < ∼_{σ} N iff ∀P ∈Prg_{σ→nat}. P (M) ⊏ ∼_{nat} P (N)

where the underlying intuition is that every “observation” which can be made about M can also be made about N. Obviously, from M < ∼_{σ} N it follows that M ⊏ ∼_{σ} N as in the latter one quantifies only over a restricted class of observations, namely those of the form λx:σ. xP⃗.

The classical Milner’s Context Lemma says that both orderings are actually the same. However, its proof requires some sophistication and mathematical machinery. Accordingly, we postpone it to a subsequent chapter.

It is straightforward to see that for computationally adequate models it holds that M < ∼ N whenever [[M]] ⊑ [[N]]. The reverse implications holds only for fully abstract models which, however, are difficult to construct.

An Abstract Environment Machine for PCF

We now will describe an abstract machine for evaluating PCF terms in order to give an idea of how functional languages can be implemented on traditional von Neumann machines.

At first sight one might be inclined to directly implement the small step semantics considered above, i.e. to implement the partial function on terms whose graph is the reduction relation ▷. However, this is not very efficient since replacing (λx.M)(N) by M[N/x] is somewhat costy if there are many free occurrences of x in M which is in conflict with the intuitive requirement that single steps in a computation process should all be simple and change state only in a very local manner.

28 Domain-theoretic foundations of functional programming

The key idea of an environment machine is to postpone the possibly costy operation of substitution as long as possible. For this reason the machine manipulates so-called closures which are pairs [M, e] where M is a term and e is an environment, i.e. a finite function from variables to closures.

The syntax of untyped PCF terms is given by the grammar

M ::= x | λx.M | M(M) | Y(M) | zero | succ(M) | pred(M) | ifz(M, M, M)

in BNF form. We consider untyped PCF terms as type information is irrelevant for the computation process.

We write ∅ for the empty environment and e[x:=c] for the environment which behaves like e for variables different from x and sends x to the closure c. We also write dom(e) for the finite set of variables to which e assigns a closure. Obviously, we have dom(e[x:=c]) = dom(e) ∪ {x}.

The states of the abstract machines will be pairs ⟨c, S⟩ where c is a closure and S is a stack or continuation which are defined by the following grammar

S ::= stop | arg(c, S) | succ(S) | pred(S) | ifz(M, M, e, S)

in BNF form.

Finally the transition rules of the Abstract Environment Machine for PCF are given in Figure 2.4.

We now try to reveal the intuition behind the various transition rules. The first three rules are sufficient to compute weak head normal forms

of terms of untyped λ-calculus. Recall that a weak head normal form is either a variable or a λ-abstraction. For this fragment the continuations are stacks where arg takes a closure c and pushes it on stack S. When an application term has to be evaluated its argument together with the current environment is pushed on the stack. This is iterated until one lands in case (1) or (2). In the first case the variable x is replaced by the closure e(x) where e is the current environment provided e(x) is defined and otherwise we have found the head variable of the term. A λ-expression λx.M under current environment e is evaluated by evaluating its body M in the environment e[x:=c] where c is the closure on top of the current stack. If the current stack is empty then (λx.M)[e] is the weak head normal form.

Rule (4) extends this to general recursion as given by Y. Thus, in order to evaluate Y(M) under the environment e evaluate M(Y(M)) under environment e which, however, by (3) is evaluated as follows: push the

PCF and its Operational Semantics 29

argument Y(M) together with e on the stack and then evaluate M w.r.t. e. Rule (4) has the same effect but achieves it in one single step.

Transition Rules of the Abstract Environment Machine

(1) ⟨[x, e], S⟩ → ⟨e(x), S⟩ if x ∈ dom(e)

(2) ⟨[λx.M, e], arg(c, S)⟩ → ⟨[M, e[x:=c]], S⟩

(3) ⟨[M(N), e], S⟩ → ⟨[M, e], arg([N, e], S)⟩

(4) ⟨[Y(M), e], S⟩ → ⟨[M, e], arg([Y(M), e], S)⟩

(5) ⟨[succ(M), e], S⟩ → ⟨[M, e], succ(S)⟩

⟨[\underline{n}, e], succ(S)⟩ → ⟨[\underline{n+1}, e], S⟩

(6) ⟨[pred(M), e], S⟩ → ⟨[M, e], pred(S)⟩

⟨[\underline{0}, e], pred(S)⟩ → ⟨[\underline{0}, e], S⟩

⟨[\underline{n+}1, e], pred(S)⟩ → ⟨[\underline{n}, e], S⟩

(7) ⟨[ifz(M, N_{1}, N_{2}), e], S⟩ → ⟨[M, e], ifz(N_{1}, N_{2}, e, S)⟩

⟨[\underline{0}, e′], ifz(N_{1}, N_{2}, e, S)⟩ → ⟨[N_{1}, e], S⟩

⟨[\underline{n+1}, e′], ifz(N_{1}, N_{2}, e, S)⟩ → ⟨[N_{2}, e], S⟩

Figure 2.4 Abstract Environment Machine for PCF

Whereas application follows a call-by-name strategy expressions of the form succ(M) or pred(M) are evaluated following a call-by-value strategy. Therefore it is not appropriate to push the argument M together with the current environment e on the current stack S. Instead one evaluates M w.r.t. e and the stack succ(S). When this evaluation has resulted in the closure [\underline{n}, e′] (tacitly assuming that the current stack is again succ(S)) then evaluate [\underline{n+1}, e′] w.r.t. the original stack S. For pred the procedure is analogous.

As ifz is call-by-value in its first argument when evaluating an expression of the form ifz(M, N_{1}, N_{2}) w.r.t. environment e and stack S one first has to evaluate M w.r.t. e but relative to the stack ifz(N_{1}, N_{2}, e, S) which keeps the information how to continue^{4} when [M, e] has been evaluated to a

4That is the reason why one speaks of “continuations”. They tell us how to “continue”

30 Domain-theoretic foundations of functional programming

numeral. Depending on whether this numeral is 0 or greater 0 one proceeds by evaluating N_{1} w.r.t. e and S or by evaluating N_{1} w.r.t. e and S.

The formal verification of the correctness of our environment machine is somewhat delicate and we omit it as it isn’t the main concern of this course but rather of a course on implementations of functional programming languages.

after an intermediary result has been found.

Chapter 3

The Scott Model of PCF

In this chapter we introduce the kind of structures within which Dana Scott has interpreted the language PCF (and its logic LCF). (See [Scott 1969] for a reprint of a widely circulated “underground” paper from 1969 where this interpretation was presented the first time.) But before we will discuss the general form of a denotational semantics for PCF and try to motivate some of the structural requirements we impose.

A denotational semantics for PCF associates with every type σ a socalled domain D_{σ} and with every term x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ M : σ a function

[[x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ M : σ]] : D_{σ_{1}} × ⋯ × D_{σ_{n}} → D_{σ}

assuming that cartesian products of domains exist. In case M is a closed term (i.e. n=0) we have [[⊢ M : σ]] : 1 → D_{σ} where 1 stands for the empty product containing just the empty tuple ⟨⟩ as its single element.

We have tacitly assumed that domains are sets (and that their finite products are defined as for sets). But notice that one must not interpret D_{σ→τ} as the set of all functions from D_{σ} to D_{τ} as then one would run into problems with interpreting the fixpoint operators Y_{σ} as their interpretation would have to associate with every f ∈ D_{σ→σ}, i.e. with every function f from D_{σ} to D_{σ}, a fixpoint of f, i.e. a Y_{σ}(f) ∈ D_{σ} satisfying the fixpoint equation Y_{σ}(f) = f(Y_{σ}(f)), and such a fixpoint need not exist in general (e.g. if f is a fixpoint free permutation of the set D_{σ}). The solution to this problem is to endow the domains D_{σ} with additional structure and to require that D_{σ→τ} consists of all maps from D_{σ} to D_{τ} which do preserve this structure. Of course, we then have to endow this set also with an appropriate structure of that kind.

The question now is to identify what is an appropriate structure to impose on domains which serve the purpose of interpreting PCF (or other

32 Domain-theoretic foundations of functional programming

programming languages). In particular, this kind of structure should not be arbitrary but rather well motivated by operational phenomena. Well, in the previous chapter we have seen that for every type σ one can define the preorder ⊏ ∼_{σ} on the set Prg_{σ} of programs of type σ where M ⊏ ∼_{σ} N means that N contains all the information of M and possibly more. By analogy this suggests to endow the domains with a partial ordering called “information ordering”.

If one factors the closed terms of type nat by ⊏ ∼_{nat} one obtains the poset (i.e. partially ordered set) N whose underlying set is ℕ∪{⊥} where ⊥ (read “bottom”) is a distinguished object (not contained in ℕ) representing nontermination or divergence. Actually, for every type σ there is a closed term Ω_{σ} ≡ Y_{σ}(λx:σ.x) with Ω_{σ} ⊏ ∼_{σ} M for all M ∈ Prg_{σ}. Thus, we require every domain D_{σ} to be endowed with a partial order ⊑_{σ} and to contain a least element ⊥_{D_{σ}}. As ⊏ ∼ coincides with < ∼ by Milner’s Context Lemma^{1} every program P of type σ→τ preserves ⊏ ∼ as it obviously preserves < ∼. This leads us to the requirement that the functions f ∈ D_{σ→τ} should be monotonic, i.e. preserve the partial order ⊑. As by definition M ⊏ ∼_{σ→τ} N iff M(P) ⊏ ∼ N(P) for all programs P of type σ it appears as natural to define the partial order ⊑ on D_{σ→τ} as the pointwise ordering according to which f ⊑ g iff ∀d∈D_{σ}. f(d) ⊑ g(d).

However, it is not sufficient to require that domains are partial orders with a least element and functions between them have to be monotonic because this does not yet guarantee the existence of fixpoints. Consider for example the set ℕ of natural numbers under their usual ordering ≤ for which the successor function f : ℕ → ℕ : n ↦ n+1 is surely monotonic but obviously has no fixpoint.

This problem can be overcome by postulating that every domain has suprema of chains and functions between domains are not only monotonic but have to preserve also suprema of chains. Such functions between domains are called “(Scott) continuous”. This has the advantage that for every domain D every continuous function f : D → D has a least fixpoint μ(f) which is obtained as the supremum of the chain

⊥ ⊑ f(⊥) ⊑ f^{2}(⊥) ⊑ ⋯ ⊑ f^{n}(⊥) ⊑ …

That μ(f) is actually a fixpoint of f follows from continuity of f as we have f(⨆_{n} f^{n}(⊥)) = ⨆_{n} f(f^{n}(⊥)) = ⨆_{n} f^{n}(⊥). That μ(f) is actually the least fixpoint of f can be seen as follows: if d = f(d) then by induction one

1which still has to be proved but may well serve the purpose of motivation!

The Scott Model of PCF 33

easily shows that f^{n}(⊥) ⊑ d for all n ∈ ℕ and thus μ(f) ⊑ d since μ(f) is the supremum of the f^{n}(⊥) which are bounded by d.

Summarizing we notice that the above considerations suggest that

• domains are partially ordered sets with a least element and suprema for all (weakly) increasing chains and

• functions between domains should preserve the partial ordering and suprema of (weakly) increasing chains.

One might be inclined to require functions between domains to preserve also least elements. This, however, would have the most undesirable consequences that (1) every constant map has value ⊥ and (2) the least fixpoint of every endomap is ⊥ rendering all recursive definitions trivial.

In the following for aesthetical reasons we require not only existence and preservation of suprema of chains but existence and preservation of suprema of so-called directed sets.

In the next two sections we develop some basic domain theory and then introduce the Scott model of PCF.

3.1 Basic Domain Theory

Definition 3.1 A partial order (poset) on a set D is a binary relation ⊑_{D}⊆ D×D satisfying the following conditions

(reflexive) x ⊑_{D} x
(transitive) x ⊑_{D} z whenever x ⊑_{D} y and y ⊑_{D} z
(antisymmetric) x = y whenever x ⊑_{D} y and y ⊑_{D} x.

A reflexive and transitive relation is called a preorder.

If (D_{1}, ⊑_{D_{1}}) and (D_{2}, ⊑_{D_{2}}) are preorders then a function f : D_{1} → D_{2} is called monotonic iff f(x) ⊑_{D_{2}} f(y) whenever x ⊑_{D_{1}} y. ♢

Obviously, monotonic maps are closed under composition and the identity function id_{D} : D → D : d ↦ d is a monotonic map from (D, ⊑_{D}) to itself.

Definition 3.2 Let (A, ⊑) be a poset. A subset X ⊆ A is called directed iff every finite subset X_{0} of X has an upper bound in X, i.e.

∀X_{0}⊆_{fin}X.∃y∈X.∀x∈X_{0}. x ⊑ y .

34 Domain-theoretic foundations of functional programming

Thus, a directed set X is always nonempty because the empty set ∅ ⊆_{fin} X has an upper bound in X.

A partial order (A, ⊑) is called predomain or complete partial order (cpo) iff every directed subset of A has a least upper bound. A predomain (A, ⊑) is called a domain or pcpo (pointed cpo) iff it has a least element ⊥.

Let (A_{1}, ⊑_{A_{1}}) and (A_{2}, ⊑_{A_{2}}) be cpo’s. A function from (A_{1}, ⊑_{A_{1}}) to (A_{2}, ⊑_{A_{2}}) is called (Scott) continuous iff it preserves suprema of directed sets, i.e.

f(⨆ X) = ⨆ f(X)

for all directed X ⊆ A_{1}. A function between domains is called strict iff it preserves least elements. ♢

It is a straightforward exercise(!) to show that continuous functions between predomains are always monotonic.

Theorem 3.3 Let (A_{i} | i∈I) be a family of predomains. Then their product ∏_{i∈I} A_{i} is a predomain under the componentwise ordering and the projections π_{i} : ∏_{i∈I} A_{i} → A_{i} are Scott continuous. If, moreover, all A_{i} are domains then so is their product ∏_{i∈I} A_{i}.

If (f : B → A_{i} | i∈I) is a family of continuous maps between predomains then there is a unique continuous function f : B → ∏_{i∈I} A_{i} with

π_{i} ∘ f = f_{i}

for all i ∈ I.

Proof. Straightforward exercise! □

Lemma 3.4 Let A_{1}, A_{2} and A_{3} be cpos. Then a function f : A_{1}×A_{2} → A_{3} is continuous iff it is continuous in each argument.

Proof. The implication from left to right is obvious.

For the reverse direction suppose that f is continuous in each argument. For showing that f is continuous consider an arbitrary directed subset X ⊆ A_{1}×A_{2}. Then for i=1, 2 the sets X_{i} := π_{i}(X) are directed in A_{i}. Obviously, we have ⨆ X = (⨆ X_{1}, ⨆ X_{2}). As f is monotonic it suffices to show that

f(⨆ X) ⊑ ⨆_{x∈X} f(x)

Suppose z ⊒ ⨆_{x∈X} f(x). Then z ⊒ f(x_{1}, x_{2}) for all x_{1} ∈ X_{1} and x_{2} ∈ X_{2} (as if (x_{1}, x′_{2}) ∈ X and (x′_{1}, x_{2}) ∈ X then by directedness of X there

The Scott Model of PCF 35

is a (y_{1}, y_{2}) ∈ X with (y_{1}, y_{2}) ⊒ (x_{1}, x′_{2}), (x′_{1}, x_{2})). Thus, for all x_{1} ∈ X_{1} we have z ⊒ f(x_{1}, ⨆ X_{2}) as f is continuous in its second argument. Accordingly, as f is continuous also in its first argument we conclude that z ⊒ f(⨆ X_{1}, ⨆ X_{2}) = f(⨆ X) as desired. □

Next we show that there are appropriate function spaces or exponentials in the category of predomains and continuous maps.

Theorem 3.5 Let A_{1} and A_{2} be cpo’s. Then the set A_{2}^{A_{1}} = [A_{1}→A_{2}] of all Scott continuous maps from A_{1} to A_{2} is itself a cpo when ordered pointwise, i.e. when defining

f ⊑ g  iff  ∀a∈A_{1}. f(a) ⊑ g(a)

for Scott continuous functions f and g.

Proof. Let F be a directed subset of [A_{1}→A_{2}]. We show that its supremum ⨆ F is given by the function g with

g(a) = ⨆_{f∈F} f(a)

for a ∈ A_{1}. Notice that g(a) is always defined because {f(a) | f∈F } is directed. Obviously, the map g is the supremum of F provided g is continuous. It is easy to see that g is monotonic. Thus, for showing the continuity of g assume that X is a directed subset of A_{1}. As g is monotonic it suffices to show that

g(⨆ X) ⊑ ⨆ g(X)

For this purpose assume that z ⊒ ⨆ g(X), i.e. z ⊒ g(x) for all x ∈ X. Then z is also an upper bound for {f(x) | f∈F, x∈X}. Thus, for all f ∈ F we have

z ⊒ ⨆ f(X) = f(⨆ X)

as f is continuous. Accordingly, the element z is also an upper bound of g(⨆ X) as desired. □

As the evaluation map

ev : [A_{1}→A_{2}]×A_{1} → A_{2} : (f, a) ↦ f(a)

is continuous in each argument (exercise!) it follows by Lemma 3.4 that ev itself is continuous.

36 Domain-theoretic foundations of functional programming

Theorem 3.6 Let A, B and C be predomains. Then for every Scott continuous function f : C×A → B there exists a unique Scott continuous function g : C → [A→B] with

g(z)(x) = f(z, x)

for all x ∈ A and z ∈ C.

Proof. Obviously, the function g is uniquely determined by the requirement that g(z)(x) = f(z, x) for all x ∈ A and z ∈ C. As g(z) = f(z, −) is continuous for all z ∈ C it remains to show that g is continuous. For this purpose assume that Z is a directed subset of C. But then we have for all x ∈ X

g(⨆ Z)(x) = f(⨆ Z, x) = ⨆_{z∈Z} f(z, x) = ( ⨆_{z∈Z} g(z))(x)

where the last equality follows from the fact that directed suprema in [A→B] are constructed pointwise (see proof of Theorem 3.5). Thus, we have g(⨆ Z) = ⨆_{z∈Z} g(z) as desired. □

The claim of the previous theorem may be formulated more abstractly as follows: for every continuous f : C×A → B there is a unique continuous g : C → [A→B] such that the following diagram commutes

[figure: [A→B]×A; ev; B; C×A; g×id_{A}; f]

where (g×id_{A})(c, a) = (g(c), a). This requirement makes sense in every category with (binary) cartesian products and characterises the exponential [A→B] uniquely up to isomorphism. A category with finite products where for all objects A and B the exponential [A→B] exists is usually called cartesian closed (see e.g. [Scott 1980]).

One often writes Λ(f) for the unique map g with f = ev ∘ (g×id_{A}). We will see later that projections, ev and Λ provide enough structure for interpreting the simply typed λ-calculus in the category of predomains and continuous maps (and, actually, in an arbitrary cartesian closed category).

But now we dicuss fixpoints and fixpoint operators for domains.

The Scott Model of PCF 37

Theorem 3.7 Let D be a domain and f : D → D be continuous. Then the supremum

μ(f) = ⨆_{n∈ℕ} f^{n}(⊥)

exists and satisfies the conditions

(1) μ(f) = f(μ(f)) and

(2) μ(f) ⊑ d whenever f(d) ⊑ d.

Thus, in particular μ(f) is the least fixpoint of f.

Proof. First we show by induction on n that f^{n}(⊥) ⊑ f^{n+1}(⊥). Obviously, we have f^{0}(⊥) = ⊥ ⊑ f(⊥) = f^{1}(⊥) as ⊥ is the least element of D. If f^{n}(⊥) ⊑ f^{n+1}(⊥) then f^{n+1}(⊥) = f(f^{n}(⊥)) ⊑ f(f^{n+1}(⊥)) = f^{n+2}(⊥) as f is monotonic. Thus μ(f) = ⨆_{n∈ℕ} f^{n}(⊥) exists because directed sets have suprema in D. The element μ(f) is a fixpoint of f as we have

f(μ(f)) = f( ⨆_{n∈ℕ} f^{n}(⊥)) = ⨆_{n∈ℕ} f(f^{n}(⊥)) = ⨆_{n∈ℕ} f^{n+1}(⊥) = μ(f)

where the second equality intrinsically makes use of continuity of f.

For the second claim suppose that f(d) ⊑ d. We show by induction that f^{n}(⊥) ⊑ d. Of course, we have f^{0}(⊥) = ⊥ ⊑ d as ⊥ is the least element. If f^{n}(⊥) ⊑ d then f^{n+1}(⊥) = f(f^{n}(⊥)) ⊑ f(d) ⊑ d. Thus, it follows that μ(f) = ⨆_{n∈ℕ} f^{n}(⊥) ⊑ d. That μ(f) is the least fixpoint follows immediately from the fact that μ(f) is below all prefixpoints f(d) ⊑ d. □

Obviously, for arbitrary predomains A not every continuous endofunction f : A → A will have a fixpoint as this is wrong for sets and those live within predomains as the discrete partial orders.

By the previous theorem there is a function μ from [D→D] to D sending continuous f to their least fixpoint. One could show directly that μ is continuous, i.e. preserves suprema of directed sets. However, the following proof is much nicer.

Theorem 3.8 Let D be a domain and Φ : [[D→D]→D] → [[D→D]→D] the continuous operator with

Φ(F)(f) = f(F (f))

for F ∈ [[D→D]→D] and f ∈ [D→D]. The fixpoints of Φ are the continuous fixpoint operators on D and μ is the least fixpoint of Φ. Thus, the least fixpoint operator μ is continuous.

38 Domain-theoretic foundations of functional programming

Proof. First observe that

Ψ : [[D→D]→D]×[D→D] → D : (F, f) ↦ f(F (f))

is continuous in each argument (exercise!) and thus continuous by Lemma 3.4. The operator Φ is continuous as one easily sees that Φ = Λ(Ψ).

A continuous function F ∈ [[D→D]→D] is a fixpoint operator iff F (f) is a fixpoint of f for all f ∈ [D→D], i.e. F (f) = f(F (f)) for all f ∈ [D→D], i.e. iff F = Φ(F). Thus, the fixpoints of Φ are precisely the continuous fixpoint operators.

The least fixpoint of Φ is μ because for all n ∈ ℕ we have

Φ^{n}(⊥)(f) = f^{n}(⊥)

for all f ∈ [D→D] as the following inductive argument shows. The claim is obvious for n=0 as Φ^{0}(⊥)(f) = ⊥(f) = ⊥ = f^{0}(⊥). Suppose as induction hypothesis that Φ^{n}(⊥)(f) = f^{n}(⊥) for all f ∈ [D→D]. Then for all f ∈ [D→D] we have

Φ^{n+1}(⊥)(f) = Φ(Φ^{n}(⊥))(f) = f(Φ^{n}(⊥)(f)) =_{(IH)} f(f^{n}(⊥)) = f^{n+1}(⊥)

proving the induction step. □

Later we will interpret Y_{σ} of PCF as the least fixpoint operator for D_{σ}. The previous theorem guarantees that recursive definitions in PCF via the recursion operators Y_{σ} will not lead out of the world of Scott continuous functions which is indispensible for further, i.e. iterated, applications of Y.

“Induction Principles” for Least Fixpoints

As the least fixpoint operators of PCF are essential for writing nontrivial programs it is most desirable to have reasoning principles available for proving properties of least fixpoints. As some of these are formally analogous to proper induction principles it has become customary to call them “induction principles” though they do not verify that a certain property holds for all elements of some domain but rather that a property holds for a particular element, namely the least fixpoint of some given function.

Alas, most reasoning principles do not apply to arbitrary properties of domains. In the following definition we introduce a class of predicates on domains for which the subsequent induction principles are “admissible”.

Definition 3.9 A subset P of a predomain A is called an admissible predicate on A iff P is closed under suprema of directed sets, i.e. P (⨆ X)

The Scott Model of PCF 39

for all directed X ⊆ P. ♢

Notice that we often write P (d) for d ∈ P as we identify predicates with subsets. The first and most general reasoning principle is “computational induction”.

Theorem 3.10 (Computational Induction) Let D be a domain, f : D → D a continuous function and P ⊆ D an admissible predicate on D. Then P (μ(f)) whenever P (f^{n}(⊥)) for all n ∈ ℕ.

Proof. As by assumption all elements of the directed set {f^{n}(⊥) | n∈ℕ} are in P its supremum μ(f) is in P, too, as P is admissible. □

The following immediate consequence called “fixpoint induction” is often easier to use.

Theorem 3.11 (Fixpoint Induction) Let D be a domain, f : D → D a continuous function and P ⊆ D an admissible predicate on D.

Then P (μ(f)) whenever P (⊥) and ∀x∈D. P (x) ⇒ P (f(x)).

Proof. From the premisses P (⊥) and ∀x∈D. P (x) ⇒ P (f(x)) one easily shows by ordinary induction on ℕ that ∀n∈ℕ. P (f^{n}(⊥)) from which it follows by Theorem 3.10 that P (μ(f)). □

Notice the formal analogy of the structure of premisses in ordinary induction

P (0) ∧ (∀x. P (x) ⇒ P (succ(x))) ⇒ ∀x. P (x)

and fixpoint induction

P (⊥) ∧ (∀x. P (x) ⇒ P (f(x))) ⇒ P (μ(f))

which was the reason for calling Theorem 3.11 “fixpoint induction”.

Finally we mention a proof principle due to David Park which is useful for showing that recursively defined functions diverge for some arguments.

Theorem 3.12 (Park Induction) Let D be a domain and f : D → D a continuous function. Then μ(f) ⊑ d whenever f(d) ⊑ d.

Proof. This is just Theorem 3.7 (2). □

Now we have accumulated sufficiently much basic Domain Theory for introducing Scott’s famous domain model for PCF.

40 Domain-theoretic foundations of functional programming

3.2 Domain Model of PCF

We first describe the domains interpreting PCF types. For this purpose we need the following definition.

Definition 3.13 Let X be a set. Then X_{⊥} is the poset whose underlying set of elements is X∪{⊥} where ⊥ ∉ X and which is partially ordered by

x ⊑ y iff x=⊥ ∨ x = y .

The element ⊥ is a fresh least element and the elements of X are all incomparable w.r.t. this ordering. ♢

Now the domains D_{σ} associated with PCF types σ are defined inductively as follows

D_{nat} = N where N = ℕ_{⊥} and
D_{σ→τ} = [D_{σ}→D_{τ}].

Notice that all D_{σ} contain a least element ⊥. If one considers the extension of PCF by Boolean values then one puts D_{bool} = 𝔹_{⊥} where 𝔹 = {true, false} is the set of truth values.

If Γ ≡ x_{1}:σ_{1}, …, x_{n}:σ_{n} then we define [[Γ]] as D_{σ_{1}}× … ×D_{σ_{n}}. A term in context Γ ⊢ M : τ will be interpreted as a function

[[Γ ⊢ M]] : [[Γ]] → D_{τ}

which is required to be Scott continuous. The definition of the interpretation of terms in context proceeds by recursion over the structure of derivations as in the following definition.

Definition 3.14 The interpretation of terms in contexts is given by the following recursive clauses

[[x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ x_{i}]](d_{1}, …, d_{n}) = d_{i}
[[Γ ⊢ λx:σ. M]] = Λ([[Γ, x:σ ⊢ M]])
i.e. [[Γ ⊢ λx:σ. M]](d⃗)(d) = [[Γ, x:σ ⊢ M]](d⃗, d)
[[Γ ⊢ M(N)]](d⃗) = ev([[Γ ⊢ M]](d⃗), [[Γ ⊢ N]](d⃗))
[[Γ ⊢ Y_{σ}(M)]](d⃗) = μ([[Γ ⊢ M]](d⃗))
[[Γ ⊢ zero]](d⃗) = 0
[[Γ ⊢ succ(M)]](d⃗) = [[succ]]([[Γ ⊢ M]](d⃗))

The Scott Model of PCF 41

[[Γ ⊢ pred(M)]](d⃗) = [[pred]]([[Γ ⊢ M]](d⃗))

[[Γ ⊢ ifz(M, N_{1}, N_{2})]](d⃗) = [[ifz]]([[Γ ⊢ M]](d⃗), [[Γ ⊢ N_{1}]](d⃗), [[Γ ⊢ N_{2}]](d⃗))

where [[succ]], [[pred]] : N → N are defined as

[[succ]](⊥) = ⊥ [[succ]](n) = n+1

[[pred]](⊥) = ⊥  [[pred]](0) = 0  [[pred]](n+1) = n

and [[ifz]] : N^{3} → N is defined as

[[ifz]](⊥, x, y) = ⊥  [[ifz]](0, x, y) = x  [[ifz]](n+1, x, y) = y

with n ranging over ℕ and x and y ranging over N = ℕ_{⊥}. ♢

Notice that [[succ]] and [[pred]] are the strict extensions of the ordinary successor and predecessor functions on ℕ. The function [[ifz]] is strict in its first argument but non-strict in its second and third argument.

We now collect a few basic properties of the domain interpretation of PCF whose proof is fairly standard.

Lemma 3.15 (Substitution Lemma) Let Γ ≡ x_{1}:σ_{1}, …, x_{n}:σ_{n} be a context and Γ ⊢ M : τ a term. Then for all contexts Δ and terms Δ ⊢ N_{i} : σ_{i} with i=1, …, n it holds that

[[Δ ⊢ M[N⃗/x⃗]]](d⃗) = [[Γ ⊢ M]]([[Δ ⊢ N_{1}]](d⃗), …, [[Δ ⊢ N_{n}]](d⃗))

for all d⃗ ∈ [[Δ]].

Proof. Straightforward by induction on derivations of Γ ⊢ M. □

As corollaries to the Substitution Lemma we obtain correctness of the β- and η-equalities as known from λ-calculus.

Corollary 3.16 (β-equality) If Γ, x:σ ⊢ M : τ and Γ ⊢ N : σ then

[[Γ ⊢ (λx:σ. M)(N)]] = [[Γ ⊢ M[N/x]]] .

Proof. Straightforward exercise! □

Corollary 3.17 (η-equality) If Γ ⊢ M : σ→τ then

[[Γ ⊢ λx:σ. M(x)]] = [[Γ ⊢ M]]

for x ∉ Var(Γ).

42 Domain-theoretic foundations of functional programming

Proof. Straightforward exercise! □

The next theorem relates the domain–theoretic fixpoint semantics to our operational intuition about recursive definitions.

Theorem 3.18 Let Ω_{σ} ≡ Y_{σ}(λx:σ. x). Obviously, we have [[Ω_{σ}]] = ⊥. For every term Γ ⊢ M : σ→σ we have

[[Γ ⊢ Y_{σ}(M)]] = ⨆_{n∈ℕ}[[Γ ⊢ M^{n}(Ω_{σ})]]

where M^{n}(Ω_{σ}) is defined recursively as M^{0}(Ω_{σ}) ≡ Ω_{σ} and M^{n+1}(Ω_{σ}) ≡ M(M^{n}(Ω_{σ})).

Proof. As the interpretation of λx:σ. x is id_{D_{σ}} whose least fixpoint is ⊥ we get [[Ω_{σ}]] = ⊥. Now if Γ ⊢ M : σ→σ then for all d⃗ ∈ [[Γ]] we have

[[Γ ⊢ Y_{σ}(M)]](d⃗) = μ([[Γ ⊢ M]](d⃗)) = ⨆_{n∈ℕ}([[Γ ⊢ M]](d⃗))^{n}(⊥)

from which it follows that [[Γ ⊢ Y_{σ}(M)]] = ⨆_{n∈ℕ}[[Γ ⊢ M^{n}(Ω_{σ})]] because a straightforward inductive argument shows that

[[Γ ⊢ M^{n}(Ω_{σ})]](d⃗) = ([[Γ ⊢ M]](d⃗))^{n}(⊥)

holds for all n ∈ ℕ and d⃗ ∈ [[Γ]]. □

This theorem guarantees that the meaning of a recursive definition Y_{σ}(M) is the supremum of its finite unfoldings M^{n}(Ω_{σ}).

3.3 LCF – A Logic of Computable Functionals

At the same time (end of 1960ies) when Dana Scott introduced the prototypical programming language PCF in [Scott 1969] he also defined LCF (Logic of Computable Functionals) for the purpose of reasoning about PCF programs. Due to Gödel’s Incompleteness Theorem such a formal system^{2} can never be complete since it contains arithmetic. Despite its inherent incompleteness LCF contains a lot of most useful reasoning principles which we will now discuss informally.

Atomic propositions about PCF terms have the form M ⊑_{σ} N where both M and N are terms of type σ. The relations ⊑_{σ} are all supposed as

2Here “formal system” means that its set of theorems is recursively enumerable!

The Scott Model of PCF 43

reflexive and transitive. Equality for terms of type σ is then defined as

M =_{σ} N ≡ (M ⊑_{σ} N) ∧ (N ⊑_{σ} M) .

The following axioms are easily validated w.r.t. the Scott model introduced in the previous section. Notice, however, that we always assume free variables to be typed by a context which we prefer to leave implicit^{3} for sake of readability.

(1) M_{1} ⊑_{σ→τ} M_{2} ∧ N_{1} ⊑_{σ} N_{2} ⇒ M_{1}(N_{1}) ⊑_{τ} M_{2}(N_{2})

(2) λx:σ.M_{1} ⊑_{σ→τ} λx:σ.M_{2} ⇔ ∀x:σ. M_{1} ⊑_{τ} M_{2}

(3) (λx:σ.M)(N) =_{τ} M[N/x]

(4) λx:σ.M(x) =_{σ→τ} M provided x is not free in M

(5) Y_{σ}(M) =_{σ} M(Y_{σ}(M))

(6) ∀x:σ. M(x) ⊑_{σ} x ⇒ Y_{σ}(M) ⊑_{σ} x provided x is not free in M

(7) P (Ω_{σ}) ∧ (∀x:σ. P (x) ⇒ P (M(x))) ⇒ P (Y_{σ}(M))

provided x is not free in M and P (x) is a predicate built from atomic formulas via ∀,∧,∨ and A ⇒ (−) where A is an arbitrary formula without free occurrences of the variable x.

Notice that the syntactic restrictions on the predicate P in (7) guarantee that the predicate P is admissible.^{4} Whereas (7) corresponds to Fixpoint Induction (6) corresponds to Park Induction from which one may derive that Ω_{σ} = Y_{σ}(λx:σ.x) ⊑_{σ} M for all terms M of type σ.

But we also need some axioms for the data type of natural numbers. For their formulation we employ the predicate

N(x) ≡ ¬(x = Ω_{nat})

expressing that x is a proper natural number different from ⊥. The following axioms are (essentially) those of Peano Arithmetic

(8) ¬ succ(x) = zero

(9) ∀x, y:nat. N(x) ∧ N(y) ∧ succ(x) = succ(y) ⇒ x = y

3That means that “officially” one would have to consider instead of formulas A rather expressions of the form Γ ⊢ A where all free variables of A are declared in Γ.

4All these closure properties are straightforward to verify with the exception of disjunction. For this purpose suppose P and Q are admissible subsets of a cpo A. Suppose X is a directed subset of A with X ⊆ P ∪ Q. If P ∩ X is cofinal in X, i.e. for all x ∈ X there exists y ∈ P ∩X with x ⊑ y then P ∩X is directed and ⨆ X = ⨆ P ∩X from which it follows that ⨆ X = ⨆ P ∩ X ∈ P since P is admissible. Otherwise, i.e. if P ∩ X is not cofinal in X, there exists an x ∈ X with x ⋢ y for all y ∈ P ∩ X, i.e. for all y ∈ X with x ⊑ y it holds that y ∉ P and thus y ∈ Q, from which it follows that Q ∩ X is directed and has the same supremum as X and thus ⨆ X = ⨆ Q ∩ X ∈ Q since Q is admissible.

44 Domain-theoretic foundations of functional programming

(10) P (zero) ∧ (∀x:nat. N(x)∧P (x)⇒P (succ(x))) ⇒ ∀x:nat. N(x)⇒P (x)

where P in (10) is an arbitrary predicate. Finally we need a few axioms governing the use of the basic functions

(11) N(zero)

(12) ∀x:nat. N(x) ⇔ N(succ(x))

(13) pred(zero) = zero

(14) ∀x:nat. pred(succ(x)) = x

(15) ifz(Ω_{nat}, x, y) = Ω_{nat}

(16) ifz(zero, x, y) = x

(17) ∀z:nat. N(z) ⇒ ifz(succ(z), x, y) = y.

These axioms turn out as sufficient in practice for verifying properties of PCF programs. We have already mentioned that for principal reasons there cannot be a complete axiomatization of the Scott model. However, it is an interesting open problem to find a set of axioms for PCF which together with all true sentences of arithmetic allow one to derive all sentences true in the Scott model. The list of axioms given above surely does not have this property as they are known to be valid in models of PCF different from the Scott model as e.g. the fully abstract model of PCF.

Chapter 4

Computational Adequacy

One easily verifies by induction on the structure of derivations that in the Scott model we have [[M]] = [[V]] 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 M⇓\underline{n} whenever [[M]] = n ∈ ℕ.^{1}

At first one might think of proving computational adequacy by induction on the structure of programs. This, however, is impossible because subterms of programs, i.e. closed terms of type nat, need neither be closed nor of type nat. The first problem is not that serious as one may quantify over all closed instances of open terms. The second problem, however, is much more serious and requires the introduction of a new concept, namely that of a logical relation. This notion and its variations will turn out as a key concept for semantic investigations since—as we shall see later on—it has much more applications than just providing a nice perspicuous proof of computational adequacy.

Our proof of computational adequacy will be organised as follows. We define for each type σ a relation

R_{σ} ⊆ D_{σ} × Prg_{σ}

by induction on the structure of σ. The family R = (R_{σ} | σ ∈ Type) will be called a logical relation (between semantics and syntax of PCF).

1Notice that for types different from nat one cannot expect that M⇓V whenever [[M]] = [[V]] as is immediate from considering the different syntactic values

M ≡ λx:nat.x  and  V ≡ λx:nat.pred(succ(x))

whose interpretation is equal, namely the identity function on ℕ_{⊥}.

46 Domain-theoretic foundations of functional programming

Then we prove that [[M]]R_{σ}M holds for all closed terms M of type σ. As the logical relation will be defined in a way that [[M]]R_{nat}M just means ∀n∈ℕ. [[M]]=n ⇒ M⇓\underline{n} we are done.

Now we define the logical relation needed for our proof of computational adequacy.

Definition 4.1 We define a family R = (R_{σ} | σ ∈ Type) of relations R_{σ} ⊆ D_{σ} × Prg_{σ} via the clauses

dR_{nat}M iff ∀n∈ℕ. d=n ⇒ M⇓\underline{n}
fR_{σ→τ} M iff ∀d∈D_{σ}.∀N∈Prg_{σ}. dR_{σ}N ⇒ f(d)R_{τ} M(N)

by induction on the structure of types. ♢

Notice that for σ ≡ σ_{1}→ … →σ_{k}→nat we can reformulate fR_{σ}M as

∀d_{1}R_{σ_{1}}N_{1}…. ∀d_{k}R_{σ_{k}}N_{k}. f(d_{1}) … (d_{k})R_{nat}M(N_{1}) … (N_{k})

or, more explicitly, as

∀d_{1}R_{σ_{1}}N_{1}…. ∀d_{k}R_{σ_{k}}N_{k}. ∀n∈ℕ. f(d_{1}) … (d_{k})=n ⇒ M(N_{1}) … (N_{k})⇓\underline{n} .

In any case it is obvious from the definition of R_{nat} that computational adequacy is equivalent to [[M]]R_{nat}M for all programs M of type nat.

For the purpose of showing that [[M]]R_{σ}M holds for all M ∈ Prg_{σ} we need some properties of the logical relation R.

Lemma 4.2 For all types σ it holds that

(1) if d′ ⊑ d and dR_{σ}M then d′R_{σ}M

(2) for every M ∈ Prg_{σ} the set R_{σ}M := { d ∈ D_{σ} | dR_{σ}M } is closed under directed suprema and contains ⊥

(3) if dR_{σ}M and M ⊏ ∼_{σ} M′ then dR_{σ}M′.

Proof. Obviously, conditions (1)–(3) hold for base type nat. For the general case σ ≡ σ_{1}→ … →σ_{k}→nat we employ the characterisation of R_{σ} as given in the remark after Definition 4.1. ad (1) : Suppose g ⊑ f and fR_{σ}M. For showing gR_{σ}M suppose that d_{i}R_{σ_{i}}N_{i} for i=1, …, k. From fR_{σ}M it follows that f(d_{1}) … (d_{k})R_{nat}M(N_{1}) … (N_{k}). Since g ⊑ f we have g(d_{1}) … (d_{k}) ⊑ f(d_{1}) … (d_{k}). Thus, since (1) holds for base type it follows that g(d_{1}) … (d_{k})R_{nat}M(N_{1}) … (N_{k}) as desired.

Computational Adequacy 47

ad (2) : Obviously, we have ⊥R_{σ}M since (2) holds for base type and ⊥(d_{1}) … (d_{k}) = ⊥ for all d_{i} ∈ D_{σ_{i}}. For closure under directed suprema suppose that F ⊆ {d ∈ D_{σ} | dR_{σ}M} is directed. For showing that ⨆ F R_{σ}M suppose that d_{i}R_{σ_{i}}N_{i} for i=1, …, k. Then for all f ∈ F we have f(d_{1}) … (d_{k})R_{nat}M(N_{1}) … (N_{k}) since fR_{σ}M. As (⨆ F )(d_{1}) … (d_{k}) = ⨆_{f∈F} f(d_{1}) … (d_{k}) and (2) holds for base type it follows that (⨆ F )(d_{1}) … (d_{k})R_{nat}M(N_{1}) … (N_{k}) as desired. ad (3) : Suppose fR_{σ}M and M ⊏ ∼_{σ} M′. For showing fR_{σ}M′ suppose that d_{i}R_{σ_{i}}N_{i} for i=1, …, k. Since fR_{σ}M we have f(d_{1}) … (d_{k})R_{nat}M(N_{1}) … (N_{k}). From M ⊏ ∼_{σ} M′ it follows that M(N_{1}) … (N_{k}) ⊏ ∼_{nat} M′(N_{1}) … (N_{k}). Thus, since (3) holds for base type it follows that f(d_{1}) … (d_{k})R_{nat}M′(N_{1}) … (N_{k}) as desired. □

We also need that the least fixpoint operator on D_{σ} is related to Y_{σ} via R_{(σ→σ)→σ}. For showing this we need the following lemma.

Lemma 4.3 For every PCF type σ it holds that M(Y_{σ}(M)) ⊏ ∼_{σ} Y_{σ}(M).

Proof. Suppose that M(Y_{σ}(M))(N_{1}) … (N_{k})⇓\underline{n}. Then by inspection of the inductive definition of ⇓ there exist syntactic values V_{1}, …, V_{k} such that M(Y_{σ}(M))⇓V_{1}, V_{i}(N_{i})⇓V_{i+1} for i < k and V_{k}(N_{k})⇓\underline{n}. But from M(Y_{σ}(M))⇓V_{1} it follows that Y_{σ}(M)⇓V_{1} and, accordingly, that Y_{σ}(M)(N_{1}) … (N_{k})⇓\underline{n} as desired. □

A similar argument shows that Y_{σ}(M) ⊏ ∼_{σ} M(Y_{σ}(M)). Thus, by Milner’s Context Lemma (proved in the next chapter) the terms Y_{σ}(M) and M(Y_{σ}(M)) are observationally equivalent as expected.

Lemma 4.4 If fR_{σ→σ}M then μ(f)R_{σ}Y_{σ}(M).

Proof. Suppose fR_{σ→σ}M. For showing μ(f)R_{σ}Y_{σ}(M) by Lemma 4.2(2) it suffices to show that f^{n}(⊥)R_{σ}Y_{σ}(M) for all n ∈ ℕ. The base case ⊥R_{σ}Y_{σ}(M) holds by Lemma 4.2(2). Suppose f^{n}(⊥)R_{σ}Y_{σ}(M) as induction hypothesis. Thus, as fR_{σ}M it follows that f^{n+1}(⊥)R_{σ}M(Y_{σ}(M)). By Lemma 4.3 we have M(Y_{σ}(M)) ⊏ ∼_{σ} Y_{σ}(M). Using Lemma 4.2(3) conclude that f^{n+1}(⊥)R_{σ}Y_{σ}(M) as desired. □

Now we are ready to prove the following Main Lemma for the logical relation R entailing that [[M]]R_{σ}M for all M ∈ Prg_{σ}.

Lemma 4.5 (Main Lemma for R) If x_{1}:σ_{1}, …, x_{k}:σ_{k} ⊢ M : τ and d_{i}R_{σ_{i}}N_{i} for i=1, …, k then

[[x_{1}:σ_{1}, …, x_{k}:σ_{k} ⊢ M]](d⃗) R_{τ} M[N⃗/x⃗] .

48 Domain-theoretic foundations of functional programming

Proof. The proof is by induction on the structure of derivations of terms in context. For facilitating notation we write d⃗RN⃗ instead of d_{i}R_{σ_{i}}N_{i} for i=1, …, k. Variables : For x_{1}:σ_{1}, …, x_{k}:σ_{k} ⊢ x_{i} : σ_{i} and d⃗RN⃗ we have

[[x_{1}:σ_{1}, …, x_{k}:σ_{k} ⊢ x_{i}]](d⃗) = d_{i} R_{σ_{i}} N_{i} ≡ x_{i}[N⃗/x⃗]

as desired. λ-Abstraction : Suppose as induction hypothesis that the claim of the theorem holds for Γ, x:σ ⊢ M : τ. Further suppose that d⃗RN⃗. We have to show that

[[Γ ⊢ λx:σ. M]](d⃗) R_{σ→τ} (λx:σ. M)[N⃗/x⃗]

where x⃗ is the list of variables declared in Γ. For that purpose assume that dR_{σ}N. From the induction hypothesis it follows that

[[Γ, x:σ ⊢ M]](d⃗, d) R_{τ} M[N⃗, N/x⃗, x]

and, therefore, by Lemma 4.2(3) that

[[Γ ⊢ λx:σ. M]](d⃗)(d) R_{τ} (λx:σ. M)[N⃗/x⃗](N)

because

[[Γ ⊢ λx:σ. M]](d⃗)(d) = [[Γ, x:σ ⊢ M]](d⃗, d)

and^{2}

M[N⃗, N/x⃗, x] ≡ M[N⃗/x⃗][N/x] ⊏ ∼_{τ} (λx:σ. M[N⃗/x⃗])(N) ≡ (λx:σ. M)[N⃗/x⃗](N) .

Application : Suppose as induction hypothesis that the claim of the theorem holds for Γ ⊢ M_{1} : σ→τ and Γ ⊢ M_{2} : σ. Now if d⃗RN⃗ then due to the induction hypotheses we have

[[Γ ⊢ M_{i}]](d⃗) R M_{i}[N⃗/x⃗]

for i=1, 2 from which it follows that

[[Γ⊢M_{1}]](d⃗)([[Γ ⊢ M_{2}]](d⃗)) R M_{1}[N⃗/x⃗](M_{2}[N⃗/x⃗]) .

As

[[Γ⊢M_{1}(M_{2})]](d⃗) = [[Γ⊢M_{1}]](d⃗)([[Γ ⊢ M_{2}]](d⃗))

2as it generally holds that M[N/x] ⊏ ∼ (λx:σ.M)N for M ∈ Prg_{σ→τ} and N ∈ Prg_{σ}

Computational Adequacy 49

and

M_{1}[N⃗/x⃗](M_{2}[N⃗/x⃗]) ≡ M_{1}(M_{2})[N⃗/x⃗]

it then follows that

[[Γ⊢M_{1}(M_{2})]](d⃗) R M_{1}(M_{2})[N⃗/x⃗]

as desired. Recursion : Suppose as induction hypothesis that Γ ⊢ M : σ→σ satisfies the requirement of the theorem. Now if d⃗RN⃗ then due to the induction hypothesis we have

[[Γ ⊢ M]](d⃗) R M[N⃗/x⃗]

from which it follows by Lemma 4.4 that

[[Y_{σ}(M)]](d⃗) = μ([[Γ ⊢ M]](d⃗)) R Y_{σ}(M[N⃗/x⃗]) ≡ Y_{σ}(M)[N⃗/x⃗]

as desired.

Basic Operations : One easily checks that 0R_{nat}zero and that from xR_{nat}M, y_{1}R_{nat}N_{1} and y_{2}R_{nat}N_{2} it follows that [[succ]](x)R_{nat}succ(M), [[pred]](x)R_{nat}pred(M) and [[ifz]](x, y_{1}, y_{2})R_{nat}ifz(M, N_{1}, N_{2}). Using these observations the remaining cases for zero, succ, pred and ifz go through without pain. □

The following theorem is a special case of the previous lemma.

Theorem 4.6 (Computational Adequacy) For every closed term M of type nat we have M⇓\underline{n} whenever [[M]] = n.

Proof. Immediate from Lemma 4.5 since ⊢ M : nat for closed terms M of type nat. □

Thus, for ⊢ M : nat and n ∈ ℕ we have

M ⇓ \underline{n}  iff  [[M]] = n

i.e. a closed term of type nat denotes a natural number if and only if it evaluates to the corresponding numeral.

Chapter 5

Milner’s Context Lemma

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.

Theorem 5.1 (Milner’s Context Lemma) For all types σ and M, N ∈ Prg_{σ} the following conditions are equivalent

(a) M ⊏ ∼_{σ} N  (b) M < ∼_{σ} N  (c) [[M]]R_{σ}N .

Proof. (b) ⇒ (a) : since contexts of the form [ ]P⃗ are just particular contexts of base type.

(a) ⇒ (c) : Suppose M ⊏ ∼_{σ} N. From Lemma 4.5 we know that [[M]]RM. Thus, it follows from Lemma 4.2(3) that [[M]]R_{σ}N.

(c) ⇒ (b) : Suppose [[M]]R_{σ}N. Let P ∈ Prg_{σ→nat}. As by Lemma 4.5 we have [[P]]R_{σ→nat}P it follows that [[P]]([[M]])R_{nat}N(P). Thus, as [[P (M)]] = [[P]]([[M]]) we have [[P (M)]]R_{nat}P (N). If P (M)⇓\underline{n} then by correctness of the operational semantics we have [[M(P)]] = n and, therefore, also nR_{nat}P (N) from which it follows that P (N)⇓\underline{n} as desired. □

The following corollary gives a further characterisation of < ∼.

Corollary 5.2 For all types σ and M, N ∈ Prg_{σ} we have

M < ∼_{σ} N  iff  ∀d∈D_{σ}. dR_{σ}M ⇒ dR_{σ}N .

Proof. The forward direction follows from Lemma 4.2(3) since by Theorem 5.1 the relations < ∼_{σ} and ⊏ ∼_{σ} coincide.

For the reverse direction suppose that ∀d∈D_{σ}. dR_{σ}M ⇒ dR_{σ}N. Then, in particular, we have [[M]]R_{σ}M ⇒ [[M]]R_{σ}N. As by Lemma 4.5 we have

52 Domain-theoretic foundations of functional programming

[[M]]R_{σ}M it follows that [[M]]R_{σ}N. Thus, by Theorem 5.1 it follows that M < ∼_{σ} N as desired. □

This corollary tells us that we may replace quantification over syntactic experiments of the form P (−)⇓\underline{n} equivalently by quantification over semantic experiments of the form dR_{σ}(−).

We may also use the logical relation R for defining an alternative partial order ≤_{σ} on D_{σ} as follows

d_{1} ≤_{σ} d_{2}  iff  ∀P ∈ Prg_{σ}. d_{2}R_{σ}P ⇒ d_{1}R_{σ}P

which by Lemma 4.2(1) contains ⊑_{D_{σ}}. It is an easy exercise(!) to show that ≤_{σ} (as a subset of D_{σ}×D_{σ}) is closed under suprema of directed sets. For closed terms M and N of type σ we have

[[M]] ≤_{σ} [[N]]  iff  M < ∼_{σ} N

as by Theorem 5.1 the condition ∀P ∈ Prg_{σ}. [[N]]R_{σ}P ⇒ [[M]]R_{σ}P is equivalent to ∀P ∈ Prg_{σ}. N < ∼_{σ} P ⇒ M < ∼_{σ} P, i.e. M < ∼_{σ} N. Thus, in a very precise sense ≤ is the denotational analogue of < ∼.

Chapter 6

The Full Abstraction Problem

In the previous chapter we have seen that [[M]] ⊑ [[N]] entails M < ∼ N as from [[M]] ⊑ [[N]] and [[N]]RN it follows that [[M]]RN 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 [[M]] = [[N]] need not hold even if M and N are observationally equal. This phenomenon occurs already at type (ι→ι→ι)→ι and the reason is that there are not enough PCF-definable objects within D_{ι→ι→ι}.

For the reader’s convenience we officially fix some terminology introduced informally already in the introduction.

Definition 6.1 (Full Abstraction) A model of PCF is called equationally fully abstract iff

M ≃ N ⇒ [[M]] = [[N]]

for all closed terms M and N of the same type where M ≃ N is an abbreviation for M < ∼ N ∧ N < ∼ N. A model of PCF is called fully abstract iff

M < ∼ N ⇒ [[M]] ⊑ [[N]]

for all closed terms M and N of the same type. ♢

Obviously, every fully abstract model is also equationally fully abstract.

In the next chapter we will show that there is no PCF-definable function f ∈ D_{ι→ι→ι} satisfying the constraints

(†)  f0⊥ = 0  f⊥0 = 0  f11 = 1 .

54 Domain-theoretic foundations of functional programming

In the Scott model there is a least one such function, namely

porxy = \{ \begin{matrix}0 & if x = 0 or y = 0 \\ 1 & if x = 1 = y \\ ⊥ & otherwise \end{matrix}

called “parallel or”. In the following lemma we exhibit two functionals of type (ι→ι→ι)→ι which are definable in PCF and give different results only when applied to f satisfying condition (†).

Lemma 6.2 Consider the terms

portest_{i} ≡ λf:ι→ι→ι. ifz(f \underline{0} Ω_{ι}, ifz(f Ω_{ι} \underline{0}, ifz(p̃red(f \underline{1} \underline{1}), \underline{i}, Ω_{ι}), Ω_{ι}), Ω_{ι})

of type (ι→ι→ι)→ι for i=0, 1 where Ω_{ι} ≡ Y_{ι}(λx:ι.x) and p̃red stands for the term λx:ι.ifz(x, Ω_{ι}, ifz(pred(x), \underline{0}, Ω_{ι})). Then for all f ∈ D_{ι→ι→ι}

• [[portest_{i}]](f) = i whenever f satisfies condition (†) and

• [[portest_{i}]] = ⊥ otherwise.

Proof. Obvious by unfolding the definition of portest_{0} and portest_{1}. □

Thus, if for all closed terms of type ι→ι→ι their interpretation does not satify condition (†) then by Milner’s Context Lemma (and computational adequacy) the programs portest_{0} and portest_{1} are observationally equal although their interpretations are different in the Scott model since [[portest_{0}]](por) = 0 and [[portest_{1}]](por) = 1.

Intuitively, it is clear that one cannot implement a function satisfying (†) in PCF because evaluation strategies for PCF terms are necessarily sequential, i.e. either the first or the second argument has to be evaluated first, whereas any implementation of an f satisfying condition (†) has to evaluate both arguments in parallel.^{1} However, a precise mathematical proof of this fact requires some sophistication and, therefore, we postpone it to the next chapter where we develop the necessary machinery of logical relations.

Actually, we will show a bit more, namely that all first order PCFdefinable functions are stable, i.e. preserve binary infima (denoted by ⊓) of consistent pairs, i.e. pairs of elements having a common extension^{2}.

1For example the first argument may diverge whereas the second argument evaluates to 0. In this case it would be wrong to evaluate the first argument first as this would lead to non-termination of the function call although it should evaluate to 0. A symmetric argument shows that it is also wrong to evaluate always the second argument first.

2We write x↑y as an abbreviation for ∃z. x ⊑ z ∧ y ⊑ z and say that “x and y are consistent” if this condition holds.

The Full Abstraction Problem 55

Lemma 6.3 For every term M of first order type, i.e. of type

\overbrace{ι→ … →ι→}^{k times} ι

for some k ∈ ℕ, it holds that

[[M]](x_{1}⊓y_{1}) … (x_{k}⊓y_{k}) = [[M]](x_{1}) … (x_{k}) ⊓ [[M]](y_{1}) … (y_{k})

for all x⃗, y⃗ ∈ D_{ι}^{k} with x_{i}↑y_{i} for i=1, …, k.

This has the consequence that

Corollary 6.4 There are no PCF definable functions of type D_{ι→ι→ι} satisfying the constraint (†).

Proof. Suppose f is PCF definable and satisfies (†). Then f0⊥ = 0 = f⊥0 and, therefore, we have

f⊥⊥ = f(0 ⊓ ⊥)(⊥ ⊓ 0) = f0⊥ ⊓ f⊥0 = 0 ⊓ 0 = 0

by Lemma 6.3. However, by (†) we have f11 = 1 and, thus, by monotonicity of f it follows that 0 ⊑ 1 which is impossible. □

The observation of Lemma 6.3 was taken as a starting point by G. Berry, who in his Thése d’ Etat [Berry 1979] introduced and investigated a category of so-called “stable domains” where all morphisms are required not only to be Scott continuous but also stable in the sense that

x↑y ⇒ f(x⊓y) = f(x)⊓f(y)

for all arguments x and y. The obvious advantage of stable domain theory is that it refutes the existence of maps like “parallel or” which—as we have seen—are responsible for the lack of full abstraction of the Scott model. This, however, is achieved only at the price that the order on function spaces is not pointwise anymore.

Notice that in the Scott model even very simple PCF-definable functions are not stable as for example the evaluation function

ev = λf:ι→ι.λx:ι.f(x)

which can be seen as follows. Consider the functions f_{1} = [[λx:ι.zero]] and f_{2} = [[λx:ι.ifz(x, zero, zero)]]. We have f_{1}⊥ = 0 and f_{2}0 = 0 and, therefore, also f_{1}⊥ ⊓ f_{2}0 = 0 whereas (f_{1}⊓f_{2})(⊥⊓0) = f_{2}⊥ = ⊥ which is a counterexample to stability of ev as f_{2} ⊑ f_{1} and ⊥ ⊑ 0. Accordingly, in the stable domains model f_{2} ⋢ f_{1} as otherwise ev were not even monotonic. But

56 Domain-theoretic foundations of functional programming

we have λx:ι.ifz(x, zero, zero) < ∼ λx:ι.zero and, accordingly, Berry’s stable domains models is not fully abstract either.

A remarkable consequence of the stability of PCF-definable first order functions f is that whenever fx⃗ = n ∈ ι then there exists a least y⃗ ⊑ x⃗ with fy⃗ = n, namely the infimum of all z⃗ ⊑ x⃗ with fz⃗ = n. Notice that if there is a sequential evaluation strategy for f then this property is automatic. Thus, there is no sequential algorithm for functions f satisfying condition (†) as then f0⊥ = 0 = f⊥0 whereas f⊥⊥ = ⊥, i.e. (0, ⊥) and (⊥, 0) are different minimal approximations to (0, 0) giving rise to output 0.

An operational semantics for por for which the Scott model is computationally adequate is given by the rules

{M⇓\underline{0} \atop porMN⇓\underline{0}}  {N⇓\underline{0} \atop porMN⇓\underline{0}}  {M⇓\underline{1} N⇓\underline{1} \atop porMN⇓\underline{1}}

where the first two rules do overlap as there are two different derivations of por\underline{0}\underline{0}⇓\underline{0}. Although for every term M there is still at most one V with M⇓V there is no sequential evaluation strategy for terms of the form porMN. As if one would always evaluate the first argument first then the evaluation of the whole term may diverge even if the second argument evaluates to \underline{0}. A symmetric argument shows that it is also wrong to evaluate always the second argument first.

For reasons of efficiency deterministic parallel language constructs like por are not implemented in actual functional languages and, accordingly, the Scott model is not fully abstract for them. However, it should be emphasized that por is computable and thus can be implemented in principle. It corresponds to the well known dove tailing technique known from recursion theory (see e.g. [Rogers 1987]) where it is used e.g. for showing that semi-decidable predicates are closed under binary unions. Dove tailing as used in recursion theory is highly intensional as it uses Kleene’s T -predicate which amounts to a primitive recursive coding^{3} of operational semantics: if A_{i} = {n∈ℕ | ∃k.T (e_{i}, n, k)} then A_{1}∪A_{2} is the halting set of the algorithm μk.T (e_{1}, n, k)∨T (e_{2}, n, k). The language construct por may be considered as an extensional version of dove tailing avoiding any coding of the operational semantics. In recursion theory one uses also infinite variants of dove tailing e.g. for showing that the union of an r.e. set of r.e. sets is r.e. again. This can be implemented in PCF using por via the functional

3Recall that T (e, n, k) means “k is a code for a terminating computation sequence for the application of program with number e to argument n”.

The Full Abstraction Problem 57

por_{∞} : (ι→ι)→ι defined via the recursion equation

por_{∞}(p) = por(p(zero))(por_{∞}(λx:nat.p(succ(x))))

from which one can read off easily an implementing PCF term.

In his famous paper “LCF considered as a programming language” [Plotkin 1977] G. Plotkin has shown that the Scott model is fully abstract for PCF+por. The clue of the proof^{4} was to show that for every type σ sufficiently many elements, namely the so-called compact (or finite) elements, are all definable in PCF + por. These compact elements suffice as every element of D_{σ} appears as directed supremum of the compact elements approximating it. Thus, if continuous functions are identical on the compact elements then they are identical on all arguments. In the same paper [Plotkin 1977] Plotkin has shown that, however, not all “computable” elements of the Scott model can be denoted by terms of PCF+por.^{5} This, however, can be remedied by adding the “continuous existential quantifier” ∃ : (ι→ι)→ι whose operational semantics is given by the rules

M\underline{n} ⇓ \underline{0} ; (n ∈ ℕ) ; ∃(M) ⇓ \underline{0}  {MΩ_{ι} ⇓ \underline{1} \atop ∃(M) ⇓ \underline{1}}

Summarizing we can say that the Scott model is neither fully abstract nor universal for PCF. However, this doesn’t diminish the relevance of the Scott model as there are reasonable extensions of PCF for which the Scott model is fully abstract and even universal. Much later in Chapters 11 and 12 we will use a somewhat sophisticated logical relation technique for transforming the Scott model into a fully abstract model for PCF.

4for details see Chapter 13

5An element is called “computable” iff the set of codes of approximating compact elements is recursively enumerable.

Chapter 7

Logical Relations

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.

Definition 7.1 (Logical Relation) Let W be an arbitrary set. A logical relation of arity W on the Scott model of PCF is a family

R = (R_{σ} ∈ P(D_{σ}^{W}) | σ ∈ Type)

such that

f ∈ R_{σ→τ} ⇔ ∀d∈R_{σ}. \underline{λ}i∈W.f(i)(d(i)) ∈ R_{τ} ⇔ ∀d∈R_{σ}. ev∘⟨f, d⟩ ∈ R_{τ}

for all types σ and τ. ♢

Notice that a logical relation R of arity W is uniquely determined by R_{nat} and that for all subsets P ⊆ D_{nat}^{W} there exists a unique logical relation R of arity W with R_{nat} = P.

Theorem 7.2 (Main Lemma for Logical Relations) Let R be a logical relation of arity W on the Scott model of PCF. Then for λ-terms x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ M : τ and d_{j} ∈ R_{σ_{j}} for j=1, .., n it holds that

\underline{λ}i∈W. [[x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ M]](d⃗(i)) ∈ R_{τ}

where d⃗(i) = ⟨d_{1}(i), …, d_{n}(i)⟩ for i ∈ W.

Proof. We proceed by induction on the structure of derivations of judgements of the form Γ ⊢ M : σ using only the rules for variables, λ-abstraction and application.

60 Domain-theoretic foundations of functional programming

(1) If M is a variable then the claim is trivial (exercise!).

(2) Suppose as induction hypothesis that the claim holds for Γ, x:σ ⊢ M : τ where Γ ≡ x_{1}:σ_{1}, …, x_{n}:σ_{n}. Suppose that d_{j} ∈ R_{σ_{j}} for j=1, …, n. We have to show that

\underline{λ}i∈W. [[Γ ⊢ λx:σ.M]](d⃗(i)) ∈ R_{σ→τ} .

For that purpose assume that d ∈ R_{σ}. Then we have

\underline{λ}i∈W. [[Γ ⊢ λx:σ.M]](d⃗(i))(d(i)) = \underline{λ}i∈W. [[Γ, x:σ ⊢ M]](⟨d⃗(i), d(i)⟩)

whose right hand side is in R_{τ} due to the induction hypothesis.

(3) Suppose as induction hypotheses that the claim holds for Γ ⊢ M : σ→τ and Γ ⊢ N : σ where Γ ≡ x_{1}:σ_{1}, …, x_{n}:σ_{n}. Let d_{j} ∈ R_{σ_{j}} for j=1, …, n. We have to show that

\underline{λ}i∈W. [[Γ ⊢ M(N)]](d⃗(i)) ∈ R_{τ} .

As [[Γ ⊢ M(N)]](d⃗(i)) = [[Γ ⊢ M]](d⃗(i))([[Γ ⊢ N]](d⃗(i))) this amounts to showing

\underline{λ}i∈W. [[Γ ⊢ M]](d⃗(i))([[Γ ⊢ N]](d⃗(i))) ∈ R_{τ}

which, however, follows immediately from the definition of R_{σ→τ} because we have \underline{λ}i∈W. [[Γ ⊢ M]](d⃗(i)) ∈ R_{σ→τ} and \underline{λ}i∈W. [[Γ ⊢ N]](d⃗(i)) ∈ R_{σ} by the induction hypotheses on M and N. □

Thus, for closed λ-terms we get that in particular

Corollary 7.3 If R is a logical relation of arity W and M is a closed λ–term of type σ then \underline{λ}i∈W. [[M]] ∈ R_{σ}.

Proof. Immediate from Theorem 7.2 specializing to empty contexts. □

which motivates the following

Definition 7.4 (R-invariant) Let R be a logical relation of arity W. Then an object d ∈ D_{σ} is called R-invariant iff δ_{W} (d) := \underline{λ}i∈W.d ∈ R_{σ}. ♢

Thus Corollary 7.3 can be reformulated as follows: the denotation of a closed λ-term is R-invariant for all logical relations R.

Corollary 7.5 Let R be a logical relation on the Scott model of arity W and x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ M : τ a λ-term. Then [[Γ ⊢ M]](d⃗) is R-invariant whenever all d_{i} in d⃗ are R-invariant.

Logical Relations 61

Proof. If all d_{i} are R–invariant then all δ_{W} (d_{i}) ∈ R_{σ_{i}} and, therefore,

δ_{W} ([[Γ ⊢ M]](d⃗)) = \underline{λ}i∈W. [[Γ ⊢ M]](⟨δ_{W} (d_{1})(i), …, δ_{W} (d_{n})(i)⟩) ∈ R_{τ}

by Theorem 7.2. □

Thus, an element of the Scott model is R-invariant if it is λ-definable from elements which are R-invariant. Accordingly, the interpretation of a closed PCF-term is R-invariant if the interpretations of the terms

zero λx:ι.succ(x) λx:ι.pred(x) λx:ι.λy:ι.λz:ι.ifz(x, y, z) λf:σ→σ.Y_{σ}(f)

are all R-invariant in which case we say that “all PCF constants are Rinvariant”.

We now discuss a property of logical relations guaranteeing that the interpretations of all λf:σ→σ.Y_{σ}(f) are R-invariant.

Definition 7.6 A logical relation R of arity W is called admissible iff δ_{W} (⊥) ∈ R_{ι} and R_{ι} is closed under suprema of directed subsets. ♢

Notice that for finite W there are no nontrivial directed subsets of D_{ι}^{W} and, accordingly, in this case a logical relation of arity W is admissible if and only if δ_{W} (⊥) ∈ R_{ι}.

Theorem 7.7 Let R be a an admissible logical relation on the Scott model of arity W. Then for all types σ we have that

(1) δ_{W} (⊥) ∈ R_{σ} and R_{σ} is closed under suprema of directed subsets and (2) the interpretation of λf:σ→σ.Y_{σ}(f) is R-invariant.

Proof. First we show claim (1) by induction on the structure of σ. For ι claim (1) holds by definition of admissibility. Suppose as induction hypotheses that claim (1) holds for σ and τ. That δ_{W} (⊥) ∈ R_{σ→τ} follows from δ_{W} (⊥) ∈ R_{τ} as insured by the induction hypothesis for τ. Suppose that F is a directed subset of R_{σ→τ}. For showing that ⨆ F ∈ R_{σ→τ} assume that d ∈ R_{σ}. Then \underline{λ}i∈W.f(i)(d(i)) ∈ R_{τ} for all f ∈ F and, therefore, also ⨆_{f∈F} \underline{λ}i∈W.f(i)(d(i)) ∈ R_{τ} as R_{τ} is closed under suprema of directed sets by induction hypothesis for τ. Thus, as ⨆_{f∈F} \underline{λ}i∈W.f(i)(d(i)) = \underline{λ}i∈W. ⨆_{f∈F} f(i)(d(i)) = \underline{λ}i∈W.(⨆ F )(i)(d(i)) it follows that

\underline{λ}i∈W.(⨆ F )(i)(d(i)) ∈ R_{τ}

as desired.

62 Domain-theoretic foundations of functional programming

For claim (2) suppose that f ∈ R_{σ→σ}. Then one easily shows by induction that \underline{λ}i∈W.f(i)^{n}(⊥) ∈ R_{σ} for all n ∈ ℕ. As by (1) the set R_{σ} is closed under suprema of directed sets it follows that

\underline{λ}i∈W.δ_{W} ([[λf:σ→σ.Y_{σ}(f)]])(i)(f(i)) = \underline{λ}i∈W.μ(f(i)) ∈ R_{σ}

as desired. □

This has the following immediate consequence.

Theorem 7.8 Let R be an admissible logical relation on the Scott model such that the interpretations of the terms

zero  λx:ι.succ(x)  λx:ι.pred(x)  λx:ι.λy:ι.λz:ι.ifz(x, y, z)

are all R-invariant. Then all interpretations of closed PCF-terms are Rinvariant.

Proof. Immediate from (the remark after) Corollary 7.5 and Theorem 7.7(2). □

We now consider some (useful) examples of logical relations satisfying the premisses of Theorem 7.8.

(x, y, z) ∈ R_{ι}^{(1)} ⇔ x↑y ∧ z = x ⊓ y
(x, y, z) ∈ R_{ι}^{(2)} ⇔ x=⊥ ∨ y=⊥ ∨ z=⊥ ∨ x=y=z

where x↑y is an abbreviation for ∃z. x ⊑ z ∧ y ⊑ z.

As the arity of these relations is finite and (⊥, ⊥, ⊥) is an element of both R_{ι}^{(1)} and R_{ι}^{(2)} it follows that they are admissible. That the interpretations of zero, λx:ι.succ(x), λx:ι.pred(x) and λx:ι.λy:ι.λz:ι.ifz(x, y, z) are all invariant under both R^{(1)} and R^{(2)} is a straightforward, but tedious exercise.

Thus, we can now give the

Proof (of Lemma 6.3) : As the logical relation R^{(1)} satisfies the premisses of Theorem 7.8 we know that the interpretation of every closed PCF term of first order type is R^{(1)}- invariant and thus stable. □

As R^{(2)} satisfies the premisses of Theorem 7.8 we know that every PCF definable f ∈ D_{ι→ι→ι} is R^{(2)}-invariant. Such an f cannot simultaneously satisfy f0⊥ = 0 = f⊥0 and f11 = 1 as (⊥, 0, 1) and (0, ⊥, 1) are in R_{ι}^{(2)} whereas (f⊥0, f0⊥, f11) = (0, 0, 1) is not. This consideration provides an alternative proof of Lemma 6.3.

However, we have that

Logical Relations 63

Lemma 7.9 Plotkin’s continuous existential quantifier is R^{(2)}-invariant.

Proof. Suppose (∃(f_{1}), ∃(f_{2}), ∃(f_{3})) ∉ R_{ι}^{(2)} then w.l.o.g. one of the following to cases applies

(1) ∃(f_{1}) = 0 = ∃(f_{2}) and ∃(f_{3}) = 1

(2) ∃(f_{1}) = 0 and ∃(f_{2}) = 1 = ∃(f_{3}).

In case (1) there exist n_{1}, n_{2} ∈ ℕ with f_{1}(n_{1}) = 0 = f_{2}(n_{2}) and f_{3}(⊥) = 1. As (n_{1}, n_{2}, ⊥) ∈ R_{ι}^{(2)} it follows that (f_{1}, f_{2}, f_{3}) ∉ R_{ι→ι}^{(2)}. In case (2) there exists an n ∈ ℕ with f_{1}(n) = 0 and f_{2}(⊥) = 1 = f_{3}(⊥). As (n, ⊥, ⊥) ∈ R_{ι}^{(2)} it follows that (f_{1}, f_{2}, f_{3}) ∉ R_{ι→ι}^{(2)}. □

As ∃ is R^{(2)}-invariant but por is not R^{(2)}-invariant it follows from Corollary 7.5 that por is not PCF definable from ∃.

More generally, there arises the question to which extent one can characterise PCF definability via logical relations. To some extent K. Sieber has achieved such a characterization up to type level ≤ 2, i.e. for types σ_{1}→ … →σ_{n}→ι where the σ_{i} are all first order, in [Sieber 1992] where he has shown that for types σ of type level ≤ 2 an element d ∈ D_{σ} arises as supremum of a directed set of PCF-definable elements if and only if d is invariant under all logical relations of finite arity satisfying the premisses of Theorem 7.8. Moreover, he has given also a purely combinatorial, syntaxfree characterization of this class of logical relations. However, using a wider class of logical relations (of varying arity also called Kripke logical relations) one may characterise for arbitrary types σ those d ∈ D_{σ} which arise as suprema of directed sets of PCF-definable elements. Later in Chapters 10 and 11 we will use Kripke logical relations for constructing a fully abstract model of PCF in a completely syntax-free way.

In his seminal paper [Plotkin 1977] G. Plotkin has shown that ∃ is not definable from por by a purely syntactical argument. The following consideration shows that this cannot be achieved by an argument using admissible logical relations. Consider

∃_{n}(f : ι→ι) = ifz(f(\underline{0}) por … porf(\underline{n}), \underline{0}, f(Ω_{ι}))

which is obviously definable in PCF+por. As ∃ is the supremum of the increasing chain (∃_{n})_{n∈ℕ} it follows that ∃ is invariant under all admissible logical relations under which the constants of PCF and por are invariant.

Chapter 8

Some Structural Properties of the D_{σ}

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.

Lemma 8.1 For every PCF type σ the cpo D_{σ} has infima of nonempty finite subsets and there exists a closed PCF term glb^{σ} of type σ→σ→σ such that [[glb^{σ}]]xy is the infimum of x and y for all x, y ∈ D_{σ}.

Proof. For ι we may define glb^{ι} as λx:ι.λy:ι.ifz(eqxy, x, Ω_{ι}) where eq is a PCF term deciding equality of natural numbers. The function eq can for example be implemented by the PCF term λx:ι.λy:ι. (x− . y)+(y− . x) where − . stands for truncated subtraction. Obviously, [[glb^{ι}]]xy = x if x = y and ⊥ otherwise and, therefore, delivers the binary infimum of x and y as desired.

Now if by induction hypothesis there is a PCF term glb^{σ} computing the binary infimum for D_{σ} then

glb^{τ→σ} ≡ λf:τ→σ.λg:τ→σ.λy:τ. glb^{σ}(f(y), g(y))

computes the binary infimum in D_{τ→σ} which can be seen as follows. If f and g are continuous functions from D_{τ} to D_{σ} then [[glb^{τ→σ}]]fg is continuous and [[glb^{τ→σ}]]fgy = f(y)⊓g(y) for all y ∈ D_{τ}. Obviously, we have [[glb^{τ→σ}]]fg ⊑ f, g and if h : D_{τ} →D_{σ} with h ⊑ f, g then h(y) ⊑ f(y) ⊓ g(y) for all y ∈ D_{τ}, i.e. h ⊑ [[glb^{τ→σ}]]fg. Thus [[glb^{τ→σ}]]fg is the infimum of f and g as desired. □

Next we will show that every element in D_{σ} appears as supremum of an ascending chain of “finite approximations”.

66 Domain-theoretic foundations of functional programming

Definition 8.2 Let less be a PCF term of type ι→ι→ι with

[[less]]xy = \{ \begin{matrix}0 & if x, y ∈ ℕ and x < y \\ 1 & if x, y ∈ ℕ and x ≥ y \\ ⊥ & otherwise. \end{matrix}

For all PCF types σ we define closed PCF terms ψ_{n}^{σ} of type σ→σ by recursion on the structure of σ via the following two clauses

ψ_{n}^{ι} ≡ λx:ι. ifz(less x \underline{n}, x, Ω_{ι})
ψ_{n}^{σ→τ} ≡ λf:σ→τ.λx:σ.ψ_{n}^{τ}(f(ψ_{n}^{σ}(x)))

for all n∈ℕ. ♢

The next lemma identifies characteristic properties of the functions denoted by the ψ_{n}^{σ}.

Lemma 8.3 For h_{n}^{σ} := [[ψ_{n}^{σ}]] it holds that

(1) h_{n}^{σ} ∘ h_{n}^{σ} = h_{n}^{σ} ⊑ id_{D_{σ}}

(2) (h_{n}^{σ})_{n∈ℕ} is an ascending chain whose supremum is id_{D_{σ}}

(3) h_{n}^{σ}[D_{σ}] := {h_{n}^{σ}(d) | d ∈ D_{σ}} is finite.

Proof. Obviously, the three requirements hold for ι.

Suppose as induction hypotheses that the three requirements hold for σ and τ. Obviously, we have h_{n}^{σ→τ} (f) = h_{n}^{τ} ∘f ∘h_{n}^{σ} from which (1) and (2) for σ→τ follow easily from the requirements (1) and (2) for σ and τ as ensured by the induction hypotheses. Furthermore, from h_{n}^{σ→τ} (f) = h_{n}^{τ} ∘ f ∘ h_{n}^{σ}

it follows^{1} that |h_{n}^{σ→τ} [D_{σ→τ)}]| ≤ |h_{n}^{τ}[D_{τ}]|^{|h_{n}^{σ}[D_{σ}]|} which is finite as by induction hypothesis |h_{n}^{σ}[D_{σ}]| and |h_{n}^{τ}[D_{τ}]| are finite. □

Now we will study the properties identified in Lemma 8.1 and Lemma 8.3 axiomatically as requirements for cpo’s.

Definition 8.4 A cpo D is called SFP iff there exists an ascending chain (h_{n} : D→D)_{n∈ℕ} of continuous functions such that

(1) every h_{n} is a projection, i.e. h_{n} ∘ h_{n} = h_{n} ⊑ id_{D}

(2) ⨆_{n∈ℕ} h_{n} = id_{D}

(3) every h_{n} is finitary, i.e. h_{n}[D] is finite.

Accordingly, a cpo D is called SFP iff id_{D} is the supremum of an ascending chain of finitary projections. ♢

1as h_{n}^{σ→τ} (f) = h_{n}^{σ→τ} (g) are equal iff their restrictions to h_{n}^{σ}[D_{σ}] are equal

Some Structural Properties of the D_{σ} 67

If id_{D} is the supremum of a chain h_{n} of finitary projections then we may call an element d ∈ D compact (or simply finite) iff d = h_{n}(d) for some n ∈ ℕ. The next lemma shows that this notion is independent from the choice of the sequence (h_{n})_{n∈ℕ} exhibiting D as an SFP cpo.

Lemma 8.5 Let (h_{n}:D→D)_{n∈ℕ} be an increasing sequence of finitary projections whose supremum is id_{D}. Then for e ∈ D the following two conditions are equivalent

(1) e = h_{n}(e) for some n ∈ ℕ

(2) for every directed subset X ⊆ D with e ⊑ ⨆ X there exists an x ∈ X with e ⊑ x.

Proof. Suppose e = h_{n}(e). Let X be a directed subset of D with e ⊑ ⨆ X. Then e = h_{n}(e) ⊑ h_{n}(⨆ X) = ⨆ h_{n}[X]. As h_{n}[X] is finite (since h_{n}[D] is finite) and directed there exists an x ∈ X with h_{n}(x) = ⨆ h_{n}[X] ⊒ e. For such an x we have e ⊑ h_{n}(x) ⊑ x ∈ X as desired.

For the reverse direction suppose that e satisfies (2). Notice that the set {h_{n}(e) | n ∈ ℕ} is directed and its supremum is e. Thus, as e satisfies (2) there exists an n ∈ ℕ with e ⊑ h_{n}(e). As h_{n}(e) ⊑ e it follows that e = h_{n}(e) as desired. □

Notice that condition (2) of the previous lemma makes sense for arbitrary cpo’s (and not only for those satisfying the SFP property).

Definition 8.6 (compact elements) Let A be a cpo. An element e ∈ A is called compact (or finite) iff for every directed subset X of A with e ⊑ ⨆ X there exists already an x ∈ X with e ⊑ x. We write K(A) for the set of compact elements of A. ♢

Lemma 8.7 Let A be a cpo with the property SFP. Then for every a ∈ A the set K_{a} := {e ∈ K(A) | e ⊑ a} is directed and a = ⨆ K_{a}.

Proof. Let (h_{n}) be a chain of finitary projections whose supremum is id_{A} and a ∈ A. First we show that K_{a} is directed. For that purpose suppose that e_{1}, e_{2} ∈ K_{a}. Thus, since {h_{n}(a) | n ∈ ℕ} is directed and has supremum a there exists n_{1}, n_{2} ∈ ℕ with e_{i} ⊑ h_{n_{i}}(a) for i=1, 2. Then for n := max(n_{1}, n_{2}) we have e_{1}, e_{2} ⊑ h_{n}(a). As by Lemma 8.5 we have h_{n}(a) ∈ K(A) it is an element of K_{a} above e_{1} and e_{2}. Thus K_{a} is directed. As {h_{n}(a) | n ∈ ℕ} is a subset of K_{a} and a = ⨆ h_{n}(a) it follows that a = ⨆ K_{a} as desired. □

Next we will show that elements of an SFP predomain A are in 1-1-correspondence with order-theoretic ideals in the poset K(A).

68 Domain-theoretic foundations of functional programming

Theorem 8.8 Let A be an SFP predomain. A subset I of K(A) is called an ideal iff I is downward closed and directed. We write Idl(K(A)) for the poset of ideals in K(A) ordered by ⊆. Then the map

i_{A} : A → Idl(K(A)) : a ↦ K_{a}

is an isomorphism of posets.

Proof. Obviously, the map i_{A} is monotonic. It reflects the order as if K_{a_{1}} ⊆ K_{a_{2}} then a_{1} = ⨆ K_{a_{1}} ⊑ ⨆ K_{a_{2}} = a_{2} by Lemma 8.7. As i_{A} reflects the order it is one-to-one. Thus, it remains to show that i_{A} is surjective. Suppose that I is an ideal in K(A). Let a:= ⨆ I. We show that I = K_{a}. Obviously, we have I ⊆ K_{a}. But if e ∈ K_{a} then (as e is compact) there is an e′ ∈ I with e ⊑ e′ from which it follows that e ∈ I since I is downward closed. □

Next we show that SFP predomains are closed under a lot of useful constructions.

Theorem 8.9 SFP predomains are closed under × and → and for a set S the domain S_{⊥} is SFP iff S is countable.

Proof. Let A and B be SFP predomains. Then there exist ascending chains (h_{n})_{n∈ℕ} and (k_{n})_{n∈ℕ}, respectively, of finitary projections with id_{A}= ⨆_{n∈ℕ} h_{n} and id_{B}= ⨆_{n∈ℕ} k_{n}.

The predomain A×B is SFP as

h_{n}×k_{n} : A×B → A×B : (a, b) ↦ (h_{n}(a), k_{n}(b))

is a finitary projection for all n ∈ ℕ and id_{A×B} = id_{A}×id_{B} = ⨆_{n∈ℕ} h_{n}×k_{n}. The predomain [A→B] is SFP as

h_{n}→k_{n} : [A→B] → [A→B] : f ↦ k_{n} ∘ f ∘ h_{n}

is a finitary projection for all n ∈ ℕ and id_{A→B} = id_{A}→id_{B} = ⨆_{n∈ℕ} h_{n}→k_{n}. That the image of h_{n}→k_{n} is finite follows from the facts that there are just finitely many functions from h_{n}[A] to k_{n}[B] and that k_{n}∘f∘h_{n} is determined uniquely by its restriction to h_{n}[A].

For a set S all elements of S_{⊥} are compact. If S_{⊥} is SFP then S_{⊥} = K(S_{⊥}) is countable and, therefore, the set S itself has to be countable. On the other hand if S is countable then one may enumerate its elements as s_{0}, s_{1}, …, s_{n}, . . .. Define h_{n} as the mapping sending s_{i} with i < n to s_{i} and all other arguments to ⊥. Obviously, the h_{n} form an ascending sequence of finitary projections whose supremum is id_{S_{⊥}}. □

Some Structural Properties of the D_{σ} 69

Thus the D_{σ} and their finite cartesian products are all SFP domains and accordingly determined by their subposets of compact elements as ensured by Theorem 8.8.

It is a straightforward exercise(!) to show that SFP predomains are also closed under (−)_{⊥} (lifting^{2}) and + and that SFP domains are closed under ⊕ (coalesced sum^{3}), ⊗ (smash product^{4}.) and ∘→ (strict function space^{5}).

Next we show that continuous functions from SFP predomains A to arbitray cpo’s B are (by restriction to K(A)) in 1-1-correspondence with the monotonic maps from K(A) to B.

Theorem 8.10 Let A be an SFP predomain and B an arbitrary cpo. Then every continuous map f : A → B is uniquely determined by its restriction to K(A) and every monotonic map h : K(A) → B extends to a continuous map f : A → B, i.e. there is a unique continuous f : A → B with h = f↾K(A).

Proof. Suppose f and g are continuous maps from A to B with f↾K(A) = g↾K(A). We have to show that for an arbitrary a ∈ A it holds that f(a) = g(a). For all e ∈ K_{a} we have f(e) = g(e) since f↾K(A) = g↾K(A) and, therefore, we have f(a) = ⨆_{e∈K_{a}} f(e) = ⨆_{e∈K_{a}} g(e) = g(a) as desired.

Suppose h : K(A) → B is monotonic. Its tentative continuous extension f is defined by putting f(a) = ⨆ h[K_{a}]. Obviously, the map f is monotonic and f(e) = h(e) for compact e in A. For showing that f is also continuous consider a directed set X ⊆ A. As f is monotonic it suffices to show that f(⨆ X) ⊑ ⨆ f(X). From the definition of f we know that f(⨆ X) is the supremum of all h(e) with e compact and e ⊑ ⨆ X. But a compact e is below ⨆ X if and only if e ⊑ x for some x∈X. Thus we get that f(⨆ X) is the supremum of all h(e) where e is compact and e ⊑ x for some x∈X. As this latter supremum is below ⨆ f(X) it follows that f(⨆ X) ⊑ ⨆ f(X) as desired. □

Finally, we introduce the notion of a Scott domain and show that, in particular, all D_{σ} and their finite products are actually Scott domains.

2The “lifting” A_{⊥} of a predomain A is the domain obtained from A by adding a new bottom element.

3A ⊕ B is obtained from the disjoint union A + B by identifying its two minimal elements.

4A ⊗ B is obtained from A × B by identifying all pairs where at least one component equals ⊥

5[A∘→B] is obtained from [A→B] by removing all non-strict maps.

70 Domain-theoretic foundations of functional programming

Definition 8.11 A cpo A has continuous binary infima iff for all x, y ∈ A their infimum x ⊓ y exists and the function

⊓ : A×A → A : (x, y) ↦ x ⊓ y

is Scott continuous. A Scott (pre)domain is an SFP (pre)domain with continuous binary infima. ♢

Obviously, a cpo A has continuous binary infima iff it has binary infima and ⊓ satisfies the following restricted distributivity law, namely

a ⊓ ⨆_{x∈X} x = ⨆_{x∈X} a ⊓ x

for all a ∈ A and all directed X ⊆ A.

For showing that Scott domains are closed under the usual type forming operations we need besides Theorem 8.9 the following lemma.

Lemma 8.12 Cpo’s with continuous binary infima are closed under × and →. Moreover, for all sets S the cpo S_{⊥} has binary continuous infima.

Proof. That S_{⊥} has continuous binary infima is an easy exercise.

Suppose that A and B are cpo’s having continuous binary infima. That A×B has continuous binary infima follows from the fact that

(x_{1}, y_{1}) ⊓ (x_{2}, y_{2}) = (x_{1} ⊓_{A} x_{2}, y_{1} ⊓_{B} y_{2})

and ⊓_{A} and ⊓_{B} are continuous by assumption. That [A→B] has continuous binary infima can be seen as follows. Given f, g ∈ [A→B] the function f ⊓ g = \underline{λ}x:A.f(x) ⊓_{B} g(x) is continuous as ⊓_{B} is continuous and one easily sees that f ⊓ g is the infimum of f and g. That the binary function ⊓ on [A→B] is continuous follows from the fact that it is λ-definable from the continuous function ⊓_{B}. □

Theorem 8.13 Scott domains are closed under × and → and S_{⊥} is a Scott domain for all countable sets S.

Proof. Immediate from Theorem 8.9 and Lemma 8.12. □

Moreover, it is an easy exercise(!) to show that Scott domains are closed under the further domain constructions (−)_{⊥}, separated sum ((−_{1})+ (−_{2}))_{⊥}, ⊕, ⊗ and ∘→.

Notice that our definition of Scott domain is somewhat unorthodox but equivalent to the usual one (as e.g. in [Griffor et.al. 1994]) as shown in the next theorem.

Some Structural Properties of the D_{σ} 71

Theorem 8.14 A cpo D with ⊥ is a Scott domain iff D is

(1) bounded complete, i.e. all bounded subsets of D have a supremum in D, and

(2) countably algebraic, i.e. K(D) is countable and for every d ∈ D the set K_{d} = {e ∈ K(D) | e ⊑ d} is directed and has supremum d.

Proof. Suppose D is a Scott domain. Since D is SFP it is countably algebraic. For showing that D is bounded complete it suffices to show that every finite bounded set of compact elements has a supremum in D.

Suppose e_{1}, …, e_{n} are compact elements of D having a common upper bound b in D. Since D is SFP there exists a finitary projection h : D → D with e_{1}, …, e_{n} ∈ h[D]. Obviously, the elements e_{1}, …, e_{n} are bounded in h[D] by h(b). Thus {e_{1}, …, e_{n}} has a minimal upper bound in h[D] because h[D] is finite. Suppose e′ and e′′ are minimal upper bounds of {e_{1}, …, e_{n}} in h[D]. Then for i ∈ {1, …, n} we have e_{i} = h(e_{i}) ⊑ h(e′ ⊓ e′′) ⊑ e′, e′′ from which it follows that e′ = e′′. Now let e be the supremum of e_{1}, …, e_{n} in h[D]. Suppose d is an upper bound of e_{1}, …, e_{n} in D. Then h(d) is an upper bound of e_{1}, …, e_{n} in h[D] and thus e ⊑ h(d) ⊑ d. Thus e is the supremum of e_{1}, …, e_{n} in D.

Suppose D is bounded complete and countably algebraic. Let {e_{n} | n ∈ ℕ} be an enumeration of K(D). First observe that suprema of bounded finite subsets of K(D) are compact (exercise!). Let D_{n} be the least subset of D which is closed under finite suprema and contains all e_{i} with i < n. Obviously D_{n} is a finite set of compact elements. Let h_{n} : D → D : d ↦ ⨆{e ∈ D_{n} | e ⊑ d}. One easily shows (exercise!) that all h_{n} are finitary projections and id_{D} = ⨆_{n∈ℕ} h_{n} thus exhibiting D as an SFP domain.

It remains to show that D has binary continuous infima. Suppose x, y ∈ D. Then the set {z ∈ D | z ⊑ x, y} is bounded and thus has a supremum giving rise to x ⊓ y. For showing continuity of ⊓ : D × D → D suppose that X ⊆ D is directed and y ∈ D. Obviously, we have y ⊓ x ⊑ y ⊓ ⨆ X for all x ∈ X and thus ⨆_{x∈X} y ⊓ x ⊑ y ⊓ ⨆ X. For the reverse direction suppose e ∈ K(D) with e ⊑ y ⊓ ⨆ X. Then e ⊑ y and e ⊑ ⨆ X. Since e is compact there exists x ∈ X with e ⊑ x. Thus, we have e ⊑ y ⊓ x ⊑ ⨆_{x∈X} y ⊓ x. Since this implication holds for all e ∈ K(D) and D is countably algebraic we conclude that y ⊓ ⨆ X ⊑ ⨆_{x∈X} y ⊓ x as desired. □

Notice that the above proof shows in particular that in algebraic domains binary infima are continuous provided they always exist.

72 Domain-theoretic foundations of functional programming

The motivation for our definition of Scott domain is that it appears as the most natural one when starting to investigate the structure of the domains arising in the Scott model of PCF. The usual definition, however, is motivated by weakening the most respectable notion of a “countably algebraic lattice”, i.e. a complete lattice satisfying condition (2). As one wants to get rid of the annoying ⊤ element which does not have a computational meaning it appears as most natural to weaken completeness by requiring (besides directed completeness) the existence of suprema just for bounded sets and not for arbitrary subsets.

Notice, however, that the class of Scott domains is a bit wider than actually needed because all domains showing up in Scott semantics of programming languages actually satisfy the following stronger requirement.

Definition 8.15 A cpo A is called coherently complete iff all coherent subsets X of A have a supremum in A where a subset X of A is called coherent iff all x, y ∈ X have an upper bound in A. ♢

The reader is invited to show that all D_{σ} are coherently complete. Actually, one can show that coherently complete domains are closed under all the usual domain constructions.^{6}

An aesthetically pleasing aspect of coherently complete domains is that they can be characterised as those partial orders where every coherent subset has a supremum (because every directed set is coherent).

6One exception is the so-called Smyth powerdomain. However, Scott domains are not closed under the Plotkin powerdomain construction whereas SFP domains are closed under this latter construction and were introduced by G. Plotkin (see [Plotkin 1978])

precisely for this purpose. Thus, if one wants to have closure under (all sorts of) powerdomains then one should work with SFP domains and otherwise coherently complete SFP domains are absolutely sufficient.

Chapter 9

Solutions of Recursive Domain Equations

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 defined type A. Typical examples of such domain equations are

N = 1_{⊥} ⊕ N  S = A ⊗ S_{⊥}  D = N ⊕ [D→D]_{⊥}  C = R^{C}×C

where (−)_{⊥} stands for lifting, ⊕ for coalesced sum and ⊗ for the so-called “smash product”^{1}. Although we use the symbol = in domain equations we rather mean ≅, i.e. that the domain on the left hand side should be isomorphic to the domain on the right hand side of the domain equation. The intended solution for the domain equation for N is ℕ_{⊥}. If A is a flat domain M_{⊥} (where M is a set of “tokens”) then the intended solution for the domain equation for S is the domain of “streams over M, i.e. the finite and infinite sequences of elements of M under the prefix-ordering. The intended solution of the domain equation for D is not so easy to describe but the intention is that the elements of D different from ⊥_{D} are either natural numbers or continuous functions from D to D (where ⊥_{D} is distinguished from the function \underline{λ}d:D.⊥_{D}). Solutions of C = R^{C}×C are also not so easy to visualize or describe in a concrete way but notice that for any such C we have that R^{C} ≅ R^{R^{C}×C} ≅ (R^{C})^{(R^{C})}, i.e. we get a nontrivial solution of the domain equation D = D^{D} when R is nontrivial.

The general form of a domain equation is D = F (D, D) where F is a locally continuous functor from C^{op}×C to C and C is the category of domains and strict functions. Here “locally continuous” means that the function

1If A and B are domains then their smash product A ⊗ B consists of all pairs (a, b) ∈ A×B with a=⊥ ∨ b=⊥ ⇒ a=⊥=b and the order on A⊗B is inherited from A×B.

74 Domain-theoretic foundations of functional programming

F : C(Y_{2}, Y_{1}) × C(X_{1}, X_{2}) → C(F (Y_{1}, X_{1}), F (Y_{2}, X_{2})) is Scott continuous for all objects X_{1}, X_{2}, Y_{1}, Y_{2} in C. This assumption is guaranteed when the right hand side of a domain equation is built up from 1 (containing just ⊥) by the functors (−)_{⊥} (lifting), × (cartesian product), ⊗ (smash product), + (separated sum), ⊕ (coalesced sum), → (function space) and ∘→ (strict function space) where only the last two make proper use of their contravariant argument.

Definition 9.1 Let F : C^{op} × C → C be a locally continuous functor. A bifree solution of X = F (X, X) is a domain D together with an isomorphism α : F (D, D) → D such that every strict e : D → D with e = α∘F (e, e)∘α^{−1} is equal to id_{D}. ♢

We show now that bifree solutions are unique up to isomorphism.

Lemma 9.2 Let F : C^{op} × C → C be a locally continuous functor. If α : F (A, A) → A and β : F (B, B) → B are bifree solutions of the domain equation X = F (X, X) then there exists a unique isomorphism i : A → B with i = β ∘ F (i^{−1}, i) ∘ α^{−1}.

Proof. Let (i : A → B, j : B → A) be the least solution of the equations

i = β ∘ F (j, i) ∘ α^{−1} j = α ∘ F (i, j) ∘ β^{−1}

which exists as the assignment (i, j) ↦ (β ∘ F (j, i) ∘ α^{−1}, α ∘ F (i, j) ∘ β^{−1}) gives rise to a continuous function φ = ⟨φ_{1}, φ_{2}⟩ : C(A, B) × C(B, A) → C(A, B) × C(B, A). But then we have

j ∘ i = α ∘ F (j ∘ i, j ∘ i) ∘ α^{−1} i ∘ j = β ∘ F (i ∘ j, i ∘ j) ∘ β^{−1}

from which it follows that j ∘ i = id_{A} and i ∘ j = id_{B} as both α and β are bifree solutions by assumption. Thus, the map j equals i^{−1} from which it follows that i = β ∘ F (i^{−1}, i) ∘ α^{−1} as desired.

Let ι : A → B be some isomorphism with ι = β ∘ F (ι^{−1}, ι) ∘ α^{−1}. We want to show that ι = i and ι^{−1} = j where i and j are defined as above. For this purpose consider the continuous function δ : C(A, A) → C(A, A) : e ↦ α ∘ F (e, e) ∘ α^{−1}. We write e_{n} for δ^{n}(⊥). As α is bifree we have id_{A} = ⨆_{n∈ℕ} e_{n}. We will show now by induction on n that

(ι ∘ e_{n}, e_{n} ∘ ι^{−1}) = φ^{n}(⊥, ⊥)

from which it follows that (ι, ι^{−1}) = (i, j). For n=0 we have (ι∘e_{0}, e_{0}∘ι^{−1}) = (⊥, ⊥) since ι∘⊥ = ⊥ and ⊥∘ι^{−1} = ⊥. Now suppose as induction hypothesis that (ι ∘ e_{n}, e_{n} ∘ ι^{−1}) = φ^{n}(⊥, ⊥). Then

Solutions of Recursive Domain Equations 75

ι ∘ e_{n+1} = β ∘ F (ι^{−1}, ι) ∘ α^{−1} ∘ α ∘ F (e_{n}, e_{n}) ∘ α^{−1} =
= β ∘ F (e_{n} ∘ ι^{−1}, ι ∘ e_{n}) ∘ α^{−1} = φ_{1}(φ^{n}(⊥, ⊥))

where the last equality follows from the induction hypothesis and

e_{n+1} ∘ ι^{−1} = α ∘ F (e_{n}, e_{n}) ∘ α^{−1} ∘ α ∘ F (ι, ι^{−1}) ∘ β^{−1} =
= α ∘ F (ι ∘ e_{n}, e_{n} ∘ ι^{−1}) ∘ β^{−1} = φ_{2}(φ^{n}(⊥, ⊥))

where the last equality follows from the induction hypothesis. Thus, we have

(ι ∘ e_{n+1}, e_{n+1} ∘ ι^{−1}) = ⟨φ_{1}(φ^{n}(⊥, ⊥)), φ_{2}(φ^{n}(⊥, ⊥))⟩ = φ^{n+1}(⊥, ⊥)

as desired. □

Now we will show that for every locally continuous functor F : C^{op}×C → C there exists a bifree solution of the domain equation X = F (X, X) which we know to be unique up to isomorphism by the previous Lemma 9.2. However, for this purpose we need some preparatory notions and lemmas.

Definition 9.3 An embedding/projection pair from A to B is a pair (e, p) where e : A → B and p : B → A are continuous functions with p ∘ e = id_{A} and e ∘ p ⊑ id_{B}. We call e embedding and p projection. ♢

One easily sees that for an embedding/projection pair (e, p) from A to B we have e(a) ⊑ b ⇔ a ⊑ p(b) for all a ∈ A and b ∈ B from which it follows that p(b) is the greatest a with e(a) ⊑ b. We leave it as an exercise(!) to show that embeddings and projections are always strict.

Next we show that one component of an embedding/projection pair determines the other one uniquely.

Lemma 9.4 Let (e, p) and (e′, p′) be embedding projection pairs from A to B. Then (e, p) = (e′, p′) whenever e = e′ or p = p′.

Proof. If e = e′ then we have p = p′ ∘ e ∘ p ⊑ p′ and similarly p′ ⊑ p from which it follows that p = p′. If p = p′ then e = e ∘ p ∘ e′ ⊑ e′ and similarly e′ ⊑ e from which it follows that e = e′. □

Accordingly, we say that a map e is an embedding iff there is a map p such that (e, p) is an embedding/projection pair and that a map p is a projection iff there is a map e such that (e, p) is an embedding/projection pair.

76 Domain-theoretic foundations of functional programming

Canonical solutions of domain equations will be constructed as inverse limits of projections. The notion of inverse limit will be explained in the next theorem.

Theorem 9.5 Let (f_{n} : D_{n+1} → D_{n} | n ∈ ℕ) be a sequence of maps in C. Its inverse limit is given by the sequence q_{n} : D → D_{n} where

|D| = { d ∈ ∏_{n∈ℕ} D_{n} | ∀n ∈ ℕ. d_{n} = f_{n}(d_{n+1}) }

and d ⊑_{D} d′ iff ∀n∈ℕ. d_{n} ⊑ d′_{n} and q_{n} : D → D_{n} : d ↦ d_{n}, i.e. q_{n} projects on the n-th component. Notice that q_{n} = f_{n} ∘ q_{n+1} for all n ∈ ℕ.

The inverse limit satisfies the universal property that for all sequences (g_{n} : E → D_{n} | n ∈ ℕ) with g_{n} = f_{n} ∘ g_{n+1} for all n ∈ ℕ there exists a unique map h : E → D with g_{n} = q_{n} ∘ h for all n ∈ ℕ.

Proof. Directed suprema in D = (|D|, ⊑_{D}) are computed pointwise which does not lead out of D as the f_{n} preserve directed suprema. As suprema in D are computed pointwise it readily follows that the q_{n} preserve them. For d ∈ D we have f_{n}(q_{n+1}(d)) = f_{n}(d_{n+1}) = d_{n} = q_{n}(d) where the penultimate equality holds as d ∈ |D|.

For showing that D satisfies the universal property suppose that (g_{n} : E → D_{n} | n ∈ ℕ) with g_{n} = f_{n} ∘ g_{n+1} for all n ∈ ℕ. The map h : E → D with g_{n} = q_{n} ∘ h for all n ∈ ℕ is uniquely determined by this property, i.e. we have h(y) = (g_{n}(y))_{n∈ℕ}. That this h is Scott continuous follows from the fact that suprema in D are computed pointwise and the assumption that the g_{n} are all Scott continuous. □

Notice that the universal property of inverse limits determines them uniquely up to isomorphism. If we take inverse limits of sequences consisting of projections we can characterise their inverse limit (up to isomorphism) in a purely local way as follows.

Theorem 9.6 Let (p_{n} : D_{n+1} → D_{n} | n ∈ ℕ) be a sequence of projections. We write e_{n} for the embeddings associated uniquely with the p_{n}. Then the q_{n} of the inverse limit are all projections whose associated embeddings i_{n} : D_{n} → D can be defined explicitly as follows

i_{n}(x)_{m} = \{ \begin{matrix}(e_{m−1} ∘ ⋯ ∘ e_{n})(x) & if n ≤ m \\ (p_{m} ∘ ⋯ ∘ p_{n−1})(x) & otherwise. \end{matrix}

Solutions of Recursive Domain Equations 77

Moreover, we have

(‡)  ⨆_{n∈ℕ} i_{n} ∘ q_{n} = id_{D}

and this property together with the requirement q_{n} = p_{n} ∘q_{n+1} characterises inverse limits up to isomorphism.

Proof. Straightforward computation checks that the i_{n} are continuous strict maps from D_{n} to D and that the (i_{n}, q_{n}) are embedding/projection pairs. Moreover, one easily sees that i_{n+1} ∘ e_{n} = i_{n} for all n ∈ ℕ. Thus, we have

i_{n+1} ∘ q_{n+1} ⊒ i_{n+1} ∘ e_{n} ∘ p_{n} ∘ q_{n+1} = i_{n} ∘ q_{n}

i.e. that the sequence i_{n} ∘ q_{n} is ascending in [D→D]. As

q_{n} ∘ ⨆_{k∈ℕ} i_{k} ∘ q_{k} = ⨆_{k∈ℕ} q_{n} ∘ i_{k} ∘ q_{k} = ⨆_{k≥n} q_{n} ∘ i_{k} ∘ q_{k} = ⨆_{k≥n} q_{n} = q_{n} = q_{n} ∘ id_{D}

it follows from the universal property of (q_{n})_{n∈ℕ} that (‡) holds.

On the other hand suppose that we have a sequence of embedding/projection pairs (i′_{n}, q′_{n}) from D_{n} to D′ with q′_{n} = p_{n} ∘ q′_{n+1} and ⨆_{n∈ℕ} i′_{n} ∘ q′_{n} = id_{D′}. By the universal property of the inverse limit (q_{n})_{n∈ℕ} there is a unique map ι : D′ → D with q′_{n} = q_{n} ∘ ι. We show now that this ι is an isomorphism by constructing its (tentative) inverse as

ι^{−1} = ⨆_{n∈ℕ} i′_{n} ∘ q_{n} .

First notice that from q′_{n} = p_{n} ∘ q′_{n+1} it follows by Lemma 9.4 that i′_{n} = i′_{n+1} ∘ e_{n} from which it follows that the sequence (i′_{n} ∘ q_{n})_{n∈ℕ} is ascending and, therefore, the map ι^{−1} is well defined. That ι^{−1} ∘ ι = id_{D′} can be seen as follows

ι^{−1} ∘ ι = ( ⨆_{n∈ℕ} i′_{n} ∘ q_{n}) ∘ ι = ⨆_{n∈ℕ} i′_{n} ∘ q_{n} ∘ ι = ⨆_{n∈ℕ} i′_{n} ∘ q′_{n} = id_{D′} .

For showing that ι ∘ ι^{−1} = id_{D} we first observe that

(∗) q′_{n} ∘ i′_{n+k} ∘ q_{n+k} = q_{n}

for all k, n ∈ ℕ which can be seen as follows. For k=0 claim (∗) is obvious as q′_{n} ∘i′_{n} = id_{D_{n}}. Suppose now as induction hypothesis that q′_{n} ∘i′_{n+k} ∘q_{n+k} = q_{n} for all n ∈ ℕ. Now for arbitrary n ∈ ℕ it follows from the induction

78 Domain-theoretic foundations of functional programming

hypothesis that q′_{n+1} ∘ i′_{n+1+k} ∘ q_{n+1+k} = q_{n+1}. Thus, by postcomposition with p_{n} we get

q′_{n} ∘ i′_{n+k+1} ∘ q_{n+k+1} = p_{n} ∘ q′_{n+1} ∘ i′_{n+1+k} ∘ q_{n+1+k} = p_{n} ∘ q_{n+1} = q_{n}

as desired. Now from (∗) it follows that

q_{n}∘ι∘ι^{−1} = q′_{n}∘ ⨆_{k∈ℕ} i′_{k}∘q_{k} = ⨆_{k∈ℕ} q′_{n}∘i′_{k}∘q_{k} = ⨆_{k≥n} q′_{n}∘i′_{k}∘q_{k} = ⨆_{k≥n} q_{n} = q_{n}∘id_{D}

which by the universal property of (q_{n})_{n∈ℕ} implies ι ∘ ι^{−1} = id_{D}.

Thus, we have shown that ι^{−1} is actually the inverse of ι. We have q_{n} ∘ ι = q′_{n} by definition of ι and, therefore, also q_{n} = q′_{n} ∘ ι^{−1}. Thus, the cone (q′_{n})_{n∈ℕ} is isomorphic to the limiting cone (q_{n})_{n∈ℕ} via the isomorphism ι as desired. □

Now we can construct bifree solutions of domain equations X = F (X, X) for arbitrary locally continuous functors F : C^{op} × C → C.

Theorem 9.7 Let F : C^{op} × C → C be a locally continuous functor. Consider the sequence of embedding/projection pairs (e_{n}, p_{n}) from D_{n} to D_{n+1} defined recursively as follows

D_{0} = 1 = {⊥} D_{n+1} = F (D_{n}, D_{n})
e_{0} = ⊥ : D_{0}→D_{1} e_{n+1} = F (p_{n}, e_{n}) : D_{n+1}→D_{n+2}
p_{0} = ⊥ : D_{1}→D_{0} p_{n+1} = F (e_{n}, p_{n}) : D_{n+2}→D_{n+1}

and let (i_{n}, q_{n}) be the inverse limit for the sequence (e_{n}, p_{n}). Then α = ⨆_{n∈ℕ} i_{n+1} ∘ F (i_{n}, q_{n}) : F (D, D) → D is a bifree solution of the domain equation X = F (X, X). The inverse of α is given by ⨆_{n∈ℕ} F (q_{n}, i_{n})∘q_{n+1}.

Proof. Straighforward induction (using monotonicity of the morphism part of F) shows that the (e_{n}, p_{n}) are actually embedding/projection pairs. By Theorem 9.6 the sequence i_{n} ∘ q_{n} is ascending and has supremum id_{D}. From this it follows (again by local monotonicity and continuity of F) that the sequence F (q_{n}, i_{n}) ∘ F (i_{n}, q_{n}) is ascending and has supremum id_{F (D,D)}. Thus, by Theorem 9.6 we know that both (q_{n+1})_{n∈ℕ} and (F (i_{n}, q_{n}))_{n∈ℕ} are limiting cones for the diagram (p_{n+1})_{n∈ℕ}. From Theorem 9.6 we know that the unique map α : F (D, D) → D with q_{n+1} ∘ α = F (i_{n}, q_{n}) is an isomorphism. That α^{−1} = ⨆_{n∈ℕ} F (q_{n}, i_{n}) ∘ q_{n+1} follows from inspection of the proof of Theorem 9.6 (namely the construction of ι^{−1} in this proof). Similarly it follows that α = ⨆_{n∈ℕ} i_{n+1} ∘ F (i_{n}, q_{n}) since α is the inverse of

Solutions of Recursive Domain Equations 79

α^{−1} which is the mediating arrow from the limiting cone (q_{n+1})_{n∈ℕ} to the limiting cone (F (i_{n}, q_{n}))_{n∈ℕ}.

Thus, for bifreeness it remains to show that every e : D ∘→ D with e = δ(e) := α ∘ F (e, e) ∘ α^{−1} is actually equal to id_{D}. We show that

q_{n} ∘ e = q_{n}  and  e ∘ i_{n} = i_{n}

for all n ∈ ℕ by induction on n from which it follows by the universal property of the limiting cone (q_{n})_{n∈ℕ} that e = id_{D}. For n=0 we have q_{n} ∘ e = q_{n} as all maps from D to 1 = D_{0} are equal and e ∘ i_{n} = i_{n} as all strict maps from 1 to D are equal. Suppose as induction hypothesis that q_{n} ∘ e = q_{n} and e ∘ i_{n} = i_{n}. Then using the induction hypothesis we have

q_{n+1} ∘ e = q_{n+1} ∘ α ∘ F (e, e) ∘ α^{−1} = F (i_{n}, q_{n}) ∘ F (e, e) ∘ α^{−1}
= F (e ∘ i_{n}, q_{n} ∘ e) ∘ α^{−1} = F (i_{n}, q_{n}) ∘ α^{−1} =
= q_{n+1}

and

e ∘ i_{n+1} = α ∘ F (e, e) ∘ α^{−1} ∘ i_{n+1} = α ∘ F (e, e) ∘ F (q_{n}, i_{n}) =
= α ∘ F (q_{n} ∘ e, e ∘ i_{n}) = α ∘ F (q_{n}, i_{n}) =
= i_{n+1}

proving the induction step. □

Having shown that canonical solutions which are unique up to isomorphism do exist we now give an alternative characterisation of them.

Theorem 9.8 Let F : C^{op} × C → C be a locally continuous functor. Then α : F (A, A) → A is a bifree solution of the domain equation X = F (X, X) if and only if for all morphisms f : F (C, B) → B and g : C → F (B, C) in C there exist unique morphisms h : A → B and k : C → A in C making the diagrams

[figure: F (C, B); f; B; F (B, C); g; C; F (A, A); F (k, h); α^{−1}; A; h; F (A, A); F (h, k); α; A; k]

commute.

80 Domain-theoretic foundations of functional programming

Proof. We first show the implication from right to left. Instantiating B and C by A and f by α and g by α^{−1} we get that from e = α ∘F (e, e)∘α^{−1} it follows that e = id_{A} as both h = id_{A} = k and h = e = k make the above diagrams commute and the choice of h and k is unique by assumption.

For the reverse direction assume that α is a bifree solution and that the two diagrams commute. We show that h and k are actually the least (simultaneous) solutions of the equations

h = f ∘ F (k, h) ∘ α^{−1}  and  k = α ∘ F (h, k) ∘ g .

The least solution of this system of equations is given by ⨆_{n∈ℕ} h_{n} and ⨆_{n∈ℕ} k_{n}, respectively, where the h_{n} and k_{n} are defined recursively as follows

h_{0} = ⊥ : A → B h_{n+1} = f ∘ F (k_{n}, h_{n}) ∘ α^{−1}
k_{0} = ⊥ : C → A k_{n+1} = α ∘ F (h_{n}, k_{n}) ∘ g.

As α is a bifree solution we also have id_{A} = ⨆_{n∈ℕ} e_{n} where

e_{0} = ⊥ : A → A e_{n+1} = α ∘ F (e_{n}, e_{n}) ∘ α^{−1} .

We show now by induction on n that

h_{n} = h ∘ e_{n}  and  k_{n} = e_{n} ∘ k

from which it follows that

h = h ∘ id_{A} = h ∘ ⨆_{n∈ℕ} e_{n} = ⨆_{n∈ℕ} h ∘ e_{n} = ⨆_{n∈ℕ} h_{n}

and

k = id_{A} ∘ k = ( ⨆_{n∈ℕ} e_{n}) ∘ k = ⨆_{n∈ℕ} e_{n} ∘ k = ⨆_{n∈ℕ} k_{n}

i.e., that the pair (h, k) is the least solution of the equations

h = f ∘ F (k, h) ∘ α^{−1}  and  k = α ∘ F (k, h) ∘ g .

For n=0 the claim holds as ⊥ = h∘⊥ because h is strict and ⊥ = ⊥∘k holds anyway. Suppose as induction hypothesis that h_{n} = h ∘ e_{n} and k_{n} = e_{n} ∘ k. Then we have

h ∘ e_{n+1} = f ∘ F (k, h) ∘ α^{−1} ∘ α ∘ F (e_{n}, e_{n}) ∘ α^{−1} =
= f ∘ F (k, h) ∘ F (e_{n}, e_{n}) ∘ α^{−1} =
= f ∘ F (e_{n} ∘ k, h ∘ e_{n}) ∘ α^{−1} = f ∘ F (k_{n}, h_{n}) ∘ α^{−1} =

Solutions of Recursive Domain Equations 81

= h_{n+1}

and

e_{n+1} ∘ k = α ∘ F (e_{n}, e_{n}) ∘ α^{−1} ∘ α ∘ F (h, k) ∘ g =
= α ∘ F (e_{n}, e_{n}) ∘ F (h, k) ∘ g =
= α ∘ F (h ∘ e_{n}, e_{n} ∘ k) ∘ g = α ∘ F (k_{n}, h_{n}) ∘ g =
= k_{n+1}

as desired. □

Notice that in the above proof we have used intrinsically that h is strict. There may arise the question why it is essential to restrict attention to C, i.e. to strict continuous maps. This will get clear from the following theorem where one considers the particular case of mixed variant functors induced by locally continuous covariant endofunctors on C which are also practically most important.

Theorem 9.9 Let T : C → C be a locally continuous covariant functor. Let F_{T} : C^{op} × C → C be the locally continuous mixed variant functor defined from T by putting F_{T} (Y, X) = T (X) and F_{T} (g, f) = T (f). Then an isomorphism α : T (A) → A is a bifree solution of the domain equation X = F_{T} (X, X) = T (X) iff one of the following three equivalent conditions is satisfied

(1) if e : A ∘→ A with e = α ∘ T (e) ∘ α^{−1} then e = id_{A}

(2) for every f : T (B) ∘→ B there exists a unique map h : A ∘→ B with h = f ∘ T (h) ∘ α^{−1}, i.e.

[figure: T (B); f; B; T (A); T (h); α; A; h]

since α is an isomorphism.

(3) for every g : B ∘→ T (B) there exists a unique map k : B ∘→ A with

82 Domain-theoretic foundations of functional programming

k = α ∘ T (k) ∘ g, i.e.

[figure: B; g; T (B); A; k; α^{−1}; T (A); T (k)]

since α is an isomorphism.

Proof. Obviously, condition (1) is equivalent to α being a bifree solution of X = F_{T} (X, X). By Theorem 9.8 condition (1) implies conditions (2) and (3). But each of the conditions (2) and (3) entails condition (1) instantiating f and g by α and α^{−1}, respectively. □

If we allowed in C also non-strict continuous maps as morphisms then condition (2) of Theorem 9.9 would not be satisfied anymore for bifree solutions of the domain equation X = X for the following reason. Obviously, the isomorphism id_{1} where 1 = {⊥} is a bifree solution for X = Id_{C}(X) where Id_{C} is the identity functor on C. But now for every domain A and continuous a : 1 → A we have

[figure: A; id_{A}; A; 1; a; id_{1}; 1; a]

but if we do not require a to be strict there are as many a as there are elements of A. Thus, for A with more than one element condition (2) of Theorem 9.9 were violated if we allowed non-strict maps in C.

We conclude this chapter by observing that condition (2) of Theorem 9.9 gives rise to an induction principle for recursive types A = T (A) where T : C → C is locally continuous. Suppose that P ⊆ A is closed under directed suprema and contains ⊥. Let us write i for the inclusion from P into A. If there exists a map π : T (P) → P with

[figure: T (A); α; A; T (P); T (i); π; P; i_{∪}]

Solutions of Recursive Domain Equations 83

then one easily shows (exercise!) that i is an isomorphism whose inverse is given by the unique j : A → P with π ∘ T (j) = j ∘ α (using condition (2) of Theorem 9.9). Thus, the map i is surjective and P = A. We leave it as an exercise(!) for the inclined reader to show that admissibility of P ⊆ A and ⊥ ∈ P are necessary assumptions for this induction principle.

Alas, for general mixed variant locally continuous F : C^{op}×C → C such an induction principle is not available. The best we can get is the following. Let α : F (A, A) → A be a bifree solution and P ⊆ A be closed under directed suprema and ⊥ ∈ P. Then a ∈ P iff ∀n∈ℕ.δ^{n}(⊥)(a) ∈ P where δ : C(A, A) → C(A, A) : e ↦ α ∘ F (e, e) ∘ α^{−1}. We leave the verification of this claim to the inclined reader.

Models of Untyped λ-Calculus

Historically, the first domain equation ever considered was D = [D→D]. It was solved by Dana Scott in fall 1969 with the intention of finding mathematical models for untyped λ-calculus where every term can be used as a function. Up to that time there were not known any set-theoretic models of the untyped λ-calculus. The reason was that for every set S containing more than one element the set S^{S} of endofunctions on S has greater cardinality than S itself because of |S| < |P(S)| ≤ |S^{S}| already known to Cantor. The ingenious idea of Scott was to take instead of a set S a domain D and consider instead of all endofunctions on D just the continuous ones!

Obviously, the bifree solution of D = [D→D] is trivial, i.e. the trivial domain 1 = {⊥}. To obtain a non-trivial solution D. Scott started with an arbitrary^{2} domain R, considered the following sequence of embedding/projection pairs

R_{0} = R R_{n+1} = [R_{n}→R_{n}]
e_{0} = R_{0}→R_{1} : r ↦ λx.r e_{n+1} = [p_{n}→e_{n}]
p_{0} : R_{1}→R_{0} : f ↦ f(⊥) p_{n+1} = [e_{n}→p_{n}]

and showed (as in our Theorem 9.7) that its inverse limit R_{∞} is isomorphic to [R_{∞}→R_{∞}]. Notice, however, that one may show (exercise!) that—as first observed in [Riecke and Sandholm 2002]—the domain R_{∞} is isomorphic to [C→R] where C is the bifree solution of C = [C→R]×C rendering the consideration of non-bifree solutions unnecessary.

2Actually, he used the more common complete lattices instead but, nevertheless, Scott continuous maps as morphisms between them!

84 Domain-theoretic foundations of functional programming

A more liberal notion of model for untyped λ-calculus is the following: a domain D such that [D→D] is a retract of D, i.e. there exist continuous maps s : [D→D] → D and p : D → [D→D] with p ∘ s = id_{[D→D]}. An example for this is the lattice P(ℕ) which contains [P(ℕ)→P(ℕ)] as a retract in the following way. Let e : ℕ → P_{fin}(ℕ) be a primitive recursive bijection^{3} between natural numbers and finite subsets of them such that the relation m ∈ e_{n} is decidable. Then define p : P(ℕ) → [P(ℕ)→P(ℕ)] as p(A)(B) = {n ∈ ℕ | ⟨m, n⟩ ∈ A and e_{m} ⊆ B} and s(f) = {⟨m, n⟩ | n ∈ f(e_{m})}. One easily checks that p∘s = id_{[P(ℕ)→P(ℕ)]} and s∘p∘s∘p = s∘p ⊒ id_{P(ℕ)}. Notice that for arbitrary infinite sets S one can organize P(S) into a model of λ-calculus exploiting the fact that S ≅ P_{fin}(S)×S for all infinite sets S.

Notice, however, that models of the form P(S) (usually called graph models) do not model η-equality as [[λy. x(y)]]ρ = s(p(ρ(x))) whereas [[x]]ρ = ρ(x) and s ∘ p ≠ id_{P(ℕ)}. The latter can be seen by considering the set I = {⟨2^{n}, n⟩ | n ∈ ℕ} for which we have s(p(I)) = {⟨m, n⟩ | n ∈ e_{m}} strictly bigger than I.

For an in-depth investigation of these models see e.g. the encyclopedic book [Barendregt 1981] by H. Barendregt.

3e.g. by putting e(n) = A iff n = ∑_{i∈A} 2^{i}

Chapter 10

Characterisation of Fully Abstract Models

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

Definition 10.1 A domain-enriched category C is given by

(1) a collection |C| of objects

(2) for all A, B ∈ |C| a domain C(A, B) whose least element is denoted by ⊥_{A,B}

(3) a Scott continuous function ∘_{A,B,C} : C(B, C) × C(A, B) → C(A, C) for all objects A, B, C ∈ |C|

(4) a morphism id_{A} ∈ C(A, A) for every object A ∈ |C|

such that

(Assoc) h ∘ (g ∘ f) = (h ∘ g) ∘ f
(Neutr) id ∘ f = f = f ∘ id

whenever both sides of the equations are defined. ♢

Subsequently we often write f : A → B for f ∈ C(A, B).

Definition 10.2 (Λ-category) A cartesian closed domain-enriched category (or Λ-category) is a domainenriched category C with

(1) an object 1 ∈ |C| such that for all A ∈ |C| there is a unique f ∈ C(A, 1), namely ⊥_{A,1}

(2) for all A, B ∈ |C| a distinguished object A×B ∈ |C| and distinguished maps π_{1}^{A,B} ∈ C(A×B, A) and π_{2}^{A,B} ∈ C(A×B, B) such that for all maps f ∈ C(C, A) and g ∈ C(C, B) there exists a unique map h ∈ C(C, A×B)

86 Domain-theoretic foundations of functional programming

with π_{1}^{A,B} ∘ h = f and π_{2}^{A,B} ∘ h = g which is denoted by ⟨f, g⟩ Notation If f ∈ C(C, A) and g ∈ C(D, B) then we write f×g as an abbreviation for ⟨f ∘ π_{1}^{C,D}, g ∘ π_{2}^{C,D}⟩.

(3) for all A, B ∈ |C| a distinguished object [A→B] ∈ |C| and a distinguished map ev_{A,B} ∈ C([A→B]×A, B]) such that for all f ∈ C(C×A, B) there is a unique map g ∈ C(C, [A→B]) with ev_{A,B} ∘ (g×id_{A}) = f for which we write Λ_{A,B,C}(f) or simply Λ(f)

such that

(i) ⟨f, g⟩ ⊑ ⟨f′, g′⟩ whenever f ⊑ f′ and g ⊑ g′ (ii) Λ(f) ⊑ Λ(g) whenever f ⊑ g (iii) ⊥ ∘ f = ⊥ (iv) ev ∘ ⟨⊥, a⟩ = ⊥

where the last two equations are required to hold whenever both sides of the equation are defined. ♢

It follows from the above axioms that for all objects A, B and C the mappings

⟨−, −⟩ : C(C, A) × C(C, B) → C(C, A×B)

and

Λ : C(C×A, B) → C(C, [A→B])

are order isomorphisms and thus continuous. Their inverses are given by the assignments h ↦ (π_{1}∘h, π_{2}∘h) and g ↦ ev ∘ (g×id_{A}), respectively.

Next we show that in Λ-categories one has least fixpoint operators.

Lemma 10.3 Let C be a Λ-category and A ∈ |C|. Then there exists a least morphism fix_{A} ∈ C([A→A], A) with ev ∘ ⟨id_{[A→A]}, fix_{A}⟩ = fix_{A}.

Proof. For A ∈ |C| the function

F_{A} : C([A→A], A) → C([A→A], A) : h ↦ ev ∘ ⟨id_{[A→A]}, h⟩

is Scott continuous due to the properties required for a Λ-category. Thus, the mapping F_{A} has a least fixpoint fix_{A} = ⨆_{n∈ℕ} F_{A}^{n}(⊥_{[A→A],A}). □

Using the fix of the previous lemma one can construct least fixpoints in the following way.

Characterisation of Fully Abstract Models 87

Theorem 10.4 Let C be a Λ-category and f ∈ C(C, [A→A]). Then fix_{A}∘f is the least morphism a ∈ C(C, A) satisfying

a = ev ∘ ⟨f, a⟩

where fix_{A} is as in Lemma 10.3.

Proof. Obviously, for f : C → [A→A] we have

fix_{A} ∘ f = ev ∘ ⟨id_{[A→A]}, fix_{A}⟩ ∘ f = ev ∘ ⟨id_{[A→A]}∘f, fix_{A}∘f⟩ = ev ∘ ⟨f, fix_{A}∘f⟩

due to the defining equation for fix_{A}. Now if a : C → A satisfies the inequality ev∘⟨f, a⟩ ⊑ a then it follows by fixpoint induction that fix_{A}∘f ⊑ a because

⊥_{[A→A],A} ∘ f = ⊥_{C,A} ⊑ a

and

F_{A}(h) ∘ f = ev ∘ ⟨id_{[A→A]}, h⟩ ∘ f = ev ∘ ⟨f, h∘f⟩ ⊑ ev ∘ ⟨f, a⟩ ⊑ a

whenever h ∘ f ⊑ a. □

As C(A, A) ≅ C(1×A, A) ≅ C(1, [A→A]) by f ↦ f ∘ π_{2}^{1,A} ↦ Λ(f∘π_{2}^{1,A}) =: ^{⌜}f^{⌝} one easily shows (exercise!) that fix_{A} ∘ ^{⌜}f^{⌝} : 1 → A is the least a : 1 → A with a = f ∘ a.

From the above considerations it appears that a Λ-category is endowed with enough structure to interpret typed λ-calculus with fixpoint operators at all types. For interpreting full PCF one just needs an object N together with appropriate morphisms zero : 1 → N, succ, pred : N → N and ifz : N×N×N → N for interpreting base type nat and the basic operations on it. In order to formulate the necessary requirements we need some notation introduced in the next definition.

Definition 10.5 Let C be a Λ-category. For A ∈ |C| we write Γ(A) as an abbreviation for the domain C(1, A) and for morphisms f : A → B in C we write Γ(f) for the continuous map Γ(A) → Γ(B) : a ↦ f ∘ a. ♢

The elements of Γ(A) are often referred to as “global elements of A”.

Definition 10.6 (N-structure) An N-structure or natural numbers structure in a Λ-category is given by

• an object N ∈ |C|

• zero ∈ C(1, N)

88 Domain-theoretic foundations of functional programming

• succ, pred : N → N

• ifz : N×N×N → N

such that the map i_{N} : ℕ_{⊥} → Γ(N) sending ⊥ to ⊥_{1,N} and n ∈ ℕ to succ^{n}∘zero is an isomorphism of domains and the following conditions are satisfied

(1) pred ∘ zero = zero and pred ∘ succ = id_{N}

(2) ifz ∘ ⟨zero ∘!_{N×N}, π_{1}^{N,N}, π_{2}^{N,N}⟩ = π_{1}^{N,N} and

ifz ∘ ⟨succ^{n+1} ∘ zero ∘!_{N×N}, π_{1}^{N,N}, π_{2}^{N,N}⟩ = π_{2}^{N,N} and

ifz ∘ ⟨⊥_{N×N,N}, π_{1}^{N,N}, π_{2}^{N,N}⟩ = ⊥_{N×N,N}. ♢

We are particularly interested in Λ-categories where equality and order on morphisms is determined by their behaviour on global elements.

Definition 10.7 ((order) extensional) A Λ-category C is called extensional iff Γ(f) = Γ(g) implies f = g for all morphisms f, g : A → B in C and it is called order extensional iff Γ(f) ⊑ Γ(g) implies f ⊑ g for all morphisms f, g : A → B in C. ♢

The notions of extensionality and order extensionality can be explicitated as follows: the Λ-category C is extensional iff

∀a ∈ C(1, A). f ∘ a = g ∘ b ∈ C(1, B) ⇒ f = g ∈ C(A, B)

and it is order extensional iff

∀a ∈ C(1, A). f ∘ a ⊑ g ∘ b ∈ C(1, B) ⇒ f ⊑ g ∈ C(A, B) .

In an extensional Λ-category the continuous function

App : Γ(B^{A}) × Γ(A) → Γ(B) : (f, a) ↦ ev ∘ ⟨f, a⟩

induces by functional abstraction the function

Λ(App) : Γ(B^{A}) → Γ(B)^{Γ(B)}

which is injective iff the model is extensional and which reflects the order iff the model is order extensional in which latter case Γ(B^{A}) appears as a subposet of Γ(B)^{Γ(A)} via Λ(App).

Now we define a notion of PCF model appropriate for our later characterisation of full abstraction.

Characterisation of Fully Abstract Models 89

Definition 10.8 (PCF model) A PCF model is a Λ-category C together with an N -structure in C. Such a model is called (order) extensional iff C is (order) extensional.

In extensional PCF models we make no notational distinction between A and Γ(A) and between f and Γ(f) since no information is lost when restricting attention to global elements. ♢

One can interpret PCF in arbitrary PCF models and not only in the Scott model as the semantic equations of Definition 3.14 do still make sense when reformulated in an “element-free” way (exercise!). One easily shows that the evaluation relation preserves semantic equality w.r.t. such models, i.e. if Γ ⊢ M : σ and M⇓V then [[Γ ⊢ M]] = [[Γ ⊢ V]]. The proof of this correctness property can be copied almost verbatim from the proof for the case of the Scott model.

Notice also that for PCF models one may prove computational adequacy essentially in the same way as in Chapter 4.

As in Chapter 8 using the interpretations of the PCF terms ψ_{n}^{σ} one can show (see [Stoughton 1990]) that in extensional PCF models the [[σ]] are all SFP domains (as for this purpose one does not need that the order on the [[σ→τ]] is pointwise). In case of order extensionality one can even show (see [Stoughton 1990]) that all [[σ]] are Scott domains because in this case infima in functions spaces are pointwise and thus PCF definable (see Chapter 8).

Following [Stoughton 1990] (Theorem 5.7) we show now that in extensional equationally fully abstract PCF models all compact elements of PCF types are PCF definable.

Lemma 10.9 In equationally fully abstract PCF models all compact elements of PCF types arise as interpretations of closed PCF terms.

Proof. For the sake of deriving a contradiction suppose that not all compact elements of PCF types are PCF definable. Then there is a minimal such type σ = σ_{1}→ … →σ_{n}→ι where the compact elements of the [[σ_{i}]] are all PCF definable but some e = [[ψ_{k}^{σ}]](e) ∈ [[σ]] is not PCF definable.

Let ≤ denote the pointwise order of [[σ]], i.e. f ≤ g iff fa_{1} … a_{n} ⊑ ga_{1} … a_{n} for all a_{i} ∈ [[σ_{i}]]. As f and g are continuous and the [[σ_{i}]] are SFP domains we have f ≤ g iff fe_{1} … e_{n} ⊑ ge_{1} … e_{n} for all e_{i} ∈ K([[σ_{i}]]). It is easy to see (exercise!) that f ⊓ g := [[glb^{σ}]]fg (where glb is defined as in Lemma 8.1) is the infimum of f and g w.r.t ≤ .

90 Domain-theoretic foundations of functional programming

Let K be the set of PCF definable elements in the image of [[ψ_{k}^{σ}]] and K = K^{+} ˙∪K^{−} where K^{+} = {d ∈ K | e ≤ d}.^{1} As K is finite the elements of K^{+} and K^{−} can be enumerated, i.e. K^{+} = {d_{0}, …, d_{p−1}} and K^{−} = {c_{0}, …, c_{q−1}}. For every i < q let b_{j}^{i} be compact elements in [[σ_{j}]] for j=1, …, n such that

eb_{1}^{i} … b_{n}^{i} ⋢ c_{i}b_{1}^{i} … b_{n}^{i}

which must exists as otherwise e ≤ c_{i} contradicting c_{i} ∉ K^{+}. By minimality of σ all the b_{j}^{i} are PCF definable by some closed PCF term B_{j}^{i}.

Now we distinguish two cases.

Case 1 : K^{+} is nonempty As all d_{i} are PCF definable their infimum d := d_{0} ⊓ ⋯ ⊓ d_{p−1} (w.r.t. ≤) is PCF definable, too. As by assumption e is not PCF definable we have e ≨ d. Thus, there exist compact elements a_{1}, …, a_{n} with

ea_{1} … a_{n} = ⊥  and  da_{1} … a_{n} ≠ ⊥

as otherwise e ≤ d.

For x ∈ [[ι]] let [x↘0] be a PCF term denoting the function f_{x} : D_{ι} → D_{ι} with f_{x}(y) = 0 if x ⊑ y and f_{x}(y) = ⊥ otherwise. For i < q consider the closed PCF terms

M_{i} ≡ λf:σ. [eb_{1}^{i} … b_{n}^{i}↘0](ψ_{k}^{σ}fB_{1}^{i} … B_{n}^{i})

and furthermore the closed PCF terms

\begin{matrix}N_{1} ≡ λf:σ. [ea_{1} … a_{n}↘0](ψ_{k}^{σ}fA_{1} … A_{n}) \\ N_{2} ≡ λf:σ. [da_{1} … a_{n}↘0](ψ_{k}^{σ}fA_{1} … A_{n}) \end{matrix}

where the A_{i} are closed PCF terms with [[A_{i}]] = a_{i} (which exist since compact elements of the [[σ_{i}]] are PCF definable by minimality of σ).

Now for M ≡ M_{0} ⊓ ⋯ ⊓ M_{q−1} we have [[M]](e) = 0 since [[M_{i}]](e) = 0 for i < q. As e = [[ψ_{k}^{σ}]](e) we have [[N_{1}]](e) = 0 and [[N_{1}]](e) = ⊥ because da_{1} … a_{n} ⋢ ea_{1} … a_{n}. Thus, we have [[M ⊓ N_{1}]](e) = 0 whereas [[M ⊓ N_{2}]](e) = ⊥ from which it follows that the denotations of M ⊓ N_{1} and M ⊓ N_{2} are different. But for arbitrary closed terms N of type σ we have

[[M ⊓ N_{1}]]([[N]]) = 0 = [[M ⊓ N_{2}]]([[N]]) if [[ψ_{k}^{σ}N]] ∈ K^{+}

1We use the symbol ˙∪ to denote disjoint union, i.e. M = M_{1} ˙∪M_{2} iff M = M_{1}∪M_{2} and M_{1}∩M_{2} = ∅.

Characterisation of Fully Abstract Models 91

as then ea_{1} … a_{n} ⊑ [[ψ_{k}^{σ}N]]a_{1} … a_{n} and

[[M ⊓ N_{1}]]([[N]]) = ⊥ = [[M ⊓ N_{2}]]([[N]]) if [[ψ_{k}^{σ}N]] ∈ K^{−}

as then for i < q with c_{i} = [[ψ_{k}^{σ}N]] we have [[M_{i}]]([[N]]) = ⊥ because eb_{1}^{i} … b_{n}^{i} ⋢ c_{i}b_{1}^{i} … b_{n}^{i}. Thus, by Milner’s Context Lemma the terms M ⊓N_{1} and M ⊓ N_{2} are observationally equal although their denotations are different in contradiction with the assumption that the model under consideration is equationally fully abstract.

Case 2 : K^{+} is empty For the M as defined above we have [[M]](e) = 0 whereas [[Ω_{σ}]](e) = ⊥ and thus [[M]] ≠ [[Ω_{σ}]]. For arbitrary closed terms N of type σ we have [[ψ_{k}^{σ}N]] ∈ K^{−} (as K = K^{−}) and, therefore,

[[M]]([[N]]) = ⊥ = [[Ω_{σ}]]([[N]])

since for i < q with c_{i} = [[ψ_{k}^{σ}N]] we have [[M_{i}]]([[N]]) = ⊥ because eb_{1}^{i} … b_{n}^{i} ⋢ c_{i}b_{1}^{i} … b_{n}^{i}. Thus, by Milner’s Context Lemma the terms M and Ω_{σ} are observationally equal although their denotations are different in contradiction with the assumption that the model under consideration is equationally fully abstract. □

This lemma is crucial for proving the following characterisation of equational full abstraction for extensional PCF models.

Theorem 10.10 (Characterisation of Equational Full Abstraction) An extensional PCF model is equationally fully abstract iff all compact elements of PCF types are PCF definable.

Proof. Lemma 10.9 says that all compact elements in an extensional equationally fully abstract PCF model are PCF definable.

For the reverse direction suppose we are given an extensional PCF model where all compact elements of PCF types are PCF definable. Suppose M and N are observationally equal closed PCF terms. Then [[M]] and [[N]] are equal on all PCF definable arguments and, therefore, on all compact arguments since these are all assumed to be PCF definable. Thus, as [[M]] and [[N]] are continuous maps and all interpretations of PCF types are SFP domains it follows that [[M]] = [[N]] as desired. □

Theorem 10.11 (Characterization of Full Abstraction) An extensional PCF model is fully abstract iff it is order extensional and all compact elements of PCF types are PCF definable.

92 Domain-theoretic foundations of functional programming

Proof. Suppose an extensional PCF model is fully abstract. Then it is in particular also equationally fully abstract from which it follows by Theorem 10.10 that all compact elements of PCF types are PCF definable. For showing that the model is also order extensional suppose f, g ∈ [[σ→τ]] with f(a) ⊑ g(a) for all a ∈ [[σ]]. For n ∈ ℕ let f_{n} = [[ψ_{n}^{σ→τ}]](f) and g_{n} = [[ψ_{n}^{σ→τ}]](g), respectively. Obviously, for all a ∈ [[σ]] we have f_{n}(a) ⊑ g_{n}(a). Thus, as f_{n} and g_{n} are compact and thus PCF definable it follows that f_{n} ⊑ g_{n} since the model is fully abstract and f_{n}(a) ⊑ g_{n}(a) for all PCF definable a ∈ [[σ]]. As f_{n} ⊑ g_{n} for al n ∈ ℕ it follows that f = ⨆_{n∈ℕ} f_{n} ⊑ ⨆_{n∈ℕ} g_{n} = g.

For the reverse direction suppose we are given an order extensional PCF model where all compact elements of PCF types are PCF definable. First recall that an (order) extensional PCF model is computationally adequate. Now suppose that M < ∼_{σ} N. If σ = ι then by computational adequacy [[M]] ⊑ [[N]] because all elements of [[ι]] which are not numerals are equal to ⊥. If σ is a functional type then by computational adequacy we have [[M]](d⃗) ⊑ [[N]](d⃗) for all PCF definable arguments d⃗. Thus, as all compact elements in the model are PCF definable, [[M]] and [[N]] are continuous functions and all domains in the model are SFP domains it follows by order extensionality that [[M]] ⊑ [[N]] as desired. □

See [Stoughton 1990] for an example of an extensional equationally fully abstract PCF model which, however, is not fully abstract, i.e. where for some closed terms M and N it holds that M < ∼ N although [[M]] ⋢ [[N]]. Thus, extensional equationally fully abstract PCF models are not unique up to isomorphism. However, as a consequence of Theorem 10.11, we get the following uniqueness result for extensional fully abstract models.

Theorem 10.12 (Uniqueness of Extensional Fully Abstract Models) Extensional fully abstract models of PCF are unique up to isomorphism. In particular, each [[σ]] is isomorphic to the ideal completion of the preorder (FT_{σ}, < ∼_{σ}) where FT_{σ} is the set of all ψ_{n}^{σ}(M) with M ∈ Prg_{σ} and n ∈ ℕ.

Proof. From Lemma 10.9 it follows that an element of [[σ]] is compact iff it can be denoted by some term of the form ψ_{n}^{σ}(M). As in a fully abstract model M < ∼_{σ} N iff [[M]] ⊑ [[N]] it follows that the subposet K([[σ]]) of [[σ]] is isomorphic to FT_{σ} modulo^{2} < ∼_{σ}. Thus, as [[σ]] is an SFP domain it follows that [[σ]] ≅ Idl(FT_{σ}, < ∼_{σ}). Accordingly, all extensional fully abstract models of PCF are isomorphic. □

2meaning that M, N ∈ FT_{σ} get identified iff M < ∼_{σ} N and N < ∼_{σ} M

Characterisation of Fully Abstract Models 93

This theorem allows one to construct the extensional fully abstract model of PCF as the ideal completion of some order-enriched many-sorted algebra. This construction was first performed by R. Milner in [Milner 1977] already back in 1977 and, therefore, the extensional fully abstract model of PCF is commonly called the Milner model.

However, people were not satisfied by Milner’s model construction because it is not at all syntax-free since the relation < ∼ is defined in terms of the operational semantics of PCF. Moreover, in Milner’s construction the elements of function types are ideals of equivalence classes of terms instead of—as one might hope—in terms of continuous functions preserving some additional structure common to all Scott domains in the Milner model.

In Chapter 11 we will identify such a structure. We will define so-called “sequential domains” which are domains together with a huge bunch of relations of finite arity and require morphisms between sequential domains to be continuous maps which preserve all the relational structure. In the subsequent Chapter 12 we will then show that the category S of sequential domains hosts the Milner model of PCF.

Notice, however, that in [Normann 2006] Dag Normann has shown that already at type level 3 the Milner model contains functionals which cannot be computed by a sequential strategy. This means that already at type level 3 there are functionals which are not sequential but can be obtained as the pointwise supremum of an increasing (w.r.t. the pointwise order) chain of PCF definable functionals.^{3}

3This also gives a negative answer to the old question whether the fully abstract models considered in Game Semantics (see [Hyland and Ong 2000; Abramsky et.al.

2000]) are cpo-enriched.

Chapter 11

Sequential Domains as a Model of PCF

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.

Definition 11.1 (partial partition) Let w be a finite subset of ℕ. A partial partition of w is a subset P of P(w) such that

(1) every element u of P is non-empty and

(2) all u, v ∈ P are either equal or disjoint, i.e.

u, v ∈ P ⇒ u = v ∨ u ∩ v = ∅.

We write pPart(w) for the set of all partial partitions of w. ♢

Notice that every P ∈ pPart(w) is a partition of the set ⋃ P.

Definition 11.2 (ssp) A structural system of partitions (ssp) on a finite subset w of ℕ is a subset S ⊆ pPart(w) such that

(SSP1) {w} ∈ S

(SSP2) whenever u ∈ P ∈ S then P \{u} ∈ S

(SSP3) whenever S ∈ P and u, v ∈ P then (P \{u, v}) ∪ {u ∪ v} ∈ P

(SSP4) whenever P, Q ∈ S and u ∈ P then (P \{u}) ∪ ({u ∩ v | v ∈ Q}\{∅}) ∈ S.

We say that (w, S) is structural system of partitions (ssp) iff S is a structural system of partitions on w ∈ P_{fin}(ℕ). A homomorphism from (w_{1}, S_{1}) to

96 Domain-theoretic foundations of functional programming

(w_{2}, S_{2}) is a function h : w_{1} → w_{2} such that

{h^{−1}[u] | u ∈ P }\{∅} ∈ S_{1}

for all P ∈ S_{2}. We write h : (w_{1}, S_{1}) → (w_{2}, S_{2}) if h is a homomorphism from (w_{1}, S_{1}) to (w_{2}, S_{2}). Obviously, ssp-homorphisms are closed under composition and id_{w} : (w, S) → (w, S) for all ssp’s (w, S). Thus, structural systems of partitions and their homomorphisms form a category which we denote by SSP. ♢

The intuition behind ssp’s (w, S) is that they are “finite data types” (with underlying set w) together with the collection S of those partial partitions that are induced by partial maps

f : w ⇀ {1, …, n}

arising from functional programs on this data type to some “enumeration type” {1, …, n}. The requirements (SSP1)–(SSP4) reflect some obvious closure properties of such partitions induced by functional programs:

(SSP1) says that we always have the trivial partition as induced by constant total maps which certainly arise from programs.

(SSP2) says that from any P ∈ S one may remove any of its elements corresponding to the fact that if f : w ⇀ {1, …, n} arises from a program then the function f′ with f′(k)↑ if f(k) = i and f′(k) = f(k) otherwise arises from a program, too.

(SSP3) says that if from some P ∈ S we remove u, v ∈ P and instead add u ∪ v then the resulting set of equivalence classes is also in S corresponding to the fact that if f : w ⇀ {1, …, n} arises from a program then f′ with f′(k) = i if f(k) = i or f(k) = j and f′(k) = f(k) otherwise arises from a program, too.

(SSP4) says that if for some P ∈ S we remove u ∈ P and replace it for some Q ∈ S by all non-empty intersections u∩v with v ∈ Q corresponding to the fact that if f : w ⇀ {1, …, n} and g : w ⇀ {1, …, m} arise from programs then for every i with 1≤i≤n the function h : w ⇀ {1, …, n+m−1} with

h(k) = \{ \begin{matrix}f(k) & if f(k) < i \\ i−1+g(k) & if f(k) = i and g(k)↓ \\ f(k)+m & if f(k) > i \\ ↑ & otherwise \end{matrix}

Sequential Domains as a Model of PCF 97

arises from a program, too.

We now define what is a logical relation of arity (w, S) on a domain A.

Definition 11.3 (logical relation of arity (w, S)) Let (w, S) be a ssp and A a domain. A logical relation on A of arity (w, S) is a subset R ⊆ A^{w} such that

(R1) R is closed under directed suprema (taken in A^{w}) (R2) R contains all constant maps from w to A,

i.e. δ(a) := \underline{λ}i∈w.a ∈ R for all a ∈ A (R3) whenever f ∈ R and {u} ∈ S then f↾u ∈ R where

(f↾u)(i) = \{ \begin{matrix}f(i) & if i ∈ u \\ ⊥ & otherwise \end{matrix}

(R4) if f ∈ A^{w} and P ∈ S with f↾u ∈ R for all u ∈ P then f↾ ⋃ P ∈ R. ♢

Condition (R3) expresses stability under restriction and condition (R4) says that one may “ glue elements of R w.r.t. some P ∈ S ”.

Definition 11.4 (Kripke logical relation) A (varying) arity is a (in general non-full) subcategory of SSP.

For a varying arity A and a domain A a Kripke logical relation on A of arity A is a function R assigning to every (w, S) ∈ |A| a logical relation R^{(w,S)} on A of arity (w, S) in such a way that f ∘ h ∈ R^{(w′,S′)} whenever f ∈ R^{(w,S)} and h : (w′, S′) → (w, S) is an arrow in A. ♢

Now we have collected enough notions to define the category S of sequential domains.

Definition 11.5 (Category S of Sequential Domains) A sequential domain A consists of a domain |A| together with a mapping R(A) which assigns to every varying arity A a Kripke logical relation R(A)_{A} on |A| of arity A.

Sequential domains form the objects of a category S whose morphisms are defined as follows: an S-morphism from A to B is a Scott continuous function f : |A| → |B| such that for all varying arities A it holds that

a ∈ R(A)_{A}^{(w,S)} ⟹ f ∘ a ∈ R(B)_{A}^{(w,S)}

for all (w, S) ∈ |A|. Composition of morphisms and identity maps are inherited from the category of domains and continuous maps. ♢

98 Domain-theoretic foundations of functional programming

The category of domains and Scott continuous maps is contained in S as the full subcategory on those objects A = (|A|, R(A)) where R(A)_{A}^{(w,S)} = A^{w} for all varying arities A and all objects (w, S) ∈ A because any Scott continuous function between such objects necessarily preserves all relations as required by the above definition of an S-morphism.

The following lemma gives a non-trivial example of a sequential domain that will later serve as the interpretation of nat in the fully abstract model.

Lemma 11.6 Let |N| = ℕ_{⊥} and for all arities A and (w, S) ∈ |A| let

f ∈ R(N)_{A}^{(w,S)} ⟺ {f^{−1}[{n}] | n ∈ ℕ}\{∅} ∈ S

for f : w → ℕ_{⊥}. Then N = (|N|, R(N)) is an object of S.

Proof. Straightforward, but lengthy exercise! □

Next we show that the category S is cartesian closed.

Theorem 11.7 The category S is cartesian closed, i.e. has finite products and exponential objects.

Proof. The terminal object 1 is given by |1| = {⊥} and R(1)_{A}^{(w,S)} = {⊥}^{w}. One readily checks that for every A ∈ |S| the constant map from |A| to {⊥} is the unique S-morphism from A to 1.

Let A and B be arbitrary sequential domains for which we will give the construction of A×B and [A→B] next.

The underlying domain of A×B is the cartesian product of the underlying domains of A and B, respectively, i.e. |A×B| = |A|×|B|, and

f ∈ R(A×B)_{A}^{(w,S)}  iff  π_{1} ∘ f ∈ R(A)_{A}^{(w,S)} and π_{2} ∘ f ∈ R(B)_{A}^{(w,S)}

where π_{1} and π_{2} are first and second projection, respectively. Thus, the continuous maps π_{1} : A×B → A and π_{2} : A×B → B preserve all relations and, accordingly, are S-morphisms. We leave it as a simple exercise(!) to show that for S-morphisms f : C → A and g : C → B their target tupling ⟨f, g⟩ is an S-morphism from C to A×B.

The underlying domain of [A→B] is S(A, B), the set of S-morphisms from A to B, under the pointwise ordering. One readily checks (using intrinsically condition (R1) from Definition 11.3) that S(A, B) is closed under directed suprema taken in [|A|→|B|]. Due to condition (R2) of Definition 11.3 every constant map from |A| to |B| is in S(A, B) and thus the map λx:|A|.⊥_{|B|} is the least element of S(A, B). For variable arities

Sequential Domains as a Model of PCF 99

A and (w, S) ∈ |A| we define the relation R([A→B])_{A}^{(w,S)} as follows: f ∈ R([A→B])_{A}^{(w,S)} iff

ev ∘ ⟨f∘h, a⟩ = \underline{λ}j∈w′.f(h(j))(a(j)) ∈ R(B)_{A}^{(w′,S′)}

for all h : (w′, S′) → (w, S) in A and a ∈ R(A)_{A}^{(w′,S′)}. If all R([A→B])_{A}^{(w,S)} are logical relations in the sense of Definition 11.3 then it is obvious that the R([A→B])_{A} are actually Kripke logical relations of arity A (because of the quantification over all h : (w′, S′) → (w, S) in A).

That R([A→B])_{A}^{(w,S)} satisfies conditions (R1) and (R2) of Definition 11.3 is left as an easy exercise(!).

For verifying condition (R3) suppose that f ∈ R([A→B])_{A}^{(w,S)} and {u} ∈ S. We have to show that f↾u ∈ R([A→B])_{A}^{(w,S)}, too. For that purpose suppose that h : (w′, S′) → (w, S) is in A and a ∈ R(A)_{A}^{(w′,S′)}. Due to the assumption f ∈ R([A→B])_{A}^{(w,S)} we know that ev ∘ ⟨f∘h, a⟩ ∈ R(B)_{A}^{(w′,S′)} and, therefore, also ev∘⟨f∘h, a⟩ ↾ h^{−1}[u] ∈ R(B)_{A}^{(w′,S′)} (because R(B)_{A}^{(w′,S′)} satisfies condition (R3) and either h^{−1}[u] = ∅ or {h^{−1}[u]} ∈ S′). One easily checks that ev∘⟨f∘h, a⟩ ↾ h^{−1}[u] = ev∘⟨(f↾u)∘h, a⟩ and, therefore, it follows that ev ∘ ⟨(f↾u) ∘ h, a⟩ ∈ R(B)_{A}^{(w′,S′)} as required by condition (R3).

For verifying condition (R4) suppose that f ∈ S(A, B)^{w} and P ∈ S with f↾u ∈ R([A→B])_{A}^{(w,S)} for all u ∈ P. We have to show that f↾ ⋃ P ∈ R([A→B])_{A}^{(w,S)}, too. For that purpose assume that h : (w′, S′) → (w, S) is a morphism in A and a ∈ R(A)_{A}^{(w′,S′)}. We have to show that ev∘⟨(f↾ ⋃ P)∘ h, a⟩ ∈ R(B)_{A}^{(w′,S′)}. As ev ∘ ⟨(f↾ ⋃ P) ∘ h, a⟩ = ev ∘ ⟨f ∘ h, a⟩ ↾ h^{−1}[⋃ P ] and h^{−1}[⋃ P ] = ⋃_{u∈P} h^{−1}[u] it suffices to show that ev ∘ ⟨f∘h, a⟩ ↾ h^{−1}[u] ∈ R(B)_{A}^{(w′,S′)} for all u ∈ P with h^{−1}[u] ≠ ∅ (because R(B)_{A}^{(w′,S′)} satisfies condition (R4) and {h^{−1}[u] | u ∈ S} \ {∅} ∈ S′). This, however, holds as {h^{−1}[u]} ∈ S′ for u ∈ S with h^{−1}[u] ≠ ∅ from which it follows by (R4) that ev∘⟨f∘h, a⟩ ↾ h^{−1}[u] = ev∘⟨(f↾u)∘h, a⟩ ∈ R(B)_{A}^{(w′,S′)} since we have assumed that f↾u ∈ R([A→B])_{A}^{(w,S)}.

It is immediate that the evaluation map ev : |[A→B]|×|A| → |B| : (f, a) ↦ f(a) preserves all relations and, therefore, is an S-morphism. Suppose that f : C×A → B is an S-morphism. We show now that Λ(f) with Λ(f)(z)(x) = f(z, x) is an S-morphism from C to [A→B]. Suppose that z ∈ |C|. We have to show that f(z, −) ∈ S(A, B). Suppose a ∈ R(A)_{A}^{(w,S)}. Then λi∈w.f(z, a(i)) = λi∈w.f(δ_{w}(z)(i), a(i)) = ev∘⟨δ_{w}(z), a⟩ ∈ R(B)_{A}^{(w,S)}

100 Domain-theoretic foundations of functional programming

because δ_{w}(z) ∈ R(C)_{A}^{(w,S)} by (R2) and a ∈ R(A)_{A}^{(w,S)} by assumption. Thus, we have shown that Λ(f) sends elements of |C| to S(A, B). For showing that Λ(f) preserves all relations suppose c ∈ R(C)_{A}^{(w,S)}. We have to show that Λ(f)∘c ∈ R([A→B])_{A}^{(w,S)}. Suppose that h : (w′, S′) → (w, S) is in A and a ∈ R(A)_{A}^{(w′,S′)}. Then we have ev∘⟨Λ(f)∘c∘h, a⟩ = f ∘⟨c∘h, a⟩ ∈ R(B)_{A}^{(w′,S′)} since c∘h ∈ R(C)_{A}^{(w′,S′)} (as R(C)_{A} is a Kripke logical relation) and a ∈ R(A)_{A}^{(w′,S′)} by assumption. □

Next we show that the usual interpretation of the arithmetic operations of PCF are actually S-morphisms.

Lemma 11.8 The usual interpretations of the arithmetic basic operations zero, succ, pred and ifz are morphisms in S when nat is interpreted by the object N as specified in Lemma 11.6.

Proof. This is trivial for zero, succ and pred and, therefore, left to the reader as an exercise(!). The case of cond = [[ifz]] is more subtle and illustrates the role of conditions (R3) and (R4) in Def. 11.3 and, therefore, we give it here in detail.

Suppose for that purpose that f = ⟨f_{0}, f_{1}, f_{2}⟩ ∈ R(N×N×N)_{A}^{(w,S)}, i.e. that the f_{i} ∈ R(N)_{A}^{(w,S)}. By definition of N (see Lemma 11.6) we know that {u, v} ∈ S where u := f_{0}^{−1}[{0}] and v := f_{0}^{−1}[ℕ\{0}]. Thus, by condition (R3) of Definition 11.3 we have

(cond∘f)↾u = f_{1}↾u ∈ R(N)_{A}^{(w,S)} and (cond∘f)↾v = f_{2}↾v ∈ R(N)_{A}^{(w,S)}

from which it follows by condition (R4) of Definition 11.3 that

cond∘f = (cond∘f)↾u∪v ∈ R(N)_{A}^{(w,S)}

as desired. □

Now we have assembled enough information to show that we get a model for PCF in S when interpreting nat as N.

Theorem 11.9 The category S is a Λ-category when endowing the homsets S(A, B) with the pointwise ordering. Moreover, S is an order extensional model of PCF when interpreting nat as in Lemma 11.6 and the basic arithmetic operations as in the Scott model.

Proof. One easily checks that when defining pairing ⟨−, −⟩ and functional abstraction Λ as usual^{1} this gives rise to a Λ-category (in the sense

1namely, as ⟨f, g⟩(x) = ⟨f(x), g(x)⟩ and Λ(f)(x)(y) = f(x, y)

Sequential Domains as a Model of PCF 101

of Definition 10.2). That S is order extensional follows from the pointwise definition of order on the hom-sets of S and the fact that for all sequential domains A all constant functions a : {⊥} → |A| are S-morphisms (because by condition (R2) of Definition 11.3 each R(B)_{A}^{(w,S)} contains all constant maps from w to |B|), i.e. we have enough global elements of each A available to distinguish different functions from A to B. From Lemma 11.6 we know that N is a sequemtial domain and from Lemma 11.8 we know that the usual interpreations of the basic arithmetic operations actually live in S as morphisms. Finally, we have least fixpoints as in any Λ-category (see Theorem 10.4). That least fixpoints are computed as usual by sending f to ⨆_{n∈ℕ} f^{n}(⊥) follows from Theorem 10.4 and the fact that in S pairing and application are constructed as usual. □

In a sense the model S appears as sort of a “restriction of the Scott model to the sequential objects and their limits”. This, however, is literally true only for first order types as for types of higher order one cannot really compare the functions because their domains of definition are too different. One may, however, define Kripke logical relations on the full Scott model and then verify (see [Liguoro 1996]) that the objects of the Scott model that are invariant under all these Kripke logical relations are precisely those elements of the Scott model which are the directed supremum of its approximating PCF definable compact elements, i.e. one may characterise by invariance properties the closure under directed suprema of the PCF definable elements of the Scott model. Instead, in the current chapter we have cut down “on the fly” all types to the closure of the PCF definable elements as we shall show in the following Chapter 12.

Chapter 12

The Model of PCF in S is 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.

Definition 12.1 For every PCF type σ let A^{σ} be its interpretation in the PCF model in S. For n ∈ ℕ let h_{n}^{σ} : A^{σ} → A^{σ} be the interpretation of ψ_{n}^{σ} in S. Like in the Scott model the h_{n}^{σ} form an ascending chain of finitary projections whose supremum is id_{A^{σ}}. We write A_{n}^{σ} for h_{n}^{σ}[A^{σ}], the image of h_{n}^{σ}. If Γ ≡ x_{1}:σ_{1}, …, x_{k}:σ_{k} then we write A^{Γ} for A^{σ_{1}}× … ×A^{σ_{k}}, h_{n}^{Γ} for h_{n}^{σ_{1}}× … ×h_{n}^{σ_{k}} and A_{n}^{Γ} for the image of h_{n}^{Γ}.

As there are only countably many contexts Γ and each K(A^{Γ}) = ⋃_{n∈ℕ} A_{n}^{Γ} is countable we may choose an arbitrary, but fixed bijection between ℕ and the (disjoint) union of all K(A^{Γ}). This bijection allows us to identify finite subsets of K(A^{Γ}) with (certain) finite subsets of ℕ. This identification will tacitly apply subsequently without further mention. ♢

We now define the sequence A_{n} of arities needed for the proof of full abstraction.

Definition 12.2 For a PCF context Γ and n ∈ ℕ the ssp Γ_{n} = (w_{Γ_{n}}, S_{Γ_{n}}) is defined as follows

• w_{Γ_{n}} is A_{n}^{Γ} considered as a subset of ℕ

• P ∈ S_{Γ_{n}} iff there is a term Γ ⊢ M : ι such that

P = { [[Γ⊢M]]^{−1}[{i}] ∩ w_{Γ_{n}} | i ∈ ℕ } \ {∅} .

104 Domain-theoretic foundations of functional programming

Now the arities A_{n} are defined as the subcategories of SSP whose objects are the Γ_{n} for arbitrary PCF contexts Γ and n ∈ ℕ and whose morphisms are the projections

(Γ, Δ)_{n} → Γ_{n} : (γ, δ) ↦ γ

which, obviously, are closed under composition. ♢

Of course, one has to verify that the Γ_{n} are actually ssp’s but this follows quite straightforwardly from closure properties of PCF terms of type ι in context Γ ensuring the requirements (SSP1)–(SSP4) of Definition 11.2 (see discussion after Def. 11.2 ). That the A_{n} are actually arities, i.e. that the projections (Γ, Δ)_{n} → Γ_{n} are SSP-morphisms, follows from the fact that Γ, Δ ⊢ M : ι whenever Γ ⊢ M : ι.

Now we prove the main lemma ensuring full abstraction for the PCF model in S where nat is interpreted as the sequential domain N introduced in Lemma 11.6.

Lemma 12.3 Let σ be a PCF type and n ∈ ℕ. Then for all contexts Γ and f : A_{n}^{Γ} → A_{n}^{σ} the following two conditions are equivalent

(1) f ∈ R(A^{σ})_{A_{n}}^{Γ_{n}}

(2) f = [[Γ⊢M]]↾A_{n}^{Γ} for some term Γ ⊢ M : σ.

Proof. The proof proceeds by induction on the structure of σ.

The base case is trivial because from the definition of S_{Γ_{n}} it is immediate that R(A^{ι})_{A_{n}}^{Γ_{n}} = R(N)_{A_{n}}^{Γ_{n}} contains precisely the PCF-definable functions from A_{n}^{Γ} to ℕ_{⊥}.

Now suppose as induction hypotheses that conditions (1) and (2) are equivalent for the types σ and τ. For proving that (1) and (2) are equivalent for the type σ→τ suppose f : A_{n}^{Γ} → A_{n}^{σ→τ}.

For showing that (1) implies (2) suppose that f ∈ R(A^{σ→τ})_{A_{n}}^{Γ_{n}}. Then we have

ev ∘ ⟨f∘π_{1}, π_{2}⟩ ∈ R(A^{τ})_{A_{n}}^{(Γ,x:σ)_{n}}

(where x is some fresh variable not declared in Γ) due to the definition of exponentials in S because π_{1} is a morphism in A_{n} from (Γ, x:σ)_{n} to Γ_{n} and π_{2} ∈ R(A^{σ})_{A_{n}}^{(Γ,x:σ)_{n}} by the induction hypothesis for σ since π_{2} arises as interpretation of the term Γ, x:σ ⊢ x : σ. Now from the induction hypothesis for τ it follows that

ev ∘ ⟨f∘π_{1}, π_{2}⟩ = [[Γ, x:σ ⊢ M]]↾A_{n}^{Γ,x:σ}

The Model of PCF in S is Fully Abstract 105

for some PCF term Γ, x:σ ⊢ M : τ. But then we have

f = [[Γ ⊢ ψ_{n}^{σ→τ} (λx:σ.M)]]↾A_{n}^{Γ}

as desired.

For showing that (2) implies (1) assume that f = [[Γ⊢M]]↾A_{n}^{Γ} for some PCF term Γ ⊢ M : σ→τ. For showing that f ∈ R(A^{σ→τ})_{A_{n}}^{Γ_{n}} consider an arbitrary morphism π : (Γ, Δ)_{n} → Γ_{n} in A_{n} and an arbitrary element a ∈ R(A^{σ})_{A_{n}}^{(Γ,Δ)_{n}}. By the induction hypothesis for σ there exists a PCF term Γ, Δ ⊢ N : σ with h_{n}^{σ} ∘ a = [[Γ, Δ ⊢N]]↾A_{n}^{Γ,Δ} as h_{n}^{σ} ∘ a : A_{n}^{Γ,Δ} → A_{n}^{σ} is in R(A^{σ})_{A_{n}}^{(Γ,Δ)_{n}} because h_{n}^{σ} is PCF-definable and thus an S-morphism. Now by induction hypothesis on τ we have

ev ∘ ⟨f ∘ π, a⟩ = ev ∘ ⟨h_{n}^{σ→τ} ∘ f ∘ π, a⟩ =
= ev ∘ ⟨h_{n}^{σ→τ} ∘ f ∘ π, h_{n}^{σ} ∘ a⟩ =
= ev ∘ ⟨f ∘ π, h_{n}^{σ} ∘ a⟩ =
= [[Γ, Δ ⊢ M(N)]]↾A_{n}^{Γ,Δ} ∈ R(A^{τ})_{A_{n}}^{(Γ,Δ)_{n}}

as desired. □

Now we can prove the desired full abstraction result for S.

Theorem 12.4 (Full Abstraction for Sequential Domains) For every PCF type σ every compact element of A^{σ} is definable in PCF. Thus, the model of PCF in S with [[nat]] = N is fully abstract.

Proof. Suppose that a ∈ A^{σ} is compact, i.e. a ∈ A_{n}^{σ} for some n ∈ ℕ. Then the constant function c_{a} : A_{n}^{⟨⟩} → A_{n}^{σ} with value a (where ⟨⟩ is the empty context) is an element of R(A_{n}^{σ})_{A_{n}}^{⟨⟩_{n}}. Thus, by Lemma 12.3 there exists a PCF term ⟨⟩ ⊢ M : σ with c_{a} = [[⟨⟩ ⊢M]]↾⟨⟩_{n}, i.e. a = [[M]]. Thus a is PCF definable as desired.

Now full abstraction of the PCF model in S follows from Theorem 10.11 since the model is order extensional and all compact elements of PCF types are PCF definable. □

The construction of the PCF model in S can be understood as a complete characterisation via relational invariants of PCF definability up to closure under directed suprema since we have shown that a Scott continuous function f : A^{σ} → A^{τ} appears as supremum of a chain of PCF definable functions of type σ→τ if and only if f preserves all Kripke logical relations. Thus, the relational invariants as given by the collection of all Kripke logical relations are sufficient for capturing PCF definability up to closure under directed suprema.

106 Domain-theoretic foundations of functional programming

Notice, moreover, that the category S hosts also fully abstract models of functional programming languages with recursive types as has been investigated in detail in [Marz 2000].

It might be disappointing that we have used so many relational invariants for characterising PCF-definability up to closure under directed suprema. However, one cannot expect anything dramatically simpler because it has been shown by R. Loader [Loader 2001] that already for finitary PCF, i.e. PCF with booleans as its single base type instead of natural numbers, observational equivalence is undecidable. This forever refutes the original hope of characterising PCF-definability in terms of preservation of only finitely many relations.

Chapter 13

Computability in Domains

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_{ι→ι} does contain (strict) functions that are not computable. The aim of this chapter is to remedy this shortcoming by defining domains endowed with a notion of computability, the so-called effectively given domains.^{1} As a byproduct we will arrive at a notion of higher type computability which is usually neglected^{2} in the main stream of recursion-theoretic literature. In this chapter we will concentrate exclusively on Scott domains because for other notions of domains (as e.g. stable domains à la Berry and our sequential domains) there arise intrinsic difficulties when trying to extend the notion of computability to higher types. A more detailed account of Computability in Domains can be found in [Griffor et.al. 1994]. For background information about elementary recursion theory we refer the reader to the classic text by H. Rogers [Rogers 1987].

Before giving the precise definition of effectively given domain we recall a few basic facts about Scott domains, i.e. bounded complete countably algebraic domains. The most important property of Scott domains is that they are closed under exponentiation. Moreover, for Scott domains D and E the basis K([D→E]) of [D→E] can be described explicitly in terms of the bases K(D) and K(E) in the following way. First observe that a (countably) algebraic domain D is bounded complete if and only if every finite subset of K(D) has a supremum in D which necessarily is compact, too. Based on

1Notice, however, that effectively given domains need not be effectively isomorphic even if their underlying domains are isomorphic. For an explicit counterexample see [Kanda and Park 1979].

2Although some attention is sometimes paid to the second order case when discussing effective operations and effective operators as e.g. in [Rogers 1987].

108 Domain-theoretic foundations of functional programming

this fact one easily shows that the compact elements of [D→E] are precisely those of the form

⨆_{i=1}^{n} [e_{i}, e′_{i}]

where the e_{i} and e′_{i} are elements of K(D) and K(E), respectively, and the so-called step functions [e_{i}, e′_{i}] are defined as

[e_{i}, e′_{i}](x) = \{ \begin{matrix}e′_{i} & if e_{i} ⊑ x \\ ⊥ & otherwise \end{matrix}

provided the following consistency property holds: for every I ⊆ {1, …, n} with {e_{i} | i ∈ I} bounded in D the set {e′_{i} | i ∈ I} is bounded in E. Obviously, we have

(⨆_{i=1}^{n} [e_{i}, e′_{i}])(x) = ⨆{e′_{i} | e_{i} ⊑ x}

for x ∈ D. Based on these observations one easily checks that

[ẽ, ẽ′] ⊑ ⨆_{i=1}^{n} [e_{i}, e′_{i}] iff ẽ′ ⊑ ⨆{e′_{i} | e_{i} ⊑ ẽ} .

Accordingly, we have

⨆_{j=1}^{m}[ẽ_{j}, ẽ′_{j}] ⊑ ⨆_{i=1}^{n} [e_{i}, e′_{i}] iff ∀j ∈ {1, …, m}. ẽ′_{j} ⊑ ⨆{e′_{i} | e_{i} ⊑ ẽ_{j}} .

Now we are ready to define what is an effectively given (Scott) domain.

Definition 13.1 (Effectively Given Domain) An effectively given domain is a pair (D, ε) such that D is a Scott domain and ε is an enumeration of K(D), i.e. ε : ℕ → K(D) is a surjective function, satisfying the following two conditions

(1) ↑{ε(i) | i ∈ e_{n}} is a decidable property of n (where e is some effective coding of P_{fin}(ℕ) and ↑X stands for “X bounded from above”)

(2) ⨆{ε(i) | i ∈ e_{n}} = ε(m) is a decidable relation between n and m.

An element d ∈ D is called (D, ε)-computable or simply computable iff the set {n ∈ ℕ | ε(n) ⊑ d} is recursively enumerable (r.e.). We write Comp(D, ε) for the set of computable elements of (D, ε). ♢

Computability in Domains 109

Next we define what are computable functions between effectively given domains.

Definition 13.2 (Computable Maps) Let (D_{1}, ε^{(1)}) and (D_{2}, ε^{(2)}) be effectively given domains. A Scott continuous function f : D_{1} → D_{2} is called computable (w.r.t. ε^{(1)} and ε^{(2)}) iff the set^{3} {⟨n, m⟩ | ε^{(2)}(m) ⊑ f(ε^{(1)}(n))} is r.e. To express that f is computable we write f : (D_{1}, ε^{(1)}) → (D_{2}, ε^{(2)}). ♢

Notice that for an effectively given domain (D, ε) the relation ε(n) ⊑ ε(m) is decidable as it is equivalent to ε(m) = ⨆{ε(n), ε(m)}. Accordingly, the relation ε(n) = ε(m) is decidable, too.

From these observations the following two lemmas follow rather easily.

Lemma 13.3 Computable maps between effectively given domains preserve computability of elements.

Proof. Suppose f : (D_{1}, ε^{(1)}) → (D_{2}, ε^{(2)}) and x ∈ Comp(D_{1}, ε^{(1)}). Then the sets A := {n ∈ ℕ | ε^{(1)}(n) ⊑ x} and B := {⟨n, m⟩ | ε^{(2)}(m) ⊑ f(ε^{(1)}(n))} are r.e. Thus, the set {m ∈ ℕ | ∃n ∈ A. ⟨n, m⟩ ∈ B} = {m ∈ ℕ | ε^{(2)}(m) ⊑ f(x)} is also r.e., i.e. f(x) is computable. □

Lemma 13.4 If (D, ε) is an effectively given domain then id_{D} is a computable map (w.r.t. ε). Moreover, computable maps are closed under composition, i.e. if f : (D_{1}, ε^{(1)}) → (D_{2}, ε^{(2)}) and g : (D_{2}, ε^{(2)}) → (D_{3}, ε^{(3)}) then g ∘ f : (D_{1}, ε^{(1)}) → (D_{3}, ε^{(3)}).

Accordingly, effectively given domains and computable maps give rise to a category denoted as Dom_{eff}.

Proof. As by the remark after Def. 13.1 the relation ε(n) ⊑ ε(m) is decidable and thus also r.e. the map id_{D} is computable.

As f and g are computable the sets

A := {⟨n, m⟩ | ε^{(2)}(m) ⊑ f(ε^{(1)}(n))} B := {⟨m, k⟩ | ε^{(3)}(k) ⊑ g(ε^{(2)}(m))}

are both r.e. By continuity of f and g we have ε^{(3)}(k) ⊑ (g∘f)(ε^{(1)}(n)) iff ∃m∈ℕ. ε^{(2)}(m) ⊑ f(ε^{(1)}(n)) ∧ ε^{(3)}(k) ⊑ f(ε^{(2)}(m)) iff ∃m∈ℕ. ⟨n, m⟩ ∈ A ∧ ⟨m, k⟩ ∈ B. As A and B are r.e. it follows that {⟨n, k⟩ | ε^{(3)}(k) ⊑ (g∘f)(ε^{(1)}(n))} is r.e., too, and thus g ∘ f is computable.

As all identity maps on effectively given domains are computable and computable maps between effectively given domains are closed under composition they form a category Dom_{eff}. □

3usually called the (Scott) graph of f

110 Domain-theoretic foundations of functional programming

The domain ℕ_{⊥} can be made into an effectively given domain N = (ℕ_{⊥}, ε^{N}) where ε^{N}(0) = ⊥ and ε^{N}(n+1) = n. A terminal object 1 in Dom_{eff} is given by ({⊥}, ε^{1}) where ε : ℕ → {⊥} is the unique constant map with value ⊥.

Lemma 13.5 The category Dom_{eff} is order extensional, i.e. f ⊑ g iff f ∘ a ⊑ g ∘ a for all a : 1 → A in Dom_{eff}.

Proof. Obvious from the fact that every compact element of an effectively given domain is in particular computable. □

Next we show that the category of effectively given domains is cartesian closed.

Theorem 13.6 The category Dom_{eff} is cartesian closed.

Proof. A terminal object is given by 1 = ({⊥}, ε : ℕ → {⊥}).

Suppose (D_{1}, ε^{(1)}) and (D_{2}, ε^{(2)}) are effectively given domains. Their product is given by ([D_{1}×D_{2}], [ε^{(1)}×ε^{(2)}]) with [ε^{(1)}×ε^{(2)}](⟨n, m⟩) = (ε^{(1)}(n), ε^{(}2)(m)). Their exponential is given by ([D_{1}→D_{2}], [ε^{(1)}→ε^{(2)}]) for some appropriate numbering [ε^{(1)}→ε^{(2)}] which we describe next.

We call a finite subset A of ℕ “consistent” iff the set {[ε^{(1)}(i), ε^{(2)}(j)] | ⟨i, j⟩ ∈ A} of step functions is bounded in [D_{1}→D_{2}]. Due to the remarks before Def. 13.1 it is a decidable property of n whether e_{n} is consistent in this sense. Let ẽ be an enumeration of the consistent finite subsets of ℕ obtained from the canonical enumeration e of P_{fin}(ℕ) putting ẽ_{n} = e_{n} if e_{n} is consistent and ẽ_{n} = ∅ otherwise. Now we define [ε^{(1)}→ε^{(2)}] as

[ε^{(1)}→ε^{(2)}](n) = {[ε^{(1)}(i), ε^{(2)}(j)] | ⟨i, j⟩ ∈ ẽ_{n}}

for n ∈ ℕ. Next we argue why [ε^{(1)}→ε^{(2)}] satisfies requirements (1) and (2) of Def. 13.1. In order to decide whether ↑{[ε^{(1)}→ε^{(2)}](k) | k ∈ e_{n}} decide whether ⋃_{k∈e_{n}} ẽ_{k} is consistent. Thus (1) holds for [ε^{(1)}→ε^{(2)}]. In order to decide whether ⨆_{k∈e_{n}}[ε^{(1)}→ε^{(2)}](k) = [ε^{(1)}→ε^{(2)}](m) decide whether

⨆{[ε^{(1)}(i), ε^{(2)}(j)] | ⟨i, j⟩ ∈ ẽ(k), k∈e_{n}} = ⨆{[ε^{(1)}(i), ε^{(2)}(j)] | ⟨i, j⟩ ∈ ẽ_{m}}

which can be done effectively due to the remarks before Def. 13.1. Thus (2) holds for [ε^{(1)}→ε^{(2)}].

One easily checks (exercise!) that the set

{⟨⟨n, m⟩, k⟩ | ε^{(2)}(k) ⊑ [ε^{(1)}→ε^{(2)}](n)(ε^{(1)}(m))}

Computability in Domains 111

is r.e. from which it follows that the map ev : [D_{1}→D_{2}]×D_{1} → D_{2} is computable.

Suppose (D_{3}, ε^{(3)}) is an effectively given domain and f : D_{3} × D_{1} → D_{2} is computable, i.e. F := {⟨⟨n, m⟩, k⟩ | ε^{(2)}(k) ⊑ f(ε^{(3)}(n), ε^{(1)}(m))} is r.e. Then the function Λ(f) : D_{3} → [D_{1}→D_{2}] : z ↦ (x ↦ f(z, x)) is computable because [ε^{(1)}→ε^{(2)}](m) ⊑ Λ(f)(ε^{(3)}(n)) iff ∀⟨i, j⟩ ∈ ẽ_{m}. ⟨⟨n, i⟩, j⟩ ∈ F and the latter condition is obviously semidecidable since F is semidecidable by assumption.

This concludes the proof that ([D_{1}→D_{2}], [ε^{(1)}→ε^{(2)}]) is actually the desired exponential in Dom_{eff}. □

Next we show that taking least fixpoints is a computable operation.

Theorem 13.7 For an effectively given domain (D, ε) the least fixpoint operator μ_{D} : [D→D] → D : f ↦ ⨆_{n∈ℕ} f^{n}(⊥) is computable.

Proof. Recall from the proof of the previous Theorem 13.6 that a compact element [ε→ε](n) ∈ K([D→D]) equals ⨆{[ε(i), ε(j)] | ⟨i, j⟩ ∈ ẽ(n)}. First observe that the set {k ∈ ℕ | ε(k) ⊑ μ_{D}([ε→ε](n))} is the least set I_{n} s.t.

(1) if ε(k) = ⊥_{D} then k ∈ I_{n} and

(2) if k ∈ I_{n}, ε(i) ⊑ ε(k) and ⟨i, j⟩ ∈ ẽ_{n} then j ∈ I_{n}.

As I_{n} is r.e. unifomly in n the set

{⟨n, m⟩ | m ∈ I_{n}} = {⟨n, m⟩ | ε(m) ⊑ μ_{D}([ε→ε](n))}

is r.e. and, accordingly, the map μ_{D} is computable. □

Interpreting base type ι as N = (ℕ_{⊥}, ε^{N}) gives rise to the observation that the interpretation of PCF in Scott domains factors through Dom_{eff} because the basic operations zero, succ, pred and ifz on ℕ_{⊥} are all computable and the interpretation of typed λ-calculus and recursion does not lead outside the effective world as guaranteed by Theorems 13.6 and 13.7, respectively. This model of PCF inside Dom_{eff} is called the effective Scott model.

Lemma 13.8 The interpretations of por and ∃ are computable elements of N→N→N and (N→N)→N, respectively.

Proof. One simply checks that in both cases the set of codes of approximating compact elements is r.e. (exercise!). □

112 Domain-theoretic foundations of functional programming

Thus, all terms of PCF^{++} ≡ PCF+por+∃ denote computable elements of the Scott model. We write (D_{σ}, ε^{σ}) for the interpretation of PCF type σ in Dom_{eff} where base type ι gets interpreted as N = (ℕ_{⊥}, ε^{N}).

In [Plotkin 1977] G. Plotkin has proved the following two remarkable theorems

Theorem 13.9 (Full Abstraction for PCF^{+}) Every compact element of the Scott model of PCF arises as interpretation of some closed term in PCF^{+} ≡ PCF + por. Thus, the Scott model is fully abstract for PCF^{+}.

Theorem 13.10 (Universality for PCF^{++}) All computable elements of PCF types arise as denotations of PCF^{++} terms. Thus, the effective Scott model is universal for PCF^{++}.

Moreover, every object of the Scott model of PCF is definable in PCF_{Ω}^{++}, i.e. PCF^{++} extended by constants (so-called “oracles”) for all strict total functions of type ι→ι.

telling us that the effective Scott model is the best possible one for PCF^{++} and that it is precisely (the absence of) por which is responsible for the Scott model’s lack of full abstraction for PCF. Moreover, Theorem 13.10 tells us that

PCF^{++} provides a purely extensional account of classical^{4} recursion theory extended to higher types.

However, it will take several steps to prove these two classical theorems of Plotkin. First recall that in chapter 7 we invited the reader to prove that

Theorem 13.11 In the Scott model for all PCF types σ the domain D_{σ} is coherently complete.

Proof. Obviously, ℕ_{⊥} is coherently complete and coherently complete cpo’s are are closed under ×. Suppose D and E are domains and E is coherently complete. Then [D→E] is coherently complete, too, as if F ⊆ [D→E] is coherent then for all x ∈ D the set {f(x) | f ∈ F } is coherent, too, and thus has a supremum (as E is coherently complete by assumption). One easily checks (as in the proof of Lemma 3.5) that the function g with

g(x) = ⨆ {f(x) | f ∈ F } for x ∈ D

is continuous and thus the supremum of F w.r.t. the pointwise order. □

4as in classical recursion theory por and ∃ are available via dove tailing

Computability in Domains 113

If x and y are elements of a domain D we write x↑y for ↑{x, y} and x#y for the negation of x ↑ y.

Lemma 13.12 Let D be a coherently complete Scott domain. Then for every e ∈ K(D) the function below_{e} : D → ℕ_{⊥} with

below_{e}(d) = \{ \begin{matrix}0 & if e ⊑ d \\ 1 & if e#d \\ ⊥ & otherwise \end{matrix}

is continuous.

Proof. Obviously, the function below_{e} is monotonic. Suppose X ⊆ D is directed and below_{e}(x) = ⊥ for all x ∈ X. Then e↑x for all x ∈ X from which it follows that e ↑ ⨆ X because {e} ∪ X is coherent and, thus, has a supremum. Moreover, we have e ⋢ ⨆ X as otherwise e ⊑ x for some x ∈ X since e is assumed as compact. Thus below_{e}(⨆ X) = ⊥ as well. □

Lemma 13.13 (parallel conditional in PCF^{+}) In PCF^{+} one can exhibit a term x:ι, y:ι, z:ι ⊢ pif x then y else z fip : ι whose interpretation is the ternary function pcond on ℕ_{⊥} defined as

pcond(x, y, z) = \{ \begin{matrix}y & if x = 0 or y = z ∈ ℕ \\ z & if x = 1 \\ ⊥ & otherwise \end{matrix}

for all x, y, z ∈ ℕ_{⊥}.

Proof. First observe that in PCF^{+} one can implement a function pand of type ι→ι→ι such that

pand x y = \{ \begin{matrix}0 & if x = 0 = y \\ 1 & if x = 1 or y = 1 \\ ⊥ & otherwise \end{matrix}

For the sake of readability we write x ∧ y as an abbreviation for pand x y and x ∨ y as an abbreviation for por x y. Using fixpoint operators we can define in PCF^{+} a function h : (ι→ι) → ι → ι such that

h f x = ifz(f(x), x, h(f)(succ(x))

for all h ∈ D_{ι→ι} and x ∈ D_{ι}. Then the function search : (ι→ι) → ι defined as

search(f) = h f zero

114 Domain-theoretic foundations of functional programming

is also PCF^{+} definable and implements unbounded search in ℕ, i.e., search(f) terminates iff there exists an n ∈ ℕ such that f(n) = 0 and f(k) ∈ ℕ\{0} for all k < n in which case search(f) = n.

Now when defining pif x then y else z fip as

search(λw:ι. (w=y ∧ w=z) ∨ (w=y ∧ x=0) ∨ (w=z ∧ x=1))

one easily checks that it satisfies its specification. □

Now we can prove that the Scott model is fully abstract for PCF^{+}.

Proof (of Theorem 13.9) : By induction on the structure of PCF types σ we show that the following three claims hold for all e, e′ ∈ K(D_{σ})

(1) e is definable in PCF^{+}

(2) [e, 0] is definable in PCF^{+}

(3) [e, 0] ⊔ [e′, 1] is definable in PCF^{+} whenever e#e′.

The claims obviously hold for base type ι. Suppose σ = σ_{1}→ … →σ_{k}→ι and as induction hypothesis that (1)–(3) hold for the σ_{i}.

First some notation. For compact elements e_{i} ∈ K(D_{σ_{i}}) and n ∈ ℕ we write [e_{1}, …, e_{k}, n] for the function f ∈ D_{σ} with

ff_{1} … f_{k} = \{ \begin{matrix}n & if e_{i} ⊑ f_{i} for all i ∈ \{1, …, k\} \\ ⊥ & otherwise. \end{matrix}

Such functions are called step functions. Every e ∈ K(D_{σ}) is the supremum of a finite set of such step functions. One easily checks (exercise!) that there exists a least such set which we denote as F_{e}.

We proceed by induction on the size of |F_{e}| and |F_{e′}|.

ad (1): If F_{e} is empty then e is denoted by Ω_{σ}. Thus, w.l.o.g. suppose F_{e} ≠ ∅.

If there are [e_{1}, …, e_{k}, n], [e′_{1}, …, e′_{k}, n′] ∈ F_{e} with e_{i}#e′_{i} for some i with 1≤i≤k then by induction hypothesis there exists a PCF^{+} term M denoting [e_{i}, 0] ⊔ [e′_{i}, 1]. By induction hypothesis ⨆ F_{e}\{[e_{1}, …, e_{k}, n]} and ⨆ F_{e}\{[e′_{1}, …, e′_{k}, n′]} are definable by terms N_{1} and N_{2}, respectively. But then e = ⨆ F_{e} is definable by the PCF^{+} term

λf_{1}:σ_{1}…. λf_{k}:σ_{k}. pif Mf_{i} then N_{2}f_{1} … f_{k} else N_{1}f_{1} … f_{k} fip

Otherwise for all [e_{1}, …, e_{k}, n], [e′_{1}, …, e′_{k}, n′] ∈ F_{e} we have n = n′. Take [e_{1}, …, e_{k}, n] ∈ F_{e}. By induction hypothesis there are PCF^{+}

Computability in Domains 115

terms M_{i} denoting [e_{i}, 0] for i=1, …, k and a PCF^{+} term N denoting ⨆ F_{e}\{[e_{1}, …, e_{k}, n]}. Then e = ⨆ F_{e} is denoted by the PCF^{+} term

λf_{1}:σ_{1}…. λf_{k}:σ_{k}. pif M_{1}f_{1} ∧ ⋯ ∧ M_{k}f_{k} then n else Nf_{1} … f_{k} fip

where ∧ stands for pand (as introduced in the proof of Lemma 13.13).

ad (2): If F_{e} = ∅ then λx:σ.0 denotes [e, 0]. Otherwise take some [e_{1}, …, e_{k}, n] ∈ F. By induction hypothesis there exist PCF^{+} terms M_{1}, …, M_{k}, E and N denoting the compact elements e_{1}, …, e_{k}, [n, 0] and [⨆ F_{e}\{[e_{1}, …, e_{k}, n]}, 0], respectively. Then the PCF^{+} term

λf:σ. ifz(E(fM_{1} … M_{k}), Nf, Ω_{ι})

denotes [e, 0].

ad (3): Suppose e#e′. Then there exist [e_{1}, …, e_{k}, n] ∈ F_{e} and [e′_{1}, …, e′_{k}, n′] ∈ F_{e′} such that n ≠ n′ and e_{i}↑e′_{i} for i=1, …, k. By induction hypothesis there are PCF^{+} terms M_{1}, …, M_{k} denoting e_{1}⊔e′_{1}, …, e_{k}⊔e′_{k}, respectively. As (2) has already been established for σ there exist PCF^{+} terms N and N′ denoting [e, 0] and [e′, 0], respectively. Let K be a PCF term denoting [n, 0] ⊔ [n′, 1]. Then [e, 0] ⊔ [e′, 1] is denoted by

λf:σ. ifz(K(fM_{1} … M_{k}), Nf, succ(N′f))

which, obviously, is a PCF^{+} term. □

For proving universality of PCF^{++} we have to observe that sort of a “continuous universal quantifier” is definable in PCF^{++}.

Lemma 13.14 The function ∀ : [ℕ_{⊥}→ℕ_{⊥}] → ℕ_{⊥} with

∀(f) = \{ \begin{matrix}0 & if f(⊥) = 0 \\ 1 & if f(n) = 1 for some n ∈ ℕ \\ ⊥ & otherwise \end{matrix}

is definable in PCF^{++}.

Proof. Let swap be a PCF term of type ι→ι with

swap(x) = \{ \begin{matrix}0 & if x = 1 \\ 1 & if x = 0 \\ x & otherwise. \end{matrix}

Then the PCF^{++} term λf:ι→ι. swap(∃(λx:ι. swap(f(x)))) denotes ∀. □

116 Domain-theoretic foundations of functional programming

Moreover, we will employ the following extension of ifz and the parallel conditional to arbitrary types σ = σ_{1}→ … →σ_{k}→ι : if M is of type ι and N_{1} and N_{2} are of type σ (relative to some typing context) then we write ifz(M, N_{1}, N_{2}) as a shorthand for

λx_{1}:σ_{1}…. λx_{n}:σ_{n}.ifz(M, N_{1}x_{1} … x_{n}, M_{2}x_{1} … x_{n})

and pif M then N_{1} else N_{2} fip as a shorthand for

λx_{1}:σ_{1}…. λx_{n}:σ_{n}.pif M then N_{1}x_{1} … x_{n} else M_{2}x_{1} … x_{n} fip .

We leave it as an exercise(!) to check that

pif Ω_{ι} then N_{1} else N_{2} fip = N_{1} ⊓ N_{2}

which fact we will tacitly use in the subsequent proof of Theorem 13.10 which is due to [Escardó 1997] and easier to follow than the original proof in [Plotkin 1977].

Proof (of Theorem 13.10) : By induction on the structure of PCF types we will show that for every type σ there exist PCF^{++} terms join^{σ} : ι→σ→σ, up^{σ} : ι→ι→σ and below^{σ} : ι→σ→ι whose denotations (also denoted as join^{σ}, up^{σ} and below^{σ}) satisfy the requirements that

(1) for all d ∈ D_{σ} and n ∈ ℕ

(i) join^{σ}(⊥)(d) = ⊥ and

(ii) join^{σ}(n)(d) = ε_{n}^{σ} ⊔ d whenever ε_{n}^{σ} ↑ d

(2) for every n ∈ ℕ the set {d ∈ Comp(D_{σ}, ε^{σ}) | ε_{n}^{σ} ⊑ d} is enumerated by the function up^{σ}(n) : ℕ_{⊥}→D_{σ}d

(3) for all n ∈ ℕ and d ∈ D_{σ}

below^{σ}(n)(d) = \{ \begin{matrix}0 & if ε_{n}^{σ} ⊑ d \\ 1 & if ε_{n}^{σ} # d \\ ⊥ & otherwise \end{matrix}

i.e. below^{σ}(n) implements the function below_{ε_{n}^{σ}} of Lemma 13.12.

Before verifying the existence of such terms we show how they allow one to prove that all computable elements of D_{σ} can be denoted by PCF^{++} terms.

Computability in Domains 117

Suppose d ∈ Comp(D_{σ}, ε^{σ}). Then there exists a PCF term g_{d} : ι→ι with {g_{d}(n) | n ∈ ℕ} = {n ∈ ℕ | ε_{n}^{σ} ⊑ d}. We write h_{d} for the PCF^{++} term λk:ι.join^{σ}(g_{d}(k)) of type ι→σ→σ. Let Φ_{σ} be the PCF term

λF:(ι→σ→σ)→σ.λf:ι→σ→σ.f(0)(F (λn:ι.f(succ(n))))

of type ((ι→σ→σ)→σ) → (ι→σ→σ)→σ. Then we have

Y(Φ_{σ})(h_{d}) = ⨆_{n∈ℕ} Φ_{σ}^{n}(⊥)(h_{d}) =
= ⨆_{n∈ℕ} h_{d}(0) ∘ ⋯ ∘ h_{d}(n)(⊥) =
= ⨆_{n∈ℕ} ε_{g_{d}(0)}^{σ} ⊔ ⋯ ⊔ ε_{g_{d}(n)}^{σ} =
= d

where the last equality holds as g_{d} enumerates the codes of finite approximations to d. Thus, the PCF^{++} term Y(Φ_{σ})(h_{d}) denotes d and hence d is definable in PCF^{++}.

For arbitrary d ∈ D_{σ} there still exists a total function g_{d} : ℕ → ℕ enumerating {n ∈ ℕ | ε_{n}^{σ} ⊑ d} which, however, in general will not be recursive anymore. Nevertheless, we still have d = Y(Φ)(λk:ι.join^{σ}(g_{d}(k))) and hence d is definable in PCF_{Ω}^{++} (using the oracle g_{d}).

Now we will turn back to the task of exhibiting terms join^{σ}, up^{σ} and below^{σ} satisfying requirements (1)–(3). We proceed by induction on the structure of σ. For base type ι the claim is obvious. Suppose as induction hypotheses that the claim holds already for σ and τ.

There is a PCF^{++} definable function sjoin : ℕ_{⊥} → D_{σ→τ} → D_{σ→τ} with

sjoin(⟨n, m⟩)(f)(d) = pif below^{σ}(n)(d) then join^{τ} (m)(f(d)) else f(d) fip

for all n, m ∈ ℕ. If [ε_{n}^{σ}, ε_{m}^{τ}] ↑ f then sjoin(⟨n, m⟩)(f) = [ε_{n}^{σ}, ε_{m}^{τ}] ⊔ f as can be seen from the following case analysis

i) if ε_{n}^{σ} ⊑ d then sjoin(⟨n, m⟩)(f)(d) = ε_{m}^{τ} ⊔ f(d) = ([ε_{n}^{σ}, ε_{m}^{τ}] ⊔ f)(d) ii) if ε_{n}^{σ} ↑ d but not ε_{n}^{σ} ⊑ d then ε_{m}^{τ} ↑ f(d) and below^{σ}(n)(d) = ⊥ and,

thus, we have sjoin(⟨n, m⟩)(f)(d) = join^{τ} (m)(f(d)) ⊓ f(d) = f(d) = ([ε_{n}^{σ}, ε_{m}^{τ}] ⊔ f)(d) because f(d) ⊑ ε_{m}^{τ} ⊔ f(d) = join^{τ} (m)(f(d)) as guaranteed by ε_{m}^{τ} ↑ f(d) and the induction hypothesis for join^{τ}

iii) if ε_{n}^{σ}#d then sjoin(⟨n, m⟩)(f)(d) = f(d) = ([ε_{n}^{σ}, ε_{m}^{τ}] ⊔ f)(d).

Now join^{σ→τ} is PCF definable from sjoin putting

join^{σ→τ} (n)(f)(d) = ifz(b^{σ→τ} (n), f(d), sjoin(δ(n))(join^{σ→τ} (ρ(n))(f))(d))

118 Domain-theoretic foundations of functional programming

where b^{σ→τ} is a recursive function deciding ε_{n}^{σ→τ} = ⊥ and δ and ρ are recursive functions such that for n ≠ 0, δ(n) is the least element of e_{n} and e_{ρ(n)} = e_{n}\{δ(n)}.

For defining up^{σ} first consider the PCF^{++} term

enum_{1}^{σ} ≡ λf:ι→ι.Y(Φ_{σ})(λk:ι.join^{σ}(f(k)))

where Φ_{σ} is defined as above. Obviously, if d ∈ D_{σ} and f ∈ D_{ι→ι} with {f(n) | n ∈ ℕ} = {n ∈ ℕ | ε_{n}^{σ} ⊑ d} then d = enum_{1}^{σ}(f). Let U be a PCF term of type ι→ι→ι such that {U(n) | n ∈ ℕ} is the set of all unary partial recursive functions.^{5} Then λx:ι.enum_{1}^{σ}(U(x)) enumerates Comp(D_{σ}, ε^{σ}). Thus, the PCF^{++} definable function

up^{σ→τ} (n)(m) = join^{σ→τ} (n)(enum_{1}^{σ→τ} (m))

satisfies the requirement formulated in (2).

Finally below^{σ→τ} can be defined as

below^{σ→τ} (n)(f) = ∀_{⟨i,j⟩∈e_{n}}∀(λk:ι. below^{τ} (j)(f(up^{σ}(i)(k))))

where ∀ is the continuous universal quantifier of Lemma 13.14 and the quantification over e_{n} can be expressed in terms of pand (as introduced in the proof of Lemma 13.13). As below^{τ} and up^{σ} are PCF^{++} definable by induction hypothesis the function below^{σ→τ} is PCF^{++} definable as well. □

See pp. 250-251 of [Plotkin 1977] for a syntactic argument showing that ∃ is not PCF^{+} definable. That already PCF^{+} suffices for denoting all compact elements of the Scott model we consider rather as a mere curiosity. But the following two facts one certainly should remember.

• The Scott model is not fully abstract for PCF as the latter lacks parallel features.

• If one adds por and ∃ to PCF, i.e. extensional parallel features providing all the benefits of dove tailing, then one can denote all computable elements of the Scott model, i.e. the language PCF^{++} is universal for the effective Scott model Dom_{eff}.

5where a unary partial function f on ℕ is identified with the element f̃ ∈ D_{ι→ι} defined as

f̃(x) = \{ \begin{matrix}f(x) & if x ∈ ℕ and f(x)↓ \\ ⊥ & otherwise \end{matrix}

Computability in Domains 119

The above universality theorem has been extended to PCF^{++} with recursive types in [Streicher 1994] by showing that every recursive type appears as a PCF^{++} definable retract of the type ι→ι.^{6} However, it is an open problem whether in the category S of sequential domains there is a PCF type υ such that every (recursive) type appears as PCF definable retract of υ.

As we have seen there is a smooth notion of computability for Scott domains. When trying to achieve something similar for the sequential domains (introduced in Chapter 11) one runs into the following problems.

Consider the projections π_{1}, π_{2} : Σ × Σ → Σ (where Σ is the 2-element lattice {⊥, ⊤}). Then in any sequential model the pointwise supremum π_{1} ⊔ π_{2} does not exist as it is the inherently parallel supremum operation ∨ : Σ×Σ → Σ. The only (pointwise) upper bound of π_{1} and π_{2} in a sequential model is the constant map with value ⊤. Thus, in order extensional sequential models suprema in function spaces are not pointwise. Moreover, it follows from [Loader 2001] that already in the fully abstract model for finitary PCF, i.e. over base type bool, where all elements are compact, it is not decidable whether an element is the supremum of a finite set of elements.

Any attempt to develop a notion of computability for sequential domains is hampered by the following observation. Let K be a non-recursive, but r.e. set of natural numbers (e.g. K = {n ∈ ℕ | {n}(n)↓}). For every n ∈ ℕ consider the function f_{n} : Σ → [ℕ→Σ] defined as

f_{n}(u) = \{ \begin{matrix}ℕ & if u = ⊤ \\ \{k ∈ K | k < n\} & otherwise. \end{matrix}

Obviously, each f_{n} is sequential and computable as it can be implemented e.g. by an obvious ML program of type unit−>nat−>unit. The sequence (f_{n})_{n∈ℕ} is effective and ascending w.r.t. the extensional order but, nevertheless, its limit f = ⨆ f_{n} as given by

f(u) = \{ \begin{matrix}ℕ & if u = ⊤ \\ K & otherwise \end{matrix}

6Thus, in case of the effective Scott model, i.e. higher type computability in the sense of recursion theory, higher types are just a “figure of speech” because they can all be simulated within ι→ι, i.e. the partial recursive functions (together with all constant functions). Nevertheless, higher types are very convenient from a “stylistic” point of view.

120 Domain-theoretic foundations of functional programming

is not sequentially computable since

f(u)(n) = ⊤ iff n ∈ K ∨ u=⊤

and the right hand side obviously requires parallel evaluation. Thus, for sequential domains the computable elements are not closed under suprema of effective chains of effective elements.

However, via realizability one may construct universal models for sequential languages (even with recursive types), see [Rohr 2002].^{7}

But for the stable model of PCF (see [Amadio and Curien 1998]) a notion computability has been successfully developed by A. Asperti in [Asperti 1990]. This is possible because the sequence (f_{n})_{n∈ℕ} considered above is not increasing w.r.t. the stable ordering.

We conclude this chapter with some more recursion theoretic considerations.

Principal Numberings and the Myhill-Shepherdson Theorem

For an effectively given domain we will define a notion of principal numbering of Comp(D, ε) which in a certain sense will be optimal. For this purpose recall the Gödel numbering W of r.e. sets of natural numbers where

W_{e} = {n ∈ ℕ | {e}(n)↓}

see e.g. [Rogers 1987].

Definition 13.15 (principal numbering) Let (D, ε) be an effectively given domain. A principal numbering of (D, ε) is a surjective function ζ : ℕ → Comp(D, ε) such that there exist total recursive functions f and g satisfying the conditions

(ζ1) W_{f(n)} = {k ∈ ℕ | ε_{k} ⊑ ζ(n)} (ζ2) ζ(g(n)) = ⨆ ε[W_{n}] whenever ε[W_{n}] is directed.

7See also John Longley’s treatise [Longley 2002] on Sequentially Realizable Functionals where he constructs a universal model for PCF+H where H is a non-order-extensional but sequential constant of type 2 having a somewhat complicated operational semantics.

Longley’s sequentially realizable functionals are equivalent to the extensional collapse of Curien’s Sequential Algorithms (see [Amadio and Curien 1998]) providing a nonextensional model for PCF.

But notice that this notion of sequentiality is more liberal than the one arising from PCF definability as studied in this book.

Computability in Domains 121

A computable numbering is a surjective map ν : ℕ → Comp(D, ε) for which there exists a total recursive function h with W_{h(n)} = {k ∈ ℕ | ε_{k} ⊑ ν(n)} for all n ∈ ℕ. ♢

Obviously, for every computable numbering ν of Comp(D, ε) there exists a total recursive function t with ζ ∘t = ν (namely t = g∘h). On computable numberings one may consider the following preorder

ν_{1} ⪯ ν_{2} iff there exists a total recursive h with ν_{2} ∘ h = ν_{1}.

Obviously, a principal numbering is a greatest (w.r.t. ⪯) computable numbering from which it is immediate that principal numberings are unique up to recursive reindexing, i.e. whenever ζ and ζ′ are principal numberings then ζ ∘ f = ζ′ and ζ ∘ g = ζ for some total recursive functions f and g.^{8} We leave it as an exercise(!) for the inclined reader to verify that for every effectively given domain there does actually exist a principal numbering of its computable elements.

Next we consider a notion of semidecidable subsets for effectively given domains.

Definition 13.16 (extensionally r.e.) A subset P ⊆ Comp(D, ε) is called extensionally recursively enumerable (e.r.e.) iff {n ∈ ℕ | ζ_{n} ∈ P } is r.e. where ζ is some principal numbering of Comp(D, ε). ♢

Theorem 13.17 (Rice-Shapiro) For every e.r.e. subset P ⊆ Comp(D, ε) it holds that

(1) for every d ∈ P there exists an e ∈ K(D) ∩ P with e ⊑ d

(2) if d ∈ P and d ⊑ d′ ∈ Comp(D, ε) then d′ ∈ P as well.

Proof. Let ζ be a principal numbering of Comp(D, ε) and f and g be total recursive functions satisfying the requirements (ζ_{1}) and (ζ_{2}) of Def. 13.15. ad (1) : If d is compact then one may take for e the element d itself. Suppose that d is not compact. For the sake of deriving a contradiction suppose that e ∉ P for all compact e ⊑ d. As by assumption d ∈ Comp(D, ε) there exists a r.e. set A such that ε[A] is a chain in D with supremum d. Let h be a total recursive function such that for all n ∈ ℕ

W_{h(n)} = {m ∈ A | ∀k ≤ m. ¬T (n, n, k)}

8cf. the admissible numberings of partial recursive functions as introduced and studied in [Rogers 1987]

122 Domain-theoretic foundations of functional programming

where T is Kleene’s T -predicate (see e.g. [Rogers 1987]). Obviously, for every n ∈ ℕ the set ε[W_{h(n)}] is a chain in D and thus its supremum is ζ_{g(h(n))}. Now for all n ∈ ℕ we have {n}(n)↑ iff ⨆ ε[W_{h(n)}] = d, i.e.

n ∉ K iff ζ_{g(h(n))} ∈ P

where K = {n ∈ ℕ | {n}(n)↓}. As P is e.r.e. the complement of K is r.e. in contradiction to the well-known undecidability of the r.e. set K (see [Rogers 1987]). ad (2) : Suppose d ∈ P and d ⊑ d′ ∈ Comp(D, ε). W.l.o.g. assume that d ≠ d′. Due to the already established condition (1) there exists an e ∈ K(D)∩P with e ⊑ d. Let A be a r.e. set such that ε[A] is a chain in D with supremum d′. W.l.o.g. assume that e = ε_{i_{0}} for some i_{0} ∈ A. The partial function

h̃(n, k) = \{ \begin{matrix}0 & if (n ∈ K ∧ k ∈ A) ∨ k = i_{0} \\ ↑ & otherwise \end{matrix}

is obviously partial recursive. Thus, there exists a total recursive function h with

W_{h(n)} = {k ∈ ℕ | h̃(n, k)↓}

for all n ∈ ℕ. Now if d′ ∉ P then we have

n ∉ K iff W_{h(n)} = {i_{0}} iff ζ_{g(h(n))} ∈ P

rendering the complement of K r.e. (since P is .r.e.) in contradiction with the undecidability of the halting problem. □

Notice that the Rice-Shapiro theorem can be rephrased as follows: e.r.e. subsets of Comp(D, ε) are open (w.r.t. the subspace topology on Comp(D, ε) induced by the Scott topology on D). It is a straightforward exercise(!) to show that an open subset U of Comp(D, ε) is e.r.e. provided {n ∈ ℕ | ε_{n} ∈ U} is r.e.

A fairly immediate consequence of the Rice-Shapiro theorem is the Myhill-Shepherdson Theorem whose formulation, however, requires the following notion.

Definition 13.18 (effective morphism of e.g. domains) A function f : Comp(D_{1}, ε^{(1)}) → Comp(D_{2}, ε^{(2)}) is called an effective morphism iff there exists a total recursive function h with ζ^{(2)} ∘ h = f ∘ ζ^{(1)},

Computability in Domains 123

i.e. making the diagram

ℕ  \overline{h} ℕ

[figure: Comp(D_{1}, ε^{(1)}); ζ^{(1)}; f; Comp(D_{2}, ε^{(2)}); ζ^{(2)}]

commute, where the ζ^{(i)} are principal numberings of Comp(D_{i}, ε^{(i)}). ♢

The Myhill-Shepherdson theorem says that every effective morphism of e.g. domains is Scott continuous (i.e. continuous w.r.t. the subspace topologies induced by the Scott topologies).

Theorem 13.19 (Myhill-Shepherdson) Every effective morphism f : Comp(D_{1}, ε^{(1)}) → Comp(D_{2}, ε^{(2)}) is monotonic and whenever f(d) ⊒ e_{2} ∈ K(D_{2}) then there exists an e_{1} ∈ K(D_{1}) with f(e_{1}) ⊒ e_{2} and e_{1} ⊑ d.

Proof. Suppose d ∈ Comp(D_{1}, ε^{(1)}) and e_{2} ∈ K(D_{2}) with e_{2} ⊑ f(d). The set A_{2} = {n ∈ ℕ | e_{2} ⊑ ζ_{n}^{(2)}} is r.e. from which it follows (as f is effective) that the set A_{1} = {m ∈ ℕ | e_{2} ⊑ f(ζ_{m}^{(1)})} is also r.e. Thus, the set {d ∈ Comp(D_{1}, ε^{(1)}) | e_{2} ⊑ f(d)} is e.r.e. and contains d as an element from which it follows by Theorem 13.17(1) that there exists a compact e_{1} ⊑ d with e_{2} ⊑ f(e_{1}).

It remains to show that f is monotonic. For that purpose suppose d_{1}, d_{2} ∈ Comp(D_{1}, ε^{(1)}) with d_{1} ⊑ d_{2}. Suppose e_{2} ∈ K(D_{2}) with e_{2} ⊑ f(d_{1}). As f is effective the set {d ∈ Comp(D_{1}, ε^{(1)}) | e_{2} ⊑ f(d)} is e.r.e. and contains d_{1} as an element. From Theorem 13.17(2) it follows that e_{2} ⊑ f(d_{2}). As this implication holds for all e_{2} ∈ K(D_{2}) we conclude that f(d_{1}) ⊑ f(d_{2}) as desired. □

This gives rise to the following characterisation of effective morphims.

Theorem 13.20 A function f : Comp(D_{1}, ε^{(1)}) → Comp(D_{2}, ε^{(2)}) is an effective morphism if and only if f = f̄↾Comp(D_{1}, ε^{(1)}) for a (unique) continuous function f̄: D_{1} → D_{2} computable w.r.t. ε^{(1)} and ε^{(2)}.

Proof. An effective morphism f : Comp(D_{1}, ε^{(1)}) → Comp(D_{2}, ε^{(2)}) is Scott continuous by Theorem 13.19. Moreover, the set {⟨n, m⟩ | ε_{m}^{(2)} ⊑ f(ε_{n}^{(1)})} is r.e. as there is a recursive function h with ζ_{h(n)}^{(1)} = ε_{n}^{(1)} for all n ∈ ℕ. Take for f̄ the unique continuous function whose (Scott) graph is {⟨n, m⟩ | ε_{m}^{(2)} ⊑ f(ε_{n}^{(1)})}, i.e. f̄(d) = ⨆{ε_{m}^{(2)} | ε_{n}^{(1)} ⊑ d and ε_{m}^{(2)} ⊑ f(ε_{n}^{(1)})}.

124 Domain-theoretic foundations of functional programming

For the reverse direction suppose f̄: D_{1} → D_{2} is continuous and computable w.r.t. ε^{(1)} and ε^{(2)}. Then the set A = {⟨n, m⟩ | ε_{m}^{(2)} ⊑ f̄(ε_{n}^{(1)})} is r.e. Let g be a total recursive function with W_{g(n)} = {k ∈ ℕ | ε_{k}^{(1)} ⊑ ζ_{n}^{(1)}} and h a total recursive function with ζ_{h(n)}^{(2)} = ⨆ ε^{(2)}[W_{n}] whenever ε^{(2)}[W_{n}] is directed. Obviously, the set B = {⟨n, m⟩ | ∃k. k ∈ W_{g(n)} ∧ ⟨k, m⟩ ∈ A} is r.e. as well. Thus, there exists a total recursive function b with W_{b(n)} = {m ∈ ℕ | ⟨n, m⟩ ∈ B}. Then for the restriction f = f̄↾Comp(D_{1}, ε^{(1)}) it holds that f(ζ_{n}^{(1)}) = ζ_{h(b(n))}^{(2)} for all n ∈ ℕ, i.e.

f ∘ ζ^{(1)} = ζ^{(2)} ∘ h ∘ b

from which it follows that f is an effective morphism since h∘b is recursive.

As a continuous function on a Scott domain is uniquely determined by its behaviour on compact elements the function f̄ is uniquely determined by f since compact elements are in particular computable. □

Thus, we have established a 1-1-correspondence between computable continuous maps and effective morphisms which generalizes the Myhill-Shepherdson theorem for effective operations and operators as discussed in [Rogers 1987] to effectively given domains.

Moreover, one easily checks (exercise!) that e.r.e. subsets of Comp(D, ε) are in 1-1-correspondence with effective morphisms from (D, ε) to the socalled Sierpinski space Σ = {⊥, ⊤} w.r.t. the effective presentation ε^{Σ}(0) = ⊥ and ε^{Σ}(n+1) = ⊤. This analogy between topological and recursiontheoretic notions was D. Scott’s main motivation for his Domain Theory and lies at the heart of so-called Synthetic Domain Theory (SDT) introduced around 1990 independently by Martin Hyland in [Hyland 1990] and Paul Taylor in [Taylor 1991]. SDT aims at axiomatizing domains as particular sets within constructive higher order logic or set theory. This slogan of domains as particular sets was promoted by D. Scott during the 1980ies and finally taken up by Hyland and Taylor. See [Simpson 2004; Reus and Streicher 1999] for an up-to-date account of SDT.

Bibliography

S. Abramsky, R. Jagadeesan, P. Malacaria Full Abstraction for PCF Inform. and

Comput. 163, no. 2, 409–470 (2000). R. Amadio and P.-L. Curien Domains and λ-Calculi. Cambridge Univ. Press

(1998). A. Asperti Stability and computability in coherent domains. Inform. and Com-

put. 86, no. 2, 115-139 (1990). H. Barendregt The Lambda Calculus. Its Syntax and Semantics. North Holland

(1981). M. Barr and Ch. Wells Category theory for computing science. Prentice Hall

International (1990). G. Berry Modèles complètement adéquats et stables des lambda calculs typés Thése

d’ Etat, Université Paris 7 (1979). M. .H. Escardó PCF extended with real numbers: a domain-theoretic approach to

higher-order exact real number computation. PhD Thesis, Imperial College, Univ. of London (1997).

E. Griffor, I. Lindström and V. Stoltenberg-Hansen Mathematical Theory of

Domains. Cambridge Univ. Press (1994). J. M. E. Hyland First steps in synthetic domain theory. in Category Theory

(Como 1990) pp.131–156, Lecture Notes in Math. 1488 Springer, Berlin, 1991.

M. Hyland, L. Ong On Full Abstraction for PCF: I,II and III. Inform. and

Comput. 163, no. 2, pp.285–408 (2000). A. Kanda, D. Park When are two effectively given domains identical? pp.

563–577, LNCS 67, Springer, Berlin-New York, 1979. U. de’Liguoro PCF definability via Kripke logical relations (after O’Hearn and

Riecke) Lab. Inf. ENS, Report LIENS-96-7, Paris (1996). R. Loader Finitary PCF is not decidable TCS 266, no. 1-2, pp. 341-364 (2001). J. Longley Sequentially Realizable Functionals APAL 117, no. 1-3, pp. 1-93

(2002). S. MacLane Categories for the Working Mathematician Second edition. Graduate

Texts in Mathematics 5, Springer (1998). M. Marz A Fully Abstract Model for Sequential Computation PhD Thesis, TU

126 Book Title

Darmstadt (2000) electronically available from

www.mathematik.tu-darmstadt.de/~streicher/THESES/marz.ps.gz

G. McCusker Games and full abstraction for a functional metalanguage with recursive types. CPHC/BCS Distinguished Dissertations, Springer Verlag London (1998).

R. Milner Fully Abstract Models of Typed λ-Calculi TCS 4, pp. 1-22 (1977). D. Normann On sequential functionals of type 3 to appear in Math. Struct. Com-

put. Sc. as part of a Festschrift for K. Keimel (2006). G. Plotkin LCF considered as a programming language TCS 5, pp. 223-255

(1977). G. Plotkin 𝕋^{ω} as a universal domain J. Comput. System Sci. 17 (1978), no. 2,

209–236. P. O’Hearn, J. Riecke Kripke logical relations and PCF Inf. and Comp. 120,

no. 1, pp. 107-116 (1995). B. Reus, T. Streicher General synthetic domain theory—a logical approach.

Math. Structures Comput. Sci. 9, no. 2, pp. 177–223 (1999). J. Riecke, A. Sandholm A relational account of call-by-value sequentiality Inf. and

Comp. 179, no. 2, pp. 296-331 (2002). H. Rogers jr. Theory of recursive functions and effective computability. 2^{nd}

edition, MIT Press, Cambridge, MA, 1987. A. Rohr A Universal Realizability Model for Sequential Computation. PhD Thesis,

TU Darmstadt (2002) electronically available from

www.mathematik.tu-darmstadt.de/~streicher/THESES/rohr.ps.gz

Dana S. Scott A type-theoretical alternative to ISWIM, CUCH, OWHY unpublished paper from 1969 reprinted in Böhm Festschrift TCS 121 No.1-2, pp. 411-440 (1993).

Dana S. Scott Relating theories of the λ-calculus in To H. B. Curry: essays on combinatory logic, lambda calculus and formalism pp. 403-450 Academic Press, London-New York (1980).

K. Sieber Reasoning about sequential functions via logical relations in Applications of category theory in computer science pp.258–269 London Math. Soc. Lecture Note Ser., 177, CUP (1992).

A. Simpson Computational Adequacy for Recursive Types in Models of Intuition-

istic Set Theory. Ann. Pure Appl. Logic 130, no. 1-3, pp. 207–275 (2004). A. Stoughton Equationally fully abstract models of PCF Proc. of Fifth Interna-

tional Conference on the Mathematical Foundations of Computer Science Springer Lecture Notes in Comput. Sci. 442, pp.271–283 (1990)

T. Streicher A universality theorem for PCF with recursive types, parallel-or and

∃. Math. Struct. Comput. Sc. 4, no. 1, pp.111-115 (1994). T. Streicher, B. Reus Classical logic, continuation semantics and abstract ma-

chines. J. Funct. Programming 8 (1998), no. 6, 543–572. P. Taylor The fixed point property in synthetic domain theory. in Proc. 6th IEEE

Symposium on Logic in Computer Science, pp.152-160 (1991). G. Winskel The formal semantics of programming languages. An introduction.

MIT Press, Cambridge MA (1993).

Index

N, 98 N-structure, 87 R_{∞}, 83 K, 67 K_{a}, 67 Comp(D, ε), 108 Λ-category, 85 Ω, 42 Prg_{σ}, 26 S, 97 α-conversion, 22 ⊏ ∼, 27 Dom_{eff}, 109 ≤, 52 ˙∪, 90 < ∼, 27 ⊕, 69 ⊗, 69 ∘→, 69

admissible, 39, 61 arity (varying), 97

bifree solution, 74 bigstep semantics, 23 boolean values, 24 bounded complete, 71

call-by-name, 29 call-by-value, 29 capture-free substitution, 22 closure, 28 coherently complete, 72 compact element (of a cpo), 67 computable element, 108 computable maps, 109 computational adequacy, 14, 49 continuation, 28 correctness, 14 countably algebraic, 71 cpo, 34

directed, 34 domain, 34 domain equation, 73 dove tailing, 56

effective morphism, 122 effective Scott model, 111 effectively given domain, 108 embedding/projection pair, 75 environment, 28 environment machine, 28 equationally fully abstract, 53 exponential, 35 extensional, 88 extensionally r.e., 121

fixpoint (least), 37 full abstraction, 15 full abstraction for PCF^{+}, 112 fully abstract, 53

global elements, 87

128 Book Title

graph model, 84

ideals (order-theoretic), 67 interpretation, 41 inverse limit, 76

Kripke logical relation, 97

LCF, 42 lifting, 69 locally continuous, 73 logical relation, 45, 59 logical relation of arity (w, S), 97

Main Lemma for R, 47 Milner model, 93 Milner’s Context Lemma, 51 Myhill-Shepherdson Theorem, 123

numeral, 23

oracles, 112 order extensional, 88

parallel conditional, 113 partial partition, 95 PCF, 21 PCF model, 89 PCF terms, 21 PCF types, 21 pcpo, 34 pointwise, 35 predomain, 34 prefixpoint, 37 principal numbering, 120

R-invariant, 60 Rice-Shapiro Theorem, 121

Scott continuous, 34 Scott domain, 70 Scott model (for PCF), 39 separated sum, 70 sequential, 56 sequential algorithms, 120 sequentially realizable functionals,

120 single step semantics, 25 ssp, 95 stable, 54 step functions, 108, 114 strict, 34 subject reduction, 24 Synthetic Domain Theory, 124

type contexts, 21

types, 21

Typing rules, 22

unfolding, 42 universality, 17 universality of PCF^{++}, 112

values, 24