Full Abstraction and the Context Lemma^{1}

Trevor Jim^{2} and Albert R. Meyer^{3} MIT Laboratory for Computer Science

December 20, 1991

1Extended version of the paper appearing in the proceedings of TACS ’91 (Meyer and Ito, Eds., volume 526 of Lecture Notes in Computer Science, pages 131–151, Springer-Verlag, 1991).

2E-mail: trevor@theory.lcs.mit.edu. Work supported by ARO grant DAAL03-89-G-0071.

3E-mail: meyer@theory.lcs.mit.edu. Work supported by ONR grant N00014-89-J-1988 and NSF grant 8819761-CCR.

Abstract

It is impossible to add a combinator to PCF to achieve full abstraction for models such as Berry’s stable domains in a way analogous to the addition of the “parallel-or” combinator that achieves full abstraction for the familiar cpo model. In particular, we define a general notion of rewriting system of the kind used for evaluating simply typed λ-terms in Scott’s PCF. Any simply typed λ-calculus with such a “PCF-like” rewriting semantics is shown necessarily to satisfy Milner’s Context Lemma. A simple argument demonstrates that any denotational semantics that is adequate for PCF, and in which certain simple Boolean functionals exist, cannot be fully abstract for any extension of PCF satisfying the Context Lemma. An immediate corollary is that stable domains cannot be fully abstract for any extension of PCF definable by PCF-like rules.

Keywords: Stable functions, full abstraction, context lemma, PCF, standardization.

AMS(MOS) subject classifications: 03B40 68N15 68Q40 68Q50 68Q55

1 Introduction

A paradigmatic example of a functional programming language is PCF, Scott’s simply typed λ-calculus for recursive functions on the integers [32]. Many categories of denotational meaning are known to adequately reflect the computational behavior of PCF in a precise technical sense, namely, a PCF term evaluates to the numeral \underline{n} iff it means the integer n. But typically there are pairs of terms with distinct meanings that nevertheless are computationally indistinguishable in PCF. For example, with the semantics based on cpo’s, PCF must be extended with a “parallel-or” combinator in order to express enough computations to be fully abstract, i.e., semantical distinctions and computational distinctions between terms coincide [31, 30].

The problem of characterizing a fully abstract model of unextended PCF remains open after nearly two decades, cf. [27, 8, 28, 36]. Efforts to construct spaces of “sequential” functions corresponding to those definable in the original PCF without parallelism have led to the discovery of a number of new domains suitable for denotational semantics. Although none are fully abstract for PCF, one motivation for the development of spaces such as the stable functions, bistable functions, sequential algorithms [5, 4, 8, 7, 15], and most recently the strongly stable functions [13] was that they captured various aspects of sequentiality and so seemed “closer” to full abstraction for unextended PCF than the popular cpo model.

The stable function model in particular has a simple definition and attractive categorytheoretic properties. Its only apparent technical peculiarity is that stable domains of functions are not partially ordered pointwise; in general, the stable ordering strictly refines the pointwise ordering. Nevertheless, just as for the cpo model, the elements of stable domains of type σ → τ are actually total functions from elements of type σ to elements of type τ. Likewise, there is a natural notion of finite and effective elements of stable domains, and these domains yield an adequate least fixed-point model for PCF. Further, they form a Cartesian Closed Category with solutions for domain equations [5]. This category was also independently discovered and used in constructing a model of polymorphic λ-calculus [16]. So the stable domains seem to offer a setting for a theory for higher-order recursive computation with many of the attractions of the cpo category.

However, one important result about cpo’s is not known for stable domains, namely, full abstraction with respect to some extension of PCF analogous to the parallel-or extension which Plotkin and Sazonov provided for the cpo model. What might a symbolicevaluator for an extended PCF look like if it was well matched—fully abstract—with the stable model? We conclude that such an evaluator will have to be unusual looking: it cannot be specified by the kind of term-rewriting based evaluation rules known for PCF and its extensions.

The significance of this negative result hinges heavily on how drastic we judge it to go beyond the scope of PCF-like rules. It is of course possible that some operational behavior that we declare to be non-PCF-like, in our technical sense, will nevertheless offer a useful extension of PCF for which stable domains are fully abstract. For example, Bloom [10] provides such an extension for complete lattice models, though he goes on to criticize the rather complex algorithmic specification of the combinators in his extension. (The general benefits of structured approaches to operational semantics and connections to full abstraction are discussed in [26, 11].)

To illustrate the generality of our notion of PCF-like rules, we note that the standard extensions of PCF by parallel-or and existential combinators are easily seen to be PCFlike. For example, we can define an evaluator for Plotkin’s ∃ constant [30] while remaining within a term rewriting discipline, as follows. Let p : ι → o be an “integer predicate” variable, and use the rules:

∃p → cond (p\underline{n}) tt Ω,
∃p → cond (pΩ) Ω ff.

The resulting PCF-like language no longer has a confluent rewriting system, though it remains single-valued, viz., every term rewrites to at most one numeral. In general, our PCF-like rules need not even be single valued.

A substantial technical contribution of this paper is a simple, modest restriction on the format of rewrite rules which is sufficient to guarantee Milner’s Context Lemma [27] for languages defined by such rules. Informally, this “Approximation” Context Lemma requires that if two phrases M, N of the same syntactic functional type yield visibly distinct computational outcomes when used in some language context, then there are actual parameters of appropriate argument type, such that M and N each simply applied to these arguments, yield visibly distinct computational outcomes. This property, more perspicuously dubbed operational extensionality by Bloom [9, 10], has been identified by many authors as technically significant in program semantics [37, 29, 24, 1, 18, 2, 35]. The key to the proof of the Context Lemma is a new Standard Reduction Theorem 25 for PCF-like rewrite systems.

Our work borrows much from Bloom [9, 10]. The second author raised the question of whether there is a “reasonable” extension of PCF that would yield a fully abstract evaluator for lattice models [33, 34]. In answering this question, Bloom emphasized how the Context Lemma and full abstraction were incompatible with single-valued evaluators for the lattice model. He also characterized a general class of consistent rewrite rules that ensured the soundness of the Context Lemma. However, in order to encompass the computational behavior of the ∃ combinator, Bloom needed to develop an auxiliary notion of “observation calculi”.

Our PCF-like rules are, in an appropriate sense, as powerful as Bloom’s observational calculi, and strictly subsume the class of consistent rules. In particular, consistent rules are necessarily confluent and hence single-valued; as Bloom remarks [9], introducing a join combinator with simple multiple-valued rewrite rules yields a PCF extension both fully abstract for the lattice model and also satisfying the Context Lemma. Our wish to simplify Bloom’s criteria while dealing with nonconfluent rewriting systems forced us, however, to a rather elaborate theory of standard reductions.

As an aside, we also point out that it is questionable whether the (bi)stable and similar domains are closer to full abstraction for PCF. In particular, although some operationally valid equations that fail in the cpo model do hold, for example, in the stable model, we note in Corollary 15 that the converse also happens: some equations that hold in the cpo model fail in the stable model. The cpo, stable and likewise the bistable models thus offer information about the operational behavior of PCF terms that is not apparently comparable, and it is hard to see how to judge which is a more accurate model.

The outline of our argument is as follows: in Section 2 we formulate the key concepts of observational approximation, adequacy, and full abstraction in a fairly general setting. Then in Section 3, Theorem 14, we give a short proof that any denotational semantics that is adequate for PCF, and in which a certain simple Boolean functional exists, cannot be fully abstract for extensions of PCF satisfying the Context Lemma. The Boolean functional is obviously not continuous in Scott’s sense, but it is stably continuous, and so does appear in the stable model. We also formulate a Comparability Context Lemma which applies to the bistable domains. Section 4 gives our general notion of term rewriting systems of the kind used for symbolic evaluation of PCF terms. Then in Section 5, we show that any such system defines an observational approximation relation that must satisfy the Context Lemma [27]. An immediate corollary is Theorem 30 that there is no extension of PCF defined by PCF-like rewriting rules for which the stable domain semantics is fully abstract. A similar result for the bistable domains is announced but not proved.

2 Adequacy and Full Abstraction

Concepts concerning program behavior, such as observational congruence, adequacy, and full abstraction, can usefully be defined in a general setting consisting of:

• an arbitrary set L, called a language, whose elements, M, N, …, are called terms;

• partial operators C[·] on terms called contexts; and

• an arbitrary set O, called a notion of observation, whose elements are predicates on terms called observations. When an observation is true of a term, the term is said to yield the observation.

We will work with languages whose operational behavior is specified by (possibly nondeterministic) symbolic evaluation of terms, so we further assume a binary relation, “evaluates to”, on terms. For such languages, O_{eval} captures the familiar notion of observing the final output of an evaluation:

O_{eval} = { “evaluates to O” | O is an output term}.

Here the output terms are those terms regarded as observable “output values”. These typically include the ground constants (integers, truth values, …); λ-abstractions and finite lists of output values might also be included.

There are other notions of observation based on evaluation. For instance, O_{lazy} consists of the single predicate true of exactly those terms whose evaluation can terminate. And notions of observation can be based on semantics of terms, e.g.,

O_{int} = {“has the meaning of O” | O is an output term}.

In this paper, however, we will be mainly concerned with O_{eval}.

Any notion of observation induces a preordering on terms called observational approximation. Intuitively, one term approximates another if, according to the chosen notion of observation, the approximated term exhibits at least as much observable behavior when used in any program as the approximating term.

Definition 1 Let L be a language with a notion of observation O. A term M observationally approximates a term N, written M ⊑_{obs}N, if for all contexts C[·], whenever C[M] is a term yielding an observation from O, then C[N] is a term yielding it as well. M and N are observationally congruent, written M ≡_{obs} N, iff M ⊑_{obs}N and N ⊑_{obs}M.

Observational approximation provides precise meaning for questions such as, “Does my code meet a specification?” or “Will my new implementation of a module change the behavior of the program?”

In languages like PCF with applicative syntax and a suitable notion of closed terms, analysis of observational approximation can be simplified by appealing to a Context Lemma:

Definition 2 Let L be a language with a notion of observation O. We say a term M applicatively approximates a term N, written M ⊑_{app}N, iff for all vectors of closed terms, P⃗, whenever MP⃗ is a term yielding an observation, NP⃗ is a term yielding it as well. The Approximation Context Lemma^{1} holds if for all closed terms M and N,

M ⊑_{app}N iff M ⊑_{obs}N.

A fundamental result of Milner [27] is that under O_{eval} with numerals taken as the output terms, PCF itself, as well as its extension with parallel-or, satisfies the Approximation Context Lemma. We will see later that the Approximation Context Lemma holds for all languages defined in a “PCF-like” operational discipline, including, of course, PCF and its familiar extensions.

One method for proving observational approximations is by developing an abstract meaning, [[M]], of a term M that is adequate to determine its observations.

1In particular when O is O_{eval}, Bloom [9] calls this “operational extensionality” while Milner [27] uses simply “the Context Lemma”. We use the more descriptive “Approximation Context Lemma” because we will later consider Context Lemma’s that are not based on approximation.

Definition 3 A meaning function for a language L is a function [[·]] from terms M to values [[M]] in some set, partially ordered by a relation ⊑. A meaning function is compositional iff for all terms M, N and contexts C[·], if [[M]] ⊑ [[N]] and C[M] is a term, then C[N] is a term and [[C[M]]] ⊑ [[C[N]]].

A meaning function is adequate^{2} for a notion of observation O iff for all terms M, N and all observations obs ∈ O,

([[M]] ⊑ [[N]] and obs(M)) implies obs(N).

Adequacy and compositionality guarantee that the meanings accurately predict observational approximation.

Lemma 4 A compositional meaning function [[·]] is adequate for a notion of observation iff for all terms M and N,

[[M]] ⊑ [[N]] implies M ⊑_{obs}N.

The ordering on adequate meanings may be strictly finer than observational approximation. In the ideal situation, known as full abstraction, the two orderings coincide:

Definition 5 Let [[·]] be a meaning function for a language L with a notion of observation O. We say [[·]] is approximation fully abstract^{3} if for all terms M and N,

[[M]] ⊑ [[N]] iff M ⊑_{obs}N.

It is equationally fully abstract if for all M and N,

[[M]] = [[N]] iff M ≡_{obs} N.

Approximation full abstraction trivially implies adequacy for compositional meaning functions. Assuming that each output term evaluates to itself, it follows immediately that if [[·]] is adequate for O_{eval} and [[O]] ⊑ [[M]], then M evaluates to O, for any output term O. If, in addition, the meaning function is sound for the evaluator, we easily obtain a familiar (cf. [26]) alternate characterization of adequacy:

Definition 6 A meaning function [[·]] is sound for an “evaluates to” relation if for all terms M and N,

M evaluates to N implies [[M]] = [[N]].

2As with the Context Lemma, we might more descriptively call this “approximation adequate”; but we will use only the version of adequacy based on approximation, and call it simply adequacy for brevity.

3Stoughton [36] calls this “inequationally fully abstract”.

Lemma 7 A sound, compositional meaning function [[·]] is adequate for O_{eval} iff

[[O]] = [[M]] iff M evaluates to O,

for all terms M and output terms O.

This paper focuses specifically on the language PCF and its extensions. The precise (usual) definitions of PCF syntax and semantics appear in Appendix A, and we provide only a quick review here.

PCF is a simply typed λ-calculus with Boolean and natural number ground types, numerals \underline{n} for n ≥ 0, Boolean constants tt and ff, and simple arithmetic, recursion, and conditional operators. The evaluation relation ↠ of the language is given by term rewriting rules.

Definition 8 An extension of PCF is a simply typed language together with a set of rewrite rules. The types, typed constants, and rewrite rules of the extension must include those of PCF. The extension is conservative iff for all PCF terms M, and all terms N in the extension,

M ↠_{extended} N iff M ↠_{PCF} N.

Observational congruence, adequacy, etc., for PCF and its extensions will be defined with respect to O_{eval}, where we take the rewriting relation ↠ as the “evaluates to” relation, and the output terms are the ground constants tt, ff, and \underline{n} for n ≥ 0.

The results of the next section, which examines full abstraction for models of extensions of PCF, require that we prove facts about the meanings of terms while knowing very little about the extensions or the models. We will only have adequacy, conservativity, and a few other assumptions to work with. The following lemma shows that this gives us enough to reason about the unextended terms of the language.

Lemma 9 If a model is adequate for a conservative extension of PCF, then it is also adequate for PCF.

Proof: Suppose a model [[·]] is adequate for a conservative extension of PCF, and [[M]] ⊑ [[N]] for some PCF terms M, N. All models are compositional, so [[C[M]]] ⊑ [[C[N]]] for any PCF context C[·]. So for any ground PCF constant c, if C[M] ↠_{extended} c, then C[N] ↠_{extended} c by adequacy. And then by conservativity, if C[M] ↠_{PCF} c, then C[N] ↠_{PCF} c. Hence, M ⊑_{obs}^{PCF} N. ■

We will further require that our models be sound, and that the ground types o and ι be interpreted as the flat cpos {tt, ff }_{⊥} and {0, 1, …}_{⊥}, with the standard interpretation of tt, ff, and the numerals \underline{n}. Such models will be called models with Booleans (though they are indeed also models with integers). Two models with Booleans of particular interest are the cpo model C[[·]] and the stable model S[[·]]. Both models are adequate but not fully abstract for PCF.

The additional information about the ground types of models with Booleans is in fact enough to determine the meanings of ground PCF terms.

Lemma 10 The meaning of any closed PCF term of ground type is the same in all models with Booleans that are adequate for PCF.

Proof: Let M be a closed PCF term of type o (the case M : ι is similar). In PCF, exactly one of the following holds: (1) M ↠_{PCF} tt; (2) M ↠_{PCF} ff; or (3) neither (1) nor (2) holds. And by Lemma 7, M ↠_{PCF} tt iff [[M]] = [[tt]] = tt for any model with Booleans [[·]] adequate for PCF. Similarly, cases (2) and (3) imply [[M]] = ff and [[M]] = ⊥ respectively. ■

Thus we can use any particular adequate model with Booleans, like the familiar cpo model, to discover the meaning of ground PCF terms for arbitrary adequate models with Booleans. We have less to say about terms of higher type. But the following notions are useful:

Definition 11 Let τ be a first-order type, that is, a type of the form σ_{1} → ⋯ → σ_{n}, where σ_{j} is a ground type for 1 ≤ j ≤ n. Let [[·]]_{i} for i = 1, 2 be type frames such that ⊑_{1} on [[σ_{j}]]_{1} equals ⊑_{2} on [[σ_{j}]]_{2}, and let f_{i} ∈ [[τ]]_{i}. Then f_{1} pointwise approximates f_{2}, written f_{1}⊑_{pnt}f_{2}, iff for all d_{j} ∈ [[σ_{j}]]_{1},

f_{1}(d_{1}) ⋯ (d_{n}) ⊑_{1} f_{2}(d_{1}) ⋯ (d_{n}).

It follows immediately from Lemma 10 that the functions that are the meanings of a PCF term of first-order type agree pointwise in all models with Booleans that are adequate for PCF. So we can use the meaning of a first-order PCF term in some particular model to reason about its meaning in any adequate model with Booleans.

However, pointwise equality is not quite the same as equality of functions. For example, consider the conditional constant cond_{o} : o → o → o → o. Now S[[cond_{o}]] ≡_{pnt} C[[cond_{o}]]. But the stable domain does not contain parallel-or, so the stable and cpo meanings of o → o → o are different. Thus, S[[cond_{o}]] ≠ C[[cond_{o}]] since the two functions have different codomains.

Nevertheless, it follows immediately from the definitions that pointwise approximation has the following useful property:

Lemma 12 Let [[·]] be a model with Booleans that is adequate for PCF, and let M and N be closed PCF terms of first-order type. Then

[[M]]⊑_{pnt}[[N]] implies M⊑_{app}N.

3 Failures of Full Abstraction

Our first theorem hinges on the presence of certain simple functionals over the Booleans.

Definition 13 Let True be the constant tt function on the flat Booleans, and True! be the strict constant tt function. A true-separator is a function f satisfying

f(True) = tt,
f(True!) = ff.

Theorem 14 Let [[·]] be a model with Booleans that is adequate for some conservative extension of PCF satisfying the Approximation Context Lemma. If [[·]] contains a trueseparator, it is not equationally fully abstract.

Proof: Define the terms

True  ≡^{def} λx.tt,

                        True!  ≡^{def} λx.cond x tttt.

By the definition of model with Booleans, we have [[True]] = True. And by Lemma 10, [[cond]] ≡_{pnt} C[[cond]], so by definition of model with Booleans, we have [[True!]] = True!. Then True!⊑_{app}True by Lemmas 9 and 12. So by the Approximation Context Lemma,

True!⊑_{obs}True.

We conclude that there is no term P defining a true-separator; otherwise True! and True yield distinct observations in the context (P [·]), contradicting the fact that

True!⊑_{obs}True.

However, we can define a true-separator detector, D, as follows:

D ≡^{def} λx.cond (x True) (cond (x True!) Ω^{o} tt) Ω^{o},

where Ω^{o} is the divergent term (Y_{o}(λz^{o}.z)). By Lemma 10, [[Ω^{o}]] = C[[Ω^{o}]] = ⊥, and so

