Logical Full Abstraction and PCF

John Longley  Gordon Plotkin^{∗}

Abstract

We introduce the concept of logical full abstraction, generalising the usual equational notion. We consider the language PCF and two extensions with “parallel” operations. The main result is that, for standard interpretations, logical full abstraction is equivalent to equational full abstraction together with universality; the proof involves constructing enumeration operators. We also consider restrictions on logical complexity and on the level of types.

1 Introduction

The study of denotational semantics seeks to provide mathematical descriptions of programming languages by giving denotations of programs in terms of previously understood mathematical structures. For example, if P is a program that takes an input and produces an output, we might take its denotation to be a function from a set of input-values to a set of output-values. The most widely-known approach to denotational semantics is that of traditional domain theory, see e.g., Plotkin (1977), where the mathematical structures involved are certain kinds of complete partial order (cpo). Other kinds of mathematical structure have also been used successfully—for a selection of different approaches see Abramsky, Jagadeesan and Malacaria (1994), Longley (1995) and O’Hearn and Riecke (1995).

One of the principal aims of denotational semantics is to deepen our understanding of the logic of programming languages, and to provide conceptual and mathematical tools for reasoning about programs. A more specific goal is to provide mathematical foundations for “program logics” of a kind that could be used by ordinary programmers.

Denotational semantics can be used to establish relationships between a programming language L and a logic J. By giving interpretations of both L and J in some common mathematical structure M, we may be able to show that if certain theorems are provable in the logic then certain properties of programs hold—for example, that if the sentence P (3) = 5 is provable in J then the program P (3) returns the answer 5. Such a result would show that the logic J was indeed useful for proving certain facts about programs in L.

∗To appear in J. Ginzburg, ed., Tbilisi Symposium on Language, Logic and Computation, SiLLI/CSLI Publications, 1997.

In this kind of situation we have a way of directly understanding the meaning of certain simple sentences of J (e.g., P (3) = 5) as statements about computations in L. One is then prompted to ask whether one could extend this to all sentences of the logic, and give an interpretation of J purely in terms of the language L and its evaluation rules, without reference to the structure M. For example, one might interpret quantifiers as ranging over closed programs or terms of appropriate type. We might call this an operational interpretation of J, in contrast to its denotational interpretation in M. Besides the intrinsic interest of such an interpretation, it seems likely that an operational interpretation would be more easily grasped by a non-specialist than a denotational one.

Now, given a logic J with both an operational interpretation in terms of L and a denotational interpretation in M, it is natural to ask whether these “agree” in the sense that a sentence is true under one interpretation if and only if it is true under the other. In this case, we will say that the interpretation of L in M is logically fully abstract (or LFA) for J. A logically fully abstract interpretation can be used to show that all sentences provable in J express true facts about L under the operational interpretation. Note that the familiar notion of (equational) full abstraction can be seen as a special case of logical full abstraction: consider a logic J whose only assertions are equations between terms of L, and whose operational interpretation is “observational equivalence”.

Both the general concept and the name “logical full abstraction” are due to the second author, though the idea was first worked out in the first author’s Ph.D. thesis, see Longley (1995). The idea as we have outlined it above is of course extremely general, as it depends not only on L and J but also on the kinds of operational and denotational interpretation we have in mind. The aim of the present paper is to illustrate the basic idea by discussing one particular kind of logical full abstraction, in the context of a simple logic for the prototypical functional language PCF, see Plotkin (1977) and Curien (1993). We anticipate that the study of other notions of logical full abstraction (whether for PCF or other languages) will prove a very interesting area for further research.

The study of equational full abstraction commonly results in theories of extensional objects, often of functions and data structures; these objects have a natural mathematical structure, perhaps of order-theoretic, topological or algebraic character. The study here of logical full abstraction results rather in intensional concerns, such as the study of definability and so of computability. These distinctions harken back to Scott’s original explicit choice—see Scott (1970) and Scott and Strachey (1971)—to investigate first extensional theories and only then to consider questions of computability and of the relation with symbolic computation. They also bring to mind the much more recent programme of synthetic domain theory, where one tries to integrate the different approaches by working in, for example, the effective topos, see Hyland (1990). One should also remark that intensional aspects may nonetheless play a role in the study of equational full abstraction—see the studies of games in Abramsky, Jagadeesan and Malacaria (1994) and Hyland and Ong (1995).

The rest of the paper is structured as follows. In Section 2 we review the definitions of the three versions of PCF that we will consider. We also define the syntax of a program logic for these languages, and propose a simple operational interpretation of this logic. In Section 3 we introduce a very general notion of denotational interpretation for our languages, and show how such an interpretation gives rise to a denotational interpretation of the logic. We thus obtain a notion of logical full abstraction. In Section 4 we prove the main result of the paper: a standard interpretation is LFA if and only if it is both equationally fully abstract (EFA) and universal (meaning, roughly, that every element of the model is definable). We end in Section 5 with a few further observations, and mention some open questions and some avenues for future investigation. In particular, we consider restrictions on logical complexity and on the level of types. For example, it follows from our main theorem that a standard interpretation is LFA iff it is Π_{2}-LFA (i.e., LFA for Π_{2}-sentences). There are standard interpretations which are EFA, but not Π_{1}-LFA; it is an open question whether there are any interpretations which are Π_{1}-LFA but not Π_{2}-LFA.

2 PCF and its Logic

PCF is an extension of the simply-typed λ-calculus with arithmetic operators and general recursion. It can be regarded as a prototypical “sequential” functional language; an understanding of PCF is thus an important step towards an understanding of modern functional languages such as Haskell, Miranda and ML. We begin by reviewing the syntax and evaluation rules for PCF, and for two extensions, PCF^{+} and PCF^{++}, obtained by adding “parallel” operations. All three of these languages appear essentially in Plotkin (1977); the formulations here differ in two inessential respects: one is the absence of a Boolean type; the other is the use of a “parallel-or” constant rather than a parallel conditional, for which see Stoughton (1991).

The types of PCF are built up from a single ground type ι (the natural numbers) using the right-associative binary type constructor →; we write M : σ to mean “M is a term of type σ”. For each type σ we have a countably infinite set of variables of type σ, ranged over by x^{σ}, y^{σ}, z^{σ}, …; we also have the following collection of constants:

0, 1, 2, …: ι,  cond : ι → ι → ι → ι,
succ , pred : ι → ι,  Y_{σ} : (σ → σ) → σ.

The terms of PCF are built up from the variables and constants as usual in the simply-typed λ-calculus:

• if M:τ, then (λx^{σ}.M):σ → τ;

• if M:σ → τ and N:σ, then (MN):τ.

We often omit unnecessary parentheses, treating juxtaposition as a left-associa-tive operator; we also omit type superscripts on variables, when this causes no ambiguity. We identify terms up to change of bound variables (that is, α-conversion); we write M[N_{1}/x_{1}^{σ_{1}}, …, N_{n}/x_{n}^{σ_{n}}] for the capture-avoiding simultaneous substitution of the terms N_{1} :σ_{1}, …, N_{n}:σ_{n} for x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} in M.

An environment is a finite non-repetitive list x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} of variables (where n ≥ 0); the empty environment is written ⟨⟩. We say that M is a term of type σ in environment Γ (and write Γ ⊢ M : σ) if M : σ and all the free variables of M occur in Γ. If x^{σ} is a variable not in Γ, we write Γ, x^{σ} for the environment obtained by appending x^{σ} to Γ.

The evaluation rules for PCF are given by defining a notion of reduction (or rewriting) on closed terms. Specifically, we inductively define a binary relation M → N on closed terms of the same type as follows (here n ranges over the numerals 0, 1, 2, …):

• (λx^{σ}.M)N → M[N/x^{σ}];

• succ n → (n + 1), pred (n + 1) → n, pred 0 → 0, cond 0 NP → N, cond (n + 1)NP → P, Y_{σ}M → M(Y_{σ}M);

• if M → M′ then MN → M′N;

• if M → M′:ι then succ M → succ M′, pred M → pred M′, cond MNP → cond M′NP.

We think of → as a “one-step reduction relation”; we write →^{+} for its transitive closure, and →^{∗} for its transitive reflexive closure. We say that a term M:ι terminates if M →^{∗} n for some (necessarily unique) numeral n.

The language defined above is intuitively “sequential”—no two subterms of a term are ever evaluated “in parallel”. We now introduce two extensions of PCF including parallel operators. The language PCF^{+} is defined in the same way as PCF except that we add an extra constant por : ι → ι → ι (“parallel-or”), together with the reduction rules:

• por 0M → 0, por M0 → 0, por (m + 1)(n + 1) → 1;

• if M → M′:ι then por MN → por M′N, por NM → por NM′.

The syntax of PCF^{++} is defined in the same way as PCF^{+}, except that we add a further constant exists : (ι → ι) → ι (“existential quantification”). Its reduction rules are those for PCF^{+} together with the following, writing Ω_{σ} for Y_{σ}(λx^{σ}.x):

• if Mn →^{+} 0 for some n, then exists M → 0;

• if MΩ_{ι} →^{+} m + 1, then exists M → 1.

We say that a one-step reduction M → M′ is deterministic if whenever M → M′′ then M′ = M′′, and write M →_{d} M′ for this relationship. Note that whereas for PCF every one-step reduction is deterministic, this is not so for PCF^{+} and PCF^{++}. Nevertheless, in all these languages evaluation is deterministic: if M →^{∗} n and M →^{∗} n′ then n = n′. (In fact the more general Church-Rosser Property holds, that if M →^{∗} N_{i}, for i = 1, 2, then for some P, N_{i} →^{∗} P, for i = 1, 2).

We need some standard notions. Suppose L is one of the three languages PCF, PCF^{+} or PCF^{++}. A (one-place) term context C[ ] of L is a term of L with zero or more holes, to be filled by a term of appropriate type. Two terms M, M′: σ are observationally equivalent (and we write M ≈ M′) if for all term contexts C[ ] such that C[M], C[M′] are closed terms of type ι we have C[M] →^{∗} n iff C[M′] →^{∗} n. The Context Lemma characterises this equivalence. When M and M′ are both closed, the lemma asserts that for σ = σ_{1} → ⋯ → σ_{h} → ι, M ≈ M′ iff for all closed terms N_{1} : σ_{1}, …, N_{h} : σ_{h} and numerals n, MN_{1} … N_{h} →^{∗} n iff M′N_{1} … N_{h} →^{∗} n (a more general version for open terms is easily derived). An operational proof of the Context Lemma for PCF can be found in Milner (1977) and Curien (1993), and similar proofs can be obtained for PCF^{+} and PCF^{++}; for these latter two languages it is also a consequence of the facts that the usual cpo model is adequate and that all finite elements are definable (see Section 3 below for a definition of adequacy). Operational soundness (that is, if M →^{∗} N then M ≈ N) is a consequence of the Context Lemma, together with the Church-Rosser Property.

Now that we have defined the languages of interest, we introduce the syntax of a simple many-sorted program logic J_{L}, much in the spirit of LCF, see Gordon, Milner and Wadsworth (1978). We believe that this is the kind of logic that would in principle be useful for specifying and proving properties of programs. The sorts of J_{L} are the types of L; the expressions of sort σ in J_{L} are precisely the terms of type σ in L; and the logical variables of sort σ are just the term variables of type σ. The syntax of the formulae of J_{L} is as follows (here M, N are expressions of the same type and P:ι):

ϕ ::= ⊥ | M = N | P ⇓ | ϕ_{1} ∧ ϕ_{2} | ϕ_{1} ∨ ϕ_{2} | ϕ_{1} ⊃ ϕ_{2} | ∀x^{σ}.ϕ_{1} | ∃x^{σ}.ϕ_{1}.

Note that J_{L} is really a many-sorted first-order logic—we have a separate ground sort for each type σ. We identify formulae up to change of bound variables (αconversion); we write ϕ[N_{1}/x_{1}^{σ_{1}}, …, N_{n}/x_{n}^{σ_{n}}] for capture-avoiding simultaneous substitution into formulae (where N_{1} : σ_{1}, …, N_{n} : σ_{n}). We will not be specific here about the axioms and inference rules of J_{L}, however we essentially have in mind those of classical first-order logic.

Next we give a simple operational interpretation of J_{L}; this gives us a way of translating formulae into statements about computations in L. We define a relation ⊧_{op} ϕ (read “ϕ is operationally true”) on sentences (i.e., closed formulae) of J_{L} as follows:

• ⊧_{op} ⊥ doesn’t hold;

• ⊧_{op} (M = N) iff M ≈ N;

• ⊧_{op} (P ⇓) iff P terminates;

• ⊧_{op} φ ∧ ψ iff ⊧_{op} φ and ⊧_{op} ψ;

• ⊧_{op} φ ∨ ψ iff ⊧_{op} φ or ⊧_{op} ψ;

• ⊧_{op} φ ⊃ ψ iff either |̸=_{op} φ or ⊧_{op} ψ;

• ⊧_{op} ∀x^{σ}.φ iff ⊧_{op} φ[M/x] for all closed M:σ;

• ⊧_{op} ∃x^{σ}.φ iff ⊧_{op} φ[M/x] for some closed M:σ.

We extend the relation ⊧_{op} to all formulae as follows: if ϕ has free variables among x_{1}, …, x_{n}, then ⊧_{op} ϕ iff ⊧_{op} ϕ[M_{1}/x_{1}, …, M_{n}/x_{n}] for all closed expressions M_{1}, …, M_{n} of appropriate types.

Notice that the notion of operational truth only requires concepts relating to L itself—we are thus hopeful that this interpretation of the logic would be readily understood by a non-specialist. However, we should point out that operational interpretations of the formulae of J_{L} other than the “classical” one we have given are possible—for an alternative (arguably more “computational”) interpretation, see Longley (1995), Section 8.2.

3 Denotational Interpretations of PCF

We now introduce a very general notion of denotational interpretation for our languages; it is convenient to use the language of category theory. Given a category C with finite products, we interpret types of L by objects of C, and terms of L by morphisms of C; we also need a semantic correlate of termination. We therefore say that an interpretation I of L in C is given by the following data:

• for each type σ an object I[[ σ]] of C (and for each environment Γ = x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} we write I[[ Γ ]] for I[[ σ_{1} ]] × ⋯ × I[[ σ_{n}]]);

• for each L-term M:σ in environment Γ a morphism I[[ Γ ⊢ M ]] from I[[ Γ ]] to I[[ σ]] (and if M is closed we write I[[ M ]] for I[[ ⟨⟩ ⊢ M ]]);

• a set T ⊂ Hom(1, I[[ ι]]) (to be thought of as the set of “fully defined” or “terminating” elements of I[[ ι]]).

We impose two requirements. First, for any environment Γ = x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} we require, for 1 ≤ i ≤ n, that I[[ Γ ⊢ x_{i}^{σ_{i}}]] : I[[ Γ ]] → I[[ σ_{i}]] be the evident projection. Second, we require that I be compositional in the following sense: if Γ = x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}}, Γ ⊢ M:τ and Δ ⊢ N_{i}:σ_{i}, for 1 ≤ i ≤ n, then

I[[ Δ ⊢ M[N_{1}/x_{1}, …, N_{n}/x_{n}] ]] = I[[ Γ ⊢ M ]] ∘ ⟨I[[ Δ ⊢ N_{1} ]], …, I[[ Δ ⊢ N_{n}]]⟩.

That is, tupling and composition in C corresponds to substitution in L.

This definition of interpretation for L is extremely weak (we do not require C to be cartesian-closed, for instance), but it suffices for our purposes. The most familiar concrete example is given by the category of cpos: all three of our languages have a canonical interpretation in this category, see Plotkin (1977).

The following concepts play a significant role:

• I is sound if M → M′ implies I[[ M ]] = I[[ M′]];

• I is adequate if for all closed M:ι we have I[[ M ]] = I[[ n]] iff M →^{∗} n;