[[D]](f) = \{ \begin{matrix}tt & if f is a true-separator, \\ ⊥ & otherwise. \end{matrix}

Now [[λx.Ω^{o}]] is the constant ⊥ function, so [[D]] ≠ [[λx.Ω^{o}]], since they differ exactly on arguments that are true-separators. But since true-separators are not definable by terms, D and λx.Ω^{o} are applicatively congruent. Then by the Approximation Context Lemma, they are observationally congruent, contradicting equational full abstraction. ■

Corollary 15 If a stable function model with Booleans is adequate for a conservative extension of PCF that satisfies the Approximation Context Lemma, then the model is not equationally fully abstract.

Proof: Every stable function model with Booleans contains a true-separator truesep, defined as follows:

truesep(g) = \{ \begin{matrix}tt & if g = True, \\ ff & if g = True!, \\ ⊥ & otherwise. \end{matrix}

■

Corollary 16 The PCF equations valid in the stable model do not include those valid in the cpo model.

Proof: Just note that C[[D]] = C[[λx.Ω^{o}]], but S[[D]] ≠ S[[λx.Ω^{o}]]. ■

Our proof of Corollary 15 of course takes advantage of the notable fact that the stable ordering of functions differs from the pointwise ordering, e.g., the pair of functions True and True! are ordered pointwise but are stable-incomparable. In fact, the first few lines of the proof of Theorem 14 already show that inequational full abstraction is incompatible with the Approximation Context Lemma for any model in which True and True! are incomparable; the rest of the proof justifies the stronger conclusion that equational full abstraction fails as well.

We remark that the authors of [13] have informed us that their strongly stable models are adequate models with Booleans for PCF, and that truesep is strongly stable, so Theorem 15 and Corollary 16 hold for strongly stable models.

Berry realized that altering the pointwise ordering of functions caused difficulties, and he proposed from the start an additional bistable model which combines stability with the pointwise ordering. Since the counterexample of Corollary 15 relies on the non-pointwise stable ordering, it does not apply to the bistable model.

There is, however, an interesting counterexample to the full abstraction of the bistable model that provides a starting point for extending our results. The counterexample, noted in [15], has its roots in the fundamental motivation behind stable models, viz., to eliminate elements like parallel-or. Consider the following definition:

Definition 17 Let lor be the or-function that is strict in its left argument, and ror be the or-function that is strict in its right argument. An or-separator is a function f satisfying

f(lor) = tt,
f(ror) = ff.

The cpo model contains a parallel-or function which bounds the left- and right-strict or-functions, and thus, by monotonicity, cannot contain an or-separator. Since the cpo model is adequate for PCF, an or-separator is not definable in PCF. On the other hand, the stable and bistable models do not contain parallel-or, and in fact, both contain orseparators.

Thus in extending the results to the bistable model, one might try to use an orseparator in the role played by the true-separator in the stable case. Since neither lor nor ror applicatively approximates the other, an argument based on the Approximation Context Lemma will not work; but a similar argument based on a notion of observational comparability does apply:

Definition 18 Let L be a language with a notion of observation O. Terms M and N are directly comparable provided the set of observations yielded by M is setwise comparable to that yielded by N. The terms are observationally comparable, written M ∼_{obs}N, if for all contexts C[·], the terms C[M] and C[N] are directly comparable. They are applicatively comparable, written M ∼_{app}N, if for all vectors P⃗ of closed terms, MP⃗ and NP⃗ are directly comparable. L with O is said to satisfy the Comparability Context Lemma if for all closed terms M and N,

M ∼_{app}N iff M ∼_{obs}N.

Theorem 19 Let [[·]] be a model with Booleans that is adequate for some conservative extension of PCF satisfying the Comparability and Approximation Context Lemmas. If [[·]] contains an or-separator, it is not equationally fully abstract.

Proof: Consider the terms

                    lor  ≡^{def} λxy.cond x tt (cond y ttff),
                    ror  ≡^{def} λxy.cond y tt (cond x ttff).

By Lemmas 9, 10 and 12, we have [[lor]] = lor, [[ror]] = ror, and lor ∼_{app}ror. So by the Comparability Context Lemma, lor ∼_{obs}ror.

We conclude that there is no term P defining an or-separator; otherwise lor and ror yield distinct observations in the context (P [·]), contradicting the fact that lor∼_{obs}ror.

However, we can define an or-separator detector as follows:

D ≡^{def} λx.cond (x lor) (cond (x ror) Ω^{o} tt) Ω^{o}.

By Lemma 10,

[[D]](f) = \{ \begin{matrix}tt & if f is an or-separator, \\ ⊥ & otherwise. \end{matrix}

Now [[D]] ≠ [[λx.Ω^{o}]], since they differ exactly on arguments that are or-separators. But since or-separators are not definable by terms, D and [[λx.Ω^{o}]] are applicatively congruent. Then by the Approximation Context Lemma, they are observationally congruent, contradicting equational full abstraction. ■

Corollary 20 If a bistable model with Booleans is adequate for a conservative extension of PCF that satisfies the Comparability and Approximation Context Lemmas, then the model is not equationally fully abstract.

Proof: Every bistable model with Booleans contains an or-separator orsep, defined as follows:

orsep(g) = \{ \begin{matrix}tt & if g = lor, \\ ff & if g = ror, \\ ⊥ & otherwise. \end{matrix}

■

Corollary 21 ([21]) The PCF equations valid in the bistable model do not include those valid in the cpo model.

Proof: Just note that C[[D]] = C[[λx.Ω^{o}]], but B[[D]] ≠ B[[λx.Ω^{o}]], where B[[·]] is the bistable model of [5]. ■

The PCF-like languages, defined in the next section, do not satisfy the Comparability Context Lemma. In fact, an or-separator constant can defined through the following PCF-like rules:

    orsep(f) → cond (f tt Ω^{o}) (cond (f fftt) (cond (f ffff) tt Ω^{o}) Ω^{o}) Ω^{o},
    orsep(f) → cond (f Ω^{o} tt) (cond (f ttff) (cond (f ffff) ff Ω^{o}) Ω^{o}) Ω^{o}.

Thus we will have to restrict the class of rules we consider if we wish to apply Theorem 19. The consistent rules of Bloom [10] are an important, natural candidate for the restricted class. We do not know whether the Comparability Context Lemma holds for them. However, we can prove that an or-separator is not definable in consistent systems by a method involving a notion of comparability based on logical relations, as we indicate at the end of the next section.

4 PCF-like rewrite systems

Symbolic evaluators for PCF terms are often presented as term rewriting systems. In this section, we give the basic definitions for such systems, and give our criteria for calling such a system “PCF-like”. Our evaluator for PCF is given in Appendix A.

A rewrite rule is a pair l → r of terms of the same type, such that the free variables of the right-hand side r are included in those of the left-hand side l. We write M →^{Δ}_{π} N if for some subterm Δ of M, Δ → Δ′ is an instance of the rule π, and N is obtained from M by replacing Δ with Δ′. We will omit Δ or π as convenient.

Since all of our languages are simply typed λ-calculi, we will always include βreduction in the rewrite rules of the language. Additionally, we may specify some set Θ of δ-rules defining the behavior of the constants. Together, Θ and β define the rewriting relation →_{Θ,β} on the language L. We omit Θ and β when they can be recovered from context.

The δ-rules of PCF have a particularly simple form:

Definition 22 A linear ground δ-rule is a rewrite rule of the form

δm_{1}m_{2} ⋯ m_{n} → P,

where each m_{i} is either a ground constant c_{i} or a variable x_{i}. The variables x_{i} must be distinct. A PCF-like rewrite system is a language L together with a set Θ of linear ground δ-rules on the constants of L.

Note that this definition of “PCF-like” is meant to be generous. In particular, although the system for pure, unextended PCF is both single-valued—every term reduces to at most one constant—and confluent, PCF-like systems in general may be multiplevalued and nonconfluent.

An interesting example of a multiple-valued PCF-like system arises in [9]. There, Bloom defines an extension of PCF that is both fully abstract and denotationally universal for the lattice model of PCF. The key to the construction amounts to the addition of operators ⊤ : o and join : o → o → o with rules

join x y → x,
join x y → y,
join\underline{n_{1}} \underline{n_{2}} → ⊤, \underline{n_{1}} ≠ \underline{n_{2}},
⊤ → \underline{n}, n ≥ 0.

Nonconfluent but single-valued systems are also of interest. For example, [30] extends parallel PCF by an existential operator, ∃ : (ι → o) → o, to achieve a language that is fully abstract and denotationally universal for the cpo model. There, ∃ is defined by the deductive rules

\frac{p\underline{n} ↠ tt}{∃p → tt} , \frac{pΩ ↠ ff}{∃p → ff} ,

where ↠ is the reflexive transitive closure of →. The resulting language is indeed confluent, but goes beyond mere term rewriting. Because he wanted to be able to specify constants like ∃, Bloom [10] introduced observation calculi as a definition of “PCF-like” deductive rules.

But note that if we give up confluence, it is possible to define an ∃ constant while remaining in a term rewriting discipline. One such definition was given in the introduction; we provide here a second implementation, which uses the parallel-or combinator por.

∃p → por (p0) (∃(λx.p(succ x))),

                     ∃p → cond (pΩ) ttff.

This kind of rewriting is more straightforward, but actually as powerful as the deductive discipline.

Since PCF-like systems are not confluent in general, we will not be able to use confluence in our proof of the Context Lemma. Instead we will rely on a standardization theorem, which states that if a term M rewrites to a term N, then there is a “standard” reduction from M to N. Thus we only need consider these standard reductions in our proof.

Typically, the standard reductions are a class of reductions with a particularly nice structure. For instance, in the pure, typed λ-calculus, a standard reduction is one in which redexes are contracted from left to right.

The definition of standard reductions in PCF-like rewrite systems is more complicated because they admit the upwards creation of redexes, cf. [19]. However, there is a simple inductive characterization of those standard reductions that end at a ground constant. This will be sufficient to follow the proof of the Context Lemma given in the next section, so we defer the general definition of standard reductions, and the proof of the Standardization Theorem, to Appendix C.

Before defining the standard reductions to ground constants, we introduce some useful notation. Consider the set of indices

{ i | m_{i} is a constant c_{i} in rule θ : δm⃗ → P }.

These indices identify what we call the critical arguments of θ, since the rule θ applies to a term δQ⃗ iff Q_{i} ≡ c_{i} for i in the set. For expository purposes it will be convenient to separate the critical and non-critical arguments of a constant δ (relative to some linear ground δ-rule θ).

Notation 23 Let θ : δm⃗ → P be a linear ground δ-rule with j critical arguments and k non-critical arguments. Then for vectors A⃗ ≡ A_{1} ⋯ A_{j} and B⃗ ≡ B_{1} ⋯ B_{k}, we let

δ_{θ}⟨A⃗, B⃗⟩ ≡^{def} δQ⃗,

where Q⃗ is the interleaving of A⃗ and B⃗ such that the A_{i}’s appear at the critical indices of Q⃗. We drop the subscript θ when it can be recovered from context.

Note that we do not require that δQ⃗ be an instance of δm⃗; we will want to use the δ⟨·, ·⟩ notation on terms that we anticipate becoming θ-redexes over the course of a reduction.

In this notation, we write linear ground δ-rules as

θ : δ⟨c⃗, x⃗⟩ → P

or even

θ : δ⟨c⃗, x⃗⟩ → P (x⃗)

when we wish to make the dependence of P on x⃗ explicit.

Definition 24 The standard reductions to ground constants in a PCF-like rewrite system are defined inductively as follows. We will write M ↠_{s} c for a standard reduction of a term M to a ground constant c.

• If c is a ground constant, then the 0-step reduction c ↠ c is standard.

• If M_{1}, M_{2}, …, M_{n} are terms, and c is a ground constant, then a reduction

(λxM_{1})M_{2}M_{3} ⋯ M_{n} →_{β} M_{1}[x := M_{2}]M_{3} ⋯ M_{n}
↠_{s} c

is standard.

• If C_{1}, C_{2}, …, C_{n}, D⃗, E⃗ are terms, and c, c_{1}, c_{2}, …, c_{n} are ground constants, then a reduction of the following form is standard:

σ_{1} : δ_{θ}⟨C_{1}C_{2} ⋯ C_{n}, D⃗⟩E⃗ ↠ δ_{θ}⟨c_{1}C_{2} ⋯ C_{n}, D⃗⟩E⃗
σ_{2} :  ↠ δ_{θ}⟨c_{1}c_{2} ⋯ C_{n}, D⃗⟩E⃗
⋮  ↠ ⋯
σ_{n} :  ↠ δ_{θ}⟨c_{1}c_{2} ⋯ c_{n}, D⃗⟩E⃗
→_{θ} P_{θ}(D⃗)E⃗
↠_{s} c,

where for 1 ≤ i ≤ n, the subreduction σ_{i} consists of a standard reduction from the subterm C_{i} to the ground constant c_{i}.

Theorem 25 (Standardization) For any PCF-like rewrite system, if M ↠ N, then there is a standard reduction M ↠_{s} N.

Note that if we require our rules to be non-overlapping, then they are a special case of orthogonal rewrite systems, for which both confluence and standardization have been known for some time [19]. Similarly, confluence and standardization have been known for the systems of Bloom [10], which restrict our systems by allowing only so-called consistent overlaps at the root. However, it is not clear whether ∃ can be defined in such systems, and we certainly lose the ability to define interesting non-confluent systems, such as PCF extended with join.

5 The Context Lemma

Once standardization is known, the Context Lemma can be proved by a straightforward adaptation of Bloom’s proof for his observation calculi [10]. First we recall the following basic facts about substitutions.

Lemma 26 (Substitution Lemma) If x ≢ y and y ∉ FV(L), then

M[x := L][y := N[x := L]] ≡ M[y := N][x := L].

Lemma 27 If x ∉ FV(P), then

P [y⃗ := N⃗[x := M]] ≡ (P [y⃗ := N⃗])[x := M].

The Context Lemma will follow immediately from this next result.

Lemma 28 Suppose C is a ground term, c is a ground constant, M and N are closed terms of the same type, and M⊑_{app}N. If C[x := M] ↠ c, then C[x := N] ↠ c.

Proof: By Standardization, C[x := M] ↠_{s} c. We show C[x := N] ↠ c by induction on the length of the reduction C[x := M] ↠_{s} c.

1. The only reduction C[x := M] ↠_{s} c of length zero is c ↠ c. Then one of the following holds:

(a) C ≡ c. Then clearly C[x := N] ≡ c ↠ c.

(b) C ≡ x and M ≡ c. Here C[x := N] ↠ c because M⊑_{app}N.

For the induction, we consider subcases on the form of C.

2. C ≡ (λyC_{1})C_{2} ⋯ C_{n}. Assume x ≢ y (the case x ≡ y is similar). Since M is closed, we have

C[x := M] ≡ (λy(C_{1}[x := M]))C_{2}[x := M] ⋯ C_{n}[x := M].

Then the reduction C[x := M] ↠_{s} c is of the form

C[x := M] ≡ (λy(C_{1}[x := M]))C_{2}[x := M] ⋯ C_{n}[x := M]
→_{β} (C_{1}[x := M])[y := C_{2}[x := M]]C_{3}[x := M] ⋯ C_{n}[x := M]
↠_{s} c.

By the Substitution Lemma,

(C_{1}[x := M])[y := C_{2}[x := M]] ≡ (C_{1}[y := C_{2}])[x := M],

so our reduction can be rewritten

C[x := M] ≡ ((λyC_{1})C_{2} ⋯ C_{n})[x := M]
→_{β} ((C_{1}[y := C_{2}])C_{3} ⋯ C_{n})[x := M]
↠_{s} c.

Now by β-reduction, the fact that N is closed, and the Substitution Lemma,

C[x := N] ≡ ((λyC_{1})C_{2} ⋯ C_{n})[x := N]
→_{β} ((C_{1}[y := C_{2}])C_{3} ⋯ C_{n})[x := N].

And by induction,

((C_{1}[y := C_{2}])C_{3} ⋯ C_{n})[x := N] ↠ c.

Thus we have a reduction C[x := N] ↠ c as desired.

3. C ≡ δC_{1} ⋯ C_{n}. Then the reduction C[x := M] ↠_{s} c must contract the head δ by some rule θ : δ_{θ}⟨d⃗, y⃗⟩ → P (y⃗) (where each d_{i} is a ground constant). Accordingly, we rewrite C as

C ≡ δ_{θ}⟨D⃗, E⃗⟩F⃗ .

Then the reduction C[x := M] ↠_{s} c is of the form

C[x := M] ≡ δ_{θ}⟨D⃗[x := M], E⃗[x := M]⟩F⃗ [x := M]
↠ δ_{θ}⟨d⃗, E⃗[x := M]⟩F⃗ [x := M]
→_{θ} P (E⃗[x := M])F⃗ [x := M]
↠_{s} c,

where each D_{i}[x := M] ↠_{s} d_{i} in turn. By Lemma 27,

P (E⃗[x := M]) ≡ P (E⃗)[x := M],

so the reduction can be rewritten

C[x := M] ≡ (δ_{θ}⟨D⃗, E⃗⟩F⃗)[x := M]
↠ (δ_{θ}⟨d⃗, E⃗⟩F⃗)[x := M]
→_{θ} (P (E⃗)F⃗)[x := M]
↠_{s} c.

Again by Lemma 27,

P (E⃗[x := N])F⃗ [x := N] ≡ (P (E⃗)F⃗)[x := N].

And by induction, (P (E⃗)F⃗)[x := N] ↠ c, and D_{i}[x := N] ↠ d_{i}. Thus we have found a reduction

C[x := N] ≡ (δ_{θ}⟨D⃗, E⃗⟩F⃗)[x := N]
↠ (δ_{θ}⟨d⃗, E⃗⟩F⃗)[x := N]
→_{θ} (P (E⃗)F⃗)[x := N]
↠ c.

4. C ≡ xC_{1} ⋯ C_{n}. Then consider the term

C′ ≡^{def} MC_{1} ⋯ C_{n}.

Note that C[x := M] ≡ C′[x := M], so C′[x := M] ↠_{s} c. Moreover C′ must be of a form considered in the two previous cases, and so by the previous argument we conclude C′[x := N] ↠ c. Now consider the applicative context

C′′[·] ≡^{def} [·]C_{1}[x := N] ⋯ C_{n}[x := N].

Since C′′[M] ≡ C′[x := N], we have C′′[M] ↠ c. Finally, M⊑_{app}N implies C′′[N] ↠ c; and

C′′[N] ≡ NC_{1}[x := N] ⋯ C_{n}[x := N]
≡ C[x := N],

so C[x := N] ↠ c.

Note that we need not consider the case C ≡ yC_{1} ⋯ C_{n}, where y ≢ x, since then C[x := M] can never reduce to a ground constant. ■

Theorem 29 (Approximation Context Lemma) In any PCF-like rewrite system,

M⊑_{obs}N iff M⊑_{app}N

for all closed terms M and N.

Proof:

(⟹) Trivial. (⟸) It is sufficient to show the following: for all ground contexts C[·] and ground

constants c, if C[M] ↠ c, then C[N] ↠ c.

Remember that the action of placing a term into the “holes” of a context differs from substitution only in that free variables of the term can be captured. But M and N are closed, with no free variables to capture; so for any context C[·],

\begin{aligned}& C[M] & ≡ & (C[x])[x := M], \\ and & C[N] & ≡ & (C[x])[x := N], \end{aligned}

where x is a fresh variable. So by Lemma 28, if C[M] ↠ c, then C[N] ↠ c as well. ■

We now have immediately from Corollary 15:

Theorem 30 Every stable function model with Booleans that is adequate for a conservative extension of PCF defined by PCF-like rewrite rules is not equationally fully abstract.

We remark that a simple sufficient condition to ensure that an extension of PCF by PCF-like rules is conservative is that δ-rules whose left-hand sides involve no new (non-PCF) constants must be exactly the rules of PCF.

Because we are unable to prove a Comparability Context Lemma for consistent PCFlike rewrite rules, Corollary 20 cannot be applied. Nevertheless, our analysis of comparability can be extended to show:

Theorem 31 Every bistable model with Booleans that is adequate for a conservative extension of PCF defined by consistent PCF-like rewrite rules is not equationally fully abstract.

This will be proved in a forthcoming paper.

6 Conclusions and Future Work

We have extended the metatheory of term rewriting semantics for simply typed λ-calculi and have shown that certain denotational models, in particular those based on stable and strongly stable domains, cannot be fully abstract for such operational semantics. Our proof exploits the lack of order-extensionality in these domains, but an extension of our results to certain order-extensional domains such as the bistable domains is possible and will be the subject of a forthcoming paper.

The category of sequential algorithms [6] is technically not a model in our sense, but is like the stable model in that it is a Cartesian Closed Category with partially ordered function objects that are not pointwise ordered. We believe that with some minor modifications our results will apply to it as well. (This claim stands in apparent contradiction to the results of [6], which shows that the language CDS, based on concrete data structures [22], is fully abstract for the sequential algorithm model. However, it seems questionable to us to call a language such as CDS “PCF-like”, since it does not have λ-abstraction or even variables.)

We conjecture that our methods and results will extend to untyped versions of PCFlike languages. Extensions to lazy and call-by-value languages also seem plausible, though with more difficulties, since higher order terms now yield observations and the notion of lazy model is more technical.

A particular open problem that we have not yet resolved is the case when the definition of model with Booleans is relaxed to allow “extra” Boolean elements, e.g., if the Boolean type is interpreted as {tt, ff, error}_{⊥}. Finally, although we are able to show the failures of some order-extensional models, like the bistable models, the extensional embedding methods of [12] offer a more sophisticated way to restore order-extensionality which, for example, guarantees that the theory of the extensionally embedded models includes that of cpo’s. We do not know whether these models can avoid the kind of failure of full abstraction that we have identified.

How great a failing of, for example, the stable domains, is lack of full abstraction? The category of stable domains is mathematically rich and offers a plausible formulation of higher-order effective computability. We have shown that stable computability cannot be captured precisely in the familiar rewriting style of operational semantics which works for the cpo or even the lattice models. But as we observed in the introduction, the failures of full abstraction we have shown might be avoidable by some other attractive, as yet undeveloped, operational semantics. Such an operational semantics would be interesting to see; and indeed, some recent work of Cartwright and Felleisen [14] suggests a fruitful development in this direction.

Acknowledgments

We are grateful to G. Berry, B. Bloom, P.-L. Curien, J.-J. Lévy, G.D. Plotkin, and Scott Smith for helpful discussions.

References

[1] S. Abramsky. The lazy lambda calculus. In D. L. Turner, editor, Research Topics in Functional Programming. Addison-Wesley Publishing Co., 1989.

[2] S. Abramsky. Domain theory in logical form. Ann. Pure Appl. Logic, 51:1–77, 1991.

[3] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, second edition, 1984.

[4] G. Berry. Séquentialité de l’evaluation formelle des lambda-expressions. In B. Robinet, editor, Program Transformations, 3^{eme} Colloque International sur la programmation, pages 67–80, 1978.

[5] G. Berry. Stable models of typed lambda-calculi. In G. Ausiello and C. Böhm, editors, Automata, Languages and Programming: Fifth Colloquium, volume 62 of Lecture Notes in Computer Science, pages 72–89. Springer-Verlag, July 1978.

[6] G. Berry and P.-L. Curien. Sequential algorithms on concrete data structures. Theor. Comput. Sci., 20(3):265–321, July 1982.

[7] G. Berry and P.-L. Curien. Theory and practice of sequential algorithms: the kernel of the programming language CDS. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 2, pages 35–87. Cambridge Univ. Press, 1985.

[8] G. Berry, P.-L. Curien, and J.-J. Lévy. Full abstraction for sequential languages: the state of the art. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 3, pages 89–132. Cambridge Univ. Press, 1985.

[9] B. Bloom. Can LCF be topped? Flat lattice models of typed lambda calculus (preliminary report). In Third Annual Symposium on Logic in Computer Science [20], pages 282–295.

[10] B. Bloom. Can LCF be topped? Flat lattice models of typed λ-calculus. Information and Computation, 87(1/2):263–300, July/Aug. 1990.

[11] B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can’t be traced (preliminary report). In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 229–239, 1988. Also appears as MIT Technical Memo MIT/LCS/TM-345; submitted for journal publication.

[12] A. Bucciarelli and T. Ehrard. Extensional embedding of a strongly stable model of PCF. In Automata, Languages and Programming: Eighteenth Colloquium, July 1991.

[13] A. Bucciarelli and T. Ehrard. Sequentiality and strong stability. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, 1991.

[14] R. Cartwright and M. Felleisen. Observable sequentiality and full abstraction. Draft of October 1, 1991; to appear in POPL ’92.

[15] P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. John Wiley and Sons, 1986.

[16] J.-Y. Girard. The system F of variable types, fifteen years later. Theor. Comput. Sci., 45:152–192, 1986.

[17] J. R. Hindley and J. P. Seldin. Introduction to Combinators and λ-calculus, volume 1 of London Math. Soc. Student Texts. Cambridge Univ. Press, 1986.

[18] D. J. Howe. Equality in lazy computation systems. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 198–203. IEEE, 1989.

[19] G. Huet and J.-J. Lévy. Computations in nonambiguous term rewriting systems. Technical Report 359, INRIA, Rocquencourt, France, 1979.

[20] IEEE. Third Annual Symposium on Logic in Computer Science, 1988.

[21] T. Jim and A. R. Meyer. Communication in the types electronic forum (types@theory.lcs.mit.edu). June 17^{th}, 1989.

[22] G. Kahn and D. B. MacQueen. Coroutines and networks of parallel processes. In B. Gilchrist, editor, Information Processing ’77, pages 993–998. North-Holland Publishing Co., 1977.

[23] J. W. Klop. Combinatory reduction systems. Tract 127, Mathematisch Centrum, Amsterdam, 1980.

[24] I. Mason and C. Talcott. Programming, transforming, and proving with function abstractions and memories. In G. Ausiello, M. Dezani-Ciancaglini, and S. R. D. Rocca, editors, Automata, Languages and Programming: 16^{th} International Colloquium, volume 372 of Lecture Notes in Computer Science. Springer-Verlag, 1989.

[25] A. R. Meyer. What is a model of the lambda calculus? Information and Control, 52(1):87–122, Jan. 1982.

[26] A. R. Meyer. Semantical paradigms: Notes for an invited lecture, with two appendices by Stavros Cosmadakis. In Third Annual Symposium on Logic in Computer Science [20], pages 236–253.

[27] R. Milner. Fully abstract models of the typed lambda calculus. Theor. Comput. Sci., 4:1–22, 1977.

[28] K. Mulmuley. Full Abstraction and Semantic Equivalence. ACM Doctoral Dissertation Award 1986. MIT Press, 1987.

[29] C.-H. L. Ong. The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. PhD thesis, Imperial College, University of London, 1988.

[30] G. D. Plotkin. LCF considered as a programming language. Theor. Comput. Sci., 5(3):223–256, Dec. 1977.

[31] V. Sazonov. Expressibility of functions in D. Scott’s LCF language. Algebra i Logika, 15:308–330, 1976. (Russian).

[32] D. S. Scott. A type theoretical alternative to CUCH, ISWIM, OWHY. Manuscript, Oxford Univ., 1969.

[33] D. S. Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97–136. Springer-Verlag, 1972.

[34] D. S. Scott. Data types as lattices. SIAM J. Comput., 5:522–587, 1976.

[35] S. Smith. From operational to denotational semantics. In Mathematical Foundations of Programming Semantics, 1991. To appear.

[36] A. Stoughton. Fully Abstract Models of Progamming Languages. Research Notes in Theoretical Computer Science. Pitman/Wiley, 1988. Revision of Ph.D thesis, Dept. of Computer Science, Univ. Edinburgh, Report No. CST-40-86, 1986.

[37] C. Talcott. Programming and proving with function and control abstractions. Technical Report STAN-CS-89-1288, Stanford Univ., 1988.

A PCF

Because we will work with both PCF and its extensions, we give the general definitions for simply typed λ-calculi. A language is parameterized by its ground types and typed constants; for instance, PCF’s ground types are the Booleans o and the numerals ι, and its constants are listed in Figure 1.

The set of types of the language is the least set containing the ground types and (σ → τ) for types σ and τ. The set of first-order types is the least set containing the ground types and (σ → τ) for ground types σ and first-order types τ.

The typed terms of the language are defined inductively:

• A constant δ^{σ} is a term of type σ.

• A variable x^{σ} is a term of type σ.

• If M is a term of type (σ → τ) and N is a term of type σ, then (MN) is a term of type τ.

• If M is a term of type τ, then (λx^{σ}M) is a term of type (σ → τ).

We omit types and parentheses whenever possible, adopting the standard conventions of association: application associates to the left, and types associate to the right. We will use M, N, P, … to denote arbitrary terms; x, y, z, … to denote arbitrary variables; and σ, τ, γ, … to denote arbitrary types. δ will always denote a constant, and c will always be a ground constant. The binary relation symbol ≡ denotes syntactic equality.

Free and bound variables are defined as usual, and we consider terms that are identical modulo a change of bound variables to be syntactically identical. A term is closed if it has no free variables; otherwise it is open. A program is a closed term of ground type.

A substitution is a typed-respecting mapping of variables to terms. Substitutions are extended to terms as usual (taking care to avoid capture of free variables), and are written postfix, so that Mρ is the application of the substitution ρ to the term M. We call Mρ an instance of M. If x⃗ ≡ x_{1}, …, x_{n} and N⃗ ≡ N_{1}, …, N_{n}, then [x⃗ := N⃗] is the

                    tt, ff : o

\underline{n} : ι  for each integer n ≥ 0

                succ, pred : ι → ι
                    zero? : ι → o

cond_{o} : o → o → o → o
cond_{ι} : o → ι → ι → ι
Y_{σ} : (σ → σ) → σ  for each type σ

Figure 1: Constants of PCF

                              condtt x y → x
                              condff x y → y
                                 zero?\underline{0} → tt
                             zero?\underline{n + 1} → ff

succ\underline{n} → \underline{n + 1}

                                  pred\underline{0} → \underline{0}

pred\underline{n + 1} → \underline{n}
Y f → f(Y f)

Figure 2: Rewrite rules for PCF

substitution that maps each x_{i} to N_{i} (simultaneously), and is the identity otherwise. A special case is [x := N], so that M[x := N] is the result of substituting N for x in M. Sometimes we write M ≡ M(x⃗), with the intent that M(N⃗) ≡ M[x⃗ := N⃗].

A context C[·] is a term with some “holes”. C[M] denotes the result of putting M into the holes of C[·], which may cause free variables of M to become bound. We say C[·] is a program context for M if C[M] is a closed term of ground type.

The interpreter of the language is defined via a rewrite system; any set of δ-rules, together with the classical rule (β), induces the one-step reduction relation →. The relation ↠ is the reflexive transitive closure of →. Figure 2 gives the δ-rules for PCF.

B Simply Typed Models

Here we develop the general framework for function-based models of simply typed λcalculi.

A type frame {[[σ]]} is collection of sets indexed by type such that [[σ → τ]] is a set of functions from [[σ]] to [[τ]]. The sets [[σ]] are called domains, and the elements of each [[σ]] are called meanings or values of type σ.

Since our discussion focuses on issues of adequacy and full abstraction, we also require the following:

• there is a partial order ⊑_{σ} associated with each domain [[σ]];

• the functions of [[σ → τ]] are monotone with respect to the orderings ⊑_{σ} and ⊑_{τ}; • and the relation ⊑_{σ→τ} refines the pointwise relation on functions f, g ∈ [[σ → τ]],

i.e.,

f ⊑_{σ→τ} g implies f(d) ⊑_{τ} g(d) for all d ∈ [[σ]].

The last two conditions say that function application is monotone in both arguments; this implies that models, defined below, are compositional.

An environment is a type-respecting mapping from variables to values. If ρ is an environment, then the environment ρ[x := d] is ρ with the value of x updated to d:

ρ[x := d](y) = \{ \begin{matrix}d & if y ≡ x, \\ ρ(y) & otherwise. \end{matrix}

An interpretation is a type-respecting mapping from constants to values. For a given type frame {[[σ]]} and interpretation I we can try to define a model, [[·]], that is a mapping from each term to a meaning with respect to an environment, satisfying the following conditions:

[[δ]]ρ = I(δ)  (1)
[[x]]ρ = ρ(x)  (2)
[[(MN)]]ρ = ([[M]]ρ)([[N]]ρ)  (3)
([[λxM]]ρ)(d) = [[M]]ρ[x := d]  (4)

Implicit in condition (4) is the requirement that the function defined to be ([[λxM]]ρ) must be an element of the type frame. In other words, a model is a type frame that is closed under lambda-definability. Such closure certainly does not hold for all type frames (cf. [25]).

The meaning of a closed term is the same in any environment:

[[M]]ρ = [[M]]ρ′

for all closed M and arbitrary ρ, ρ′. Therefore we sometimes write [[M]] for the meaning of a closed term M, omitting the environment.

Continuity

We give the standard definitions for cpo’s and continuous functions, then define the cpo model of PCF.

A partial order or poset is a set D together with a binary relation ⊑ that is reflexive, transitive, and anti-symmetric. We will refer to the partial order ⟨D, ⊑⟩ as just D. A subset X ⊆ D is directed if every finite subset of X has an upper bound in X. A partial order D is a complete partial order or cpo if it has a least element ⊥_{D} and every directed subset X ⊆ D has a least upper bound ⊔X. We omit the subscript D in ⊥_{D} when it can be recovered from context. For any set X we define the cpo X_{⊥}, with elements X ∪{⊥_{X}}, ordered x ⊑ y iff x = y or x =⊥_{X}.

A function f : D → E between posets is monotone if f(x) ⊑_{E} f(y) whenever x ⊑_{D} y. We say f is continuous if it is monotone and f(⊔X) = ⊔f(X) for every directed X ⊆ D.

The set D →_{c} E of continuous functions from cpo D to cpo E is a cpo under the pointwise order ⊑_{p}, defined as follows:

f ⊑_{p} g iff f(x) ⊑_{E} g(x) for all x ∈ D.

If D is a cpo and f : D → D is continuous, then f has a least fixed point fix(f). The function fix itself is continuous, which will allow us to interpret the recursion operator Y.

Now we define the cpo model C[[·]] of PCF, based on continuous functions and cpos. First we construct a type frame with ground domains C[[o]] = {tt, ff }_{⊥} and C[[ι]] = {0, 1, 2, …}_{⊥}, and higher-order domains C[[σ → τ]] = C[[σ]] →_{c} C[[τ]]. The cpo model of PCF is then the model C[[·]] associated with {C[[σ]]} and the standard interpretation: the ground constants are interpreted in the obvious way; the constants Y_{σ} are interpreted as least fixed-point operators; and the interpretation of the remaining function constants is determined by the condition that the rewrite rules of Figure 2 be valid as equations.

Theorem 32 (Plotkin[30], Sazonov[31]) The cpo model C[[·]] is adequate but not fully abstract for PCF.

Stability

If D is a partial order and X ⊆ D, then X is bounded or consistent if there is an element y ∈ D such that x ⊑ y for all x ∈ X. If elements x and y are consistent we will write x ↑ y. We say D is bounded complete if every bounded subset X ⊆ D has a least upper bound ⊔X.

An element a ∈ D is compact if, for every directed X ⊆ D with a ⊑ ⊔X, there is some x ∈ X such that a ⊑ x. We define KD, the kernel of D, to be the set of compact elements of D. The cpo D is algebraic if, for every x ∈ D, the set ↓x = { a ∈ KD | a ⊑ x } is directed and ⊔ ↓x = x.

The greatest lower bound of a set X is denoted ⊓X. A cpo is distributive if x⊓(y⊔z) = (x ⊓ y) ⊔ (x ⊓ z) whenever y and z are consistent. An algebraic cpo D has property I if ↓a is finite for each a ∈ KD. A dI-domain is a distributive, bounded complete cpo that has property I.

A continuous function f between dI-domains is stable if whenever x ↑ y, we have that f(x⊓y) = f(x)⊓f(y). We let D →_{s} E be the set of stable functions between dI-domains D and E. As noted in [5], D →_{s} E ordered pointwise is not a dI-domain; accordingly we define the stable ordering ⊑_{s}:

f ⊑_{s} g iff f(x) = f(y) ⊓ g(x) whenever x ⊑ y.

Function tt ff ⊥
True  tt tt tt
False  ff ff ff
True!  tt tt ⊥
False!  ff ff ⊥
Id  tt ff ⊥
Not  ff tt ⊥
(tt⇒tt) tt ⊥ ⊥
(tt⇒ff) ff ⊥ ⊥
(ff⇒tt) ⊥ tt ⊥
(ff⇒ff) ⊥ ff ⊥
Bot  ⊥ ⊥ ⊥

Figure 3: Boolean functions

If D and E are dI-domains, then D →_{s} E is a dI-domain under the stable order.

It must be noted that the stable order is quite different from the pointwise order. For instance, consider the monotone Boolean functions, listed in Figure 3. These functions are both continuous and stable, and so they are elements of both the continuous and stable type frames. However, the stable ordering of o → o (Figure 5) is different from its pointwise ordering (Figure 4). In particular, consider True, the constant tt function, and True!, the strict constant tt function. Although True! ⊑_{p}True, we have True! ⋢_{s}True, since ⊥ ⊑_{s}tt but

True!(⊥) = ⊥ ≠ tt = (True!(tt) ⊓ True(⊥)).

(It is this that permits the existence of the function truesep that was needed in Corollary 15.)

Nevertheless, a stable model S[[·]] of PCF, based on dI-domains and stable functions, can be defined in much the same way as the cpo model. The ground domains S[[o]] and S[[ι]] of the stable type frame are identical to the ground domains of the cpo model. At higher types, however, we use stable functions: S[[σ → τ]] = S[[σ]] →_{s} S[[τ]]. Then we let S[[·]] be the model associated with the stable type frame and the (stable) standard interpretation (cf. the interpretation of the cpo model).

Theorem 33 (Berry[5]) The stable model S[[·]] is adequate but not fully abstract for PCF.

[figure: Bot; (tt⇒tt); (ff⇒ff); (ff⇒tt); (tt⇒ff); Id; True!; False!; Not; True; False]

Figure 4: Pointwise ordering of o → o

[figure: Bot; True; (tt⇒tt); (ff⇒ff); (ff⇒tt); (tt⇒ff); False; Id; True!; False!; Not]

Figure 5: Stable ordering of o → o

C Standard reductions in PCF-like rewrite systems

C.1 Preliminaries

This appendix gives a full definition of standard reductions and proof of the Standardization Theorem. In this section we sketch out some of the basic terminology of rewriting systems. Section C.2 introduces descendants, which allow us to trace subterms from step to step in a reduction. In Section C.3 we show that a very weak form of confluence holds for PCF-like systems; this property will be essential in proving the Standardization Theorem. Section C.4 introduces labelled rewrite systems, and proves that they are strongly normalizing. The labelled systems will be used in the proof of Standardization. The standard reductions are defined in Section C.5, and Standardization is proved in Section C.6. The proof is a variation of Klop’s proof for the pure λ-calculus [23], and involves a rewriting system on reductions. The system successively rewrites non-standard reduction paths to “more standard” paths; Standardization is proved by showing that the system is strongly normalizing, and that normal forms are standard reductions.

Our presentation of the machinery used to state and prove Standardization is necessarily brief. Much of the material is covered in more depth in standard references [3, 23]. Throughout we will work with a PCF-like rewrite system given by a language, L, and set, Θ, of linear ground δ-rules.

We assume that the reader is familiar with the following terminology. The notation M ⊂ N denotes that M is a subterm of N. A subterm may appear several times in a term; multiple occurrences of a subterm can be distinguished by their paths, which specify the exact position of a subterm inside the term. When we speak of a subterm M ⊂ N we implicitly mean a particular occurrence of M in N; the disambiguating paths are omitted.

Note that M → N iff there is an instance Δ → Δ′ of a rule π such that Δ ⊂ M, and N is obtained from M by replacing Δ with Δ′. We will write M →^{Δ}_{π} N in this case, and we call Δ a (π)-redex and Δ′ its (π)-contractum.

A reduction (path) σ is a sequence

σ : M_{1} →^{Δ_{1}}_{π_{1}} M_{2} →^{Δ_{2}}_{π_{2}} M_{3} →^{Δ_{3}}_{π_{3}} · · · .

We will use σ, τ , … to refer to reduction paths. Two reductions are coinitial if they start in the same term, and cofinal if they end in the same term.

C.2 Descendants

Consider some possible effects of a reduction M → N on a subterm Δ ⊂ M:

• Δ could be erased, as in (λx.y)Δ → y.

• Δ could be copied to some instances in N, as in (λx.δxx)Δ → δΔΔ.

• Δ could be left untouched and in its original position, as in Δ((λx.x)y) → Δy.

• The contracted redex might occur within Δ, transforming it into a syntactically different subterm in the same position.

In order to define and prove standardization, we will need to speak precisely about these cases, so we introduce descendants, which let us track a subterm throughout a reduction. We will not define descendants in their full generality, but only for certain subterms of interest. Our definition is equivalent to the standard definition [23] on those subterms.

Descendants are introduced via an annotated rewrite system derived from L and Θ, in which some λ’s and δ’s are marked with a ∗. Thus we define the language L_{∗}, whose symbols are those of L, with the addition of λ_{∗}, and δ_{∗}^{σ} for each constant δ^{σ} of L. The terms of L_{∗} are defined inductively:

• A constant δ^{σ} or δ_{∗}^{σ} is a term of type σ.

• A variable x^{σ} is a term of type σ.

• If M is a term of type (σ → τ) and N is a term of type σ, then (MN) is a term of type τ.

• If M is a term of type τ, then (λx^{σ}M) and (λ_{∗}x^{σ}M) are terms of type (σ → τ).

The erasure |M| ∈ L of M ∈ L_{∗} is obtained from M by leaving out the ∗’s. Substitution for the language is defined in the obvious way (with λ_{∗}’s binding variables just as λ’s). The rules of the new system include β and the rule scheme β_{∗}:

β_{∗} : (λ_{∗}xM)N → M[x := N].

Similarly, the δ-rules Θ_{∗} of the system are derived from the rules Θ. If θ is a rule of Θ,

θ : δ⟨c⃗, x⃗⟩ → P (x⃗),

then Θ_{∗} contains all rules of the form θ′ and θ_{∗}:

θ′ : δ⟨c⃗′, x⃗⟩ → P (x⃗),
θ_{∗} : δ_{∗}⟨c⃗′, x⃗⟩ → P (x⃗),

where c⃗′ is any vector of L_{∗} ground constants such that |c⃗′| ≡ c⃗.

There is a strong connection between the systems. Any Θ_{∗}-reduction path σ,

σ : M_{1} →^{Δ_{1}}_{π_{1}} M_{2} →^{Δ_{2}}_{π_{2}} M_{3} →^{Δ_{3}}_{π_{3}} ⋯,

projects to a Θ-reduction path |σ|:

|σ| : |M_{1}| →^{|Δ_{1}|}_{|π_{1}|} |M_{2}| →^{|Δ_{2}|}_{|π_{2}|} |M_{3}| →^{|Δ_{3}|}_{|π_{3}|} · · · .

Conversely, for any M ∈ L_{∗} and Θ-reduction path σ : |M| → ⋯, there is a unique lift of σ to a Θ_{∗}-reduction path σ′ : M → ⋯ such that σ ≡ |σ′|.

We will be interested in tracing subterms of the form (λx.M_{1})M_{2} or δM_{1} ⋯ M_{n} throughout a reduction; that is, β-redexes and possible δ-redexes. Accordingly, we introduce the following terminology. A subterm (λx.M_{1})M_{2} or δM_{1} ⋯ M_{n} of M is called a predescendant of M. If F is a set of predescendants of M ∈ L, we write (M, F) for the L_{∗} term derived from M by marking the head λ or δ of each predescendant in F with a ∗.

Definition 34 Suppose σ : M → ⋯ → N is a Θ-reduction path.

(i) If Δ is a predescendant of M, its set of descendants in N relative to σ, written (Δ/σ), is defined as follows.

Let M′ ≡ (M, {Δ}) and lift σ to σ′ : M′ → ⋯ → N′. If Δ ≡ (λxM_{1})M_{2} (resp. Δ ≡ δM_{1} ⋯ M_{n}), then (Δ/σ) =^{def} F, where F is the unique set of subterms of N of the form (λxM′_{1})M′_{2} (resp. δM′_{1} ⋯ M′_{n}), such that N′ ≡ (N, F).

(ii) If F is a set of predescendants of M, its descendants F/σ are defined

F/σ =^{def} ⋃{ Δ/σ | Δ ∈ F }.

(iii) Δ ⊂ M is an ancestor of Δ′ ⊂ N if Δ′ ∈ Δ/σ.

For a given reduction M_{1} → M_{2} → M_{3} → ⋯, we will sometimes speak of descendants and ancestors for subterms of terms M_{i} and M_{j}, where i and j are any indices such that j ≥ i. We do not specify the reduction from M_{i} to M_{j}, as it can be recovered from context.

{Note 35 \atop (i)} If M →^{Δ} N, then Δ has no descendants in N.

(ii) If M →^{Δ}_{θ} N, where Δ ≡ δ⟨c⃗, B⃗⟩, then no c_{i} has a descendant in N.

We mention that the following important property holds for our PCF-like systems, since it does not hold for all rewrite systems [23].

Note 36 If Δ ⊂ M and M → N, then descendants of Δ in N are disjoint.

Disjointness of descendants does not extend to ↠, as we indicate here:

(λy.(λx.yx)y)(λz.δ_{∗}z) →_{β} (λx.(λz.δ_{∗}z)x)(λz.δ_{∗}z)
→_{β} (λx.δ_{∗}x)(λz.δ_{∗}z)
→_{β} δ_{∗}(λz.δ_{∗}z).

Definition 37 Suppose M_{i} is a term in a reduction σ,

σ : M_{1} →^{Δ_{1}}_{π_{1}} M_{2} →^{Δ_{2}}_{π_{2}} M_{3} →^{Δ_{3}}_{π_{3}} · · · .

(i) We say Δ ⊂ M_{i} is (π)-contracted (in σ) if for some j ≥ i, Δ_{j} is a descendant of Δ and π_{j} = π.

(ii) We say Δ ⊂ M_{i} is active (in σ) if there is a Δ′ ⊂ Δ that is contracted in σ.

Sometimes it will be useful to specify a set of subterms of some term M, and consider reductions from M in which only those subterms are contracted. Such reductions are called developments. Because we work with systems in which a subterm can contract by more than one rule, our definition of developments extends the standard definition by specifying a rule for each redex contracted in a development.

Definition 38 Suppose the following: σ is a reduction from M to N; F is a set of subterms of M; and Π is a mapping that takes each Δ ∈ F to a rule π_{Δ}.

(i) We call σ a development of F from M by Π, written σ : (M, F) ↠^{Π} N, if each redex Δ′ contracted in σ is a descendant of some Δ ∈ F, and Δ′ is contracted by rule π_{Δ}.

(ii) We say a development σ is a complete development, written σ : (M, F) ↠_{cpl}^{Π} N, if

F/σ = ∅.

When Π is evident from context, we will omit mention of it.

Note 39 If F is a set of n disjoint redexes of M, then clearly all complete developments of F from M are of length n and are cofinal.

C.3 Properties related to confluence

Note 39 is a special case of a much stronger theorem, the Finite Developments theorem. We will not need to prove the Finite Developments theorem in its full generality; this section proves a weaker result that will be sufficient for our application.

Definition 40 We say two δ-redexes Δ_{1} and Δ_{2} overlap if either (i) they share the same head δ, or

(ii) one Δ_{i} appears as a critical argument of the other.

Note that in case (ii), the Δ_{i} must be a ground constant.

Often, rewrite systems are constrained to avoid overlapping redexes; such systems are guaranteed to be confluent. Because we allow overlapping rules, our systems are not confluent in general. However, they do satisfy the following much weaker property, which will be essential in our proof of standardization.

Lemma 41 Suppose σ_{1} : M_{0} →^{Δ_{1}} M_{1} and σ_{2} : M_{0} →^{Δ_{2}} M_{2}, where Δ_{1} and Δ_{2} do not overlap. Then complete developments of Δ_{2}/σ_{1} from M_{1} and Δ_{1}/σ_{2} from M_{2} are finite and cofinal.

Proof: For each of the various cases on the relative positions of Δ_{1} and Δ_{2} in M_{0}, we find a term M_{3} that is the final term of every complete development of Δ_{1}/σ_{2} and Δ_{2}/σ_{1}:

M_{0} ⟶^{Δ_{1}} M_{1}

↓^{Δ_{2}}  \begin{matrix} \\  \\  \\  \\  \\  \\  \\  &  \end{matrix}^{Δ_{2}/σ_{1}}
M_{2} −↠^{Δ_{1}/σ_{2}} M_{3}

1. Δ_{1} and Δ_{2} are disjoint. Then M_{0}, M_{1}, and M_{2} can be written

M_{0} ≡ ⋯ Δ_{1} ⋯ Δ_{2} ⋯,
M_{1} ≡ ⋯ Δ′_{1} ⋯ Δ_{2} ⋯,
M_{2} ≡ ⋯ Δ_{1} ⋯ Δ′_{2} ⋯,

where Δ′_{1} and Δ′_{2} are the respective contractums of Δ_{1} and Δ_{2}. Now defining

M_{3} ≡^{def} ⋯ Δ′_{1} ⋯ Δ′_{2} ⋯,

we see that the only complete development of Δ_{2}/σ_{1} is M_{1} →^{Δ_{2}} M_{3}, and the only complete development of Δ_{1}/σ_{2} is M_{2} →^{Δ_{1}} M_{3}, as desired.

2. Δ_{1} ⊂ Δ_{2}. Then there is a unique descendant Δ′_{2} of Δ_{2} in M_{1}, and we consider three subcases.

(a) Δ_{2} ≡ (λx. · · · Δ_{1} ⋯)N. Then we can write M_{0}, M_{1}, and M_{2} as

M_{0} ≡ ⋯ ((λx. · · · Δ_{1} ⋯)N) ⋯,
M_{1} ≡ ⋯ ((λx. · · · Δ′_{1} ⋯)N) ⋯,
M_{2} ≡ ⋯ ((⋯ Δ_{1} ⋯)[x := N]) ⋯,

where Δ′_{1} is the contractum of Δ_{1}, and Δ′_{2} ≡ (λx. · · · Δ′_{1} ⋯)N. If we take

M_{3} ≡^{def} ⋯ ((⋯ Δ′_{1} ⋯)[x := N]) ⋯,

then the only complete development of Δ_{2}/σ_{1} is M_{1} →^{Δ′_{2}}_{β} M_{3}. Furthermore, substitutivity holds for PCF-like rewrite systems; that is,

M →^{Δ} M′ ⟹ M[x := N] →^{Δ′} M′[x := N],

where Δ′ is Δ with any free occurrences of x replaced by N. Thus the only complete development of Δ_{1}/σ_{2} is M_{2} → M_{3}.

(b) Δ_{2} ≡ (λx.N)(⋯ Δ_{1} ⋯). Then M_{0}, M_{1}, and M_{2} can be written

M_{0} ≡ ⋯ ((λx.N)(⋯ Δ_{1} ⋯)) ⋯,
M_{1} ≡ ⋯ ((λx.N)(⋯ Δ′_{1} ⋯)) ⋯,
M_{2} ≡ ⋯ (N[x := (⋯ Δ_{1} ⋯)]) ⋯,

where Δ′_{1} is the contractum of Δ_{1}, and Δ′_{2} ≡ (λx.N)(⋯ Δ′_{1} ⋯). Defining

M_{3} ≡^{def} ⋯ (N[x := (⋯ Δ′_{1} ⋯)]) ⋯,

we see that the only complete development of Δ_{2}/σ_{1} is M_{1} →^{Δ′_{2}}_{β} M_{3}. Furthermore, descendants of Δ_{1} in M_{2} are disjoint, and any contraction of them in turn is a reduction M_{2} →^{Δ_{1}} ⋯ →^{Δ_{1}} M_{3}.

(c) Δ_{2} ≡ δ_{θ}⟨⋯, ⋯ (⋯ Δ_{1} ⋯) ⋯⟩. Then we write M_{0}, M_{1}, and M_{2} as

M_{0} ≡ ⋯ (δ_{θ}⟨⋯, ⋯ (⋯ Δ_{1} ⋯) ⋯⟩) ⋯,
M_{1} ≡ ⋯ (δ_{θ}⟨⋯, ⋯ (⋯ Δ′_{1} ⋯) ⋯⟩) ⋯,
M_{2} ≡ ⋯ (P_{θ}(⋯ (⋯ Δ_{1} ⋯) ⋯)) ⋯,

where Δ′_{1} is the contractum of Δ_{1}, and Δ′_{2} ≡ δ_{θ}⟨⋯, ⋯ (⋯ Δ′_{1} ⋯) ⋯⟩. Defining

M_{3} ≡^{def} ⋯ (P_{θ}(⋯ (⋯ Δ′_{1} ⋯) ⋯)) ⋯,

we see that the only complete development of Δ_{2}/σ_{1} is M_{1} →^{Δ′_{2}}_{θ} M_{3}. And just as in case 2b, the descendants of Δ_{1} in M_{2} are disjoint, so by contracting them in turn we find a reduction M_{2} →^{Δ_{1}} ⋯ →^{Δ_{1}} M_{3}.

3. Δ_{2} ⊂ Δ_{1}. This case is handled exactly as case 2.

■

C.4 A labelled λ-calculus

For any PCF-like rewrite system, there is a corresponding labelled PCF-like system that is strongly normalizing. The labelling technique has led to some of the simplest proofs for many syntactic properties, and we will use it in our proof of standardization. This section introduces labelled calculi and proves that they are strongly normalizing.

The labelled system is similar to the system that we introduced earlier to define descendants. However, the systems are also different in important ways, since they are intended for different purposes. In the labelled system, we will mark δ’s with nonnegative integers instead of ∗’s, and we will not need to mark λ’s. Furthermore, we do not allow unmarked δ’s. The reasons for this will become apparent in what follows.

For any PCF-like language L, the language L_{ℕ} is just the PCF-like language with constants δ_{n}^{σ} for each constant δ^{σ} of L and each n ∈ ℕ.

Notation 42 (i) If M ∈ L_{ℕ}, then |M| ∈ L is the term derived from M by erasing the labels on the constants.

(ii) If M ∈ L, then M^{n} ∈ L_{ℕ} is the term derived from M by labelling each constant with n.

The δ-rules Θ_{ℕ} of the labelled calculus are defined as follows. If θ is a rule of Θ,

θ : δ⟨c⃗, x⃗⟩ → P (x⃗),

then Θ_{ℕ} contains all rules of the form θ_{ℕ}:

θ_{ℕ} : δ_{n+1}⟨c⃗′, x⃗⟩ → P^{n}(x⃗),

where c⃗′ is a vector of L_{ℕ} ground constants such that |c⃗′| ≡ c⃗. Note that there is no rule for any δ_{0}.

The projection |σ| of a Θ_{ℕ}-reduction path σ is defined in the obvious way. And any Θ-reduction σ can be lifted to a Θ_{ℕ}-reduction σ′ such that σ ≡ |σ′| (e.g., label each constant in the first term of σ by the length of σ).

Definition 43 A term M is strongly normalizable (SN) if all reductions starting at M are finite.

Theorem 44 (Strong Normalization) Every L_{ℕ} term is strongly normalizable.

The rest of this section lays out the proof of strong normalization. We use a straightforward extension of the method of [17]. Definition 45 The notion of strong computability (SC) of a term is defined by induction as follows:

(i) A term of ground type is SC iff it is SN (ii) A term M^{(σ→τ)} is SC iff, for every SC term N^{σ}, the term (MN)^{τ} is SC Note 46 By definition 45(ii) a term M is SC iff, for all vectors N⃗ of SC terms driving M to ground type, the term MN⃗ is SC. And by definition 45(i), such an MN⃗ is SC iff it is SN. Definition 47 An atom is a variable or a constant δ_{n} with no rule.

{Lemma 48 \atop (i)} If a is an atom and N⃗ is a vector of SN terms, then the term aN⃗ is SC. (ii) Every SC term M is SN. Proof: By induction on the type of aN⃗ and M.

1. Basis: aN⃗ and M have ground type. (i) Since each N_{i} is SN, aN⃗ must be SN, and therefore SC by definition 45(i). (ii) By definition 45(i).

2. Induction: aN⃗ and M have type σ → τ.

(i) Let P^{σ} be SC. By the induction hypothesis (ii), P is SN. Then by induction, the term (aN⃗P)^{τ} is SC. Therefore so is aN⃗ by definition 45(ii).

(ii) Let x^{σ} be a variable not occurring in M. By the induction hypothesis (i), x is SC. Then (Mx)^{τ} is SC, and therefore SN by induction. But any subterm of an SN term is SN, so M is SN as well.

■

Lemma 49 If N is SC and M[x := N] is SC, then so is (λxM)N. Proof: Let P⃗ ≡ P_{1}, …, P_{n} be a vector of SC terms driving M to ground type. Since M[x := N] is SC, the term

(M[x := N])P⃗  (5)

is SN by Note 46. The lemma follows from Note 46 if we can prove that

(λxM)NP⃗  (6)

is SN.

Now since (5) is SN, all of its subterms are SN, including M[x := N], P⃗. Furthermore by hypothesis and the preceding lemma, N is SN. Therefore an infinite reduction from (6) cannot consist entirely of contractions in M, N, P_{1}, …, P_{n}. So an infinite reduction of (6) must have the form

(λxM)NP_{1} ⋯ P_{n} ↠ (λxM′)N′P′_{1} ⋯ P′_{n}
→ M′[x := N′]P′_{1} ⋯ P′_{n}
↠ …

(where M ↠ M′, etc.) From the reductions M ↠ M′ and N ↠ N′ we have

M[x := N] ↠ M′[x := N′]

Then we can construct an infinite reduction from (5) as follows:

M[x := N]P_{1} ⋯ P_{n} ↠ M′[x := N′]P′_{1} ⋯ P′_{n}
↠ …

But this contradicts the fact that (5) is SN. Therefore there is no infinite reduction from (6); it must be SN. ■

Lemma 50 Consider a constant δ and a vector N⃗ of SC terms driving δ to ground type. If for each rule θ on δ,

θ : δ_{θ}⟨c⃗, x⃗⟩ → P_{θ}(x⃗),

where δN⃗ ≡ δ_{θ}⟨N⃗_{1}, N⃗_{2}⟩N⃗_{3}, we have that

P_{θ}(N⃗_{2})N⃗_{3}  (7)

is SC, then δN⃗ is SC.

Proof: We must show that δN⃗ is SN. Since the N⃗ are SC, by Lemma 48 they are SN. Therefore any infinite reduction from δN⃗ must look like

δ_{θ}⟨N⃗_{1}, N⃗_{2}⟩N⃗_{3} ↠ δ_{θ}⟨c⃗, N⃗_{2}′⟩N⃗_{3}′
→ P_{θ}(N⃗_{2}′)N⃗_{3}′
↠ ⋯

where N⃗_{1} ↠ c⃗, N⃗_{2} ↠ N⃗_{2}′, etc. But then we can construct an infinite reduction from (7) as follows:

P_{θ}(N⃗_{2})N⃗_{3} ↠ P_{θ}(N⃗_{2}′)N⃗_{3}′
↠ ⋯

But as (7) is SC, by Lemma 48 it is SN, a contradiction. Therefore δN⃗ is SN. ■

Lemma 51 For any term M and substitution ρ ≡ [x⃗ := N⃗], where each N_{i} is SC, the term Mρ is SC.

Proof: The proof is by induction on the lexicographic ordering of (m, M), where m is the maximum δ-index appearing in M.

1. M is a variable x_{i}. Then Mρ is N_{i} and the result follows.

2. M is an atom distinct from x_{1}, …, x_{n}. Then Mρ ≡ M which is SC by Lemma 48. Note that this includes all constants δ_{0}.

3. M ≡ δ_{m+1}. Then Mρ ≡ δ_{m+1}. Thus it is sufficient to show that for any vector N⃗′ of SC terms driving δ_{m+1} to ground type, the term δ_{m+1}N⃗′ is SC.

Consider any rule θ on δ_{m+1}:

θ : δ_{m+1}⟨c⃗, x⃗⟩ → P (x⃗).

By construction of the labelled calculus, no constants in P are labelled with an index greater than m. Thus we can apply the induction hypothesis to P.

If we rewrite δ_{m+1}N⃗′ as δ_{m+1}⟨N⃗_{1}′, N⃗_{2}′⟩N⃗_{3}′, by induction P (N⃗_{2}′) is SC. Then by the definition of SC, the term P (N⃗_{2}′)N⃗_{3}′ is SC. Therefore by Lemma 50, δ_{m+1}N⃗′ is SC.

4. M ≡ λy^{σ}M_{1}. Then Mρ ≡ λy(M_{1}ρ), neglecting changes in bound variables.

To show that Mρ is SC we must show that for all SC terms N^{σ}, the term (Mρ)N is SC. But (Mρ)N ≡ (λy(M_{1}ρ))N, and

(M_{1}ρ)[y := N] ≡ M_{1}[x_{1} := N_{1}] ⋯ [x_{n} := N_{n}][y := N]

which is SC by induction. Therefore (λy(M_{1}ρ))N is SC by Lemma 49.

5. M ≡ M_{1}M_{2}. Then Mρ ≡ (M_{1}ρ)(M_{2}ρ), and M_{1}ρ and M_{2}ρ are SC by induction. Therefore Mρ is SC by definition 45(ii).

■

Proof of Theorem 44 (Strong Normalization): By Lemma 51, every term M is SC (just let x⃗ be empty). Then by Lemma 48, M is strongly normalizing. ■

C.5 Standard Reductions

Our definition of standard reductions is similar to that of [19], with a few important differences. The “linear ground” restriction imposed on our systems gives us a particularly simple class of rewrite rules, and this simplicity carries over to the definition of standard reductions. On the other hand, the systems of [19] do not include λ-abstraction, and forbid overlapping rewrite rules, which we allow.

Overlapping rules do not add much complication to the definition of standard reductions, but they are more of an obstacle in the proof of standardization. Overlapping systems are not confluent in general, so we cannot use confluence and related properties in our proof. This is offset by the fact that we consider only typed systems.

The standard reductions of [19] are based on “outside-in” reductions. Informally, outside-in reductions are reductions in which no subterm of a term reduces before the term itself contracts, unless the subterm reduces outside-in and contributes towards making the term a redex. For example, consider the PCF reduction

                    cond (zero? 0) M N → condtt M N

→ M.

The reduction is standard, even though the term cond (zero? 0) M N contracts after its subterm (zero? 0), because it is the contraction of (zero? 0) that turns the cond term into a redex.

There is a natural way of testing whether or not a reduction is outside-in: first, identify “outermost” subterms that contract; each of these identifies subterms that must reduce before the outer subterm itself contracts. By iterating the process, we can identify a subterm or subterms that must reduce before any others, if the reduction is to be outside-in. This idea is the basis of our definition of standard reductions.

For each term in a reduction, we identify a principal redex, and call a reduction standard if the redex contracted at each step is the principal redex. For the pure λ-calculus, the principal redex for some M_{i} will simply be the leftmost redex of M_{i} contracted in the reduction.

For systems with constants, we must allow reductions to take place in the critical arguments of some δ-terms. To find the principal redex, then, we start by considering the leftmost contracted subterm; if it is a δ-term, we then consider critical arguments in which contractions take place, etc. Eventually, consideration of these preprincipal subterms leads to the principal redex.

Definition 52 Let M_{i} be a term in a reduction path σ,

σ : M_{1} →^{Δ_{1}} M_{2} →^{Δ_{2}} M_{3} →^{Δ_{3}} · · · .

A contracted subterm Δ of M_{i} is preprincipal in σ if (i) Δ is the leftmost subterm of M_{i} contracted in σ; or

(ii) there is a subterm Δ′ of M_{i} such that:

• Δ′ is θ-contracted in σ;

• Δ′ is of the form δ_{θ}⟨A⃗, B⃗⟩, where the leftmost active critical argument, A_{k}, is of the form ΔN⃗; and

• Δ′ is preprincipal in σ.

We write pp_{σ}(Δ) if Δ is preprincipal in σ.

This next lemma is essential in showing an important property of the preprincipal subterms: they are linearly ordered by ⊂ (see the following note):

Lemma 53 Let M_{i} be a term in a reduction path σ,

σ : M_{1} →^{Δ_{1}} M_{2} →^{Δ_{2}} M_{3} →^{Δ_{3}} ⋯,

and let Δ be a preprincipal subterm of M_{i}. If Δ ≢ Δ_{i}, then Δ has a unique, preprincipal descendant Δ′ ⊂ M_{i+1}.

Proof: By induction on how pp_{σ}(Δ).

(i) pp_{σ}(Δ) because Δ is the leftmost contracted subterm of M_{i}. Then clearly Δ has some unique descendant Δ′ in M_{i+1}. Furthermore Δ′ is the leftmost contracted subterm of M_{i+1}, as the contraction of Δ_{i} can only introduce terms to the right of Δ′. Thus pp_{σ}(Δ′).

(ii) pp_{σ}(Δ) because M_{i} contains a preprincipal, θ-contracted subterm, δ_{θ}⟨A⃗, B⃗⟩, whose leftmost active critical argument, A_{k}, is of the form ΔN⃗.

Now Δ_{i} ≢ δ_{θ}⟨A⃗, B⃗⟩, else by Note 35(ii), Δ would have no descendant in M_{i+1}, contradicting the fact that it is contracted in σ.

So by induction, δ_{θ}⟨A⃗, B⃗⟩ has a unique, preprincipal descendant, which must be of the form δ_{θ}⟨A⃗′, B⃗′⟩. But then A′_{k} ≡ Δ′N⃗′, where Δ′ is the unique descendant of Δ, and furthermore pp_{σ}(Δ′).

■

{Note 54 \atop (i)} By Lemma 53, every preprincipal subterm contracts exactly once in σ. Thus the θ and A_{k} of Definition 52(ii) are unique.

(ii) By (i), we conclude that if Δ_{1} and Δ_{2} are distinct, preprincipal subterms of M_{i}, then either Δ_{1} ⊂ Δ_{2} or Δ_{2} ⊂ Δ_{1}.

Definition 55 Suppose σ is a reduction path,

σ : M_{1} →^{Δ_{1}} M_{2} →^{Δ_{2}} M_{3} →^{Δ_{3}} · · · .

(i) We define the principal redex pr_{σ}(M_{i}) to be the innermost preprincipal subterm of M_{i}. By Note 54(ii), this is well defined.

(ii) We say σ is a standard reduction if for all i, Δ_{i} ≡ pr_{σ}(M_{i}).

The following theorem is the main result of this appendix.

Theorem 56 (Standardization) If M ↠ N is a finite reduction in a PCF-like rewrite system, then there is a standard reduction from M to N.

C.6 Path-reduction

This section gives our proof of Standardization. It is based on a proof in [23] for the pure λ-calculus, which introduced a sort of meta-reduction: a reduction relation on reduction paths. This path-reduction rewrites non-standard reductions into “more standard” reductions. The following results motivate the definition of path-reduction.

Lemma 57 Let σ be a reduction path,

σ : M_{1} →^{Δ_{1}} M_{2} →^{Δ_{2}} M_{3} →^{Δ_{3}} ⋯,

and let Δ ≡ pr_{σ}(M_{i}). If Δ_{i} ≢ Δ, then Δ has a unique descendant Δ′ ⊂ M_{i+1}, and Δ′ ≡ pr_{σ}(M_{i+1}).

Proof: Lemma 53 proves uniqueness. To show Δ′ ≡ pr_{σ}(M_{i+1}), by the definition of pr_{σ} and Lemma 53 it suffices to note the following: if Δ_{1} ⊂ Δ_{2} ⊂ M have unique descendants Δ′_{1}, Δ′_{2} ⊂ M′, where M → M′, then Δ′_{1} ⊂ Δ′_{2}. ■

Corollary 58 Suppose σ is a reduction path,

σ : M_{1} →^{Δ_{1}} M_{2} →^{Δ_{2}} ⋯ →^{Δ_{n−1}} M_{n}.

Then σ is standard iff there is no j such that Δ_{j} is the descendant of pr_{σ}(M_{j−1}).

The corollary suggests a possible way to transform a non-standard reduction into a standard reduction: successively “swap” the contraction of a principal redex with the contraction of a non-principal redex at the previous step. If we reach a reduction in which each principal redex contracts as soon as it becomes principal, we will have found a standard reduction.

Definition 59 Suppose σ is a non-standard reduction, that is, there is some j such that

σ : ⋯ → M_{j−1} →^{Δ_{j−1}} M_{j} →^{Δ_{j}} M_{j+1} → ⋯

where Δ_{j} is the descendant of Δ′_{j} ≡ pr_{σ}(M_{j−1}). The subpath

M_{j−1} →^{Δ_{j−1}} M_{j} →^{Δ_{j}} M_{j+1}

is called the path-redex at step j. Note that Δ′_{j} and Δ_{j−1} do not overlap, and furthermore, by Lemma 57, Δ_{j} is the unique descendant of Δ′_{j}. Therefore by Lemma 41, we can find a sequence

M_{j−1} →^{Δ′_{j}} M′_{j} →^{Δ′_{j−1}} ⋯ →^{Δ′_{j−1}} M_{j+1},

where the Δ′_{j−1} are the descendants of Δ_{j−1}. Such a sequence is call a path-contractum.

Finally, we define path-reduction: σ →_{path}^{j} σ′ if σ′ is obtained from σ by replacing the

path-redex at step j by a corresponding path-contractum. We will drop the index j when convenient.

Clearly, path-reduction preserves initial and final terms, and any path-reduction normal form is a standard reduction. Moreover, the next two lemmas show that pathreduction is strongly normalizing.

Lemma 60 Suppose σ →_{path}^{j} σ′, where

\begin{aligned}σ & : & M_{1} → ⋯ → M_{j−1} →^{Δ_{j−1}} M_{j} →^{Δ_{j}} M_{j+1} → ⋯, \\ σ′ & : & M_{1} → ⋯ → M_{j−1} →^{Δ′_{j}} M′_{j} →^{Δ′_{j−1}} ⋯ →^{Δ′_{j−1}} M_{j+1} → · · · . \end{aligned}

Then for i ≠ j, the following hold:

(i) If Δ ⊂ M_{i} is not contracted in σ, then it is not contracted in σ′.

(ii) If Δ ⊂ M_{i} is contracted in σ and pp_{σ}(Δ), then Δ is contracted in σ′.

(iii) If Δ ⊂ M_{i} is preprincipal in σ, then it is preprincipal in σ′.

(iv) pr_{σ}(M_{i}) ≡ pr_{σ′}(M_{i}).

Proof:

(i) Just note that path-reduction only permutes the order of contraction of subterms; it does not introduce new contractions.

(ii) It is clear that if Δ contracts in σ and does not contract in σ′, then Δ is either Δ_{j−1} or one of its ancestors. Thus we only need consider Δ_{j−1}.

If Δ_{j−1} does not contract in σ′, then it must be contained in Δ′_{j}. But Δ′_{j} is the principal redex of M_{j−1}, that is, the innermost preprincipal subterm of M_{j−1}. So if Δ_{j−1} is not contracted in σ′, it is not preprincipal in σ.

(iii) We use induction on how pp_{σ}(Δ).

1. pp_{σ}(Δ) because Δ is the leftmost contracted subterm of M_{i}. By (ii), Δ is contracted in σ′, and by (i), it is the leftmost contracted subterm of M_{i} in σ′. Therefore pp_{σ′}(Δ).

2. pp_{σ}(Δ) because pp_{σ}(δ_{θ}⟨A⃗, B⃗⟩), and the leftmost active critical argument, A_{k}, is of the form ΔN⃗. By induction, pp_{σ′}(δ_{θ}⟨A⃗, B⃗⟩), and by (ii), Δ is contracted in σ′. So A_{k} is active in σ′, and by (i), it is the leftmost active critical argument. Therefore pp_{σ′}(Δ).

(iv) This follows from (i), (iii), and the definition of pr_{σ}.

■

Lemma 61 If σ is a finite reduction, then there is no infinite path-reduction starting from σ.

Proof: Consider a path-reduction

σ ≡ σ_{1} →_{path} σ_{2} →_{path} σ_{3} →_{path} · · · .

It is not hard to see that the reduction could have been carried out in the labelled system; that is, if σ′_{i} is a labelled reduction such that |σ′_{i}| ≡ σ_{i}, and σ_{i} →_{path}^{j} σ_{i+1}, then there is

a labelled reduction σ′_{i+1} such that |σ′_{i+1}| ≡ σ_{i+1}, and σ′_{i} →_{path}^{j} σ′_{i+1}. Thus we can find

labelled reductions σ′_{1}, σ′_{2}, σ′_{3}, … such that |σ′_{i}| ≡ σ_{i}, and

σ′_{1} →_{path} σ′_{2} →_{path} σ′_{3} →_{path} · · · .

And because labelled reduction is strongly normalizing, and each σ′_{i} begins with the same L_{ℕ} term, each σ_{i} is finite.

Furthermore, the path-reduction can be thought of as constructing a tree of terms, with each path from root to leaf corresponding to a reduction σ_{i}. Each contracted path-redex introduces a branching in the tree. For example, if σ_{i} →_{path}^{j} σ_{i+1}, then the

root-to-leaf path corresponding to σ_{i+1} is obtained by branching off of the root-to-leaf path of σ_{i} at depth j − 1. The situation is depicted in the following figure, where the root of the tree is displayed at the left and the leaves are displayed at the right:

M_{1} ⟶ ⋯ ⟶ M_{j−1} ⟶^{Δ_{j−1}} M_{j} ⟶^{Δ_{j}} M_{j+1} ⟶ ⋯ ⟶ M_{n} : σ_{i}
↓_{Δ′_{j}}
M′_{j} ⟶^{Δ′_{j−1}} ⋯ ⟶^{Δ′_{j−1}} M_{j+1} ⟶ ⋯ ⟶ M_{n} : σ_{i+1}

By Lemma 60(iv), the tree is a binary tree, and we have just seen that there is no infinite path from the root. Then by König’s Lemma, the tree is finite, so the number of different reductions given by the tree must be finite. ■

Proof of Theorem 56 (Standardization): If σ : M ↠ N is a finite reduction in a PCF-like system, we can obtain a standard reduction from M to N just by finding a path-reduction normal form of σ. ■

Note that we have not shown that path-reduction normal forms are unique: that is, if

σ →_{path} ⋯ →_{path} σ_{1},

and σ →_{path} ⋯ →_{path} σ_{2},

where σ_{1} and σ_{2} are normal forms, we are not guaranteed that σ_{1} ≡ σ_{2}. We expect that the property holds, but haven’t tried to verify that it does, since it is not needed to prove Standardization.