• I is equationally fully abstract (EFA) if for all closed M, M′ : σ we have I[[ M ]] = I[[ M′]] iff M ≈ M′;

• I is atomically fully abstract (AFA) if it is EFA and for all closed M:ι we have I[[ M ]] ∈ T iff M terminates;

• I is universal if every morphism f : 1 → I[[ σ]] in C is definable (meaning that there is a closed term M:σ such that I[[ M ]] = f);

• I is standard if every morphism 1 → I[[ ι]] is definable and the set T of fully defined elements is {I[[ n]] | n is a numeral}.

Our definitions of equational full abstraction and universality are weak in that they involve only closed terms—in our general setting it is not possible to deduce the corresponding stronger facts for open terms (and arbitrary morphisms). However, the two notions of full abstraction coincide if the interpretation models β-conversion. Further, the two notions of universality coincide if the interpretation is cartesian-closed (by which we mean that the underlying category is cartesian closed, and that the higher-order types, λ-abstraction and application are interpreted accordingly—see Lambek and Scott (1986); this property implies that the interpretation models βη-conversion). It follows from operational soundness that any EFA interpretation is sound. Note that the usual interpretation in cpos is sound, adequate, standard and cartesian closed; it is AFA for PCF^{+} and PCF^{++} but not EFA for PCF, see Plotkin (1977).

Next we show how any interpretation I of L gives rise to a denotational interpretation of J_{L}. First some notation: For each type σ let S^{σ} be Hom(1, I[[ σ]]); we may think of S^{σ} informally as the set of “elements” of I[[ σ]]. For each environment Γ we also let S^{Γ} be Hom(1, I[[ Γ ]]). Then whenever Γ ⊢ M : σ we have the set-theoretic function I[[ Γ ⊢ M ]]∘ − : S^{Γ} → S^{σ}.

For any formula ϕ with FV(ϕ) ⊆ Γ, we can now define a subset [[ ϕ]]^{Γ} of S^{Γ}, corresponding intuitively to the set of tuples of elements for which the predicate ϕ holds:

• z ∈ [[ ⊥ ]]^{Γ} never;

• z ∈ [[ M = N ]]^{Γ} iff I[[ Γ ⊢ M ]] ∘ z = I[[ Γ ⊢ N ]] ∘ z;

• z ∈ [[ P ⇓]]^{Γ} iff I[[ Γ ⊢ P ]] ∘ z ∈ T;

• z ∈ [[ ϕ ∧ ψ]]^{Γ} iff z ∈ [[ ϕ]]^{Γ} and z ∈ [[ ψ]]^{Γ};

• z ∈ [[ ϕ ∨ ψ]]^{Γ} iff z ∈ [[ ϕ]]^{Γ} or z ∈ [[ ψ]]^{Γ};

• z ∈ [[ ϕ ⊃ ψ]]^{Γ} iff z ∉ [[ ϕ]]^{Γ} or z ∈ [[ ψ]]^{Γ};

• z ∈ [[ ∀x^{σ}.ϕ]]^{Γ} iff ⟨z, w⟩ ∈ [[ ϕ]]^{Γ,x^{σ}} for all w ∈ S^{σ};

• z ∈ [[ ∃x^{σ}.ϕ]]^{Γ} iff ⟨z, w⟩ ∈ [[ ϕ]]^{Γ,x^{σ}} for some w ∈ S^{σ}.

(in the last two cases, we assume—without loss of generality—that x^{σ} does not occur in Γ). We say that ϕ is denotationally true under the interpretation I (and write ⊧_{I} ϕ) if [[ ϕ]]^{Γ} is the whole of S^{Γ}, where Γ contains all the free variables of ϕ. In particular, if ϕ is closed then ⊧_{I} ϕ iff ∗ ∈ [[ ϕ]], where ∗ is the unique element of S^{⟨⟩} and we write [[ ϕ]] for [[ ϕ]]^{⟨⟩}.

Now that we have given both operational and denotational interpretations of J_{L}, we have a natural notion of logical full abstraction:

Definition 1 An interpretation I of L is logically fully abstract (LFA) if for all sentences ϕ of J_{L} we have ⊧_{op} ϕ iff ⊧_{I} ϕ. More generally, if F is a class of sentences of J_{L}, we say I is LFA for F if for all ϕ ∈ F we have ⊧_{op} ϕ iff ⊧_{I} ϕ.

Note that if an interpretation is LFA for a class of sentences, then it is also LFA for the Boolean closure of that class. The next lemma shows that such notions as adequacy^{1} and equational full abstraction can be recovered as special instances of logical full abstraction.

Proposition 2 Let I be an interpretation of L. Then

(i) I is EFA (respectively AFA) iff it is LFA for all sentences of the form M = N (respectively, and P ⇓);

(ii) I is adequate iff it is LFA for all sentences of the form P = n; (iii) Suppose that I is adequate. Then the definable elements of T are those

of the form I[[ n]] iff I is LFA for all sentences of the form P ⇓.

Proof (i) is immediate. For (ii), it suffices to note that, by the Context Lemma, P ≈ n iff P →^{∗} n for closed P : ι. For (iii), note that the condition on T is equivalent to the statement that for all closed P : ι, ⊧_{I} P ⇓ iff ⊧_{I} P = n for some n and also that the statement that I is LFA for all sentences of the form P ⇓ holds is equivalent to the statement that for all closed P : ι, ⊧_{I} P ⇓ iff ⊧_{op} P ⇓. But it is an easy consequence of adequacy and the Context Lemma that for all closed P:ι, ⊧_{I} P = n for some n iff ⊧_{op} P ⇓. □

1This observation is due to Eugenio Moggi.

The above lemma makes it clear that any EFA interpretation is adequate. Further, such an interpretation is AFA iff the definable elements of T are those of the form I[[ n]]. In particular, a standard EFA interpretation is AFA.

4 A characterization of LFA Interpretations

In this section we prove the following theorem characterizing LFA interpretations. This is the main result of the paper.

Theorem 3 Let I be a standard interpretation of L. Then it is LFA for J_{L} iff it is both EFA and universal.

The standardness condition is a mild requirement that seems to hold in all natural interpretations. (We will see below that this condition is in fact necessary for the conclusion.) Our theorem can be used to show that LFA interpretations exist, and that particular interpretations are LFA for particular languages; it also guides us in the search for LFA interpretations.

The right-to-left implication in the theorem is fairly straightforward:

Lemma 4 Let M:σ be closed, and take z in S^{Γ}. Then ⟨z, I[[ M ]]⟩ ∈ [[ ϕ]]^{Γ,x^{σ}} iff z ∈ [[ ϕ[M/x] ]]^{Γ}.

Proof First note that if Γ, x^{σ} ⊢ N : τ then, by the requirements placed on interpretations, I[[ Γ, x^{σ} ⊢ N ]] ∘ ⟨z, I[[ M ]]⟩ = I[[ Γ ⊢ N[M/x^{σ}] ]] ∘ z. The proof of the lemma is now a routine induction on ϕ. □

Proposition 5 Suppose I is a standard, EFA and universal interpretation of L. Then it is LFA.

Proof We first show by induction that ⊧_{op} ϕ iff ⊧_{I} ϕ for all sentences ϕ of J_{L}. For the sentence ⊥ this is trivial. For sentences of the form M = N or P ⇓ it is given by Proposition 2(i) and the fact that a standard EFA interpretation is AFA. The cases for the connectives ∧, ∨, ⊃ are all trivial.

For sentences ∀x^{σ}.ϕ, suppose first that ⊧_{I} ∀x^{σ}.ϕ. Then given any closed M:σ we have ⟨∗, I[[ M ]]⟩ ∈ [[ ϕ]]^{x^{σ}} by definition of [[ ∀x^{σ}.ϕ]], hence, by Lemma 4,

∗ ∈ [[ ϕ[M/x] ]] and so ⊧_{op} ϕ[M/x] by the induction hypothesis. Thus ⊧_{op} ∀x^{σ}.ϕ. Conversely, suppose ⊧_{op} ∀x^{σ}.ϕ. For any w ∈ S^{σ}, by universality we have that w = I[[ M ]] for some closed M : σ. But we have ⊧_{op} ϕ[M/x], and so, by the induction hypothesis, ∗ ∈ [[ ϕ[M/x] ]]. Hence by Lemma 4 ⟨∗, w⟩ ∈ [[ ϕ]]^{x^{σ}}. Thus [[ ϕ]]^{x^{σ}} = S^{x^{σ}}, so ⊧_{I} ∀x^{σ}.ϕ. The argument for ∃ is similar.

This completes the proof for sentences. To see that the result extends to all formulae, just observe that if ∀x⃗.ϕ is the universal closure of ϕ then ⊧_{op} ϕ iff ⊧_{op} ∀x⃗.ϕ, and ⊧_{I} ϕ iff ⊧_{I} ∀x⃗.ϕ. □

For the converse direction, we know from Proposition 2(i) that every LFA interpretation is AFA. Thus it only remains to show that every standard LFA interpretation is universal. To show this, we will for each type σ construct a closed term E^{σ}:ι → σ (called an enumerator for type σ) such that for all closed M : σ there exists n such that E^{σ}n ≈ M. It is easy to see that this suffices: we have ⊧_{op} ∀x^{σ}.∃y^{ι}.E^{σ}y = x, and so if I is LFA then also ⊧_{I} ∀x^{σ}.∃y^{ι}.E^{σ}y = x. That is, for all x ∈ S^{σ} there exists y ∈ S^{ι} such that I[[ z^{ι} ⊢ E^{σ}z^{ι}]] ∘ y = x. But I is standard so y = I[[ N ]] say, hence x = I[[ E^{σ}N ]]. Thus I is universal.

The fact that such enumerators exist is of some interest in its own right. In the case of PCF^{++}, suitable terms E^{σ} are already defined in Plotkin (1977), but for PCF and PCF^{+} we need a different technique. The method we use is, essentially, to construct a “simulator” for the relevant language within itself. A very similar method has recently (and independently) been employed in Abramsky, Jagadeesan and Malacaria (1994) to prove a definability result for an interpretation of sequential PCF based on games; a similar result has been proved in Hyland and Ong (1995). This yields an alternate semantic proof of the existence of enumerators for PCF, analogous to that in Plotkin (1977) for PCF^{++}. It is worth remarking that there is no corresponding definability result for PCF^{+}. It may well be that there can be none; it is not at all clear, however, how to even formulate a precise statement to that effect.

In what follows, L stands for either PCF or PCF^{+}, and ⌈−⌉ is some effective Gödel-numbering of L-terms as natural numbers.

Proposition 6 For each type σ there exists a closed term E^{σ}: ι → σ of L such that E^{σ}⌈M⌉ ≈ M for all closed terms M:σ of L.

We now fix σ = σ_{1} → ⋯ → σ_{h} → ι (h ≥ 0) and consider the construction of E^{σ}; we will not be completely explicit as all we require is its existence. The basic idea is that—given closed terms M : σ and N_{j} : σ_{j}, for j = 1, …, h— the computation of E^{σ}⌈M⌉N_{1} … N_{h} will simulate the reduction of MN_{1} … N_{h} via the Gödel-numbering. The problem here is that we do not have access to the Gödel-numbers of the N_{j}, but only to the terms themselves; so, in fact, we symbolically reduce (via Gödel-numbers) the term Mx_{1} … x_{h}, where the x_{j} are variables used to stand for the N_{j}. This results in a further problem when, in the course of the symbolic reduction, we come to a term of the form x_{j}M_{1} … M_{a}. In this case we do not reduce, but rather interpret, “passing” suitable simulations of M_{1}, …, M_{a} to N_{j}.

For the idea to work, it turns out that we need variables not only of the types σ_{j}, but also of all their subtypes. Let us define the relation ≺ between types to be the transitive relation generated from all instances of γ_{j} ≺ (γ_{1} → ⋯ → γ_{m} → ι), for j = 1, …, m. Let τ_{1}, …, τ_{k} be the (possibly repetitive) enumeration of all types τ ≺ σ in breadth-first order (regarding σ as a binary tree). Notice that for each i with 1 ≤ i ≤ k there exist p_{i} ≤ q_{i} such that τ_{i} = τ_{p_{i}+1} → ⋯ → τ_{q_{i}} → ι; we drop the subscripts on p and q when they are clear from the context. Note also that τ_{i} = σ_{i} for 1 ≤ i ≤ h.

To simulate MN_{1} … N_{h} we may need arbitrarily many variables of each type τ_{i}. We thus suppose that we have a countably infinite supply of variables x_{i}^{j} : τ_{i} for each i, and that the mapping (i, j) ↦ ⌈x_{i}^{j}⌉ is recursive; we say a term is σ-open if its free variables are among the x_{i}^{j}. To “store” the “values” of these variables we will use closed terms F_{i} : ι → τ_{i}, where F_{i} j stores the value of x_{i}^{j}. Since at any given stage only finitely many variables will be in use, we need a way to introduce new variables. Take push_{i} to be λv^{τ_{i}}f^{ι→τ_{i}}j^{ι}λy_{p+1}^{τ_{p+1}} … y_{q}^{τ_{q}}. cond j (vy_{p+1} … y_{q}) (f(pred j)y_{p+1} … y_{q}). The effect of push_{i} V F is to store the value given by a closed term V in the “register” x_{i}^{0}, and the previous value of x_{i}^{j} in the register x_{i}^{j+1}; we have push_{i} V F 0 ≈ V and push_{i} V F (j + 1) ≈ F j. To compensate for the use of push_{i}, we also need an operation ↑_{i} on terms of L that “bumps up” the indices on the appropriate variables; the term N↑_{i} is defined to be the term obtained by the capture-avoiding simultaneous substitution of V_{i}^{j} for x_{i}^{j} for every x_{i}^{j} occurring freely in N. Clearly the mapping ⌈N⌉ ↦ ⌈N↑_{i}⌉ is partial recursive.

So, to define E^{σ} we construct an “ι-simulator” S : ρ (where ρ is defined to be the type (ι → τ_{1}) → ⋯ → (ι → τ_{k}) → ι → ι) such that if N : ι is a σ-open term then SF_{1} … F_{k}⌈N⌉ simulates N, taking x_{i}^{j} to stand for F_{i} j. Following the idea outlined above, S will perform repeated one-step reductions, but terms of the form x_{i}^{j}N_{p+1} … N_{q} are interpreted by passing simulations of the arguments N_{p+1}, …, N_{q} to F_{i} j : τ_{i}. For this, we need “τ_{i}-simulators” S_{i} : ρ_{i}, where ρ_{i} is defined to be the type (ι → τ_{1}) → ⋯ → (ι → τ_{k}) → ι → τ_{i}; these are defined from the ι-simulator S : ρ by the terms Θ_{i} : ρ → ρ_{i} given in Lemma 7, below. Formally, S is obtained as a fixed-point of the term Φ:ρ → ρ given in Lemma 8, below; its definition makes use of the Θ_{i}, and the terms R: ρ used there and in Lemma 7 are to be thought of as “approximants” to S.

We need some special notation. First, for any vector F⃗ of terms F_{1}, …, F_{k} we write MF⃗ for (… (MF_{1}) … F_{k}). Second, we write push_{p,q}(V_{p+1}, …, V_{q}; F⃗) for F_{1}, …, F_{p}, (push_{p+1}V_{p+1}F_{p+1}), …, (push_{q}V_{q}F_{q}), F_{q+1}, …, F_{k}, where 1 ≤ p ≤ q ≤ k. Third, for any term M and 1 ≤ p ≤ q ≤ k we write M ↑_{p,q} for (… (M ↑_{p+1} ) … ↑_{q}). Finally, the notation C[|N_{1}|, …, |N_{a}|] →_{d}^{+} C′[|N′_{1}|, …, |N′_{a′} |] means that given PCF terms U_{1}, …, U_{a} such that U_{j} →^{∗} N_{j} (1 ≤ j ≤ a) there exist PCF terms U′_{1}, …, U′_{a′} such that U′_{j′} →^{∗} N′_{j′} (1 ≤ j′ ≤ a′) and C[U_{1}, …, U_{a}] →_{d}^{+} C′[U′_{1}, …, U′_{a′}]; notice that the U_{j} and U′_{j′} must be closed. (Here C[ , …, ] and C′[ , …, ] are “multi-place” contexts and →_{d} is the deterministic onestep reduction relation defined in Section 2.) This is useful because the call-by-name evaluation mechanism of L means that we cannot force subterms such as the U′_{j′} to be evaluated when we would like. The consideration of deterministic reduction (and hence of PCF terms) is only needed for Lemma 11 below. Note that transitivity holds, in that if C[|N_{1}|, …, |N_{a}|] →_{d}^{+} C′[|N′_{1}|, …, |N′_{a′} |] →_{d}^{+} C′′[|N′′_{1}|, …, |N′′_{a′′}|] then we have that C[|N_{1}|, …, |N_{a}|] →_{d}^{+} C′′[|N′′_{1}|, …, |N′′_{a′′}|].

Lemma 7 There exist closed L-terms Θ_{i}:ρ → ρ_{i} for 1 ≤ i ≤ k, such that for all σ-open N:τ_{i} and closed R:ρ, F_{1} :ι → τ_{1}, …, F_{k}:ι → τ_{k} we have

Θ_{i}RF⃗ |⌈N⌉| →_{d}^{+} λy_{p+1}^{τ_{p+1}} … y_{q}^{τ_{q}}. R push_{p,q}(y_{p+1}, …, y_{q}; F⃗) |⌈(N↑_{p,q})x_{p+1}^{0} … x_{q}^{0}⌉|.

Proof Define Θ_{i} to be the term

λr^{ρ}f_{1}^{ι→τ_{1}} … f_{k}^{ι→τ_{k}}z^{ι}y_{p+1}^{τ_{p+1}} … y_{q}^{τ_{q}}. r push_{p,q}(y_{p+1}, …, y_{q}; f⃗)(Gz)

where G:ι → ι is a closed PCF term such that for any σ-open N:τ_{i} we have that G⌈N⌉→^{+} ⌈(N↑_{p,q})x_{p+1}^{0} … x_{q}^{0}⌉. □

We now consider the term Φ. Notice that the clauses given below cover all syntactic shapes for terms of type ι. (The clause marked † applies only to PCF^{+}.)

Lemma 8 There exists a closed L-term Φ : ρ → ρ such that for all closed terms R:ρ, F_{1} :ι → τ_{1}, …, F_{k}:ι → τ_{k} we have

ΦRF⃗ |⌈n⌉|  →_{d}^{+} n;
ΦRF⃗ |⌈succ M⌉|  →_{d}^{+} succ (RF⃗ |⌈M⌉|);
ΦRF⃗ |⌈pred M⌉|  →_{d}^{+} pred (RF⃗ |⌈M⌉|);
ΦRF⃗ |⌈cond LMN⌉|  →_{d}^{+} cond (RF⃗ |⌈L⌉|)(RF⃗ |⌈M⌉|)(RF⃗ |⌈N⌉|);
ΦRF⃗ |⌈Y_{τ}N_{1}N_{2} … N_{a}⌉|  →_{d}^{+} RF⃗ |⌈N_{1}(Y_{τ}N_{1})N_{2} … N_{a}⌉| (a ≥ 2);
ΦRF⃗ |⌈(λz^{τ}.M)N_{1} … N_{a}⌉| →_{d}^{+} RF⃗ |⌈M[N_{1}/z]N_{2} … N_{a}⌉| (a ≥ 1);
† ΦRF⃗ |⌈por MN⌉|  →_{d}^{+} por (RF⃗ |⌈M⌉|)(RF⃗ |⌈N⌉|);
ΦRF⃗ |⌈x_{i}^{j}N_{p+1} … N_{q}⌉|  →_{d}^{+} F_{i} j (Θ_{p+1}RF⃗ |⌈N_{p+1}⌉|)…(Θ_{q}RF⃗ |⌈N_{q}⌉|).

Proof (Hint) We construct Φ via a “case split” with at most (k + 7) cases. The need for the consideration of PCF terms arises here, in order to ensure deterministic reduction. □

Note that terms of the forms succ M, pred M, cond LMN or por MN are interpreted rather than symbolically reduced; this is needed to handle terms such as succ x_{i}^{j}N_{p+1} … N_{q} where the operator must be interpreted since an argument is. It is also worth noting that there is no way to interpret terms such as Y_{τ}N_{1}N_{2} … N_{a} or (λz^{τ}.M)N_{1} … N_{a} as the type τ there is arbitrary and our method enables us to deal only with a finite number of given types (here the τ_{i}).

We now define S = Y_{ρ}Φ and S_{i} = Θ_{i}S, for i = 1, …, k. Note that:

SF⃗ |⌈n⌉|  →_{d}^{+} n;
SF⃗ |⌈succ M⌉| →_{d}^{+} succ (SF⃗ |⌈M⌉|);

etc., and that:

S_{i}F⃗ |⌈N⌉| →_{d}^{+} λy_{p+1}^{τ_{p+1}} … y_{q}^{τ_{q}}. Spush_{p,q}(y_{p+1}, …, y_{q}; F⃗) |⌈(N↑_{p,q})x_{p+1}^{0} … x_{q}^{0}⌉|.

Finally, we take E^{σ}:ι → σ to be a closed term such that

E^{σ}⌈M⌉ →_{d}^{+} λy_{1}^{σ_{1}}… y_{h}^{σ_{h}}. Spush_{0,h}(y_{1}, …, y_{h}; Ω⃗) |⌈Mx_{1}^{0} … x_{h}^{0}⌉|

where Ω⃗ is Ω_{ι→τ_{1}}, …, Ω_{ι→τ_{k}}.

We need to prove that E^{σ}⌈M⌉ ≈ M for all closed M : σ. By the Context Lemma, it is enough to show that for all closed N_{1} : σ_{1}, …, N_{h} : σ_{h} we have E^{σ}⌈M⌉N_{1} … N_{h} →^{∗} n iff MN_{1} … N_{h} →^{∗} n. Clearly the following lemma suffices:

Lemma 9 Suppose F_{i} j ≈ V_{i}^{j} : τ_{i} for each i, j, where the F_{i} and V_{i}^{j} are closed. Then for all σ-open N : ι and PCF terms U such that U →^{∗} ⌈N⌉ we have SF⃗ U →^{∗} n iff N[V_{i}^{j}/x_{i}^{j}] →^{∗} n.

The notation N[V_{i}^{j}/x_{i}^{j}] denotes the term obtained from N by the simultaneous substitution of V_{i}^{j} for x_{i}^{j}, for every x_{i}^{j} occurring freely in N.

The lemma is proved by relating the possible reduction sequences of N[V_{i}^{j}/x_{i}^{j}] with those of its simulation SF⃗ ⌈N⌉. Define “encoding” relations ⊳ between terms of type ι, ⊳_{i} between terms of type τ_{i}, for i = 1, …, k, and ⊵ between terms of the same type as follows:

• if U →^{∗} ⌈N⌉ where U is a PCF term and N:ι is a σ-open term and if, for each i, j, F_{i}j ≈ V_{i}^{j}:τ_{i} with F_{i} and V_{i}^{j} closed, then SF⃗ U ⊳ N[V_{i}^{j}/x_{i}^{j}];

• if U →^{∗} ⌈N⌉ where U is a PCF term and N:τ_{i} is a σ-open term and if, for each i, j, F_{i}j ≈ V_{i}^{j}:τ_{i} with F_{i} and V_{i}^{j} closed, then S_{i}F⃗ U ⊳_{i} N[V_{i}^{j}/x_{i}^{j}];

• if P_{s} ⊳ Q_{s} or P_{s} ⊳_{i} Q_{s} (for some 1 ≤ i ≤ k) for 1 ≤ s ≤ r, then, for any r-place context C[ , …, ], C[P_{1}, …, P_{r}] ⊵ C[Q_{1}, …, Q_{r}].

Note that ⊵ is reflexive; note too that ⊵ is closed under substitution in the sense that if we have that P ⊵ Q and P′ ⊵ Q′: τ then P [P′/z^{τ}] ⊵ Q[Q′/z^{τ}]. We write C[|⌈N_{1}⌉|, …, |⌈N_{a}⌉|]⊵Q (where a ≥ 0), to mean that for any PCF terms U_{1}, …, U_{a} such that U_{j} →^{∗} ⌈N_{j}⌉ (j = 1, …, a) we have C[U_{1}, …, U_{a}] ⊵ Q.

Lemma 9 is an immediate consequence of the next two lemmas.

Lemma 10 If P:ι is closed, P ⊵ Q and Q →^{∗} n then P →^{∗} n

Proof The proof proceeds by induction on the length l of a shortest reduction sequence from Q to n. If this is 0, then either P is n or else P ⊳ n, and so, by the remarks after Lemma 8, P →_{d}^{+} n. For l > 0, fixing P and Q, we first note that there is an r-place context C[ , …, ] (r ≥ 0) and there are P_{s} and Q_{s} (1 ≤ s ≤ r) such that Q = C[Q_{1}, …, Q_{r}], P = C[P_{1}, …, P_{r}] and for 1 ≤ s ≤ r, P_{s} ⊳ Q_{s} or P_{s} ⊳_{i} Q_{s}, for some 1 ≤ i ≤ k.

There are three main cases. In the first two C[ , …, ] has the form [ ]C_{1}[ , …, ] … C_{t}[ , …, ]—that is, there is a context hole in “head position”; the third is where there is not. In the first case, the proof proceeds either by reducing the length of the shortest reduction sequence (and applying the induction hypothesis) or else by reducing to the third case, with the same reduction sequence. The second case reduces to the first, with the same reduction sequence. In the third case, the length is always reduced.

So let us suppose there is indeed a context hole in head position. The first case is where C[Q⃗] = Q_{s} = Q and C[P⃗] = P_{s} = P, for some 1 ≤ s ≤ r, and P ⊳ Q (and t = 0). The second case is where C[Q⃗] = Q_{s}C_{1}[Q⃗] … C_{t}[Q⃗] and C[P⃗] = P_{s}C_{1}[P⃗] … C_{t}[P⃗], for some 1 ≤ s ≤ r, and P_{s} ⊳_{i} Q_{s}, for some 1 ≤ i ≤ k (and t = q − p).

Let us now consider the first case. Here P = SF⃗ U and Q = N[V_{i}^{j}/x_{i}^{j}] where N: ι is σ-open, where F_{i}j ≈ V_{i}^{j}: τ_{i} for each i, j, where the F_{i} and V_{i}^{j} are closed, and where U is a PCF term such that U →^{∗} ⌈N⌉. The proof now proceeds according to the form of N; it is here that the workings of the simulator are seen.

First, let us suppose N = por N_{1}N_{2}. Then, by the remarks after Lemma 8 we have SF⃗ U →_{d}^{+} por (SF⃗ U_{1})(SF⃗ U_{2}), where U_{1} and U_{2} are PCF terms such that U_{1} →^{∗} ⌈N_{1}⌉ and U_{2} →^{∗} ⌈N_{2}⌉. Therefore SF⃗ U_{1} ⊳ N_{1}[V_{i}^{j}/x_{i}^{j}] and similarly for U_{2}. Now, as (por N_{1}N_{2})[V_{i}^{j}/x_{i}^{j}] = N[V_{i}^{j}/x_{i}^{j}] reduces to n in l steps, then, in < l steps, either one of N_{1}[V_{i}^{j}/x_{i}^{j}], N_{2}[V_{i}^{j}/x_{i}^{j}] reduce to 0 or both reduce to a positive numeral. So we may apply the induction hypothesis and obtain corresponding reductions of SF⃗ U_{1} and SF⃗ U_{2}, and hence of SF⃗ U. The cases where N has any of the forms succ N_{1}, pred N_{1} or cond N_{1}N_{2}N_{3} are similar.

Next, let us suppose that N = (λz^{τ}.M)N_{1} … N_{a}. Then we have that SF⃗ U →_{d}^{+} SF⃗ |⌈M[N_{1}/z]N_{2} … N_{a}⌉| ⊵(M[N_{1}/z]N_{2} … N_{a})[V_{i}^{j}/x_{i}^{j}] = Q′, say. We can now apply the induction hypothesis, as there is a reduction of Q′ to n in l−1 steps since we have the deterministic reduction Q →_{d} Q′. The case where N = Y_{τ}N_{1}N_{2} … N_{a} is similar.

Finally, suppose that N = x_{i}^{j}N_{p+1} … N_{q}. Here we have that P = SF⃗ U →_{d}^{+} F_{i} j (S_{p+1}F⃗ U_{p+1}) … (S_{q}F⃗ U_{q}), where, for p < i′ ≤ q, U_{i′} is a PCF term such that U_{i′} →^{∗} N_{i′}. Then

V_{i}^{j}(S_{p+1}F⃗ U_{p+1}) … (S_{q}F⃗ U_{q}) ⊵ V_{i}^{j}(N_{p+1}[V_{i}^{j}/x_{i}^{j}]) … (N_{q}[V_{i}^{j}/x_{i}^{j}]) = Q,

and we are in the third case with the same shortest reduction sequence. So, V_{i}^{j}(S_{p+1}F⃗ U_{p+1}) … (S_{q}F⃗ U_{q}) →^{∗} n, by induction, and then, as F_{i} j ≈ V_{i}^{j}, P →^{+} n.

In the second case, P = S_{i}F⃗ UC⃗[P⃗] (abbreviating C_{1}[ ], …, C_{t}[ ] to C⃗[ ]) and Q = N[V_{i}^{j}/x_{i}^{j}]C⃗[Q⃗] where N:τ_{i} is σ-open, where F_{i}j ≈ V_{i}^{j} : τ_{i} for each i, j, where the F_{i} and V_{i}^{j} are closed, and where U is a PCF term such that U →^{∗} ⌈N⌉. Then S_{i}F⃗ U →^{+} λy_{p+1}^{τ_{p+1}} … y_{q}^{τ_{q}}.Spush_{p,q}(y_{p+1}, …, y_{q}; F⃗)U′ where U′ is a PCF term such that U′ →^{∗} ⌈(N↑_{p,q})x_{p+1}^{0} … x_{q}^{0}⌉. So we have that S_{i}F⃗ UC⃗[P⃗] →^{+} Spush_{p,q}(C⃗[P⃗]; F⃗)U′.

Now, for i′ = 1, …, k, define W_{i′}^{j} so that, for i′ = p+1, …, q, W_{i′}^{0} is C_{i′}[Q⃗], W_{i′}^{j+1} is V_{i′}^{j} and, for all other i′, W_{i′}^{j} is V_{i′}^{j}. Then we have that

Spush_{p,q}(C⃗[P⃗]; F⃗)U′ ⊳ ((N↑_{p,q})x_{p+1}^{0} … x_{q}^{0})[W_{i′}^{j}/x_{i′}^{j}] = N[V_{i′}^{j}/x_{i′}^{j}]C⃗[Q⃗],

and we have reduced to the first case, with the same reduction sequence.

Finally, we consider the third case, where no hole is in “head” position in C[ , …, ] (which we abbreviate to C[ ]). The proof divides into subcases according to the form of C[ ] We consider two of these; the others are similar. The first is where C[ ] is por C_{1}[ ]C_{2}[ ]. Here we have reductions to numerals in < l steps of one or both of C_{1}[ (Q)], C_{2}[ (Q)], as in the previous case involving por , and we can again apply the induction hypothesis. The second is where C[ ] is (λz^{τ}.C′[ ])C_{1}[ ] … C_{a}[ ]. Here P = (λz^{τ}.C′[P⃗])C_{1}[P⃗] … C_{a}[P⃗] → (C′[P⃗][C_{1}[P⃗]/z])C_{2}[P⃗] … C_{a}[P⃗] ⊵ (C′[Q⃗][C_{1}[Q⃗]/z])C_{2}[Q⃗] … C_{a}[Q⃗] = Q′, say (we use the closure of ⊵ under substitution here). We may now apply the induction hypothesis, for, as Q →_{d} Q′, there is a reduction of Q′ to n in l − 1 steps. □

Lemma 11 If P:ι is closed, P ⊵ Q and P →^{∗} n then Q →^{∗} n.

Proof By induction on the length of shortest reduction sequence from P to n. If this is 0, the result is immediate. Otherwise, the cases are organised as in the proof of Lemma 10(ii), but—unlike there—the length is always reduced. Let us consider the first case, where P = SF⃗ U and Q = N[V_{i}^{j}/x_{i}^{j}] where N:ι is σ-open, where F_{i} j ≈ V_{i}^{j}:τ_{i} for each i, j, where the F_{i} and V_{i}^{j} are closed, and where U is a PCF term such that U →^{∗} ⌈N⌉.

Let us first suppose N = por N_{1}N_{2}. Then SF⃗ U →_{d}^{+} por (SF⃗ U_{1})(SF⃗ U_{2}), where U_{1}, U_{2} are PCF terms which reduce to ⌈N_{1}⌉ and ⌈N_{2}⌉, respectively. As the reduction from P to por (SF⃗ U_{1})(SF⃗ U_{2}) is deterministic, the shortest reduction from P to n must proceed via por (SF⃗ U_{1})(SF⃗ U_{2}), and the proof is now similar to that of Lemma 10. The cases where N has any of the forms succ N_{1}, pred N_{1} or cond N_{1}N_{2}N_{3} are similar.

Next, let us suppose that N = (λz^{τ}.M)N_{1} … N_{a}. Then we have that SF⃗ U →_{d}^{+} SF⃗ U′ where U′ is a PCF term such that U′ →^{∗} ⌈M[N_{1}/z]N_{2} … N_{a}⌉. So SF⃗ U′ ⊵ (M[N_{1}/z]N_{2} … N_{a})[V_{i}^{j}/x_{i}^{j}], and we may now apply the induction hypothesis as there is a shorter reduction sequence of SF⃗ U′ to a numeral. The case where N = Y_{τ}N_{1}N_{2} … N_{a} is similar.

Finally, suppose that N = x_{i}^{j}N_{p+1} … N_{q}. Here we have that P = SF⃗ U →_{d}^{+} F_{i} j (S_{p+1}F⃗ U_{p+1}) … (S_{q}F⃗ U_{q}) = P′, say, where, for p < i′ ≤ q, U_{i′} is a PCF term such that U_{i′} →^{∗} N_{i′}. But P′ ⊵ F_{i} j (N_{p+1}[V_{i}^{j}/x_{i}^{j}]) … (N_{q}[V_{i}^{j}/x_{i}^{j}]), and so, by induction, we have that F_{i} j (N_{p+1}[V_{i}^{j}/x_{i}^{j}]) … (N_{q}[V_{i}^{j}/x_{i}^{j}]) →^{∗} n. But then as F_{i} j ≈ V_{i}^{j} and V_{i}^{j}(N_{p+1}[V_{i}^{j}/x_{i}^{j}]) … (N_{q}[V_{i}^{j}/x_{i}^{j}]) = Q we have that Q →^{∗} n.

In the second case, P = S_{i}F⃗ UC⃗[P⃗] and Q = N[V_{i}^{j}/x_{i}^{j}]C⃗[Q⃗] where N : τ_{i} is σ-open, where F_{i}j ≈ V_{i}^{j} : τ_{i} for each i, j, where the F_{i} and V_{i}^{j} are closed, and where U is a PCF term such that U →^{∗} ⌈N⌉. We have that S_{i}F⃗ UC⃗[P⃗] →_{d}^{+} Spush_{p,q}(C⃗[P⃗]; F⃗)U′ where U′ is a PCF term such that U′ →^{∗} ⌈(N↑_{p,q})x_{p+1}^{0} … x_{q}^{0}⌉. We now have

S push_{p,q}(C⃗[P⃗]; F⃗)U′ ⊳ ((N↑_{p,q})x_{p+1}^{0} … x_{q}^{0})[W_{i′}^{j}/x_{i′}^{j}] = N[V_{i′}^{j}/x_{i′}^{j}]C⃗[Q⃗],

defining W_{i′}^{j} as before; we may therefore apply the induction hypothesis.

Finally, in the third case no hole is in head position in C[ ] and the proof again proceeds according to the form of C[ ]; the details are omitted. □

The proof of Theorem 3 is complete.

5 Remarks and Open Problems

We conclude by drawing together some miscellaneous observations and suggesting some directions for further research.

It is easy to show using Proposition 5 that standard LFA interpretations for each of our languages L do in fact exist. Specifically, let C_{L} be the “syntactic category” whose objects are environments Γ, and whose morphisms from Γ to Δ are appropriate tuples of terms in environment Γ modulo observational equivalence. Then the canonical standard interpretation I_{L} of L in C_{L} is clearly EFA and universal, and thus LFA. In fact I_{L} is essentially the only “sensible” LFA interpretation for L. For suppose that I is a standard and cartesian-closed LFA interpretation of L in D. Then, by Theorem 3 and a previous remark, it is EFA and universal in the strong sense. It follows that the full subcategory of D consisting of the objects I[[ σ]] is equivalent to C_{L}, and then that I_{L} and I are identical, modulo the equivalence.

Given that standard LFA interpretations exist, one can prove, using an appropriate form of the Upward Löwenheim-Skolem Theorem, that non-standard (and thus non-universal) LFA interpretations also exist. This shows that the standardness condition in Theorem 3 is indeed necessary.

The syntactic interpretations C_{L} assure us of the existence of LFA interpretations, but these interpretations may not be very useful since questions about C_{L} are no easier than questions about L itself. It is more interesting to ask whether one can give more “semantic” constructions of LFA interpretations. Note that since any standard LFA interpretation is universal it must have some notion of “computability” built in; the classical category of cpos does not provide an LFA interpretation for PCF^{++}, for instance, because of the existence of noncomputable elements (this observation is sharpened in Proposition 12 below). For PCF^{++}, there are several natural examples of LFA interpretations: the category of effective Scott domains, see Plotkin (1977), and many realizability interpretations, see Longley (1995), provide instances. Examples of LFA interpretations for sequential PCF are given by the recursive versions of categories of games, see Abramsky, Jagadeesan and Malacaria (1994) and Hyland and Ong (1995). provide an LFA interpretation, as there We do not know of any natural LFA interpretations for PCF^{+}.

Although in this paper we have concentrated mainly on LFA interpretations for the whole of J_{L}, it is also natural to consider logical full abstraction for fragments of the language. One way to obtain such a fragment is to restrict attention to sentences of a certain logical complexity, e.g., the Π_{n}-sentences, for some n. (Note that, by a previous remark, logical full abstraction for Π_{n}-sentences and Σ_{n}-sentences are equivalent.) Our proof of Theorem 3 shows that if a standard interpretation is LFA for Π_{2}-sentences then it is LFA for the whole of J_{L}. In fact, the proof shows more, that it suffices to be LFA for Π_{2}-sentences with equational matrix, that is, of the form ∀x^{σ}.∃y^{τ}. M = N—one can even take τ to be ι.

The next result shows that logical full abstraction for Σ_{1}-sentences with equational matrix is already stronger than equational full abstraction (for any of PCF^{+}, PCF^{+} or PCF^{++}).

Proposition 12 Neither Milner’s EFA interpretation for PCF, nor the standard cpo interpretation, whether taken for PCF^{+} or PCF^{++}, are LFA for sentences of the form ∃f^{ι→ι}. M = N.

Proof Let K denote Kleene’s singular tree (see Beeson (1985), Chapter IV)— recall that K is a recursive prefix-closed set of finite binary sequences such that K contains arbitrarily long finite sequences but no recursive infinite path. Let ⌈−⌉ be an effective coding of finite binary sequences as natural numbers, and let T:ι → ι be such that T ⌈s⌉ →^{+} 0 iff s ∈ K. We also require a term P:ι → ι → ι such that P ⌈s⌉⌈t⌉ →^{+} 0 iff s is a proper prefix of t, and a term Z : ι → ι → ι such that Z m n →^{+} 0 iff m = n = 0. Now consider the sentence

∃f^{ι→ι}. (λx^{ι}. Z (T (fx)) (P (fx)(f(succ x)))) = (λx^{ι}. cond x 0 0).

It is easy to see that this sentence is denotationally true in all the interpretations since by König’s Lemma there exists an infinite path through K, but not operationally true as there is no recursive such path (Milner’s interpretation coincides with the cpo interpretation at type ι → ι). □

The (open) problem is now to distinguish LFA for Π_{1}-sentences from LFA.

Another way to obtain fragments of J_{L} is via a notion of type complexity. The level of a type is defined recursively:

level(ι) = 0; level(σ → τ) = max(level(σ) + 1, level(τ)).

The level of a formula is then taken to be the maximum of the levels of its quantified variables. (One could also consider stronger alternative definitions placing restrictions on the level of subexpressions.) A standard EFA interpretation is (evidently) logically fully abstract for sentences of level 0. For PCF^{++} one can say more, but first we need a lemma. A type σ is said to be an L-retract of a type τ if there are closed L-terms L_{τ}^{σ} : σ → τ and R_{σ}^{τ} : τ → σ such that λx^{σ}.R_{σ}^{τ}(L_{τ}^{σ}(x)) ≈ λx^{σ}.x holds in L.

Lemma 13 Every type is a PCF^{++}-retract of ι → ι.

Proof We use the “effective universality” remarked in Plotkin (1978), that every effectively given coherent ω-continuous cpo is a computable retract of T^{ω}. In the interpretation C of PCF^{++} provided by the classical category of cpos, every C[[ σ]] is such a cpo; further T^{ω} is a computable retract of the cpo C[[ ι → ι]]. Since any computable element of any C[[ τ ]] is PCF^{++}-definable, see Plotkin (1977), we therefore have PCF^{++}-terms defining the retracts. The conclusion follows, as the classical interpretation is EFA for PCF^{++}. □

With this we can see that a standard interpretation I of PCF^{++} is LFA iff it is for sentences of the form ∀f^{ι→ι}.∃m^{ι}. M = N. Any such interpretation must be EFA. But now we can apply the above remarks on LFA for Π_{2}-sentences, as:

⊧_{I} ∀x^{σ}.∃m^{ι}. M = N iff ⊧_{I} ∀f^{ι→ι}.∃m^{ι}. M[R_{σ}^{ι→ι}f/x] = N[R_{σ}^{ι→ι}f/x].

It is an open question as to whether PCF or PCF^{+} permit any such reduction in type complexity. It would also be interesting to understand which retractions hold for these languages.

The results in this paper should apply not just to the languages we have considered but to a wider class. As regards functional languages, one would certainly wish to consider the lazy and call-by-value variants of PCF, see Gunter (1992) and Longley (1995). A further useful extension would be to recursively typed languages, such as FPC—see Gunter (1992) and Fiore and Plotkin (1994). It would then be natural to consider polymorphic extensions of PCF; this seems not to be a straightforward matter. It would be also interesting to formulate an appropriate notion that would allow our results to be presented at their natural level of generality. This should at least include suitable extensions of PCF, in which regard see Jim and Meyer (1991), and perhaps a greater degree of abstraction is obtainable.

Finally, we have said very little about axioms and inference rules for J_{L}. It would be useful to work out the details of an axiomatization for our logics and show that our axioms were valid in some LFA interpretation. This would establish that they were also valid under the operational interpretation—thus we would obtain an attractive program logic. It seems that the appropriate axioms would be very similar to those of LCF, with a few additional “effectivity” principles. Of course, in this simple situation one can imagine that the validity of the axioms could be proved just as easily by syntactic methods, without the aid of a denotational interpretation. It would therefore be interesting to carry out a similar programme for more complex programming languages—it seems plausible that here semantic methods might show a distinct advantage over syntactic ones.

Acknowledgments

We would like to thank John Power for many helpful discussions.

References

S. Abramsky, R. Jagadeesan & P. Malacaria, Full Abstraction for PCF (Extended abstract), in Proceedings of TACS ’94, eds. M. Hagiya and J. Mitchell, LNCS 789, pp. 1–15, Springer-Verlag, Berlin, 1994; see also Full Abstraction for PCF, by the same authors, to appear.

M. Beeson, Foundations of Constructive Mathematics, Springer-Verlag, Berlin, 1985.

P-L. Curien, Categorical Combinators, Sequential Algorithms, and Functional Programming, Birkhäuser, Boston, 1993.

M. Fiore and G. D. Plotkin, An Axiomatisation of Computationally Adequate Domain Theoretic Models of FPC, in Proceedings of the Ninth Symposium on Logic in Computer Science, Paris, pp. 92 –102. Washington, IEEE Computer Society Press,1994.

M. Gordon, R. Milner and C. Wadsworth, Edinburgh LCF, LNCS 78, Springer-Verlag, Berlin, 1978.

C. A. Gunter, Semantics of Programming Languages, MIT Press, Cambridge, 1992.

J. M. E. Hyland, First Steps in Synthetic Domain Theory, in Category Theory, Proceedings, Como 1990, eds. A. Carboni, M. C. Pedicchio and G. Rosolini, LNM 1488, pp. 131–157, Springer-Verlag, Berlin, 1990.

J. M. E. Hyland and C.-H. L. Ong, Pi-calculus, Dialogue Games and PCF, in Proc. 7th ACM Conf. Functional Programming and Computer Architecture, ACM Press, 1995; see also On Full Abstraction for PCF: I, II and III, by the same authors, to appear.

T. Jim and A. R. Meyer, Full Abstraction and the Context Lemma (Preliminary Report), in Proceedings of TACS ’91, eds. T. Ito and A. R. Meyer LNCS 526, pp. 131–151, Springer-Verlag, Berlin, 1991.

J. Lambek and P. J. Scott, Introduction to Higher-Order Categorical Logic, Cambridge University Press, Cambridge, 1986.

J. R. Longley, Realizability Toposes and Language Semantics, Ph.D. thesis, University of Edinburgh, LFCS technical report number ECS-LFCS-95-332, 1995.

R. Milner, Fully Abstract Models of Typed λ-calculi, Theoretical Comp. Sci., Vol.4, pp. 1–22, 1977.

P. W. O’Hearn and J. G. Riecke, Kripke Logical Relations and PCF, Invited Lecture: Workshop on Logic Domains and Programming Languages, Darmstadt, 1995, to appear in Information and Computation.

G. Plotkin, LCF Considered as a Programming Language, Theoretical Comp. Sci., Vol. 5, pp. 223–255, 1977.

G. Plotkin, T^{ω} as a Universal Domain, JCSS, Vol. 17, pp. 209–236, 1978.

D. Scott, Outline of a Mathematical Theory of Computation, in Proc. 4th Annual Princeton Conference on Information Sciences and Systems, pp. 169–176, Princeton University, 1970.

D. Scott and C. Strachey Towards a Mathematical Semantics for Computer Languages, in Proc. Symp. on Computers and Automata, Microwave Research Institute Symposia Series, Vol. 21, pp. 19–46, Polytechnic Press, Brooklyn, New York, 1971.

A. Stoughton, Interdefinability of Parallel Operations in PCF, Theoretical Comp. Sci., Vol. 79, pp. 357–358, 1991.

M. B. Trakhtenbrot, On Representation of Sequential and Parallel Functions, in Proc. 4th Symposium on Mathematical Foundations of Computer Science, LNCS 32, pp. 411–417, Springer-Verlag, Berlin, 1975.