Observable Sequentiality and

Full Abstraction

Robert Cartwright Matthias Felleisen

Department of Computer Science

Rice University Houston, TX 77251-1892

Rice Technical Report CS 91-167

A preliminary version of this technical report appeared in the

Proceedings of the 19th Annual ACM Symposium

on Principles of Programming Languages, January 19–22, 1992, Albuquerque, New Mexico.

Copyright \begin{matrix}c \\ ◯ \end{matrix}1992 by Robert Cartwright and Matthias Felleisen 1.1 Summary of Previous Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Summary of Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 PCF 4 2.1 Formal Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Observational Equivalence, Sequentiality . . . . . . . . . . . . . . . . . . . . 8

3 Observing Sequentiality 9 3.1 Using errors, programmers can observe the order of evaluation. . . . . . . . 10 3.2 Using control operators, programs can observe the order of evaluation. … 10 3.3 Procedure denotations contain more computational structure than ordinary

function graphs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.4 Higher-order procedures explore trees sequentially. . . . . . . . . . . . . . . 13

4 The Tree Model 15 4.1 Tree Domains . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2 Application . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 4.3 Assigning Meaning to Phrases . . . . . . . . . . . . . . . . . . . . . . . . . . 31 4.4 Operational Properties of the Model . . . . . . . . . . . . . . . . . . . . . . 37

5 The Full Abstraction Theorem 41

6 Observable Sequentiality in SPCF 48

7 Generalizing Observable Sequentiality 50

A K and S 51 A.1 The K Combinator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 A.2 The S Combinator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

B Equations for catch and error 63

Observable Sequentiality and Full Abstraction

Robert Cartwright Matthias Felleisen^{∗} Department of Computer Science Rice University Houston, TX 77251-1892

August 13, 1992

Abstract

One of the major challenges in denotational semantics is the construction of fully abstract models for sequential programming languages. For the past fifteen years, research on this problem has focused on developing models for PCF, an idealized functional programming language based on the typed λ-calculus. Unlike most practical languages, PCF has no facilities for observing and exploiting the evaluation order of arguments in procedures. Since we believe that such facilities are crucial for understanding the nature of sequential computation, this paper focuses on a sequential extension of PCF (called SPCF) that includes two classes of control operators: error generators and escape handlers. These new control operators enable us to construct a fully abstract model for SPCF that interprets higher types as sets of error-sensitive functions instead of continuous functions. The error-sensitive functions form a Scott domain that is isomorphic to a domain of decision trees.

1 Full Abstraction and Sequentiality

A denotational semantics for a programming language determines two natural equivalence relations on program phrases. The first relation, denotational equivalence, equates two phrases if and only if they denote the same element in the model. The second relation, observational equivalence, equates two phrases if and only if they have the same “observable behavior”. In the denotational framework, observable behavior refers to the output produced by entire programs. Thus, two phrases are observationally equivalent if and only if they can be interchanged in an arbitrary program without affecting the output.

These two equivalence relations are different in general. Denotational equivalence implies observational equivalence because denotational models are compositional. However, the converse rarely holds for conventional models of practical programming languages; some observationally equivalent phrases inevitably have different meanings. A semantics in which denotational equivalence and observational equivalence coincide is said to be fully abstract.

Observational equivalence is the fundamental constraint governing program optimization. Since the users of a program are primarily interested in its input-output behavior, a compiler can optimize a program by interchanging observationally equivalent phrases. If a denotational semantics is fully abstract, then observational equivalence reduces to denotational equivalence, which can be analyzed using algebraic methods. Consequently, one of the primary goals of research in denotational semantics has been the construction of fully abstract models for practical languages.

∗Both authors were supported in part by NSF grants CCR 89-17022 and CR-91-22518.

The following example shows why conventional continuous function models are not fully abstract for higher-order sequential languages. Consider the following family of procedures^{1} p_{i} defined in a sequential, call-by-name functional language L:

p_{i}(f) = if f(Ω,false) then Ω else if f(false,Ω) then Ω else if f(true,true) then i else Ω .

In this equation, Ω denotes any divergent expression and i denotes an arbitrary natural number. It is easy to show by an exhaustive case analysis that the procedures p_{i} diverge for all inputs because the only possible inputs f are sequential procedures. Hence, p_{i} is observationally equivalent to the procedure p defined by p(f) = Ω.

On the other hand, the conventional model for language L includes functions that evaluate their arguments in parallel. A simple example of a parallel function is parallel-and, which returns false if either input is false and returns true if both inputs are true. If we apply p_{i} to parallel-and, the computation produces the answer i instead of ⊥ because the divergent subcomputations are ignored by parallel-and. Consequently, the conventional model for such functional languages fails to identify p_{i} and p.

Essentially the same example can be constructed in any practical deterministic programming language where procedures can be passed as parameters [15, 22]. For example, in call-by-value languages, the procedures p_{i} can be rewritten so that the parameter f takes constant procedures as arguments and uses these procedures to simulate call-by-name boolean arguments [22]. Indeed, all commonly used deterministic languages are sequential. In informal terms, a language is sequential if it can be implemented without time-slicing among multiple threads of control. Practical languages eschew parallel operations like parallel-and because they are painful to implement and encourage hideously inefficient programming. Even deterministic languages for parallel machines like C^{∗} [19] are sequential.

1.1 Summary of Previous Work

Milner [16] and Plotkin [18] were the first researchers to study the full abstraction problem for sequential languages. They focused on constructing fully abstract models for PCF, a call-by-name functional language based on the typed λ-calculus. The preceding example shows that the continuous function model for PCF is not fully abstract. Milner and Plotkin developed different strategies for eliminating the discrepancy between the continuous function model and the observable behavior of PCF.

Milner eliminated parallel functions from the model by constructing a syntactic model in which the elements are equivalence classes of observationally equivalent terms. Although Milner’s model is fully abstract, it is not generally regarded as a “denotational” model because it does not identify any algebraic structure within programs. Plotkin extended PCF by adding parallel deterministic operations, eliminating the discrepancy between the continuous function model and the procedures definable in the language. Unfortunately, neither Milner’s nor Plotkin’s result showed how to construct fully abstract denotational models for sequential languages.

1We use the term procedure rather than function to refer to the primitive operators in a functional programming language because procedures are not necessarily interpreted as functions in models.

In a subsequent investigation of sequential languages, Berry and Curien [3, 4, 6, 8] constructed models for PCF with more restrictive domains of procedure denotations. Berry eliminated many parallel functions from these domains by forcing functions to be stable. This construction eliminated some of the spurious distinctions between phrases in the conventional model, but it introduced some new ones.^{2} To address this problem, Berry and Curien [4, 5] proposed interpreting procedures as sequential algorithms over concrete domains [14]. Roughly speaking, a concrete domain is a domain that is isomorphic to a domain consisting of potentially infinite trees. A sequential algorithm is a function plus a strategy for evaluating its arguments. While this approach eliminates all parallel functions, the resulting model is not extensional because it contains different sequential algorithms with exactly the same behavior under application. In addition, PCF cannot express all of the observations that characterize sequential algorithms, such as the order of argument evaluation. As a result, the sequential algorithm model for PCF is not fully abstract.

Recently, Mulmuley [17] generalized Milner’s work by showing how to construct a fully abstract model for PCF as a quotient of a conventional model based on lattices instead of cpos. Mulmuley defined a retraction on the conventional model that equates all parallel functions with the “overdefined” element top (⊤). However, like Milner’s original fully abstract model, Mulmuley’s model is “syntactic” in flavor because it relies on a quotient construction based on observational equivalence. For more details on the history of the full abstraction problem for sequential languages, we refer the reader to two extensive surveys [6, 25].

1.2 Summary of Results

Fifteen years after Milner’s and Plotkin’s original work, the fundamental question still remains:

Are there fully abstract denotational models for sequential programming languages?

In this paper, we answer the question affirmatively by showing how to construct a fully abstract denotational model for an observably sequential functional programming language that is a simple sequential extension of PCF. The construction relies on two closely related insights:

1. In practical languages, a programmer can use run-time errors to observe the order in which a procedure evaluates its arguments. Similarly, many practical languages permit programs to determine and exploit their sequential evaluation order by using explicit control operators such as exception generators and handlers.

2This observation is due to T. Jim and A. Meyer [13]. In the stable function model, two procedures corresponding to the same continuous function can denote inconsistent stable functions. The procedures +_{l} and +_{r} defined in Section 2 have this property. As a result, there is a higher order stable function +_{l}? that maps +_{l} to 0 and +_{r} to 1. In PCF, +_{l}? is not definable, but it is easy to define a family of “recognizers”

{q_{i} | i ∈ } for +_{l}? (analogous to the procedures p_{i} described earlier) that diverge on all definable inputs but map +_{l}? to i.

2. Continuous functions can be identified with decision trees if they are constructed by composing error-sensitive operations. In informal terms, an operation is errorsensitive if it propagates any errors that it encounters in evaluating its arguments.

The remainder of this paper is organized as follows. After presenting the syntax and informal semantics of PCF in Section 2, we compare PCF to realistic functional languages in Section 3. Unlike nearly all practical languages, PCF lacks control operators for generating errors and performing non-local exits, which makes it impossible to observe the order in which procedures evaluate their arguments. If we extend PCF to include these facilities, then we can construct a fully abstract model using error-sensitive functions represented by decision trees. We define such a model in Section 4 and show that it is extensional. In Section 5, we prove the full abstraction theorem. In Section 6, we rigorously define the properties of SPCF that make the construction of a fully abstract model possible: errorsensitivity and observable sequentiality. Finally, in the last section we suggest how our model of SPCF can be adapted to other functional languages that are error-sensitive and observably sequential.

2 PCF

PCF is a simple functional language based on the typed λ-calculus with numerals, procedures to increment and decrement numbers, a conditional procedure, and a family of fixed point operators. The set Type of PCF types consists of a single ground type (o), denoting the set of non-negative integers, and an infinite collection of procedure types (σ → τ). Each procedure type σ → τ consists of the set of all procedure denotations that can be applied to values of type σ to produce values of type τ. The set Type is formally defined by the recursive rule:

Type ::= o | (Type → Type).

This rule is equivalent to the infinite set of rules

Type ::= o | (\underbrace{Type → … → Type}_{n} → o) for all n > 0,

which shows that procedures can be interpreted as maps from n-ary tuples to ground results. The second view also emphasizes the fact that all procedures have fixed arity.

A PCF phrase M is either a constant f ∈ F (including numerals ^{⌈}n^{⌉}, n ≥ 0), a typed variable x^{σ} ∈ V, a λ-abstraction, or an application:

M ::= F | V | (λV . M) | (M M)
F ::= add1 | sub1 | if0 | Y^{σ} | ^{⌈}n^{⌉}
V ::= x^{σ} | y^{σ} | …

that conforms to the type constraints of the typed λ-calculus. In the typed λ-calculus, every phrase M has a unique type τ. Each variable x^{σ} has type σ. Similarly, each constant finF in the language has a designated type τ_{f}. Within a well-formed phrase, the types of the phrases in each application (M N) must match: M must have a procedure type σ → τ and N must have type σ. The type of the application (M N) is τ. Each λ-abstraction (λx^{σ} . M) has type σ → τ where τ is the type of M.

The constants of PCF have the following types. Each numeral ^{⌈}n^{⌉} has type o. The procedural constants add1 and sub1 have type o → o, if0 has type o → o → o → o, and Y^{σ} has type (σ → σ) → σ.

The programs of PCF are the closed PCF phrases of ground type. A syntactic context C is a phrase with “holes” [ ] in place of some subexpressions. The phrase C[M_{1}, …, M_{n}] is the result of filling the holes of C with the corresponding expressions M_{1}, …, M_{n}, possibly capturing free variables in M_{1}, …, M_{n} in the process. We will denote the set of free variables in the phrase M by F V (M).

In PCF, numerals denote numbers, λ-abstractions denote call-by-name procedures, juxtapositions of the form (Y M) denote the least fixed points of the functions corresponding to M, other juxtapositions denote procedure applications, and the procedural constants add1, sub1, if0, and Y^{σ} have their usual meanings. The procedures add1 and sub1, respectively, increment and decrement their integer inputs; the latter diverges on 0. The procedure if0 evaluates its first argument: if the result is 0, it evaluates the second argument and returns it; otherwise it evaluates the third argument and returns it. The Y^{σ} operator computes the fixed points for procedures of type σ → σ. In PCF program text, we will use the constant Ω^{σ} to abbreviate the phrase (Y^{σ} (λx^{σ} . x^{σ})), the prototypical divergent expression of type σ.

The following equations define two different versions of the binary addition procedure in PCF:

+_{l} = Y(λf . (λxy . if0 x y (add1 (f (sub1 x) y))))
+_{r} = Y(λf . (λxy . if0 y x (add1 (f x (sub1 y)))))

The first version +_{l} recurs on the first argument x; the second version recurs on the second argument y. In the conventional continuous denotational semantics for PCF described below, these two procedures denote exactly the same function. We will use these two procedures in Section 3 when we discuss practical extensions to PCF.

2.1 Formal Semantics

To define the semantics of PCF more rigorously, we introduce the concept of a semantic definition.

Definition 2.1. (Semantic Definition) Let L be a language based on the typed λ-calculus. A semantic definition for L is a function P mapping the programs of L to meanings in a set of answers.

In the literature, languages are usually defined “operationally” by a collection of syntactic rules that reduce a program P to an answer a. A semantic definition only assigns meaning to programs; it says nothing about the meaning of program phrases that are not programs. In practice, programmers need to reason about the interaction of program components like procedures. To facilitate this process, language designers often develop a more comprehensive definition that assigns meanings to all program phrases. Such an interpretation is called a model. Of course, a model for a language must agree with the meanings assigned to programs by the semantic definition. A model that assigns the same meaning to programs as the semantic definition is said to be adequate.

Since a model assigns meanings to programs (as well as incomplete program phrases), it can also serve as a semantic definition. The advantage of this approach is simplicity: it eliminates the need to present a separate operational definition and prove that the model is adequate with respect to the operational definition. We will use the “model-based” approach to language definition in this paper.

In defining a model for a language based on the typed λ-calculus, it is convenient to transform programs to combinatory form, which eliminates bound variables and λ-abstractions at the cost of adding the constants S^{σ,τ,υ}, K^{σ,τ}, and I^{σ} and the binary function symbols apply^{σ,τ} for all types σ, τ, and υ. The new constants S, K, and I are called combinators. The combinator S^{σ,τ,υ} has type (σ → τ → υ) → (σ → τ) → σ → υ, K has type σ → τ → σ, and I has type σ → σ. The function symbol apply^{σ,τ} accepts inputs in the cross product of types (σ → τ) × σ and produces outputs of type τ.

In the transformation process, all procedure applications are made explicit because some models do not interpret procedures as functions. The syntactic forms produced by this translation are called combinatory terms. They are defined as follows.

Definition 2.2. (Combinatory Term) Let L be a language based on the typed λ-calculus with variables V and constants F. Let the sets of symbols O and A be defined by the equations:

O = {S^{σ,τ,υ} | σ, τ, υ ∈ Type} ∪ {K^{σ,τ} | σ, τ ∈ Type} ∪ {I^{σ} | τ ∈ Type}
A = {apply^{σ,τ} | σ, τ ∈ Type} .

A combinatory term in L is an expression E that conforms to the following inductive definition (expressed in BNF):

E ::= V | F | O | A(E, E)

and the type constraints of typed λ-calculus.

The transformation of PCF to combinatory form is given in Figure 1 as part of the definition of the conventional model for PCF.

We rigorously define the notion of a model and the semantic definition induced by a model as follows.

Definition 2.3. (Denotational Model^{3}) Let L be a language conforming to the syntax of the typed λ-calculus with variables V and constants F. A denotational model M for L is a function interpreting each type τ, each constant in F ∪ O, and each function symbol in the set A (of apply symbols). M maps each type τ to a Scott domain M^{τ}, each constant c of type τ to an element in M^{τ}, and each function symbol apply^{σ,τ} ∈ A to a function M[[apply^{σ,τ}]] : M^{σ→τ} × M^{σ} ⟶ M^{τ}.

3In the logic literature, the word structure is often used instead of model to identify an interpretation function M. In logic, the word model is usually reserved for structures that satisfy a particular set of axioms Γ. The same distinction between the words structure and model can be made in the context of program semantics: the operational semantics for a language can be interpreted as a collection of axioms about programs. But the word structure is a poor choice of words in the context of programming languages where structure is already overused. Consequently, the word model is commonly used in semantics to refer both to arbitrary structures and structures that satisfy a given set of axioms Γ. In this paper, no ambiguity arises because we never define an operational semantics for our programming languages PCF and SPCF.

A denotational model M for L determines a meaning for every closed program phrase in L.

Definition 2.4. (Semantics of Closed Phrases) The meaning of a closed phrase N determined by the model M (denoted M[[N]]) is the algebraic meaning that M assigns to the combinatory term [N]_{CL} corresponding to N. The algebraic meaning of a constant c is simply M[[c]]. The algebraic meaning of a composite term apply^{σ,τ} (N_{1}, N_{2}) is M[[apply^{σ,τ}]](M[[N_{1}]], M[[N_{2}]]). No variables appear in subterms of [N]_{CL} because N is closed.

If we restrict our attention to programs, then the model M determines a semantic definition for L. The meaning of closed phrases easily generalizes to open phrases in the context of an environment E mapping each free variable x^{τ} to an element of M^{τ}.

Definition 2.5. (Semantics of Open Phrases) Let N be an open phrase in L and let E be an environment mapping each variable x^{τ} in F V (N) to an element in M^{τ}. The meaning of N determined by the model M and the environment E (denoted M[[N]]_{E}) is the algebraic meaning that M assigns to the combinatory term [N]_{CL} in the environment E. The algebraic meaning of a variable x^{τ} is simply E(x^{τ}).

Figure 1 gives the conventional continuous function model C for PCF; it interprets each type σ → τ as the set of all continuous functions from C^{σ} into C^{τ}. We use this model to define the meaning of the language PCF.

Definition 2.6. (Semantic Definition of PCF ) The semantic definition of PCF is the restriction of the meaning function C to programs.

We will typically omit type superscripts from constants (as in Figure 1) where they can easily by reconstructed from context. In Figure 1 and the remainder of the paper, we rely on the following standard notation from domain theory.

Definition 2.7. (Notation for Domains) The symbol ⊑ denotes the approximation ordering on a domain; ⊥ denotes the least element. The compound symbol _{⊥} denotes the flat domain consisting of the natural numbers augmented by ⊥. For any domains A and B, A ⟶_{c} B denotes the domain of continuous functions mapping A into B. If f is a function mapping the domain D into itself, f^{i} denotes the i-fold composition of f with itself: f^{0} = ⊥_{D} and f^{i+1} = f ∘ f^{i}. In semantic definitions and proofs of theorems, the expression \underline{λ}x . · · · x ⋯ denotes the function f defined by the equation f(x) = ⋯ x · · ·.

Domains:

C^{o} = _{⊥}
C^{σ→τ} = [C^{σ} ⟶_{c} C^{τ}]

Meaning Functions:

C[[e]] = C[[[e]_{CL}]]
[^{⌈}n^{⌉}]_{CL} = ^{⌈}n^{⌉}
[f]_{CL} = f  (f ∈ F)
[x]_{CL} = x  (x ∈ V)
[(M_{1} M_{2})]_{CL} = apply([M_{1}]_{CL}, [M_{2}]_{CL})
[λx . M]_{CL} = λ^{∗}x . [M]_{CL}
λ^{∗}x . x^{σ} = I
λ^{∗}x . M = apply(K, M)  (x ∉ F V (M))
λ^{∗}x . apply(M_{1}, M_{2}) = apply(apply(S, λ^{∗}x . M_{1}), λ^{∗}x . M_{2})
C[[apply(f, a)]] = C[[f]](C[[a]])
C[[I]] = \underline{λ}x . x
C[[K]] = \underline{λ}x . \underline{λ}y . x
C[[S]] = \underline{λ}x . \underline{λ}y .\underline{λ}z . (x(z))(y(z))
C[[Y]] = \underline{λ}f . ⨆ \{f^{i}(⊥) | i ∈ \}
C[[^{⌈}n^{⌉}]] = n
C[[add1]] = \underline{λ}m . \{ \begin{matrix}m + 1 & m ∈ \\ ⊥ & m = ⊥ \end{matrix}

C[[sub1]] = \underline{λ}m . \{ \begin{matrix}m − 1 & m > 0 \\ ⊥ & m ∈ \{⊥, 0\} \end{matrix}

C[[if0]] = \underline{λ}l . \underline{λ}m . \underline{λ}n . \{ \begin{matrix}m & l = 0 \\ n & l > 0 \\ ⊥ & l = ⊥ \end{matrix}

Figure 1: The Continuous Function Model C for PCF

2.2 Observational Equivalence, Sequentiality

We are finally ready to give a rigorous definition of the key concepts of denotational equivalence, observational equivalence, and full abstraction.

Definition 2.8. (Denotational Equivalence, Observational Equivalence, Full Abstraction) Two phrases, N and N′, in the language L are denotationally equivalent in a model M, written N ≡_{M} N′ iff N and N′ have the same type and M[[N]]_{E} = M[[N′]]_{E} for all environments E mapping each variable x^{τ} in F V (N) ∪ F V (N′) into M^{τ}. They are observationally equivalent, written N ≃ N′, iff N and N′ have the same type and for all contexts C[ ] such that C[N] and C[N′] are programs, M[[C[N]]] = M[[C[N′]]]. A model M is fully abstract iff N ≃ N′ implies N ≡_{M} N′ for closed N, N′.

The same definitions adapt in the obvious way to combinatory terms in L.

Observational equivalence depends only on the meanings of programs. Hence, it is independent of the choice of model as long as models agree on the meanings of programs. Some references [18] in the literature define observational equivalence using a separate operational definition of the language L and prove that models for L are adequate. Our definition of observational equivalence, based on Milner’s original definition [16], eliminates the need for two different forms of semantics and a proof of adequacy. Both definitions yield the same notion of observational equivalence.

The conventional model C for PCF is not fully abstract because the domain of continuous functions includes parallel functions like parallel-and, yet PCF can only define sequential functions. The procedures p_{i} defined in the introduction exploit this discrepancy: they behave differently only on inputs that are not sequential. Hence they have different denotations, but they are observationally equivalent.

Given a semantic definition M for a language L, we can define what it means for L to be sequential.

Definition 2.9. (Sequentiality) A language L with semantic definition P is sequential iff the following condition holds. Let C be a context and M_{1}, …, M_{k} be closed phrases such that C[M_{1}, …, M_{k}] is a program in L, P[[C[M_{1}, …, M_{k}]]] ∈ , and P[[C[Ω, …, Ω]]] = P[[Ω]]. Then there exists j ∈ , called a sequentiality index of C[ , …, ], such that

P[[C[M′_{1}, …, M′_{j−1}, Ω, M′_{j+1}, …, M′_{k}]]] = P[[Ω]]

for all expressions M′_{i}, i ≠ j.

This definition is based on Vuillemin’s definition [26] of sequentiality for first order functions and Berry’s generalization [2] of Vuillemin’s definition to higher types. Plotkin proved that PCF is sequential [18:Activity Lemma] using an operational semantics for PCF that assigns the same meaning to PCF programs as the model C.

3 Observing Sequentiality

PCF omits several language constructs that are essential in practical languages. One of the most glaring omissions is the lack of any provision for producing and handling run-time errors. Although this design choice simplifies the definition of the language, it has thwarted efforts to construct fully abstract models for PCF and other sequential languages. In the following paragraphs, we explain why the addition of two simple control mechanisms to PCF is important from the perspective of a language designer and how their presence in a programming language affects the construction of a denotational model.

3.1 Using errors, programmers can observe the order of evaluation.

The most obvious omission from PCF is a provision for computations to produce errors. A practical implementation of PCF would signal an error when the procedure sub1 is applied to ^{⌈}0^{⌉} because ^{⌈}0^{⌉} is an invalid input for sub1. Although this behavior is inconsistent with the semantics of PCF (which requires (sub1 ^{⌈}0^{⌉}) to diverge), it is far more informative from a programmer’s point of view. More importantly, it permits programmers to observe the order of evaluation in programs by conducting simple experiments.

To provide PCF with error generators, we add two constants, error_{1} and error_{2}, of ground type to the language and force all procedures in the extended language to be error-sensitive.^{4} An operation is error-sensitive if it propagates any errors that it encounters in evaluating its arguments. In PCF with errors, a programmer can observe the evaluation order of subexpressions by exploiting the error-sensitivity of all program operations. For any pair of subexpressions, the programmer can replace each one by a distinct error value and observe the behavior of the modified program. If either subexpression is used in the evaluation of the original program, the modified program will return the error value corresponding to the subexpression that is evaluated first. As a result, the programmer can distinguish distinct versions of “commutative procedures” such as the addition procedures +_{l} and +_{r} defined in Section 2. The expression (+_{l} error_{1} error_{2}) produces an error_{1} because +_{l} evaluates its left argument first; (+_{r} error_{1} error_{2}) returns error_{2} because +_{r} evaluates its right argument first.

3.2 Using control operators, programs can observe the order of evaluation.

In PCF with errors, the sequential behavior of procedures is observable externally by the programmer but this information is not accessible internally within programs. Consequently, a program cannot determine the order of evaluation among the arguments in a procedure application. To express these computations, the program must be able to delimit the dynamic extent of control actions such as errors [22]. For this reason, many practical languages include an error handling facility or a non-local control operator.

The original version of Scheme [24], for example, contained a lexically-scoped CATCH construct for implementing non-local exits from expressions. The evaluation of the expression

(CATCH e (add1 (e 0)))

would return 0 by popping the control stack back through the lexical binding of e in (CATCH e …) after encountering the sub-expression (e 0). With such a CATCH construct, it is possible to write a program that determines the order of evaluation of a procedure’s arguments, e.g., the procedure

G = (λf . (CATCH x (f (x 0) (x 1))))

4We add two errors to PCF for pragmatic as well as technical reasons. Practical programming languages usually provide an error procedure that maps message strings to error elements containing the messages.

Hence, there are many different error elements. From a technical perspective, we need two errors to make our model order-extensional. The model with one error is extensional, but not order-extensional.

maps +_{l} to 0 and +_{r} to 1.

To add the same capabilities to PCF, we introduce a family of procedures catch^{τ} of type τ → o. If f is a procedure of type τ = τ_{1} → … τ_{n} → o, then (catch^{τ} f) returns either i−1 if f evaluates the ith argument first or k+n if t is a constant procedure with result k. Alternatively, (catch^{τ} f) is i−1 if

(f \underbrace{Ω … Ω}_{i−1} error_{j} \underbrace{Ω … Ω}_{n−i})

returns error_{j} for j = 1, 2. If τ = o, catch^{τ} is degenerate: it always returns 0.

In PCF, the family of catch procedures has the same expressive power as Scheme’s (downward) CATCH construct (see the corresponding note at the end of Section 4.4), but the catch procedures have a simpler definition that is better suited to proving the representability lemma (see Section 5).

We designate our sequential extension of PCF by the name SPCF.

Definition 3.1. (SPCF ) SPCF is PCF augmented by the set of constants

{error_{1}, error_{2}} ∪ {catch^{σ} | σ ∈ Type}

where error_{1} and error_{2} have type o and catch^{σ} has type (σ → o). Henceforth, the symbol F will refer to the set

{^{⌈}n^{⌉} | n ∈ } ∪ {add1, sub1, if0, error_{1}, error_{2}} ∪ {Y^{σ} | σ ∈ Type} ∪ {catch^{σ} | σ ∈ Type}

Since the meaning of the procedure catch^{σ} depends only on the arity of the type σ, we will frequently drop the type subscript σ in favor of its arity k. The symbol catch_{k} denotes any procedure catch^{σ} where σ has the form (τ_{1} → … τ_{k} → o).

3.3 Procedure denotations contain more computational structure than ordinary function graphs.

Conventional models for languages like SPCF are written in “continuation-passing style” to cope with the behavior of control operators. Since this form of model contains parallel functions, it is not fully abstract for sequential languages [22]. To construct a fully abstract model for SPCF, we want to develop a “direct” semantics that interprets procedures as functions.

The informal operational semantics of SPCF, notably the catch^{τ} operator, suggests that procedure denotations should have more internal structure than function graphs. In particular, they should reflect the order in which arguments are evaluated. Consider the procedure

p = λwxyz . (if0 x (y + 1) (z − 2)).

It has type o → (o → (o → (o → o))), which means we can view it as a procedure mapping quadruples of integers to integers. The procedure p evaluates its second argument x first, but the subsequent evaluation order depends on the value of x. If x is 0, p evaluates its third argument y next; otherwise it evaluates its fourth argument z. To capture this information, we can define the denotation of p as the index 2 paired with a “branching” function that maps the value of the second argument to appropriate information. The rest of the denotation can be described in the same manner: if the second argument is 0, p maps the third argument y to y + 1; otherwise, it skips that argument and decreases the value of the fourth argument by 2:

⟨2, \{ \begin{matrix}⊥↦⊥ \\ error_{1} ↦ error_{1} \\ error_{2} ↦ error_{2} \\ 0 ↦ ⟨3, \{ \begin{matrix}⊥↦⊥ \\ error_{1} ↦ error_{1} \\ error_{2} ↦ error_{2} \\ 0 ↦ 1 \\ 1 ↦ 2 \\ … \end{matrix} ⟩ \\ 1 ↦ ⟨4, \{ \begin{matrix}⊥↦⊥ \\ error_{1} ↦ error_{1} \\ error_{2} ↦ error_{2} \\ 0 ↦⊥ \\ 1 ↦⊥ \\ 2 ↦ 0 \\ 3 ↦ 1 \\ … \end{matrix} ⟩ \\ … \end{matrix} ⟩

Since p is continuous and error-sensitive, it must map ⊥ to ⊥ and error_{i} to error_{i}. If we rotate the preceding picture, it looks like a decision tree:

[figure: ⟨2,?⟩; 0; 1; 2; …; ⟨3,?⟩; 1; 0; 2; 1; 3; 2; …; ⟨4,?⟩; ⊥; 0; ⊥; 1; 0; 2; …]

In the tree representation, we have added a question mark “?” after each argument index labeling an internal node. An internal node with the value ⟨i,?⟩ represents the initial query about the ith argument. The rationale for this convention will become clear when we discuss procedures as arguments in the next paragraph. The edges below a node with value ⟨i,?⟩ are labeled with the possible values of the ith argument. The target node for each edge specifies what action the procedure performs next. If it is a leaf (an element of ∪ {⊥, error_{1}, error_{2}}), then p has completed its computation; otherwise, it continues to query its argument(s). In tree representations of procedures we omit branches that map ⊥ to ⊥ and error_{i} to error_{i} to avoid cluttering the representations with implied information.

3.4 Higher-order procedures explore trees sequentially.

If we interpret procedures as decision trees, we must explain how higher-order procedures gather information about procedural inputs. Since trees resemble Lisp S-expressions, we interpret higher-order procedures as processes that examine decision trees in essentially the same fashion as Lisp procedures traverse S-expressions. To simplify notation, we express queries about procedural inputs as patterns that identify nodes in decision trees. More specifically, a query is a rooted finite path of nodes and edges in a decision tree terminated by the marker “?”. The marker identifies the node that the procedure wants to inspect. The response produced by the query is the value of the specified node. If this match yields ⊥ or error_{i}, the result of the entire process is ⊥ or error_{i}. Like a Lisp procedure, a higher-order procedure can inspect a node in an input tree only after inspecting its predecessors.

To illustrate this process, let us examine the behavior of the procedure

F = λg . (add1 (g Ω 0 2 error_{1})) .

When (the tree representing) F is applied to an argument tree g, it knows nothing about the value of g. Since F must determine how g behaves on certain arguments, it asks the question ⟨1,?⟩ to determine the root of f . If the value of g is the procedure p described above, g answers this question with the response ⟨2,?⟩, which is the value of the root of p.

Now F knows that g initially demands information about its second argument. To find out more about g, F must provide the information that g has requested, which is 0. This information determines the subtree within g that F wants to inspect. So F asks the question ⟨1, Q_{1}⟩ where:

[figure: Q_{1} =^{df}; ⟨2,?⟩; 0; ?]

The query Q_{1} is a pattern identifying the node value in g that F wants to inspect; it lies just below the root of g on the edge labeled 0. Matching the pattern Q_{1} against p yields the node value ⟨3,?⟩, which is a query about p’s third argument.

F passes the value 2 as the third argument to g. Consequently, F ’s next question to g is ⟨1, Q_{3}⟩ where:

[figure: Q_{3} =^{df}; ⟨2,?⟩; 0; ⟨3,?⟩; ?; 2]

Matching this pattern against p yields the leaf value 3, which is a final answer from p. Since the subcomputation (g Ω 0 2 error_{1}) is now complete, F can add 1 to the result of calling g, yielding the final answer 4.

The preceding query-response protocol can be represented by a tree whose node values are queries and whose edges are labeled with the possible answers. Figure 2 shows part of the tree denoted by F , including the path that we just discussed. It also includes paths that

[figure: Q_{2} =^{df}; ⟨2,?⟩; 0; ?; Q_{3} =^{df}; ⟨2,?⟩; 0; ⟨3,?⟩; ?; 2; ⟨1,?⟩; ⟨3,?⟩; …; ⟨4,?⟩; ^{error^{1}}; ⟨1,?⟩; ⊥; ⟨2,?⟩; ⟨1, Q_{2}⟩; ⟨3,?⟩; ⟨1, Q_{3}⟩; 3; 4]

Figure 2: A Fragment of Procedure F

describe how F interacts with procedure arguments that immediately demand the value of their first or fourth argument: in the former case F returns ⊥; in the latter case, F signals error_{1}. The other branches in the tree representing F have been omitted.

When procedures are represented as trees, it is easy to see that higher-order procedures can extract apparently intensional information from procedural arguments. For example, the following tree represents a procedure that maps constant unary procedures to 1 and strict unary procedures to 0:

[figure: ⟨1,?⟩; ⟨1,?⟩; 0; …; 1; 1; 0; 1]

Similarly, the catch procedure extracts information about the evaluation order of its argument. However, this information is not intensional because distinct trees represent distinct continuous functions. The presence of error values in the ground domain combined with the convention that all procedures are error-sensitive makes the decision tree representation extensional. In Section 4.2, we prove that there is a one-to-one correspondence between the graphs of observably sequential functions and their tree representations. Decision trees simply identify mathematical structure that is implicitly present in error-sensitive functions.^{5}

5Berry and Curien [4] previously proposed representing procedures as trees in their work on concrete sequential algorithms. Since their domains do not include error elements, they associate distinct trees with the same function. For example, +_{l} and +_{r} correspond to distinct concrete sequential algorithms but they denote the same function [4:316]. In this framework, tree representations are intensional. In later work [5, 8], Berry and Curien noted that sequential algorithms can distinguish different algorithms for the same function, but they did not make a connection between intensional procedures and control operators like CATCH. Curien has recently shown that our model for SPCF is indeed closely related to the Berry-Curien model for PCF; the result will appear in a forthcoming paper [9].

4 The Tree Model

A model M of SPCF has essentially the same form as a model of PCF. M maps each type τ to a Scott domain M^{τ}, each constant f ∈ F of type τ to an element of M^{τ}, each auxiliary constant o ∈ O of type τ to an element of M^{τ}, and each function symbol apply^{σ,τ} ∈ A to a function M[[apply^{σ,τ}]] : M^{σ→τ} × M^{σ} ⟶ M^{τ}. In our tree model of SPCF, called T , each type τ is interpreted as a Scott domain of potentially infinite decision trees (where values of ground type are viewed as degenerate trees). Hence, the meaning of any closed SPCF phrase is a tree of the appropriate type. To define the meaning function T , we extend the translation and abstraction algorithms, [·]_{CL} and λ^{∗} for PCF (see Figure 1) in the obvious way. In contrast to the conventional model C for PCF, we interpret the constants in O as decision trees and the function symbols apply^{σ,τ} as the functions M[[apply^{σ,τ}]] on trees, which we will subsequently define. The functions apply^{σ,τ} decode decision trees of type σ→τ into functions mapping ^{σ} into ^{τ}.

We can state this definition of the model T more formally as follows.

Definition 4.1. (Tree model for SPCF ) T is the model for SPCF mapping:

1. each type τ to the tree domain ^{τ} as defined in Section 4.1;

2. each constant c in the set

O ∪ F = {S^{σ,τ,υ}, K^{σ,τ} , I^{τ} } ∪ {add1, sub1, if0, error_{1}, error_{2}, catch^{τ} } ∪ {^{⌈}n^{⌉} | n ∈ } ∪ {Y^{σ}}

to the tree (in the appropriate domain) defined in Section 4.3; and

3. the function symbols apply^{σ,τ} to the functions T [[apply^{σ,τ}]] defined in Section 4.3.

The remainder of this section of the paper focuses on filling in the gaps in this definition. The construction of the tree domains and the specific trees representing the combinators is quite intricate.

We will also show that the domain ^{σ→τ} of decision trees of type σ → τ is isomorphic to the domain ^{σ→τ} of error-sensitive functions mapping ^{σ} into ^{τ}. Hence, the higher order domains in the model T can be interpreted as sets of functions.

In the following subsection, we define the tree domain ^{τ} for each type τ. Next, we define the apply^{σ,τ} function for each function type σ → τ and prove that our tree representation is extensional: procedural trees are identical precisely when they cannot be distinguished by apply^{σ,τ}. In the third and fourth subsections, we assign interpretations to the primitive constants and the combinators of SPCF, and prove the basic equational properties of the tree model.

4.1 Tree Domains

A Scott domain is the ideal completion of a finitary basis [7, 20]. A finitary basis B is a countable, partially ordered set such that every finite, bounded subset has a least upper bound. The domain D_{B} determined by B is the set of ideals over B; the principal ideals of B are the finite elements of the domain determined by B (the set of ideals over B). By this construction, a domain is a bounded-complete, ω-algebraic cpo (complete partial order). In discussing domains, it is convenient to ignore the distinction between the elements of the finitary basis and corresponding principal ideals.

Our definition of the domains for procedure types relies on the notion of legal queries and responses for arguments (which must have lower types than the procedure). Each tree domain ^{τ} is the ideal completion of a finitary basis ^{τ}. In the process of defining the finitary bases ^{τ}, we will also define the set of legal queries ^{τ} of type τ (which higher-type objects can ask about elements of type τ) and the set of legal responses ^{τ} to queries of type τ.

As a technical convenience, we will adopt a different format for responses in our definition of ^{τ} than we used in the discussion in Section 3. Given the query q, an argument will return the response consisting of the path q with the “?” marker replaced by the value v of the matching node. In Section 3, an argument responded to a query q by simply returning the matching node value v instead of q with v substituted for “?”. Both formats clearly contain the same new information, namely the value v. In the sequel, we will refer to the value v as the answer to the query and the modified query as the response to the query. In pictures of specific trees, we will still label edges with answers rather than responses to save space.

Since the precise definition of ^{σ→τ} is intricate, we will start by giving a preliminary definition that is intuitively clear but includes too many elements. Then we refine that definition to produce an extensional representation of functions as trees—a representation that establishes a one-to-one correspondence between decision trees and error-sensitive functions.

The preliminary definition of ^{τ} for all types τ proceeds by induction on the structure of τ. In the following discussion, we will associate each higher order type τ_{1} → … → τ_{k} → o with the corresponding “uncurried” type τ_{1} × … × τ_{k} → o consisting of maps from appropriately typed k-tuples to ground values (natural numbers).

Base case: τ = o: Expressions of type o denote either a natural number, the diverging computation (⊥), or an error value:

o = _{⊥}^{}= ∪

where

= {⊥, error_{1}, error_{2}}.

The approximation ordering on _{⊥}^{}is the usual one, that is, ⊥ approximates all other elements, and the rest of the elements are mutually incomparable.

The only possible query about an argument of type o is the initial query “?” since the response completely determines the element. The only legal responses to this query are integers; the evaluation of an expression may produce an error element, but it cannot appear as a response in a tree. Consequently, we define the set of ground queries and ground responses as follows:

o = {?} ^{o} = .

Inductive case: τ = τ_{1} → … → τ_{k} → o: Finite higher-order objects are simply finite decision trees. Every path within such a tree is finite and all leaves are elements of _{⊥}^{}. Similarly, only finitely many branches below each non-terminal node are not ⊥. By hypothesis, we have already defined the sets ^{τ′}, ^{τ′}, and ^{τ′} for all types τ′ that are structurally nested within the expression τ. We inductively define the preliminary form of the set ^{τ} as follows. An element of type τ is either:

1. a leaf in _{⊥}^{}, or

2. a triple ⟨i, q, f⟩ consisting of an index i, 1 ≤ i ≤ k, a query q ∈ ^{τ_{i}} (a query about the ith argument), and a branching function f that maps responses in ^{τ_{i}} to simpler trees in ^{τ}. For all but a finite set of proper responses in ^{τ_{i}}, called the proper domain of f, the function f must produce the value ⊥.

In pictorial form, we represent the tree ⟨i, q, f⟩ by the diagram:

[figure: ⟨i, q⟩; f(r_{1}); f(r_{2}); f(r_{3}); f(r_{4}); r_{1}; r_{2}; r_{3}; r_{4}; …]

In this picture, we have assumed that the proper domain of f has at least four elements {r_{1}, r_{2}, r_{3}, r_{4}}. The root of the subtree is a node with value ⟨i, q⟩. For each response r_{j} in the proper domain of f , there is an outgoing edge running from the root to the finite subtree representing f(r_{j}). We sometimes refer to the value ⟨i, q⟩ at a node ⟨i, q, f⟩ as a node.

For each type τ, we give the following preliminary definitions for ^{τ} and ^{τ}. Queries and responses of type τ designate paths in trees of type τ. They have exactly the same form as finite trees with only one branch^{6} with one important exception: all queries end with the special leaf “?”. More precisely, the final branching function in a query must map the only response r in its proper domain to “?”.

Within a path, we will represent the branching function that maps the response r to path p by the pair ⟨r, p⟩. In other words, ⟨r, p⟩ denotes the function f where f(r) = p and f(s) =⊥ for s ≠ r. Similarly, ⊥ denotes the everywhere undefined branching function. A “?” at the end of each query identifies the requested node value. A response to query q replaces the the “?” marker in q with a final answer n in or an intermediate answer ⟨i, q, ⊥⟩. The notation q[?/a] denotes the response to q obtained by replacing “?” with the answer a. An argument responds to the query q by returning q[?/v] where v is the value of the node identified by q.

Figure 3 illustrates these conventions using the queries Q_{2} and Q_{3} presented in Section 3. R_{2} and R_{3} are legal responses to queries Q_{2} and Q_{3}, respectively.

6In a tree with only one branch, the proper domain of each branching function f contains at most one element.

[figure: Q_{2}  =^{df}  ⟨2,?, ⟨0,?⟩⟩; =; ⟨2,?⟩; 0; ?; R_{2}  =^{df}  ⟨2,?, ⟨0, ⟨3,?, ⊥⟩⟩⟩; =; ⟨2,?⟩; 0; ⟨3,?⟩; Q_{3}  =^{df}  ⟨2,?, ⟨0, ⟨3,?, ⟨2,?⟩⟩⟩⟩; =; ⟨2,?⟩; 0; ⟨3,?⟩; ?; 2; R_{3}  =^{df}  ⟨2,?, ⟨0, ⟨3,?, ⟨2, 3⟩⟩⟩⟩; =; ⟨2,?⟩; 0; ⟨3,?⟩; 3; 2]

Figure 3: Representation of Queries and Responses

Every response r of type τ is a finite tree in ^{τ}. Every query q of type τ becomes an element of ^{τ} if we replace “?” by ⊥. For the sake of brevity, we will abbreviate the path q[?/⊥] by the symbol \overline{q}. Similarly, in pictures of decision trees, we will usually label edges with answers instead of responses to save space.

Unfortunately, the preliminary definitions of ^{τ}, ^{τ}, and ^{τ} given above are too broad to constitute an extensional representation for error-sensitive functions. There are three sources for this imprecision. First, the definition of ^{τ} permits duplicate queries in trees, implying that many different trees represent the same function. Second, the definition of trees does not require a procedure to inspect all the predecessors of a node in an argument tree before inspecting the node itself. Finally, the definition of ^{τ} does not guarantee that the response to a query is consistent with previous responses.

We can correct the flaws in the preliminary definition of ^{τ} by maintaining an environment that accumulates the responses that appear on a path from the root of a decision tree to a given node. We refer to this environment as the tree context of the node. We will frequently use the term context instead of tree context, when it causes no confusion. The set of contexts of type τ is denoted by the symbol ^{τ}. Technically, a context is a relation associating argument indices with responses; we will use it as a set-valued function from indices to sets of responses. A context contains the information that a procedure has gathered about its arguments at a given point in a computation. More precisely, the context ρ of a node α in a procedure P maps each argument index i to the the finite approximation ⨆ ρ(i) in ^{τ_{i}} that P has determined for argument i at node α.

Given the context ρ of a node α, we can determine the set of legal queries at α for each argument i as follows: a query q on argument i must extend the approximation tree ⨆ ρ(i) for argument i by exactly one node, which is identified by a “?” in the query q. This restriction on queries guarantees that queries cannot be duplicated. It also guarantees that all the predecessors of a node in an argument tree are inspected before the node itself is inspected.

We will formalize the set of legal queries by defining a function Q that maps the set of prior responses for a particular index to the legal set of queries. For each previous legal response r, the function generates all queries that extend r by a legal response to the last query in r. Pictorially, we have:

[figure: ⟨i, q⟩; Q; ⟨i, q⟩; r′; ?]

for all legal responses r′ to the query q. If the response r ends in a final answer rather than a query q, Q generates the empty set because there are no legal queries.

The last flaw in the preliminary definition of ^{τ} that we need to correct is the definition of the set of legal responses to a query q. But this problem is easy to solve: a response q[?/d] to q is legal iff the information d, either a node of the form ⟨j, p, ⊥⟩ or an answer a, can appear at the point specified by q in the selected argument tree. This test reduces to confirming that the response q[?/d] is a well-formed tree (path). Since arguments are trees of lower type, this reduction is inductive.

We are finally ready to define the finitary bases ^{τ}. For each type τ, we will define:

• a set of tree contexts ^{τ},

• a function ^{τ} mapping a tree context ρ to partial orders of finite subtrees that can appear in context ρ,

• a function ^{τ} mapping a context ρ and a leaf set B to the set of paths over B starting in context ρ,

• a set ^{τ} of queries (in terms of ^{τ}),

• a set ^{τ} of responses (in terms of ^{τ}),

• a function Q^{τ} mapping a set of responses R ⊆ ^{τ} to the set of legal queries extending R, and

• a function R^{τ} mapping a query q ∈ Q^{τ} to the set of legal responses to q in ^{τ}.

In the process, we will define:

• a substitution function \underline{λ}q, x . q[?/x]^{τ} that replaces the ? at the end of q ∈ ^{τ} by the response r ∈ ^{τ}, and • the partial function \underline{λ}r, f . (r . f)^{τ} that replaces the empty branching function ⊥ at the

end of a response r ∈ ^{τ} by the branching function f.

Definition 4.2. ( ^{τ} including ^{τ}, ^{τ}, ^{τ}, ^{τ}, Q^{τ}, R^{τ}, ·[?/·]^{τ}, and (· . ·)^{τ}) The definition proceeds by induction on the structure of τ. Base Case: τ = o. In the base case the definitions are degenerate:

• ^{o} = ∅,

• ^{o}(ρ) = _{⊥}^{}(ρ must be ∅),

• ^{o}(ρ, B) = B (ρ must be ∅),

• ^{o} = {?},

• ^{o} = ,

• Q^{o}(R) = \{ \begin{matrix}∅ & if R = \{?\} \\ \{?\} & if R = ∅ \end{matrix} ,

• R^{o}(q) = (q must be ?),

• q[?/x]^{o} = x (x ∈ R^{o}(?)), and

• (r . f)^{o} is “undefined” for responses r ∈ ^{o} and branching functions f since no response in ^{o} ends in the empty branching function.

Induction Step: τ = τ_{1} → … τ_{k} → o where k > 0. By induction, we can assume that for all types σ (properly) nested within τ, the sets ^{σ}, ^{σ}, ^{σ}, the functions ^{σ}, ^{σ}, Q^{σ}, R^{σ}, and \underline{λ}q, x . q[?/x]^{σ}, and the partial function \underline{λ}r, f . (r . f)^{σ} have already been defined. We define these sets, functions, and operations for type τ as follows.

Contexts: The set of tree contexts ^{τ} is the least set of ordered pairs of the form {⟨i, r⟩} where 1 ≤ i ≤ k and r ∈ ^{τ_{i}} satisfying the closure properties:

1. ∅ ∈ ^{τ};

2. ρ ∪ {⟨i, r⟩} ∈ ^{τ} if ρ ∈ ^{τ} and r ∈ R^{τ_{i}}(q) for some q ∈ Q^{τ_{i}}(ρ(i)) where

ρ(i) =^{df} {s | ⟨i, s⟩ ∈ ρ} .

Subtrees: For each context ρ ∈ ^{τ}, the partial order ^{τ} (ρ) of finite subtrees is defined as follows. The universe of the ^{τ} (ρ) is the least set satisfying the following closure properties:

1. _{⊥}^{}⊆ ^{τ} (ρ);

2. ⟨i, q, f⟩ ∈ ^{τ} (ρ) if q ∈ Q^{τ_{i}}(ρ(i)) and f is a partial function mapping responses in ^{τ_{i}} to subtrees in ^{τ} (ρ ∪ {⟨i, r⟩}) such that the proper domain of f is a finite subset of R^{τ_{i}}(q).

The definition of the universe of ^{τ} (ρ) is succinctly summarized by the equation:

τ (ρ) = _{⊥}^{}∪

\{⟨i, q, f⟩ | \begin{matrix}1 ≤ i ≤ k, q ∈ Q^{τ_{i}}(ρ(i)), \{r | f(r) ≠⊥\} is finite, \\ f : r ∈ R^{τ_{i}}(q) ↦ d ∈ ^{τ} (ρ ∪ \{⟨i, r⟩\})\} \end{matrix}

The approximation relation ⊑ for ^{τ} (ρ) is the least relation satisfying the properties

• ⊥ ⊑ d for all d ∈ ^{τ} (ρ).

• ⟨i, q, f⟩ ⊑ ⟨i, q, g⟩ if f(r) ⊑ g(r) for all r ∈ R^{τ_{i}}(q).

It is easy to show that ⊑ is reflexive, antisymmetric and transitive. Hence ^{τ} (ρ) is a partial order.

Finite Paths: For every tree context ρ ∈ ^{τ} and every leaf set B, the set ^{τ} (ρ, B) of paths is the least set satisfying the equation:

τ (ρ, B) = B ∪

\{⟨i, q, ⟨r, p⟩⟩ | \begin{matrix}1 ≤ i ≤ k, q ∈ Q^{τ_{i}}(ρ(i)), r ∈ R^{τ_{i}}(q), \\ p ∈ ^{τ} (ρ ∪ \{⟨i, r⟩\}, B)\} \end{matrix}

The parameter B is the set of leaf values that can terminate paths. If ⊥ ∈ B, then the branching function ⟨r, ⊥⟩ for any response r is synonymous with the empty branching function ⊥. If B ⊆ _{⊥}^{}, then ^{τ} (ρ, B) ⊆ ^{τ} (ρ).

Queries: The set ^{τ} of queries is the set of paths that end in the distinct marker “?”:

τ = ^{τ} (∅, {?}) .

Responses: The set ^{τ} of responses is the set of non-empty paths ending in a final answer in or the empty leaf function ⊥:

τ = ^{τ} (∅, _{⊥} ) − {⊥} .

The definition of ^{τ} exploits the fact that the branching function ⟨r, ⊥⟩ is identical to the empty branching function ⊥.

Auxiliary functions: The function \underline{λ}q, x . q[?/x]^{τ} is defined on queries q ∈ ^{τ} and responses x ∈ ^{τ} as follows:

?[?/x] = x
⟨i, q, ⟨r, q′⟩⟩[?/x] = ⟨i, q, ⟨r, q′[?/x]⟩⟩

In other words, the expression q[?/x] denotes the path consisting of the query q with the terminating “?” replaced by the tree x. We use the abbreviation \overline{q} for q[?/⊥].

The partial function \underline{λ}q, x . (r . f)^{τ} is defined for responses r ∈ ^{τ} that end with the empty branching function ⊥:

⟨i, q, ⊥⟩ . f = ⟨i, q, f⟩
⟨i, q, ⟨r, r′⟩⟩ . f = ⟨i, q, ⟨r, r′ . f⟩⟩ .

Legal Queries: For any set of responses R ⊆ ^{τ}, the set Q^{τ} (R) of legal queries is the subset of ^{τ} defined the equation

Q^{τ} (R) = \{ \begin{matrix}\{?\} & if R = ∅ \\ \{q ∈ ^{τ} | ¬∃r [q r ⊑ (⨆ R)], ∃r ∈ R (q = r . ⟨r′,?⟩)\} & if R ≠ ∅ \end{matrix} .

Legal Responses: For any query q ∈ ^{τ}, the set R^{τ} (q) of legal responses is the subset of τ defined by the equation

R^{τ} (q) = {r ∈ ^{τ} | r = q[?/a] for a ∈ or r = q[?/⟨i, p, ⊥⟩]} .

The partial order ^{τ} of finite trees of type τ is defined as ^{τ} (∅).

It is easy to show that the set ^{τ} forms a finitary basis under the approximation ordering ⊑.

Lemma 4.3 ^{τ} is a finitary basis.

Proof. ^{τ} is a partial order because ⊑ is reflexive, anti-symmetric, and transitive. ^{τ} is countable because every branching function has a finite proper domain. It is straightforward but tedious to prove that every finite bounded subset of ^{τ} has a least upper bound.

As an immediate consequence of this lemma, we conclude that the ideal-completion of τ is a Scott domain (ω-algebraic bounded-complete cpo). The completion process adds infinite trees as the limits of ascending chains of finite elements in each domain ^{τ}. The result is the Scott domain designated ^{τ}. Recall that a directed set is non-empty and contains an upper bound for every pair of elements.

Theorem 4.4 Let I_{e} denote the principal ideal {d ∈ ^{τ} | d ⊑ e}. For each type τ, the set τ of ideals over ^{τ} forms a bounded-complete, ω-algebraic cpo under set inclusion ⊆:

1. Every directed subset of ^{τ} has a least upper bound in ^{τ}; every bounded subset of ^{τ} has a least upper bound.

2. The finite elements of ^{τ} are precisely the principal ideals over ^{τ}: {I_{d} | d ∈ ^{τ} }.

3. For every ideal I ∈ ^{τ}, the set {I_{d} | d ∈ ^{τ} , I_{d} ⊆ I} is directed and

I = ⨆ {I_{d} | d ∈ ^{τ} , I_{d} ⊆ I}.

Proof. The three properties are a consequence of Lemma 4.3 and a general theorem for ideal completions of finitary bases [7].

As the last topic in our discussion of the domain theory underlying our model, we will prove a lemma asserting that for every pair f and g of distinct trees in ^{τ}, there is a path p such that the subtrees in f and g identified by p have distinct roots. We will use this fact in the proof of several lemmas and theorems later in the paper.

Before we state and prove the lemma, we need to introduce some new terminology and notation. First we need to define the subtree d@p at position p ∈ ^{τ} in the tree d ∈ ^{τ}. In the process, we will also define some important relations on queries and trees.

Definition 4.5. (@ operator, valid query, query prefix) Given a query q ∈ ^{τ} and a tree d ∈ ^{τ}, d@q denotes the subtree identified by the “?” marker in q. More formally, @ is the least partial function mapping ^{τ} × ^{τ} into ⋃_{ρ∈ ^{τ}} ^{τ} (ρ) that satisfies the equations:

d@? = d
⟨i, p, f⟩@⟨i, p, ⟨r, q′⟩⟩ = f(r)@q′ .

If d@q is defined for d ∈ ^{τ} and q ∈ ^{τ}, then we say q is a valid query in d; the condition holds precisely when \overline{q} ⊑ d. If \overline{p} q for p ∈ ^{τ}, we say that p is a prefix of q. If \overline{q} ⊑ d and \overline{p} ⋢ d for all p q, then d@q = ⊥ and d@p is undefined for all p q. Note that d@q = ⊥ does not mean that d@q is undefined; ⊥ is a legitimate value in the range of the partial function @. When d@q = ⊥, we say that q probes the perimeter of d.

Next we need to define what it means for two subtrees f and g to have different roots. We say that f and g are immediately incomparable iff they have different roots.

Definition 4.6. (root operator, immediately incomparable subtrees) Given a subtree d ∈ τ (ρ) for some tree context ρ, the root root (d) of d is defined as follows:

root (a) = a  a ∈ _{⊥}
root (⟨i, q, f⟩) = ⟨i, q⟩ ⟨i, q, f⟩ ∈ ^{τ} (ρ) .

Two subtrees d, e ∈ ^{τ} (ρ) are immediately incomparable iff root (d) ≠ root (e). They are immediately comparable iff root (d) = root (e).

Immediately incomparable trees are obviously incomparable under the approximation relation ⊑. However, immediately comparable trees may not be comparable under ⊑.

Given this terminology, we can formally state the lemma asserting that distinct trees have immediately incomparable subtrees.

Lemma 4.7 For f, g ∈ ^{τ}, f ⋢ g implies that there is a query p such that f@p and g@p are both defined, f@p ⋢ g@p, and the subtrees f@p and g@p are immediately incomparable.

Proof. The proof of the lemma hinges on the following claim.

Claim 4.8 For d ∈ ^{τ}, d = ⨆ {q[?/a] | q ∈ ^{τ} , q[?/a] ⊑ d, a ∈ _{⊥}^{}}.

Proof (of Claim). We prove that the claim holds for all tree domains ^{τ} (ρ). The proof proceeds by induction on the size (structure) of d. Let d ∈ ^{τ} (ρ) for some context ρ. If d ∈ _{⊥}^{}, then there is only one q such that \overline{q} ⊑ d, namely q =?. In this case, the lemma obviously holds. If d ∉ _{⊥}^{}, then d must have the form ⟨i, p, f⟩ where i is an argument index, p is a query in ^{τ_{i}} and f is a branching function. For each response r in the proper domain of f , there is a subtree d_{r} = f(r) in ^{τ} (ρ∪{⟨i, r⟩}) for which the inductive hypothesis holds, i.e.,

d_{r} = ⨆ \{q[?/(d_{r}@q)] | q ∈ ^{τ} , \overline{q} ⊑ d_{r}, (d_{r}@q) ∈ _{⊥}^{}\} .

If we insert each of the subpaths q of d_{r} in the hole in the tree prefix ⟨i, p, [ ]⟩, we obtain the required set of paths for d:

d = ⟨i, p, {⟨r, d_{r}⟩ | r ∈ R^{τ_{i}}(p)}⟩
= ⟨i, p, \{⟨r, ⨆ \{q[?/(d_{r}@q)] | q ∈ ^{τ} , \overline{q} ⊑ d_{r}, (d_{r}@q) ∈ _{⊥}^{}\} ⟩ | r ∈ R^{τ_{i}}(p)\}⟩
= ⨆ \{⟨i, p, ⟨r, q[?/(d@q)]⟩⟩ | q ∈ ^{τ} , \overline{q} ⊑ d_{r}, (d_{r}@q) ∈ _{⊥}^{}, r ∈ R^{τ_{i}}(p)\}
= ⨆ \{q[?/(d@q)] | q ∈ ^{τ} , \overline{q} ⊑ d, (d_{r}@q) ∈ _{⊥}^{}\}
= ⨆ {q[?/a] | q ∈ ^{τ} , q[?/a] ⊑ d, a ∈ _{⊥}^{}} .

Since ^{τ} = ^{τ} (∅), the claim is proved. (Claim)

By this claim, we know there is a query q ∈ ^{τ} and a leaf a ∈ _{⊥}^{}such that q[?/a] ⊑ f but q[?/a] ⋢ g. Otherwise, f g. Let p be the longest prefix of q such that f_{p} = f@p and g_{p} = g@p are both defined. Such a prefix must exist because f@? and g@? are both defined and f@? ≠ ⊥. Clearly, f_{p} ⋢ g_{p}, since q[?/a] ⋢ g. Assume that f_{p} and g_{p} are immediately comparable. If f_{p}, g_{p} ∈ _{⊥}^{}, then f_{p} = g_{p} and p = q, contradicting the fact that f_{p} ⋢ g_{p}. If f_{p} = ⟨i, q, f′⟩ and g_{p} = ⟨i, q, g′⟩, then f′ ⋢ g′ since f_{p} ⋢ g_{p}. Let p′ be the query p[?/⟨i, q, ⟨r,?⟩⟩] where r is chosen so that p′ a prefix of q. The query p′ is a longer prefix of q than p, yet p′ is valid in both f and g, which contradicts the definition of p. Hence, f_{p} and g_{p} must be immediately incomparable.

4.2 Application

A critical component of any model of a language L based on the simply typed λ-calculus is the interpretation of the function symbols apply^{σ,τ}. In the tree model T , the function T [[apply^{σ,τ}]] : ^{σ→τ} × ^{σ} ⟶ ^{τ} decodes decision trees into functions. For the sake of brevity we will drop the type superscript in subsequent references to apply^{σ,τ}. Similarly, we write apply instead of T [[apply]] where the usage is clear from context.

For inputs f in ^{σ→τ} and x in ^{σ}, apply(f, x) is defined by case analysis on f :

1. If f is a constant, apply ignores the value of x and returns the value f.

2. If f has the form ⟨1, q, g⟩, apply matches q against the argument x. If x returns a proper response r, apply selects the appropriate branch in the branching function, g(r), and continues the process of constructing the output tree. If x returns an improper answer in = {⊥, error_{1}, error_{2}}, apply returns that answer.

3. If f has the form ⟨i + 1, q, g⟩ for i ≥ 1, apply must produce the tree representing the function f(x); it has the form ⟨i, q, \underline{λ}r . apply(g(r), x)⟩. But g(r) is a subtree rather than a tree, indicating that we must generalize apply to subtrees.

To define apply formally, we must generalize the informal definition given above to subtrees. In addition, since the domain and co-domain of apply include limit points (infinite trees), we will define apply as the continuous extension of an auxiliary function apply′.

Definition 4.9. (apply) The function apply : ^{σ→τ} × ^{σ} ⟶ ^{τ} is constructed from the auxiliary partial function apply′ as follows. For any tree context ρ of arity k, let ρ′(i) = ρ(i + 1), 1 ≤ i < k. The auxiliary partial function apply′ maps ^{σ→τ} (ρ) × ^{σ} into ^{τ} (ρ′). For all f ∈ ^{σ→τ} and d ∈ ^{σ},

apply(f, d) = ⨆ {apply′(f′, d′) | f′ ⊑ f, f′ ∈ ^{σ→τ} (∅), d′ ⊑ d, d′ ∈ ^{σ→τ} } .

The function apply′ : ^{σ→τ} (ρ) × ^{σ} ⟶ ^{τ} (ρ′) is defined by the following recursion equations:

apply′(f, d) = f  if f ∈ _{⊥}^{}
apply′(⟨1, q, g⟩, d) = \{ \begin{matrix}d@q & if d@q ∈ \\ apply′(g(q[?/d@q]), d) & if d@q ∈ \\ apply′(g(q[?/⟨j, p⟩]), d) & if d@q = ⟨j, p, d′_{1}⟩ \end{matrix}
apply′(⟨i + 1, q, g⟩, d) = ⟨i, q, \underline{λ}r_{i} . apply′(g(r_{i}), d)⟩

It is easy to show that apply′ produces a well-defined output in ^{τ} (ρ′) for f ∈ ^{σ→τ} (ρ) and d ∈ ^{σ} such that ⨆ ρ(1) ⊑ d. The behavior of apply′ on finite trees d ∈ ^{σ} where ⨆ ρ(1) ⋢ d is irrelevant because apply depends only on apply′ where ρ = ∅. Assume σ = τ_{1} and τ = τ_{2} → … → τ_{k} → o. The proof that apply′ is well-defined for d such that ⨆ ρ(1) ⊑ d proceeds by induction on the size of the finite element f. The induction hypothesis consists of two parts:

1. For all f ∈ ^{τ_{1}→ ... →τ_{k}→o}(ρ) and d ∈ ^{τ_{1}} such that ⨆ ρ(1) ⊑ d,

apply′(f, d) ∈ ^{τ_{2}→ ... →τ_{k}→o}(ρ′)

where ρ′(i) = ρ(i + 1) for 1 ≤ i < k.

2. If f = ⟨1, q, g⟩, then \overline{q} ⊑ d, implying that d@q is always well-defined in the definition of apply′ when ⨆ ρ(1) ⊑ d.

In addition, it is straightforward to check that for all f ∈ ^{σ→τ} and d ∈ ^{σ}, the set {apply′(f′, d′) | f′ ⊑ f, f′ ∈ ^{σ→τ} , d′ ⊑ d, d′ ∈ ^{σ→τ} } is directed, implying that it has a least upper bound. Hence, apply is a well-defined, continuous function from pairs of trees to trees. To simplify notation, we will identify the functions apply and apply′ in the rest of the paper. Note that apply′ is defined for finite subtrees as well as finite trees.

A model for a language based on the typed λ-calculus is extensional when procedure denotations are identical if and only if they behave identically under application. The model is order-extensional if this property also holds for approximations between procedure denotations.

Definition 4.10. (Extensionality, Order-extensionality) Let L be a language conforming to the syntax of the typed λ-calculus with constants. A model M for L is extensional iff for all f, g ∈ M^{σ→τ}, apply(f, d) = apply(g, d) for all d ∈ M^{σ} implies f = g. It is orderextensional iff for all f, g ∈ M^{σ→τ}, apply(f, d) ⊑ apply(g, d) for all d ∈ M^{σ} implies f ⊑ g.

Although the interpretations in our model T for the constants and combinators of SPCF are still unspecified we can prove that the model is extensional and order-extensional,^{7} because these properties depend only on the definition of the domains ^{τ} and the functions apply^{σ,τ}.

Theorem 4.11 T is extensional and order-extensional.

Proof. Since extensionality is obviously implied by order-extensionality, we will only prove the second claim. Assume f ⋢ g for f, g ∈ ^{σ→τ}. We will show that there exists d ∈ ^{σ} such that

apply(f, d) ⋢ apply(g, d).

Since the domain ^{σ→τ} is algebraic,

f = ⨆ {f′ | f′ ⊑ f, f′ ∈ ^{σ→τ} } and g = ⨆ {g′ | g′ ⊑ g, g′ ∈ ^{σ→τ} } .

Consequently there exists a finite f′ ⊑ f such that f′ ⋢ g. Moreover, for all finite g′ ⊑ g, f′ ⋢ g′. By Lemma 4.16 below, there exists a finite d ∈ ^{τ} such that

apply(f′, d) ⋢ apply(g′, d)

for all g′ ⊑ g. From the definition of apply, we know that apply(f′, d) is finite and continuous. Hence,

apply(f′, d) ⋢ ⨆ {apply(g′, d) | g′ ⊑ g′} = apply(g, d) .

By monotonicity,

apply(f′, d) ⊑ apply(f, d) ,

implying

apply(f, d) ⋢ apply(g, d) .

which is precisely what we needed to prove.

To complete the proof of the theorem, we need to state and prove a lemma asserting that extensionality holds for finite decision trees. The proof relies on the following observation. If f and g are distinct finite trees, then there must be a path from the root to a node position where the trees have different node values, e.g., one tree probes its ith argument, while the other is a constant function. If we apply f and g to an argument d corresponding to this path, we can show that f and g produce inconsistent results on the input d.

To simplify the proof of Lemma 4.14 and the proof of the full abstraction theorem in the next section, we introduce some new terminology and prove the extensionality lemma with the help of an auxiliary lemma. First, we define the tree context determined by a path.

7P.L. Curien (ENS) [personal communication, August 1991] pointed out that the order-extensionality theorem does not hold if the model only contains one error value. For example, the functions error and ⟨1,?, \underline{λ}x . error⟩ are incomparable, yet for all d, apply(⟨1,?, \underline{λ}x . error⟩, d) ⊑ apply(error, d). On the other hand, while a model based on a single error value is not order-extensional, it is still extensional. It is also fully abstract.

Definition 4.12. (Tree context determined by a query) Let τ = τ_{1} → … τ_{k} → o. A query q ∈ ^{τ} determines the tree context q̂ = R(q, ∅) where R : ^{τ} × ^{τ} ⟶ ^{τ} is the least function satisfying the equations:

R(?, ρ) = ρ
R(⟨i, p, ⟨r, q′⟩⟩, ρ) = R(q′, ρ ∪ {⟨i, r⟩})

Second, we define a function shift_{1} that maps paths of arity k to the corresponding paths of arity k − 1. The function shift_{1} simply eliminates queries about the first argument and converts queries about argument queries about argument i + 1 into queries about argument i.

Definition 4.13. (shift_{1}) The function shift_{1} from queries of type

τ_{1} → … → τ_{k} → o

to queries of type

τ_{2} → … → τ_{k} → o

is defined as follows:

shift_{1}(⟨1, p, ⟨r, q⟩⟩) = shift_{1}(q)
shift_{1}(⟨i + 1, p, ⟨r, q⟩⟩) = ⟨i, p, ⟨r, shift_{1}(q)⟩⟩
shift_{1}(?) = ?

The function also has a natural extension to paths that end in final answers:

shift_{1}(a) = a a ∈ .

Based on the two preceding definitions, it is now possible to state the lemma that relates applications of elements and paths to the context information determined by the path.

Lemma 4.14 Let d ∈ ^{τ}, let q ∈ ^{τ} be a query that determines the context q̂, and let e be a subtree in ^{τ} (q̂). If d@q = e and d_{1} ⊒ ⨆ q̂(1), then

apply(d, d_{1})@shift_{1}(q) = apply(e, d_{1}) .

Proof. The proof proceeds by induction on the query q. In the base case, q =?, implying d = e shift_{1}(q) =?, so the lemma obviously holds. In the induction step, q has the form ⟨i, p, ⟨r, q′⟩⟩ implying that d = ⟨i, p, f⟩ where f(r)@q′ = e and d_{1} ⊒ ⨆ q̂′(1). If i = 1, then shift_{1}(q) = shift_{1}(q′). In addition, d_{1} ⊒ ⨆ q̂(1) implies that r ⊑ d_{1}. As a result, we can transform apply(d, d_{1})@shift_{1}(q) as follows:

apply(d, d_{1})@shift_{1}(q) = apply(⟨i, p, f⟩, d_{1})@shift_{1}(q)
= apply(f(r), d_{1})@shift_{1}(q′)

(by definition of apply and shift_{1})

= apply(e, d_{1})  (by induction) ,

proving the lemma holds when i = 1. If i > 1, then shift_{1}(q) = ⟨i − 1, p, ⟨r, shift_{1}(q′)⟩⟩. As a result, we can transform apply(d, d_{1})@shift_{1}(q) as follows:

apply(d, d_{1})@shift_{1}(q) = apply(⟨i, p, f⟩, d_{1})@shift_{1}(q)
= ⟨i − 1, p, \underline{λ}s . apply(f(s), d_{1})⟩@⟨i − 1, p, ⟨r, shift_{1}(q′)⟩⟩

(by definition of apply and shift_{1})

= apply(f(r), d_{1})@shift_{1}(q′)  (by definition of @)
= apply(e, d_{1})  (by induction) ,

completing the proof of the lemma.

The lemma implies a simple corollary about the application of paths to all possible arguments.

Corollary 4.15 Let τ = τ_{1} → … τ_{k} → o. Let q ∈ ^{τ} be a query that determines the context q̂, and let e be a subtree in ^{τ} (q̂). If d ⊒ q[?/e] and d_{i} ⊒ ⨆ q̂(i) for i, 1 ≤ i ≤ k,

apply(d, d_{1}, …, d_{k}) = apply(q[?/e], d_{1}, …, d_{k}) = apply(e, d_{1}, …, d_{k}).

We are finally ready to prove that the model T is order-extensional and hence extensional.

Lemma 4.16 Let f, g be elements in ^{σ→τ}. If for all finite d ∈ ^{σ}, apply(f, d) ⊑ apply(g, d) then f ⊑ g.

Proof. Let f, g ∈ ^{σ→τ} such that f ⋢ g. We will prove apply(f, d) ⋢ apply(g, d) as follows. By Lemma 4.7, there must be a query (path) q′ such that f′ = f@q′ and g′ = g@q′ are defined, f′ ≠ ⊥, and f′ and g′ are immediately incomparable. Let d_{1} be ⨆ q̂′(1). By the Lemma 4.14, we know that for all d ⊒ d_{1}

apply(f, d)@shift_{1}(q′) = apply(f′, d)

and

apply(g, d)@shift_{1}(q′) = apply(g′, d) .

If we can construct d ⊒ d_{1} such that

apply(f′, d) ⋢ apply(g′, d) ,

the lemma immediately follows because @ is monotonic.

We will construct the tree d by performing a case analysis on the form of f′ and g′:

1. f′, g′ ∈ _{⊥}^{}: The two functions are constant functions returning different constants.

Let d = d_{1}. Then

apply(f′, d) = f′ ⋢ g′ = apply(g′, d)

by assumption.

2. f′ ∈ _{⊥}^{}, g′ = ⟨i, p, g′′⟩: One function is a constant function and the other inspects the ith argument. If i > 1, we let d = d_{1}, and we trivially have

apply(f′, d) = f′ ⋢ ⟨i − 1, p, \underline{λ}x . apply(g′′(x), d)⟩ = apply(g′, d).

Otherwise i = 1, and we distinguish two possible cases:

(a) f′ ≠ error_{1}: Let d = p[?/error_{1}] ⊔ d_{1}, which exists since p ∈ Q(q̂′(1)) and, in particular, d_{1}@p = ⊥. It immediately follows that d@p = error_{1} and, since by assumptionf′ ≠⊥,

apply(f′, d) = f′ ⋢ error_{1} = apply(g′, d).

(b) f′ = error_{1}: Let d = p[?/error_{2}] ⊔ d_{1}. The rest follows as in the previous subcase.

3. f′ = ⟨i, p, f′′⟩, g′ ∈ _{⊥}^{}: This case is symmetric to the preceding one.

4. f′ = ⟨i, p, f′′⟩, g′ = ⟨j, q, g′′⟩, i ≠ j: Both functions inspect one of their arguments but different ones, and thus f′ cannot approximate g′. Now we must distinguish three subcases, depending on which arguments the functions inspect:

(a) i = 1: Let d = p[?/error_{1}] ⊔ d_{1}, which is well-defined by the same argument as in the preceding case. Then, since d@p = error_{1},

apply(f′, d) = error_{1} ⋢ ⟨j − 1, q, \underline{λ}x . apply(g′′(x), d)⟩ = apply(g′, d).

(b) j = 1: Let d = q[?/error_{1}] ⊔ d_{1}. The rest is analogous to the preceding sub-case.

(c) i, j > 1: Let d = d_{1}. The two results differ because the applications yield functions that again inspect different arguments:

apply(f′, d) = ⟨i − 1, p, \underline{λ}x . apply(f′′(x), d)⟩
⋢ ⟨j − 1, q, \underline{λ}x . apply(g′′(x), d)⟩
= apply(g′, d)

5. f′ = ⟨i, p, f′′⟩, g′ = ⟨i, q, g′′⟩, p ≠ q: The two functions inspect the same argument with different queries. We distinguish two cases:

(a) i = 1: Since q, p ∈ Q(q̂′(1)), i.e. d_{1}@q = ⊥, d_{1}@p = ⊥, and q ≠ p, the domain elements q[?/error_{1}] and p[?/error_{2}] are consistent with each other and are consistent with d_{1}. Hence, let d = q[?/error_{1}] ⊔ p[?/error_{2}] ⊔ d_{1}. Clearly, d@q = error_{1}, d@p = error_{2}, and therefore,

apply(f′, d) = error_{1} ⋢ error_{2} = apply(g′, d)

(b) i > 1: Let d = d_{1}:

apply(f′, d) = ⟨i − 1, p, \underline{λ}x . apply(f′′(x), d)⟩
⋢
apply(g′, d) = ⟨i − 1, q, \underline{λ}x . apply(g′′(x), d)⟩

The proof is complete since the preceding analysis covers all the possible ways to pick immediately incomparable f′ and g′ where f′ ⋢ g′.

The extensionality theorem implies that trees behave like mathematical functions under application. Indeed, based on apply, we can define a domain of functions from ^{σ} to ^{τ} that we can use instead of the tree domain.

Definition 4.17. ( ^{σ→τ}) For each f in ^{σ→τ}, let fun(f) denote the function \underline{λ}x : σ . apply(f, x). The domain ^{σ→τ} is the set {fun(f) | f ∈ ^{σ→τ} } under the pointwise ordering on functions: f ⊑ g iff f(x) ⊑ g(x) for all x in ^{σ}.

It is straightforward to show that the function domain ^{σ→τ} is isomorphic to the tree domain ^{σ→τ}.

Corollary 4.18 ^{σ→τ} is isomorphic to ^{σ→τ}.

Proof. Let f′ = fun(f), g′ = fun(g). If f ⊑ g then apply(f, x) ⊑ apply(g, x) for all x, and therefore (\underline{λ}x . apply(f, x))(x) ⊑ (\underline{λ}x . apply(g, x))(x), which is what we claimed.

Conversely, let f ∈ ^{σ→τ} be some pre-image of f′ ∈ ^{σ→τ}, and let g ∈ ^{σ→τ} be some pre-image of g′ ∈ ^{σ→τ}. If f′ ⊑ g′ then (\underline{λ}x . apply(f, x))(x) ⊑ (\underline{λ}x . apply(g, x))(x) since f and g are pre-images. Hence, f ⊑ g by extensionality.

Clearly, fun is onto and it is also easy to check that it is one-to-one. Let f ∈ ^{σ→τ} and g ∈ ^{σ→τ} be two pre-images of f′ ∈ ^{σ→τ}. It immediately follows that f ⊑ g and g ⊑ f, which implies f = g.

[figure: ⟨1,?⟩; add1; 0; 1; 1; 2; 2; 3; 3; 4; …; ⟨1,?⟩; sub1; 0; ⊥; 1; 0; 2; 1; 3; 2; …; ⟨1,?⟩; catch_{k}; 0; k; 1; k + 1; 2; …; k + 2; ⟨1,?⟩; 0; ⟨2,?⟩; 1; …; ⟨1,?⟩; if0_{o}; 0; ⟨2,?⟩; k ∈; k; 1; ⟨3,?⟩; k ∈; k; 2; ⟨3,?⟩; k ∈; k; 3; ⟨3,?⟩; k ∈; k; …]

Figure 4: Meanings of Primitive Constants

4.3 Assigning Meaning to Phrases

To assign meaning to phrases in SPCF, we translate programs into a combinatory language in which λ-abstractions are replaced by applications of the combinators S^{σ,τ,υ}, K^{σ,τ}, and I^{σ}:

M ::= x^{σ} | ^{⌈}n^{⌉} | add1 | sub1 | if0 | Y^{σ} | catch^{σ} | error_{1} | error_{2} |
S^{σ,τ,υ} | K^{σ,τ} | I^{σ} | apply^{σ,τ} (M, M)

The translation is based on the conventional bracket elimination algorithm (see Figure 1). For convenience, we will use multi-ary abstractions and applications as abbreviations for sequences of unary applications:

apply(f, x_{1}, …, x_{n}) =^{df} apply(… (apply(f, x_{1}), …), x_{n})
λ^{∗}x_{1}, …, x_{n} . M =^{df} λ^{∗}x_{1} . (… (λ^{∗}x_{n} . M)) .

For any combinatory term M, we will let M[x/N] denote the result of substituting all occurrences of x by the term N .

The bracket elimination algorithm converts every program phrase to a combinatory term in SPCF. These terms are composed solely from variables, constants, and the binary function symbols apply^{σ,τ}. Hence, we can assign meaning to any program by defining the meaning of the constants {^{⌈}n^{⌉}}∪{add1, sub1, if0, catch^{σ}, error_{1}, error_{2}, S^{σ,τ,υ}, K^{σ,τ} , I^{σ}, Y^{σ}} and the binary function symbols apply^{σ,τ}.

In the sequel, we will say that an expression M denotes the tree d in the model M if M[M] = d. In equations, we use expressions from SPCF on both sides. Thus, M denotes the final answer a is equivalent to the equation M = ^{⌈}a^{⌉}.

With the exception of fixed point operator Y^{σ}, the primitive constants of SPCF are easy to define in T .

Definition 4.19. (add1, sub1, if0, catch) In the model T , the constants add1, sub1, if0, catch denote the following trees:

T [[add1]] = ⟨1,?, {(n, n + 1) | n ∈ } ⟩
T [[sub1]] = ⟨1,?, {(n + 1, n) | n ∈ } ∪ {(0, ⊥)} ⟩
T [[if0_{o}]] = ⟨1,?, \{(0, ⟨2,?, (\underline{λ}j : . j) ⟩)\} ∪ \{(n + 1, ⟨3,?, (\underline{λ}j : . j) ⟩) | n ∈ \} ⟩
T [[catch_{k}]] = ⟨1,?, {(j, j + k) | j ∈ } ∪ {(⟨j,?⟩, j − 1) | 1 ≤ j ≤ k} ⟩

Figure 4 contains pictorial descriptions of the primitive constants other than Y^{σ}. Since the definition of T [[Y^{σ}]] relies on the meanings of the combinators O in T , we will defer defining T [[Y^{σ}]] until the end of this subsection.

The construction of the trees representing the combinators S^{σ,τ,υ}, K^{σ,τ}, and I^{σ} is tedious. We begin with the combinator K. Recall that K must satisfy the following equation:

apply(K, x_{1}, x_{2}) = x_{1}

for all x_{1} and x_{2} in the appropriate domains. Therefore, apply(K, x_{1}) must be a tree that ignores its first argument and returns the tree x_{1}. In other words, the tree apply(K, x_{1}) does not contain any node values of the form ⟨1, q⟩; it is identical to x_{1} except that it contains node values of the form ⟨i + 1, q⟩ in place of node values of the form ⟨i, q⟩. When the tree apply(K, x_{1}) is applied to another tree d, apply traverses apply(K, x_{1}) and decrements every index at every node; d is ignored.

To “copy” the first input with incremented indices, K must completely explore its first argument x_{1}. It begins this process by probing the root of x_{1}. If x_{1} returns a constant answer, K returns this answer as its own final answer. If x_{1} responds with a query q about its ith argument, K queries its (i + 2)nd argument x_{i+2}, ignoring its second argument x_{2}. K probes argument position i + 2 because it must skip over two arguments, x_{1} and x_{2} to reach the first argument for x_{1}. The answer of x_{i+2} to K’s query is the information that x_{1} requested. Thus, after obtaining a response from x_{i+2}, K probes x_{1} again with a new query that extends x_{1}’s response with the additional information provided by x_{i+2}. The subsequent response by x_{1} is subjected to the same case analysis as the first one. Pictorially, K has the following structure at every layer of the tree:

[figure: ⟨1, q⟩; a; a; ⟨i, p⟩; ⟨i + 2, p⟩; r′; ⟨1, q . ⟨i, p, ⟨r′,?⟩⟩⟩]

The preceding discussion demonstrates that the tree representing K encodes a recursive search process. This process is formalized in the following definition.

Definition 4.20. (K) In the model T , the combinator K^{σ,τ} denotes the tree K(?) where K is a recursive function mapping queries in ^{σ} to subtrees in ^{σ→τ} (q̂) defined by the equation:

K(q) = ⟨1, q, \underline{λ}r . \{ \begin{matrix}a & r = q[?/a], a ∈ \\ ⟨i + 2, p, \underline{λ}r′ . K(r . ⟨r′,?⟩)⟩ & r = q[?/⟨i, p⟩] \end{matrix} ⟩

where ^{σ→τ} (q̂) denotes the domain determined by the finitary basis ^{σ→τ} (q̂). The solution of this recursion equation is the least-upper bound of finitely deep approximations to K (which map ^{σ} to ^{σ→τ} (q̂)):

K(q) = ⨆ {K_{n}(q) | n ∈ }

where

K_{0}(q) = ⊥

K_{n+1}(q) = ⟨1, q, \underline{λ}r . \{ \begin{matrix}a & r = q[?/a], a ∈ \\ ⟨i + 2, p, \underline{λ}r′.K_{n}(r . ⟨r′,?⟩)⟩ & r = q[?/⟨i, p⟩] \end{matrix} ⟩

It is easy to check that

K = ⨆ {K_{n}(?) | n ∈ } .

The definition of the I combinator is similar to the definition of K; the details are omitted. The S combinator is most complex primitive operation in T . It is the least solution to

the equation

apply(S, x_{1}, x_{2}, x_{3}) =^{df} apply(apply(apply(S, x_{1}), x_{2}), x_{3})
= apply(apply(x_{1}, x_{3}), apply(x_{2}, x_{3}))
= apply(x_{1}, x_{3}, apply(x_{2}, x_{3})) .

Like K, S probes its first argument with progressively deeper queries q until it gets a final answer. Intermediate responses from x_{1} are queries about its arguments in the application

apply(x_{1}, x_{3}, apply(x_{2}, x_{3}))

namely x_{3}, apply(x_{2}, x_{3}), x_{4}, x_{5}, …. To define S, we must distinguish the following responses r by x_{1} to the query q:

1. r = q[?/a]: If x_{1} returns a final answer, S returns the same final answer.

2. r = q[?/⟨i + 2, p⟩]: If x_{1}’s response is a query p about its (i + 2)nd argument, S must probe position p in x_{i+3}.

3. r = q[?/⟨1, p⟩]: If x_{1} asks for a node value from its first argument x_{3}, S must provide the requested information. But S may not have to query x_{3} to get this node value because S also gathers information about x_{3} when x_{1} asks for a node value from its second argument apply(x_{2}, x_{3}). Thus, S may have already extracted the information in handling previous responses from x_{1} of the form q[?/⟨2, p⟩]. Since S must not generate the same query twice, we must maintain a finite tree d_{3} recording the information extracted from x_{3} at each stage in the construction of S. We will use this “table” to avoid inserting redundant queries in S. At position q′ in S, d_{3} is simply q̂′(3). If S has already extracted the information requested by x_{1} (i.e. \overline{p} d_{3}), then S probes x_{1} again with the query q extended by d_{3}@p. Otherwise, S must probe x_{3} for the node value at position p before it probes x_{1} again.

4. r = q[?/⟨2, p⟩]: If x_{1} probes its second argument, S must simulate the application of x_{2} to x_{3}. The simulation must incorporate the information in the table d_{3} to avoid generating redundant queries of x_{3}. Since S must perform this simulation incrementally, we will also maintain a finite tree d_{2} that records the approximation that S has accumulated for x_{2} at each position q′ in S. The finite tree d_{2} has an unusual form. Every node of the form ⟨1, p, f⟩ has exactly one son below it, i.e., the proper domain of f contains exactly one element, because apply only explores x_{3}’s response to this query. The other sons in x_{2} below this node correspond to other values of x_{3}! To compute the node value at position p in the tree apply(x_{2}, x_{3}), S must simulate the construction of the specified node. By examining d_{2}, S can determine which node in x_{2} should be applied to x_{3}, resuming the simulation of apply(x_{2}, x_{3}) at the appropriate point. We will encapsulate the analysis of d_{2} in an auxiliary function encode that maps d_{2} and p to the appropriate query about x_{2}, which must be a member of the set Q({d_{2}}). We will defer further discussion of encode until we complete our analysis of the construction of S. When S probes x_{2} with the query encode(d_{2}, p), x_{2} can produce three different kinds of responses r′:

(a) r′ = q[?/a]: If x_{2} returns a final answer, S may resume the process of probing x_{1} with the knowledge that apply(x_{2}, x_{3})@p = a.

(b) r′ = q[?/⟨1, p′⟩]: If x_{2} returns a query p′ about its first argument, S must redirect this query to x_{3} if the information is not already available in the table d_{3}. If \overline{p′} d_{3}, then S already knows the node value of x_{3} at position p′ and continues probing x_{2} to simulate the application of x_{2} to x_{3}. On the other hand, if \overline{p′} d̸_{3}, S must probe x_{3} with query p′ to obtain the information requested by x_{2} before it continues probing x_{2}. If S probes x_{3}, it must update the table d_{3}.

(c) r′ = q[?/⟨i + 1, p′⟩]: If x_{2} returns a query p′ about an argument with index greater than 1, this query appears in shifted form as a node value in apply(x_{2}, x_{3}). Similary, all of the nodes above this node in apply(x_{2}, x_{3}) are shifted copies of the node values in r′; each node of the form ⟨j + 1, q′⟩ in x_{2} corresponds to a node of the form ⟨j, q′⟩ in apply(x_{2}, x_{3}). S must resume probing x_{1} using a shifted form of the query r′. The function shift_{1} defined in the preceding section (Definition 4.13) performs precisely this shifting transformation.

To complete our informal discussion of how to construct the tree representing S, we need to describe how the function encode works. Given inputs d_{2} (the current approximation to x_{2}) and p (the query by x_{1}), the encoding function encode traverses d_{2} and p to discover which node in x_{2} must be examined next to determine the node value at the root of the subtree apply(x_{2}, x_{3})@p. Much of the information in d_{2} and p is redundant because either (i) d_{2} = ⊥ and p =? or (ii) p = shift_{1}(d_{2}) . ⟨r,?⟩ for some response r. To identify this node position in x_{2}, encode must translate p to the corresponding path p′ in x_{2}. For every value ⟨i, q⟩ in p, there is a corresponding node ⟨i + 1, q⟩ in p′. The path p′, however, may contain more nodes than p because node values in p′ of the form ⟨1, q⟩ in x_{2} are eliminated in the formation of the tree apply(x_{2}, x_{3}). Consequently, encode must insert these node values in p′ using the information stored in d_{2}.

We can formalize the preceding description of S by defining a tree generating function S that calls an auxiliary tree generating function T and an encoding function encode. The function S generates the portions of the tree that encode the query process that S performs on x_{1}. The inputs to S are finite elements approximating x_{2} and x_{3} and a query q about x_{1}. The T function generates the parts of the tree that encode the query process on x_{2}. It uses finite elements that approximate x_{2} and x_{3}, the last response by x_{1}, and a query about x_{2}. The encode function translates queries by x_{1} about its second argument apply(x_{2}, x_{3}) into corresponding queries about x_{2}. It takes a finite element approximating x_{2} and a query about apply(x_{2}, x_{3}) as inputs.

Definition 4.21. (S) In the model T , the combinator S^{σ,τ,υ} denotes the tree S(?,?) where

S : ^{(σ→τ→υ)→(σ→τ)→σ→υ} × ^{σ→τ→υ} ⟶ ⋃_{ρ} ^{(σ→τ→υ)→(σ→τ)→σ→υ}(ρ)

is defined by the recursion equations in Figure 5. The figure also gives definitions for the auxiliary functions

T : ^{(σ→τ→υ)→(σ→τ)→σ→υ} × ^{(σ→τ)} ⟶ ⋃_{ρ} ^{(σ→τ→υ)→(σ→τ)→σ→υ}(ρ)

and encode : ^{σ→τ} × ^{τ} ⟶ ^{σ→τ}.

S(p_{S}, q_{1}) =

let {d_{2} = p̂_{S}(2); d_{3} = p̂_{S}(3)} in

⟨1, q_{1}, \underline{λ}r_{1}∈R(q_{1}) . \{ \begin{matrix}a & r_{1} = q_{1}[?/a] \\ S(p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], & r_{1} = q_{1}[?/⟨1, p⟩], \\ r_{1} . ⟨p[?/root (d_{3}@p)],?⟩) & d_{3}@p ≠ ⊥ \\ ⟨3, p, \underline{λ}s∈R(p) . & r_{1} = q_{1}[?/⟨1, p⟩], \\ S(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨3, p, ⟨s,?⟩⟩⟩⟩], & d_{3}@p = ⊥ \\ r_{1} . ⟨s,?⟩)⟩ \\ T (p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], encode(d_{2}, p)) & r_{1} = q_{1}[?/⟨2, p⟩] \\ ⟨i + 3, p, \underline{λ}s∈R(p) . & r_{1} = q_{1}[?/⟨i + 2, p⟩] \\ S(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨i + 3, p, ⟨s,?⟩⟩⟩⟩], \\ r_{1} . ⟨s,?⟩)⟩ \end{matrix} ⟩

T (p_{S}, q_{2}) =

let^{∗} {r_{1} = p̂_{S}(1); d_{2} = p̂_{S}(2); d_{3} = p̂_{S}(3); q_{1}[?/⟨2, p⟩] = r_{1}} in

⟨2, q_{2}, \underline{λ}r_{2}∈R(q_{2}) . \{ \begin{matrix}S(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], r_{1} . ⟨shift_{1}(r_{2}),?⟩) & r_{2} = q_{2}[?/a] \\ T (p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], & r_{2} = q_{2}[?/⟨1, p⟩], \\ r_{2} . ⟨p[?/root (d_{3}@p)],?⟩) & d_{3}@p ≠ ⊥ \\ ⟨3, p, \underline{λ}s∈R(p) . & r_{2} = q_{2}[?/⟨1, p⟩], \\ T (p_{S}[?/⟨2, q_{2}, ⟨r_{2}, ⟨3, p, ⟨s,?⟩⟩⟩⟩], & d_{3}@p = ⊥ \\ r_{2} . ⟨s,?⟩)⟩ \\ S(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], r_{1} . ⟨shift_{1}(r_{2}),?⟩) & r_{2} = q_{2}[?/⟨i + 1, p⟩] \end{matrix} ⟩

encode(⊥,?) = ?
encode(⟨1, q, ⟨r, d′_{2}⟩⟩, p) = ⟨1, q, encode(d′_{2}, p)⟩
encode(⟨i + 1, q, f⟩, ⟨i, q, ⟨r, p′⟩⟩) = ⟨i + 1, q, encode(f(r), p′)⟩
encode(⟨i + 1, q⟩, ⟨i, q, ⟨r,?⟩⟩) = ⟨i + 1, q, ⟨r,?⟩⟩

Figure 5: Definition of the functions S, T, and encode

A solution to the recursion equations in Figure 5 can be obtained by defining an infinite series of finitely deep approximations as in the definition of K above. The pattern matching notation in the definition of the encode function relies on two facts:

1. The approximation d_{2} has exactly one son below each node value of the form ⟨1, p⟩.

2. Every invocation of the definition encode(d_{2}, p) satisfies the invariant: there exists a query q such that d_{2}@q = ⊥ and p = shift_{1}(q).

When the preceding two conditions hold, it is easy to prove that encode(d_{2}, p) = q by induction on q. Appendix A contains a proof that the decision-tree T [[S]] is well-defined.

With the definitions of T [[K]] and T [[S]] in hand, we are finally ready to define the meaning of the constant Y^{σ} in T . The meaning T [[Y^{σ}]] must satisfy the equation

T [[apply(M, apply(Y^{σ}, M))]] = T [[apply(Y^{σ}, M)]]

for all closed combinatory terms M of type σ → σ. Since the tree domain ^{σ→σ} is isomorphic to the function domain ^{σ→σ} and the functions in ^{σ→σ} are continuous, we can exploit the usual limiting construction to define T [[Y^{σ}]]. For the duration of this construction, let Ω^{τ} for τ ∈ Type abbreviate the expression given by the following inductive definition:

Ω^{o} = apply(sub1, 0)
Ω^{τ→υ} = λ^{∗}x^{τ} . Ω^{υ} .

The expression Ω^{τ} has the same meaning (⊥_{τ}) in T as the definition for Ω^{τ} given at the beginning of Section 2, but the new definition does not contain any occurrences of constants Y^{τ}. Given the definition of Ω^{τ}, we define

T [[Y^{σ}]] = ⨆ \{T [[λ^{∗}f . \underbrace{apply(f, …, apply(f, Ω^{σ}) …)}_{n}]] | n ∈ \} .

It is straightforward to prove that T [[Y^{σ}]] is well-defined. First, the combinatory term

λ^{∗}f . \underbrace{apply(f, …, apply(f, Ω^{σ}) …)}_{n}

does not contain any constants Y^{τ}, so

T [[λ^{∗}f . \underbrace{apply(f, …, apply(x, Ω^{σ}) …)}_{n}]]

is well-defined for all n ≥ 0. Second, it is easy to prove that the set

\{T [[λ^{∗}f . \underbrace{apply(f, …, apply(f, Ω^{σ→σ}) …)}_{n}]] | n ∈ \}

forms a chain by induction on n (since T [[apply]] is monotonic). Hence, the specified least upper bound exists. We will prove that T [[Y^{σ}]] is the tree encoding the least fixed point operator of type (σ → σ) → σ in the next subsection.

4.4 Operational Properties of the Model

To provide some operational insight about the model and its combinators, we derive some equational laws that the model T satisfies. The most important properties are the equations asserting that the combinators S, K, and I satisfy their definitions.

Theorem 4.22 Let x, y, z be variables ranging over arbitrary elements in appropriate domains. Then:

apply(S, x, y, z) = apply(apply(x, z), apply(y, z))  (S)
apply(K, x, y) = x  (K)
apply(I, x) = x  (I)

Proof. The proofs for S and K are given in Appendix A. The proof for I closely follows the proof for K.

The preceding theorem implies that the β axiom holds for combinatory terms translated from λ-abstractions [1]. In addition, the extensionality theorem (Theorem 4.11) and the validity of β axiom imply that the η axiom also holds.

Corollary 4.23 (β, η) Let M and N be combinatory terms.

(i) If E is an environment that binds each variable x^{τ} in F V (M) ∪ F V (N) to an element in ^{τ}, then

T [[apply(λ^{∗}y . M, N)]]_{E} = T [[M[y/N]]]_{E} .  (β)

(ii) If E is an environment that binds each variable x^{τ} in F V (M) to an element in ^{τ}, then:

T [[λ^{∗}y . apply(M, y)]]_{E′} = T [[M]]_{E′}  (if y ∉ F V (M))  (η)

Proof. Both equations can be proved using standard methods [1]; the proof of (η) depends on the extensionality theorem (Theorem 4.11).

We can use the β axiom to prove that T [[Y]] is the tree encoding the least fixed point operator.

Corollary 4.24 (Y operator) For all closed combinatory terms M of type σ → σ,

T [[apply(M, apply(Y^{σ}, M))]] = T [[apply(Y^{σ}, M)]] .

Proof. Let the expression Ω^{τ} be defined as in Section 4.4 above. Since the function apply is continuous for any tree g ∈ ^{σ→σ},

T [[apply(M, apply(Y^{σ}, M))]]

= apply(T [[M]], apply(T [[Y^{σ}]], T [[M]]))

= apply(T [[M]], apply(⨆ \{T [[λ^{∗}f . \underbrace{apply(f, …, apply(f, Ω^{σ}) …)}_{n}]] | n ∈ \}, T [[M]]))

= ⨆ \{apply(T [[M]], T [[apply(λ^{∗}f . \underbrace{apply(f, …, apply(f, Ω^{σ}) …)}_{n}, M)]]) | n ∈ \}

= ⨆ \{T [[apply(M, apply(\underbrace{apply(M, …, apply(M, Ω^{σ}) …)}_{n}, M))]] | n ∈ \}

= ⨆ \{T [[apply(M, apply(\underbrace{apply(M, …, apply(M, Ω^{σ}) …)}_{n}, M))]] | n ∈ \}

= ⨆ \{T [[apply(λ^{∗}f . apply(f, apply(\underbrace{apply(f, …, apply(f, Ω^{σ}) …)}_{n}, f)), M)]] | n ∈ \}

= ⨆ \{apply(T [[λ^{∗}f . apply(f, apply(\underbrace{apply(f, …, apply(f, Ω^{σ}) …)}_{n}, f))]], M) | n ∈ \}

= apply(⨆ \{T [[λ^{∗}f . apply(f, apply(\underbrace{apply(f, …, apply(f, Ω^{σ}) …)}_{n}, f))]] | n ∈ \}, T [[M]])

= apply(T [[Y^{σ}]], T [[M]])

= T [[apply(Y^{σ}, M)]] .

To determine the relevant equations for the catch operators and error values, we draw on our operational intuition about the behavior of control operators [11, 12]. The key idea is to define a “program counter” for program text corresponding to the obvious reduction semantics for SPCF. This counter determines which term in a program must be evaluated next in order to determine the program’s answer. In SPCF, the order of evaluation is precisely determined because the primitive operations of SPCF are error-sensitive. We formalize the concept of a textual program counter by defining the notion of evaluation context.

Definition 4.25. (Evaluation context) An evaluation context for SPCF is a syntactic context E that conforms to the following inductive definition (expressed in BNF):

E ::= [ ] | apply(F, E) | apply(E, M) | apply(catch, (λ^{∗}x_{1}, …, x_{n} . E))
F ::= add1 | sub1 | if0 | catch

An evaluation context is a syntactic context where the hole is in “leftmost-outermost” position. A hole is in “leftmost-outermost” position iff every operator to the left of the the path from the root to the hole is a primitive function; catch operators are classified as primitive functions. If we place a variable x corresponding to a surrounding top-level abstraction in the hole of an evaluation context, the resulting term denotes a function that is strict in the argument x.

Lemma 4.26 For all variables x_{1}, …, x_{n}, for all evaluation contexts E, and for all j, 1 ≤ j ≤ n,

T [[λ^{∗}x_{1}, …, x_{n} . E[x_{j}]]] = ⟨j,?, f⟩

for some appropriate branching function f ,

Proof. See Appendix B.

If we place an error value or ⊥ in the hole of an an evaluation context, the entire term denotes the value placed in the hole. In addition, catch can determine which variable occurs in the hole of an evaluation context in its procedure argument.

Theorem 4.27 For all evaluation contexts E, types τ = τ_{1} → … → τ_{n}, and variables x_{1}, …, x_{n},

T [[E[error_{j}]]] = error_{j}  (error)
T [[E[⊥]]] = ⊥  (bottom)
T [[apply(catch^{τ} , λ^{∗}x_{1}, …, x_{n} . E[x_{j}])]] = ^{⌈}j − 1^{⌉} for 1 ≤ j ≤ n  (catch)
T [[apply(catch^{τ} , λ^{∗}x_{1}, …, x_{n} .^{⌈}k^{⌉})]] = ^{⌈}k + n^{⌉}  (return)

Proof. By the preceding lemma,

T [[λ^{∗}x_{1}, …, x_{n} . E[x_{j}]]] = ⟨j,?, f⟩

for an appropriate branching function f . Thus, for example,

T [[E[error_{1}]]] = T [[apply(λ^{∗}x . E[x], error_{1})]] by β
= apply(⟨1,?, f⟩, error_{1})
= error_{1}

The other equations follow from similarly simple calculations.

The natural equations for the primitive operations {add1, sub1, if0, Y, error_{1}, error_{2}}, the β and η rules, and the equations for catch completely determine an operational reduction semantics for SPCF [11, 12]. The equations also suffice to prove the representability lemma of the following section.

Note: call/cc_{d} vs CATCH. As indicated in Section 2, Scheme’s original CATCH construct permits the specification of a return value to the “catch label”. Since such a control construct is common in many Lisp, Scheme, and ML dialects, the question arises how this construct relates to the less pragmatic, somewhat artificial, catch construct in SPCF. To study this relationship, we introduce the procedure call/cc_{d} of type ((o → o) → o) → o (“call with current (downward) continuation”). This new procedure is similar to Scheme’s call/cc procedure. It applies its argument to the current continuation, but unlike full-fledged call/cc-type continuations, call/cc_{d}-continuations can be used at most once. While call/cc_{d} is a new functional constant, it is easy to see that the binding form of (downward) CATCH and call/cc_{d} have the same expressive power:

(CATCH e M) = (call/cc_{d} (λe . M))
(call/cc_{d} f) = (CATCH e (f e)) .

[figure: Q^{∗} =^{df}; ⟨1,?⟩; ⟨1,?⟩; ?; R^{∗}(n) =^{df}; ⟨1,?⟩; n; ?; ⟨1,?⟩; 0; 0; 1; 1; …; ⟨1,?⟩; ⟨1, Q^{∗}⟩; R^{∗}(n); n; 0; 0; 1; …; 1]

Figure 6: The denotation of call/cc_{d}

The denotation of call/cc_{d} is the tree shown in Figure 6. From an operational perspective, call/cc_{d} is defined by the equations [11,12]:

call/cc_{d}(λf^{o→o} . E[f ^{⌈}n^{⌉}]) = ^{⌈}n^{⌉}
call/cc_{d}(λf^{o→o} .^{⌈}n^{⌉}) = ^{⌈}n^{⌉}

where the set of evaluation contexts is adapted mutatis mutandis.

With call/cc_{d}, it is easy to define catch_{k} for each arity k ≥ 0:^{8}

catch_{0} = λx . x
catch_{k} = λf . call/cc_{d}(λg . (add1^{k} (f (g^{⌈}0^{⌉}) … (g ^{⌈}k − 1^{⌉})))).

The converse is more difficult. An application of the form (call/cc_{d} f) can evaluate the tree representing f to arbitrary depth. To simulate (call/cc_{d} f), we must write a procedure test_{v} with free variable v that applies f to a continuation c that determines whether f evaluates c (the continuation) and, if so, whether f passes the value v to c as its parameter. Moreover, the procedure must reveal this information in the root node of its tree representation so that catch can extract it. The following code repeatedly applies catch to the procedure test_{v} for increasing values 0, 1, … of v until v equals the value a that is “thrown” out of the body of f:^{9}

call/cc_{d} = λf . letrec L = λv .
let test_{v} = λxy . (f(λa . if0 (− a v) x y)))
let x = M in N =^{df} ((λx . N)M)

8The notation (add1^{k} x) denotes a k-fold application of add1 to x; similarly, (sub1^{k} x) denotes a k-fold application of sub1 to x.

9We are using the abbreviations:

letrec L = M in (L ^{⌈}0^{⌉}) =^{df} (Y(λL . M)^{⌈}0^{⌉})

in let root = (catch test_{v})
in (if0 root a (if0 (sub1 root) (L (add1 v)) (sub1^{2} root)))

in (L ^{⌈}0^{⌉})

This code also detects when f is some constant c and returns the same value as f, in this case (sub1^{2} root).

In summary, call/cc_{d} and catch are equally expressive in SPCF. We selected catch as the primitive operation for SPCF for purely technical reasons. Indeed, it is much simpler to program with call/cc_{d}. End of Note.

5 The Full Abstraction Theorem

Plotkin [18] showed that an extensional model of PCF with parallel operations is fully abstract if the language can define all finite elements in the model. Exactly the same argument applies to SPCF. Since we already know that the tree model T is order-extensional, we can prove that T is fully abstract by showing that all finite trees are definable in SPCF. In this section, we use this strategy to prove that T is a fully abstract model of SPCF.

Theorem 5.1 (Full Abstraction of T and SPCF) For all SPCF phrases M and N, M ≡_{T} N iff M ≃ N.

Proof. The proof follows exactly the same outline as Plotkin’s proof that continuous function model is fully abstract for PCF with parallel operations [18:240]. We only need to show that for all phrases M and N that M ≃ N implies M ≡_{T} N. The other direction is an immediate consequence of the compositionality of the meaning function T . Let M and N be any phrase such that M ≢_{T} N. We will prove that M ≄ N. Let E be an environment binding all the variables in F V (M) ∪ F V (N) to elements of appropriate type such that

T [[M]]_{E} ≠ T [[M]]_{E} .

If M and N have type o, the proof is trivial: the empty context [ ] establishes that M ≄ N in the environment E. So we can assume that M and N belong to some higher type

τ = σ_{1} → … → σ_{k} → o .

Since T [[M]]_{E} ≠ T [[N]]_{E}, the domains ^{σ_{i}} are algebraic, apply is continuous, and SPCF is extensional, it is easy to prove by contradiction that there exist finite trees d_{1} ⊑ t_{1}, …, d_{k} ⊑ t_{k} such that

apply(T [[M]]_{E}, d_{1}, …, d_{k}) ≠ apply(T [[N]]_{E}, d_{1}, …, d_{k}) .

If we construct closed expressions E_{1}, …, E_{k} in SPCF that represent the elements d_{1}, …, d_{k} (i.e. T [[E_{i}]] = d_{i}, 1 ≤ i ≤ k), then we can use the context

C[ ] = ([ ] E_{1} … E_{k})

to show that M ≄ N. In particular,

T [[C[M]]]_{E} = T [[(M E_{1} … E_{k})]]_{E} = apply(T [[M]]_{E}, e_{1}, …, e_{k})

while

T [[C[N]]]_{E} = T [[(N E_{1} … E_{k})]]_{E} = apply(T [[N]]_{E}, e_{1}, …, e_{k}) .

Thus, the proof that SPCF is fully abstract reduces to the proof of the following lemma.

Lemma 5.2 For every finite element d ∈ ^{τ}, there is a closed SPCF expression M such that T [[M]] = d.

Proof. The proof of the lemma proceeds by induction on the depth of the type

τ = τ_{1} → … → τ_{k} → o, k ≥ 0.

The depth of ground type o is 1, the depth of τ is 1 + max{depth(τ_{i}) | 1 ≤ i ≤ k}. Since the induction step decomposes the tree d into a root node, a set of proper responses, and an attached set of subtrees, we need to prove a stronger result than the lemma because subtrees of d are not necessarily trees in ^{τ}. Specifically, we must prove that for all contexts ρ ∈ ^{τ}, every finite subtree e in ^{τ} (ρ) is “representable” in SPCF. For technical reasons, we will use an equational characterization of subtree representability.

Definition 5.3. (Subtree representability) Let ρ be a context in ^{τ}. A subtree e ∈ ^{τ} (ρ) is representable iff there exists a closed expression M such that

apply(T [[M]], d_{1}, …, d_{k}) = apply(e, d_{1}, …, d_{k})

for all arguments d_{1}, …, d_{k} in ^{τ_{1}}, …, ^{τ_{k}}, such that d_{i} ⊒ ⨆ ρ(i).

When ρ = ∅, e is a complete tree and subtree representability reduces to tree representability by extensionality.

We are now ready to prove that every subtree e in D^{τ} (ρ) is representable by a term M. Without loss of generality, we assume that M has the form

λ^{∗}x_{1}, …, x_{k} . B

where B is an expression with free variables x_{1}, …, x_{k}; for k = 0, this specializes to M = B. The construction of B proceeds by induction on the depth of subtrees. Thus, the remainder of the proof is a nested induction argument, where the induction hypothesis holds for all subtrees e′ of lower type and all smaller subtrees e′ of type τ—regardless of the context of e′ in its parent tree.

Since ^{τ} (ρ) is the union of two disjoint sets, _{⊥}^{}and {⟨i, q, f⟩ | …}, we must consider two cases: (i) e ∈ _{⊥}^{}and (ii) e = ⟨i, q, f⟩ ∈ ^{τ} (ρ). In the first case, it is easy to verify that for any leaf e ∈ , the expression M = λ^{∗}x_{1}, …, x_{k} .^{⌈}e^{⌉} represents e. Similarly, if e = error_{j}, then M = λ^{∗}x_{1}, …, x_{k} . error_{j} represents e. If e = ⊥, then M = λ^{∗}x_{1}, …, x_{k} . Ω^{τ} represents e. (Recall that Ω^{τ} abbreviates Y^{τ} (λ^{∗}x^{τ} . x^{τ}).)

In the second case, e is a finite subtree ⟨i, q, f⟩ compatible with the context ρ:

[figure: root of d; f_{1}; …; f_{m}; f_{m+1}; …; f_{m+n}; ρ; root of e; ⟨i, q⟩; r_{1}; r_{m}; r_{m+1}; r_{m+n}]

Let the proper domain of the branching function f be the union of the sets {r_{1}, …, r_{m}} and {r_{m+1}, …, r_{m+n}} where the responses is the first set have the form:

r_{1} = q[?/⟨i_{1}, p_{1}⟩]
…
r_{m} = q[?/⟨i_{m}, p_{m}⟩]

and the responses in second set have the form:

r_{m+1} = q[?/a_{1}]
…
r_{m+n} = q[?/a_{n}]

where a_{1}, …, a_{n} ∈ . We refer to the elements of the first set as query responses and to the elements of the second set as final responses. Each edge r_{j} points to a subtree f_{j} ≠ ⊥. By the induction hypothesis, each subtree f_{j} is representable by an expression F_{j} in SPCF.

We want to construct M so that

apply(T [[M]], d_{1}, …, d_{k}) = apply(e, d_{1}, …, d_{k})

for all argument trees d_{1}, …, d_{k} in ^{τ_{1}}, …, ^{τ_{k}}, respectively, such that d_{i} ⊒ ⨆ ρ(i). Since the root of e has the form ⟨i, q, f⟩, the code in the body of M must extract the node value at position q in d_{i} to determine which subexpression F_{i} to evaluate. We know that the argument d_{i} (bound to x_{i} in the body of M) has type τ_{i} of the form σ_{1} → … σ_{l} → o where (l ≥ 0). Let q̂ denote the tree context determined by the query q (as defined in Definition 4.12). Naïvely, we might try to construct a body B that tries to compute the node value at position q in d_{i} by applying x_{i} to a list of argument expressions A_{1}, …, A_{l} representing the trees ⨆ q̂(1), … ⨆ q̂(l), respectively. In other words, M has the form

M = λ^{∗}x_{1}, …, x_{k} . E[(x_{i} A_{1} … A_{l})] ,

for some evaluation context E[ ] (see Definition 4.25). We know that we can construct each expression A_{j} by the induction hypothesis, because the type σ_{j} is smaller than type τ. If the subtree d_{i}@q is a leaf a ∈ , then the application

(x_{i} A_{1} … A_{l})

indeed returns the value a, which the evaluation context E[] can use to select the appropriate subexpression F_{j} to evaluate. In this case, the naïve strategy works.

On the other hand, if the root of the subtree d_{i}@q is a query asking more information about the jth argument to d_{i}, the naïve strategy fails because the argument expression A_{j} does not contain the specified information. The expressions A_{1}, …, A_{l} only encode the information embedded in q. To clarify this problem, let us consider an example. Assume that ρ = ∅, e = ⟨1,?, ⟨⟨1,?⟩, 17⟩⟩, d_{1} = ⟨1,?, ⊥⟩, and d_{j} = ⊥ for j ≥ 2. Then

apply(e, d_{1}, …, d_{k}) = 17 ,

but the naïve strategy yields

M = λ^{∗}x_{1}, …, x_{k} . E[(x_{1} Ω … Ω)] ,

implying that

apply(T [[M]], d_{1}, …, d_{k}) = ⊥ .

To solve this problem, we need to embed code in the arguments A_{1}, …, A_{l} to perform non-local exits from the application (x_{i} A_{1} … A_{l}) back to the body B whenever d_{i} (the tree bound to x_{i}) asks for information about its arguments beyond what is specified in q. In SPCF, we can simulate a non-local exit by applying the catch operator to a λ-abstraction M′ constructed from e. In particular, we can define a λ-abstraction

M′ = λ^{∗}y_{1}, …, y_{m} . (x_{i} B_{1} … B_{l})

that

• requests its j th argument when d_{i} dominates the query response r_{j}, and

• immediately returns the answer a_{j} when d_{i} dominates the answer response r_{j}.

In the first case, (catch M′) returns the integer j − 1, indicating that the code block M should execute the code block F_{j}. In the second case, (catch M′) returns the integer m + a_{j} indicating that M should execute the code block F_{m+j}.

We formalize these observations as follows. Let [x_{i} := d_{i}] be the environment that binds x_{i} to d_{i}. The expression M′ must satisfy two conditions:

Condition (i) If d_{i} ⊒ q[?/a_{j}], then T [[M′]]_{[x_{i}:=d_{i}]} = a_{j}.

Condition (ii) If d_{i} ⊒ q[?/⟨h_{j}, p_{j}⟩], then T [[M′]]_{[x_{i}:=d_{i}]} = ⟨j,?, g⟩ for some branching function g.

The key to constructing M′ is defining the expressions B_{h}. Each expression B_{h} must evaluate the variable y_{j} if the node value at position q in d_{i} matches the response r_{j}. In addition, each expression B_{h} must satisfy the constraint q̂(h) ⊑ T [[B_{h}]]_{E} for all environments E binding the variables y_{1}, …, y_{m} to values in _{⊥}^{}. The precise form of the expressions B_{1}, …, B_{l} depends on the query q. For the moment, let us assume that we can construct the argument expressions B_{1}, …, B_{l}.

Given the expression M′, M is easy to construct. The application (catch M′) identifies the proper response r_{j} (if any) below the root of e corresponding to the node value at position q in d_{i}. More precisely, conditions (i) and (ii) on M′ above imply that

T [[(catch M′)]]_{[x_{i}:=d_{i}]} = \{ \begin{matrix}a_{j} + m ∈ & if d_{i} ⊒ q[?/a_{j}] \\ j − 1 ∈ & if d_{i} ⊒ q[?/⟨i_{j}, p_{j}⟩] . \end{matrix}

where [x_{i} := d_{i}] is the environment binding x_{i} to d_{i}. Given the index j corresponding to the response r_{j} from d_{i}, M can invoke the code F_{j} representing the subtree f_{j} by performing a sequential case split. Without loss of generality, we assume that the final answers are sorted: a_{1} < a_{2} < … < a_{n}. Then,

M = λ^{∗}x_{1}^{τ_{1}} … x_{k}^{τ_{k}} . let w = (catch (λ^{∗}y_{1}, …, y_{m} . (x_{i} B_{1} … B_{l}))) in (if0 w F_{1}x_{1} … x_{k} … (if0 (sub1_{⊥}^{m−1} w) F_{m}x_{1} … x_{k} (if0 (sub1_{⊥}^{a_{1}+m} w) F_{m+1}x_{1} … x_{k} … (if0 (sub1_{⊥}^{a_{n}+m} w) F_{m+n}x_{1} … x_{k} Ω) …)) …)

where

sub1_{⊥} = λx . (if0 x ⊥ (sub1x)) ,

the expression (sub1_{⊥}^{b} N) abbreviates the b-fold application of sub1_{⊥} to the argument expression N, the expression (let w = P in Q) abbreviates ((λ^{∗}w . Q) P). The procedure sub1_{⊥} is identical to sub1 except that it diverges on the input 0.

The proof that M represents e is a straightforward consequence of the properties of the expression (catch M′) described above. There are two cases:

1. If d_{i} ⊒ q[?/a_{j}], then T [[(catch M′)]]_{[x_{i}:=d_{i}]} = a_{j} + m, implying that M ≡_{T} F_{m+j} by the simplification process described in Figure 7.

2. If d_{i} ⊒ q[?/⟨i_{j}, p_{j}⟩], then T [[(catch M′)]]_{[x_{i}:=d_{i}]} = j − 1, implying that M ≡_{T} F_{j} by a simplification process similar to the one given in Figure 7.

To complete the proof of the lemma, we must

• construct the argument expressions B_{1}, …, B_{l}, and

• prove that the expression M′, constructed from B_{1}, …, B_{l}, satisfies conditions (i) and (ii) identified above.

Let h be an index in the range 1, …, l. The construction of B_{h} falls into one of two cases. In the first case, no query response r_{j} asks for more information about the hth argument. In this case, we simply define B_{h} as the closed expression representing the tree ⨆ q̂(i), which exists by the induction hypothesis because the type σ_{i} of B_{h} is smaller than τ.

M ≡_{T} λ^{∗}x_{1}^{τ_{1}} … x_{k}^{τ_{k}} .
(if0 ^{⌈}a_{j} + m^{⌉} (F_{1} x_{1} … x_{k})
…
(if0 (sub1_{⊥}^{m−1} ^{⌈}a_{j} + m^{⌉}) (F_{m} x_{1} … x_{k})
(if0 (sub1_{⊥}^{a_{1}+m} ^{⌈}a_{j} + m^{⌉}) (F_{m+1} x_{1} … x_{k})
…
(if0 (sub1_{⊥}^{a_{n}+m} ^{⌈}a_{j} + m^{⌉}) (F_{m+n} x_{1} … x_{k})
Ω) …)) …)
≡_{T} λ^{∗}x_{1}^{τ_{1}} … x_{k}^{τ_{k}} .
(if0 false (F_{1} x_{1} … x_{k})
…
(if0 false (F_{m} x_{1} … x_{k})
(if0 false (F_{m+1} x_{1} … x_{k})
…
(if0 true (F_{m+j} x_{1} … x_{k})
…
(if0 false (F_{m+n} x_{1} … x_{k})
Ω) …)) …)
≡_{T} λ^{∗}x_{1}^{τ_{1}} … x_{k}^{τ_{k}} .
(F_{m+j} x_{1} … x_{k})
≡_{T} F_{m+j} .

Figure 7: Simplification of (catch M′) when d_{i} ⊒ q[?/a_{j}]

In the other case, a finite number s of query responses r_{j} ask for more information about the hth argument. We can assume without loss of generality that these query responses are r_{1} = q[?/⟨i_{1}, p_{1}⟩], …, r_{s} = q[?/⟨i_{s}, p_{s}⟩]. Since x_{i} has type τ_{i} = σ_{1} → … → σ_{l} → o, we know that the type of B_{h} has the form

σ_{h} = υ_{1} → … υ_{t} → o

for some integer t ≥ 0. We also know that the queries p_{1}, …, p_{s} extend the information in ⨆ q̂(h). Consequently, we can form a tree

e_{h} = ⨆ q̂(h) ⊔ p_{1}[?/⟨t + 1,?, ⊥⟩] ⊔ … ⊔ p_{s}[?/⟨t + s,?, ⊥⟩]

with type

σ′_{h} = υ_{1} → … υ_{t} → \underbrace{o → … → o}_{s−times} → o

that grafts subtrees onto the tree q̂(h). We can interpret ⨆ q̂(h) as a tree of type σ′_{h}, so we can directly compare the behavior of the trees e_{h} and ⨆ q̂(h) under application. If we apply the tree e_{h} to an argument list c_{1}, …, c_{t+s}, it performs exactly the same computation as ⨆ q̂(h) except when the information in c_{1}, …, c_{t+s} dominates p̂_{j} for some j, 1 ≤ j ≤ s. In this case,

apply(e_{h}, c_{1}, …, c_{t+s}) = apply(⟨t + j,?, ⊥⟩, c_{1}, …, c_{t+s}) = \{ \begin{matrix}⊥ & if c_{t+j} ∈ _{⊥} \\ c_{t+j} & if c_{t+j} ∈ \{error_{1}, error_{2}\} \end{matrix}

while

apply(⨆ q̂(h), c_{1}, …, c_{t+s}) = ⊥ .

When c_{t+j} ∈ {error_{1}, error_{2}}, the trees e_{h} and ⨆ q̂(h) produce different answers.

By the induction hypothesis, we can represent e_{h} by a closed expression E_{h} because its type is smaller than τ. Thus, we define the expression B_{h} as follows:

B_{h} = λ^{∗}z_{1}, …, z_{t} . (E_{h} z_{1} … z_{t} y_{i_{1}} … y_{i_{s}}) .

The body of B_{h} evaluates parameter y_{i_{j}} of M′ precisely when the node value at position q in d_{i} matches query response r_{j} below the root of e.

The meaning of B_{h} in an environment E depends on the values in _{⊥}^{}that E assigns to the free variables y_{i_{1}}, …, y_{i_{s}}. We claim that T [[B_{h}]]_{E} is the element

b_{h} = ⨆ q̂(h) ⊔ ⨆ {p_{j}[?/⊥] | E(y_{i_{j}}) ∈ _{⊥} } ⊔ ⨆ {p_{j}[?/E(y_{i_{j}})] | E(y_{i_{j}}) ∈ {error_{1}, error_{2}}}
⊒ ⨆ q̂(h) .

To verify this claim, let c_{1}, …, c_{t} be elements of ^{υ_{h}}, …, ^{υ_{t}}, respectively. It is easy to check that

apply(b_{h}, c_{1}, …, c_{t}) = apply(e_{h}, c_{1}, …, c_{t}, E(y_{i_{1}}), …, E(y_{i_{s}}))
= apply(T [[E_{h}]], c_{1}, …, c_{t}, E(y_{i_{1}}), …, E(y_{i_{s}}))
= apply(T [[B_{h}]]_{E}, c_{1}, …, c_{t}) .

By extensionality, T [[B_{h}]]_{E} = b_{h}.

Now we must show that the term M′ satisfies conditions (i) and (ii). Let E be any environment that binds x_{i} to the tree d_{i} and binds y_{1}, …, y_{m} to elements in _{⊥}^{}:

Condition (i): If d_{i} ⊒ q[?/a_{j}], then

T [[(x_{i} B_{1} … B_{l})]]_{E} ⊒ apply(q[?/a_{j}], b_{1}, …, b_{l}) .

Since b_{h} ⊒ ⨆ q̂(h) for all h, Corollary 4.15 implies that

apply(q[?/a_{j}], b_{1}, …, b_{l}) = apply(a_{j}, b_{1}, …, b_{l}) = a_{j}.

Since _{⊥}^{}is flat,

T [[(x_{i} B_{1} … B_{l})]]_{E} = a_{j} .

But the values of y_{1}, …, y_{m} in E were chosen arbitrarily. Hence, we can conclude that

T [[M′]]_{[x_{i}:=d_{i}]} = a_{j} .

Condition (ii): If d_{i} ⊒ q[?/⟨i_{j}, p_{j}⟩], then

T [[(x_{i} B_{1} … B_{l})]]_{E} ⊒ apply(q[?/⟨i_{j}, p_{j}⟩], b_{1}, …, b_{l}) .

As in the first subcase, we conclude that

apply(q[?/⟨i_{j}, p_{j}⟩], b_{1}, …, b_{l}) = apply(⟨i_{j}, p_{j}⟩, b_{1}, …, b_{l}) .

By construction, b_{i_{j}}@p_{j} ∈ , but the specific value depends on E(y_{j}). Hence,

apply(⟨i_{j}, p_{j}⟩, b_{1}, …, b_{l}) = \{ \begin{matrix}⊥ & E(y_{j}) ∈ _{⊥} \\ y_{j} & E(y_{j}) ∈ \end{matrix}

But notice that ⟨j,?, ⊥⟩ applied to E(y_{1}), …, E(y_{m}) has the same behavior as ⟨i_{j}, p_{j}⟩ applied to b_{1}, …, b_{l}. Hence,

apply(T [[(x_{i} B_{1} … B_{l})]]_{E}, E(y_{1}), …, E(y_{m})) ⊒ apply(⟨i_{j}, p_{j}⟩, b_{1}, …, b_{l})
= apply(⟨j,?, ⊥⟩, E(y_{1}), …, E(y_{m}))

By extensionality,

T [[(x_{i} B_{1} … B_{l})]]_{E} ⊒ ⟨j,?, ⊥⟩

implying that T [[M′]]_{[x_{i}:=d_{i}]} = ⟨j,?, g⟩ for some branching function g. This observation completes the proof of the lemma.

6 Observable Sequentiality in SPCF

We define the meaning of the language SPCF using the tree model T .

Definition 6.1. (Semantic Definition of SPCF ) The semantic definition of SPCF is the meaning function T determined by the model T restricted to programs.

Theorem 6.2 (Sequentiality of SPCF) SPCF is sequential.

Proof. Let M_{1}, …, M_{k} be closed phrases in SPCF and let C[M_{1}, …, M_{k}] be a program satisfying the hypotheses of Definition 2.9: (i) T [[C[M_{1}, …, M_{k}]]] = n; (ii) T [[C[Ω, …, Ω]]] = T [[Ω]]. We must show that there is one argument position j that forces divergence. Since the model satisfies the equation β, we have:

T [[C[M_{1}, …, M_{k}]]] = T [[apply(λ^{∗}x_{1} … x_{k} . C[x_{1}, …, x_{k}]), M_{1}, …, M_{k})]].

Hence, it suffices to consider the denotations of the k-ary procedure

(λ^{∗}x_{1} … x_{k} . C[x_{1}, …, x_{k}])

The possible denotations of such a procedure are either elements of _{⊥}^{}or triples of the form ⟨j,?, f⟩ for some j ≤ k and some branching function f . Clearly, the first case contradicts the hypothesis of Definition 2.9. The second case specifies that the k-ary procedure probes its j th argument first. But this fact implies that the program C[M_{1}, …, M_{k}] diverges if the expression M_{j} in j th hole diverges—regardless of the expressions in the other holes. Hence, the program behaves sequentially.

Indeed, SPCF satisfies a stronger condition than sequentiality: every procedure propagates any errors that are encountered during program evaluation. We formalize this stronger condition, called error-sensitivity as follows.

Definition 6.3. (Error-Sensitivity) Let L be a language based on λ-calculus. A semantic definition P for L is error-sensitive iff there exist two closed expressions E_{1} and E_{2}, denoting distinct and inconsistent elements of a flat domain for the ground type, with the following property. Let C[M_{1}, …, M_{k}] be a terminating program where the phrases M_{1}, …, M_{k} are closed, P[[C[M_{1}, …, M_{k}]]] ∈ , and P[[C[Ω, …, Ω]]] = P[[Ω]]. Then there exists j such that

P[[C[M′_{1}, …, M′_{j−1}, E_{j}, M′_{j+1}, …, M′_{k}]]] = P[[E_{j}]]

for all M′_{l}, 1 ≤ l ≤ k.

It is easy to show that SPCF is error-sensitive.

Theorem 6.4 SPCF is error-sensitive.

Proof. By exactly the same analysis presented in the preceding proof of the sequentiality of SPCF, the program C[…] returns error_{i} if the j th argument is error_{i}, regardless of the values of the remaining arguments.

Error-sensitivity implies sequentiality.

Theorem 6.5 If a semantic definition P of a language L is error-sensitive, then it is sequential.

Proof. Let C[M_{1}, …, M_{k}] be a terminating program such that P[[C[M_{1}, …, M_{k}]]] = n for some n ∈ yet P[[C[Ω, …, Ω]]] = P[[Ω]]. Since L is error-sensitive, there exists j such that

P[[C[M′_{1}, …, M′_{j−1}, E_{1}, M′_{j+1}, …, M′_{k}]]] = P[[E_{1}]]

and

P[[C[M′_{1}, …, M′_{j−1}, E_{2}, M′_{j+1}, …, M′_{k}]]] = P[[E_{2}]]

for all M′_{i}. By monotonicity,

P[[C[M′_{1}, …, M′_{j−1}, Ω, M′_{j+1}, …, M′_{k}]]] ⊑ P[[E_{1}]]

and

P[[C[M′_{1}, …, M′_{j−1}, Ω, M′_{j+1}, …, M′_{k}]]] ⊑ P[[E_{2}]].

Since E_{1} and E_{2} denote inconsistent ground values in a flat domain,

P[[C[M′_{1}, …, M′_{j−1}, Ω, M′_{j+1}, …, M′_{k}]]] = P[[Ω]],

which is precisely what sequentiality demands.

The error-sensitivity of SPCF implies that the tree model T is extensional. The domain of decision trees of type σ → τ is isomorphic to the domain of error-sensitive continuous functions mapping ^{σ} into ^{τ}. But error-sensitivity does not make the decision tree model fully abstract. To represent all error-sensitive functions in SPCF, we need some mechanism within the language for determining the evaluation order of programs. We call this property of languages observable sequentiality.

Definition 6.6. (Observable Sequentiality) A semantic definition P of a language L based on the typed λ-calculus is observably sequential iff it is sequential and it satisfies the following property. Let C be a context and M_{1}, …, M_{k} be closed expressions and let C[M_{1}, …, M_{k}] be a program such that P[[C[M_{1}, …, M_{k}]]] ∈ yet P[[C[Ω, …, Ω]]] = P[[Ω]]. Then there exists a program context D[ ] such that

P[[D[λx_{1} … x_{k} . C[x_{1}, …, x_{k}]]]] = P[[j]]

where j is the sequentiality index of C.

The catch procedures make SPCF observably sequential.

Theorem 6.7 SPCF is observably sequential.

Proof. We have already shown that SPCF is error-sensitive. The remainder of the proof is trivial: simply set D[ ] = (add1 (catch [ ])).

SPCF is not the first observably sequential language that has been studied in the context of the full abstraction problem. Berry and Currien [5] defined an observably sequential language called CDS0 in their work on sequential algorithms. They also constructed a fully abstract model for CDS0 based on sequential algorithms (which correspond to decision trees without errors), but the model is not extensional because the language is not error-sensitive.

Our experience with PCF suggests that error-sensitivity and observable sequentiality are necessary properties for the construction of extensional, fully abstract tree models for sequential languages. Error-sensitivity is required to obtain extensionality and observable sequentiality is required to obtain full abstraction. In the absence of error-sensitivity, procedures that are strict in several different arguments have multiple representations. Similarly, in the absence of observable sequentiality, higher order procedures cannot recognize the difference between procedures that are identical except for differences in the order in which they evaluate their arguments. In the next section, we identify some features in practical languages that interfere with the properties of error sensitivity and observable sequentiality.

7 Generalizing Observable Sequentiality

PCF is neither error-sensitive nor observably sequential. Consequently, the decision tree model for PCF is neither extensional nor fully abstract. However, the interesting issue is which practical programming languages with rich control operators are not error-sensitive or observably sequential. At this point we know of one prominent example: sequential languages with control delimiters [10], also referred to as prompts.

The task of a control delimiter is to mask any control operation that happens during the dynamic extent of some expression. Some typical examples in practical languages are Lisp’s errset, Common Lisp’s unwind-protect and ML’s wild-card error-handler. Pragmatically, control delimiters are used to recover gracefully from unforeseen errors or to attach actions to non-local control operations. Languages with control delimiters are designed not to be error-sensitive because the very task of control delimiters is to swallow all errors generated within their dynamic extent.

Consider the following example. Let PCF′ be PCF augmented by the control delimiter % [22] where % is defined by the equation

[[(% e)]] = \{ \begin{matrix}[[e]] & [[e]] ∈ _{⊥} \\ i & [[e]] = error_{i} ∈ \end{matrix} .

In PCF′, we can define an error-insensitive addition function:

+_{ei} = (λxy . (+_{l} (% x) (% y))) = (λxy . (+_{r} (% x) (% y))),

which demonstrates that PCF′ is not an error-sensitive language.

At this point, we do not know whether our construction solves the full abstraction problem for all sequential functional languages of practical interest. The preceding example shows that the problem remains open for practical languages that are sequential but not error-sensitive and observably sequential.

Acknowledgements. We thank Rama Kannegati and Dorai Sitaram for helping hone our intuitions about error-sensitivity and sequentiality. Discussions with Pierre-Louis Curien clarified the relationship of our work to sequential algorithms and convinced us that we were working in the tradition of the full abstraction literature; his comments on an early draft improved the presentation of the material. Steve Brookes pointed out a mistake in our original definition of sequentiality. John Gately found several errors in the proofs that we inserted in the expanded version of the paper.

Appendices

A K and S

A.1 The K Combinator

Lemma A.1 For all d ∈ ^{σ}, e ∈ ^{τ},

apply(K^{σ,τ} , d, e) = d.

Proof. We will prove this lemma for finite trees and then use a continuity argument to extend the lemma to all trees. To prove the lemma for finite trees, we make the following claim about the subtrees of K^{σ,τ}.

Claim A.2 Let d ∈ ^{σ}, e ∈ ^{τ} and let q ∈ ^{σ} be a valid path in d (d@q is defined). Then, apply(K(q), d, e) = d@q.

Proof (of Claim). The proof proceeds by induction on the size of the subtree d@q. Let

K′_{q} = \underline{λ}r . \{ \begin{matrix}a & r = q[?/a], a ∈ \\ ⟨i + 2, p, \underline{λ}r′.K(r . ⟨r′,?⟩)⟩ & r = q[?/⟨i, p⟩] \end{matrix} .

By the definition of the generating function K,

K(q) = ⟨1, q, K′_{q}⟩ .

A case analysis on the form of d@q yields the following values for apply(K(q), d, e):

1. d@q ∈ : If d@q = ⊥,

apply(⟨1, q, K′_{q}⟩, d, e) = ⊥ = d@q.

If d@q = error_{1} or d@q = error_{2} the same reasoning holds.

2. d@q ∈ : By the definition of K′_{q},

apply(⟨1, q, K′_{q}⟩, d, e) = apply(d@q, d, e) = d@q.

3. d@q = ⟨i, p, f⟩: Again by the definition of K′_{q}:

apply(⟨1, q, K′_{q}⟩, d, e) = apply(K′_{q}(⟨i, p⟩), d, e)
= apply(⟨i + 2, p, \underline{λ}r′ . K(q[?/⟨i, p⟩] . ⟨r′,?⟩)⟩, d, e)
= ⟨i, p, \underline{λ}r′ . apply(K(q[?/⟨i, p⟩] . ⟨r′,?⟩), d, e)⟩
= ⟨i, p, \underline{λ}r′ . f(r′)⟩  (by the induction hypothesis!)
= ⟨i, p, f⟩
= d@q .

This case analysis exhausts all possible forms for d@q proving the claim. (Claim) From the claim and the definition of K, we can immediately conclude that for d ∈ ^{σ}, e ∈ ^{τ}

apply(K^{σ,τ} , d, e) = d.

The rest of the lemma follows from continuity. For arbitrary d and e,

apply(K, d, e) = ⨆ {apply(K, d′, e′) | d′ ⊑ d, e′ ⊑ e, d′, e′ are finite }
= ⨆ {d′ | d′ ⊑ d, d′ is finite }
= d ,

which proves the lemma.

A.2 The S Combinator

Before we can prove that S^{σ,τ,υ} satisfies its characteristic equation, we need to define the generating function S for S rigorously and prove that S is a well-formed decision tree. The generating function S is the least upper bound of an ascending chain of partial functions S_{n} mapping ^{(σ→τ→υ)→(σ→τ)→σ→υ} × ^{σ→τ→υ} into ⋃_{ρ} ^{(σ→τ→υ)→(σ→τ)→σ→υ}(ρ). Since the generating functions S and T are mutually recursive, a truncated approximation function T_{n} for T must be defined in conjunction with S_{n}. The definition of S_{n} and T_{n} follows the same pattern of the of K_{n} in Section 4.3.

Definition A.3. (S, T, S_{n}, T_{n}) For n ≥ −1, the functions S_{n} and T_{n} are defined by the recursion equations in Figure 8 where n ∈ .

S(p_{S}, q_{1}) = ⨆_{n} S_{n}(p_{S}, q_{1})
S_{−1}(p_{S}, q_{1}) = ⊥
S_{0}(p_{S}, q_{1}) = ⊥
S_{n+1}(p_{S}, q_{1}) =

let {d_{2} = p̂_{S}(2); d_{3} = p̂_{S}(3)} in

⟨1, q_{1}, \underline{λ}r_{1}∈R(q_{1}) . \{ \begin{matrix}a & r_{1} = q_{1}[?/a] \\ S_{n}(p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], & r_{1} = q_{1}[?/⟨1, p⟩], \\ r_{1} . ⟨p[?/root (d_{3}@p)],?⟩) & d_{3}@p ≠ ⊥ \\ ⟨3, p, \underline{λ}s∈R(p) . & r_{1} = q_{1}[?/⟨1, p⟩], \\ S_{n−1}(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨3, p, ⟨s,?⟩⟩⟩⟩], & d_{3}@p = ⊥ \\ r_{1} . ⟨s,?⟩)⟩ \\ T_{n}(p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], encode(d_{2}, p)) & r_{1} = q_{1}[?/⟨2, p⟩] \\ ⟨i + 3, p, \underline{λ}s∈R(p) . & r_{1} = q_{1}[?/⟨i + 2, p⟩] \\ S_{n}(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨i + 3, p, ⟨s,?⟩⟩⟩⟩], \\ r_{1} . ⟨s,?⟩)⟩ \end{matrix} ⟩

T (p_{S}, q_{2}) = ⨆_{n} T_{n}(p_{S}, q_{2})
T_{−1}(p_{S}, q_{2}) = ⊥
T_{0}(p_{S}, q_{2}) = ⊥
T_{n+1}(p_{S}, q_{2}) =

let^{∗} {r_{1} = p̂_{S}(1); d_{2} = p̂_{S}(2); d_{3} = p̂_{S}(3); q_{1}[?/⟨2, p⟩] = r_{1}} in

⟨2, q_{2}, \underline{λ}r_{2}∈R(q_{2}) . \{ \begin{matrix}S_{n}(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], & r_{2} = q_{2}[?/a] \\ r_{1} . ⟨shift_{1}(r_{2}),?⟩) \\ T_{n}(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], & r_{2} = q_{2}[?/⟨1, p⟩], \\ r_{2} . ⟨p[?/root (d_{3}@p)],?⟩) & d_{3}@p ≠ ⊥ \\ ⟨3, p, \underline{λ}s∈R(p) . & r_{2} = q_{2}[?/⟨1, p⟩], \\ T_{n−1}(p_{S}[?/⟨2, q_{2}, ⟨r_{2}, ⟨3, p, ⟨s,?⟩⟩⟩⟩], & d_{3}@p = ⊥ \\ r_{2} . ⟨s,?⟩)⟩ \\ S_{n}(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], & r_{2} = q_{2}[?/⟨i + 1, p⟩] \\ r_{1} . ⟨shift_{1}(r_{2}),?⟩) \end{matrix} ⟩

Figure 8: Definition of the functions S_{n}, T_{n} for (n ≥ −1)

Informally, the finite subtree S_{n}(p_{S}, q_{1}) is simply the subtree at position p_{S} in S truncated at depth n. The arguments q_{1} and q_{2} for S_{n} and T_{n}, respectively, are redundant, but reconstructing their values from p_{S} requires a tedious case analysis.

To prove that S is well-defined, we need to introduce invariants Σ and T describing the domain of the functions S_{n} and T_{n}, respectively. Before we state the invariants, we need to introduce the idea of an error variant.

Definition A.4. (Error variant) Given a finite tree d ∈ ^{σ} that does not contain any leaves of the form error_{1} or error_{2}, a finite tree d′ ∈ ^{σ} is an error_{i} variant of d iff d′ is identical to d except for one subtree position q where d′@q = error_{i} but d@q ≠ ⊥.

Let Σ(p_{S}, q_{1}) be the property that p_{S} ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ} and q_{1} ∈ ^{(σ→τ→υ)} satisfy the following conditions where r_{1} = ⊔ p̂_{S}(1), d_{2} = ⊔ p̂_{S}(2), and d_{3} = ⊔ p̂_{S}(3):

• q_{1} = r_{1} . ⟨r_{p},?⟩ where

r_{p} = p[?/root (d_{3}@p)]  r_{1} = q[?/⟨1, p⟩]
r_{p} = p[?/root (apply(d_{2}, d_{3})@p)] r_{1} = q[?/⟨2, p⟩]
r_{p} ∈ R(p)  r_{1} = q[?/⟨i + 2, p⟩] .

• q̂_{1}(i + 2) = p̂_{S}(i + 3) for all i ≥ 0.

• ⊔ q̂_{1}(2) = apply(d_{2}, d_{3}).

• ⊔ q̂_{1}(1) ⊑ d_{3}.

• For all error_{i} variants d′_{2} of d_{2}, there exists p′ ∈ q̂_{1}(2) such apply(d′_{2}, d_{3})@p′ = error_{i}.

• For all error_{i} variants d′_{3} of d_{3} such that ⊔ q̂_{1}(1) ⊑ d′_{3}, there exists p′ ∈ q̂_{1}(2) such apply(d_{2}, d′_{3})@p′ = error_{i}.

• For all q_{1}[?/⟨2, p⟩] ∈ R(q_{1}), there exists a query q such that d_{2}@q = ⊥, p = shift_{1}(q),

and encode(d_{2}, p) = q. In the invariant Σ, the query p_{S} identifies a position in the tree S where a node of the form ⟨1, q_{1}, □⟩ appears. Note that r_{1}, d_{2}, d_{3}, and q_{1} cannot contain any error elements because error elements cannot appear in queries (e.g. p_{S}) or responses (e.g. r_{p}).

We need an analogous invariant T for each position p_{S} where a node of the form ⟨2, q_{2}, □⟩ appears in S. Let T(p_{S}, q_{2}) be the property that p_{S} ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ} and q_{2} ∈ ^{σ→τ} satisfy the following conditions where r_{1} = ⊔ p̂_{S}(1) = q_{1}[?/⟨2, p⟩], d_{2} = ⊔ p̂_{S}(2), and d_{3} = ⊔ p̂_{S}(3):

• q_{2} =

encode(d_{2}, p)  p_{S} = p′_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], r_{1} = q_{1}[?/⟨2, p⟩]
r_{2} . ⟨p[?/root (d_{3}@p)],?⟩ p_{S} = p′_{S}[?/⟨2, q′_{2}, ⟨r_{2},?⟩⟩], r_{2} = q′_{2}[?/⟨1, p⟩]
r_{2} . ⟨s,?⟩  p_{S} = p′_{S}[?/⟨3, p, ⟨s,?⟩⟩]

• d_{2}@q_{2} = ⊥.

• q̂_{1}(i + 2) = p̂_{S}(i + 3) for all i ≥ 0.

• ⊔ q̂_{1}(2) = apply(d_{2}, d_{3}).

• ⊔ q̂_{1}(1) ⊑ d_{3}.

• apply(d_{2}, d_{3})@p = ⊥.

• For all error_{i} variants d′_{2} of d_{2}, there exists p′ ∈ r̂_{1}(2) such that apply(d′_{2}, d_{3})@p′ = error_{i}.

• For all error_{i} variants d′_{3} of d_{3} such that ⊔ q̂_{1}(1) ⊑ d′_{3}, there exists p′ ∈ r̂_{1}(2) such apply(d_{2}, d′_{3})@p′ = error_{i}.

• For all r′_{2} = q_{2}[?/a] ∈ R(q_{2}), a ∈ , and r_{1} . ⟨shift_{1}(r′_{2}), ⟨2, p′⟩⟩ ∈ R(r_{1} . ⟨shift_{1}(r′_{2}),?⟩), there exists a query q such that (d_{2} ⊔ r′_{2})@q = ⊥, p′ = shift_{1}(q), and encode(d_{2} ⊔ r′_{2}, p′) = q.

• For all r′_{2} = q_{2}[?/⟨j + 1, p′⟩] ∈ R(q_{1}) and all p′ such that

r_{1} . ⟨shift_{1}(r′_{2}), ⟨2, p′⟩⟩ ∈ R(r_{1} . ⟨shift_{1}(r′_{2}),?⟩) ,

there exists a query q such that (d_{2} ⊔ r′_{2})@q = ⊥, p′ = shift_{1}(q), and

encode(d_{2} ⊔ r′_{2}, p′) = q .

We are finally ready to prove that S is well-formed.

Claim A.5 The following two statements about S_{n} and T_{n} both hold:

1. For all p_{S} and q_{1} satisfying the invariant Σ,

S_{n}(p_{S}, q_{1}) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S}) .

2. For all p_{S} and q_{2} satisfying the invariant T,

T_{n}(p_{S}, q_{2}) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S}) .

Proof. The proof of the claim proceeds by induction on n. We assume that the claim holds for all n′ < n and prove that it holds for n.

1. n ≤ 0: In the base case, S_{n}(p_{S}, q_{1}) = ⊥ and T_{n}(p_{S}, q_{2}) = ⊥, so the claim trivially holds.

2. n > 0: In the induction step, we must consider all queries p_{S} and q_{1} in the call S_{n}(p_{S}, q_{1}) satsifying the invariant Σ. Similarly, we must consider all queries p_{S} and q_{2} in the call T_{n}(p_{S}, q_{2}) satisfying the invariant T.

For n > 0, S_{n}(p_{S}, q_{1}) has the form ⟨1, q_{1}, g⟩ where the branching function g is defined at r_{1} ∈ R(q_{1}) by cases. Since the invariant Σ holds, we know that p̂_{S}(1) = \overline{q}_{1} and r_{1} ∈ R(q_{1}), implying that the subtree ⟨1, q_{1}, g⟩ is well-formed iff g(r_{1}) ∈ (σ→τ→υ)→(σ→τ)→σ→υ(p̂_{S} ∪ {(1, r_{1})}) for all r_{1} ∈ R(q_{1}). Let’s consider each of the cases in the definition of the branching function g:

(a) r_{1} = q_{1}[?/a] and g(r_{1}) = a ∈ . We immediately conclude

g(r_{1}) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(1, r_{1})})

from the definition of .

(b) r_{1} = q_{1}[?/⟨1, p⟩], d_{3}@p ≠ ⊥, and

g(r_{1}) = S_{n−1}(p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], r_{1} . ⟨p[?/root (d_{3}@p)],?⟩) .

By assumption, the response r_{1} ∈ R(q_{1}), implying p̂_{S} ∪{(1, r_{1})} is a valid context in . Similarly, s ∈ R(p) because root (d_{3}@p) ⊑ d_{3}@p and d_{3} ∈ ^{σ}. Consequently, the r_{1} . ⟨s,?⟩ is a legal query on argument 1 in context p̂_{S} ∪ {(1, r_{1})}. It is easy to confirm that the invariant Σ holds for the pair

(p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], r_{1} . ⟨p[?/root (d_{3}@p)],?⟩) .

As a result,

g(r_{1}) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(1, r_{1})})

by induction.

(c) r_{1} = q_{1}[?/⟨1, p⟩], d_{3}@p = ⊥, and

g(r_{1}) = ⟨3, p, \underline{λ}s ∈ R(p) . S_{n−2}(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨3, p, ⟨s,?⟩⟩⟩⟩], r_{1} . ⟨s,?⟩)⟩ .

As in the preceding case, r_{1} ∈ R(q_{1}) and p̂_{S} ∪ {(1, r_{1})} is a valid context in . In addition, d_{3}@p = ⊥ implies that p ∈ Q((p̂_{S} ∪ {(1, r_{1})})(3)) (since d_{3} = ⊔p̂_{S}(3)). Hence,

⟨3, p, ⊥⟩ ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(1, r_{1})}) .

For each s ∈ R(p), we can confirm that the invariant Σ holds for the pair

(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨3, p, ⟨s,?⟩⟩⟩⟩], r_{1} . ⟨s,?⟩) ,

implying

\begin{matrix}S_{n−2}(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨3, p, ⟨s,?⟩⟩⟩⟩], r_{1} . ⟨s,?⟩) ∈ \\ D^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ \{(1, r_{1})\} ∪ \{(3, s)\}) . \end{matrix}

Hence, by induction,

g(r_{1}) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(1, r_{1})}) .

(d) r_{1} = q_{1}[?/⟨2, p⟩] and

g(r_{1}) = T_{n−1}(p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], encode(d_{2}, p)) .

Since Σ holds for p_{S}, we can confirm that T holds for the pair

(p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], encode(d_{2}, p)) .

Hence, by induction,

g(r_{1}) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(1, r_{1})}) .

(e) r_{1} = q_{1}[?/⟨i + 2, p⟩] and

g(r_{1}) = ⟨i + 3, p, \underline{λ}s∈R(p) . S_{n}(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨i + 3, p, ⟨s,?⟩⟩⟩⟩], r_{1} . ⟨s,?⟩)⟩

Since Σ holds for p_{S} and r_{1} = q_{1}[?/⟨i + 2, p⟩],

⟨i + 3, p, ⊥⟩ ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(1, r_{1})}) .

In addition, for each s ∈ R(p), we can confirm that the invariant Σ holds for the pair

(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨i + 3, p, ⟨s,?⟩⟩⟩⟩], r_{1} . ⟨s,?⟩) ,

implying

\begin{matrix}S_{n}(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨i + 3, p, ⟨s,?⟩⟩⟩⟩], r_{1} . ⟨s,?⟩) ∈ \\ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ \{(1, r_{1})\} ∪ \{(i + 3, s)\}) . \end{matrix}

Hence, by induction,

g(r_{1}) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(1, r_{1})}) .

For n > 0, T_{n}(p_{S}, q_{2}) has the form ⟨2, q_{2}, g⟩ where the branching function g is defined by cases on responses r_{2} ∈ R(q_{2}). Since the invariant T holds for (p_{S}, q_{2}), we know that p̂_{S}(2) = d_{2} and d_{2}@q_{2} = ⊥, implying that the subtree ⟨2, q_{2}, g⟩ is well-formed iff g(r_{2}) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(2, r_{2})}) for all r_{2} ∈ R(q_{2}). Let’s consider each of the cases in the definition of the branching function g.

(a) r_{2} = q_{2}[?/a] and

g(r_{2}) = S_{n−1}(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], r_{1} . ⟨shift_{1}(r_{2}),?⟩)

where a ∈ N. Since the invariant T holds for (p_{S}, q_{2}), we can confirm that the invariant Σ holds for

(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], r_{1} . ⟨shift_{1}(r_{2}),?⟩) .

Hence, by induction

g(r_{2}) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(2, r_{2})}) .

(b) r_{2} = q_{2}[?/⟨1, p⟩], d_{3}@p ≠ ⊥, and

g(r_{2}) = T_{n−1}(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], r_{2} . ⟨p[?/root (d_{3}@p)],?⟩) .

Since the invariant T holds for for (p_{S}, q_{2}), we can confirm that the invariant T holds for

(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], r_{2} . ⟨p[?/root (d_{3}@p)],?⟩) .

Hence, by induction

g(r_{2}) =∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(2, r_{2}))} .

(c) r_{2} = q_{2}[?/⟨1, p⟩], d_{3}@p = ⊥, and

g(r_{2}) = ⟨3, p, \underline{λ}s ∈ R(p) . T_{n−2}(p_{S}[?/⟨2, q_{2}, ⟨r_{2}, ⟨3, p, ⟨s,?⟩⟩⟩⟩], r_{2} . ⟨s,?⟩)⟩ .

Since the invariant T holds for (p_{S}, q_{2}), we can confirm that the invariant T holds for

(p_{S}[?/⟨2, q_{2}, ⟨r_{2}, ⟨3, p, ⟨s,?⟩⟩⟩⟩], r_{2} . ⟨s,?⟩) .

Hence,

\begin{matrix}T_{n−2}(p_{S}[?/⟨2, q_{2}, ⟨r_{2}, ⟨3, p, ⟨s,?⟩⟩⟩⟩]) ∈ \\ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ \{(2, r_{2})\} ∪ \{(3, s)\}) . \end{matrix}

In addition, d_{3}@p = ⊥ implies that p ∈ Q((p̂_{S} ∪ (2, r_{2}))(3)) (since d_{3} = ⊔p̂_{S}(3)). Hence,

⟨3, p, ⊥⟩ ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(2, r_{2})}) ,

implying that

g(r_{2}) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(2, r_{2})}) .

(d) r_{2} = q_{2}[?/⟨i + 1, p⟩] and

g(r_{2}) = S_{n−1}(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], r_{1} . ⟨shift_{1}(r_{2}),?⟩) .

Since the invariant T holds for for (p_{S}, q_{2}), we can confirm that the invariant Σ holds for

(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩], r_{1} . ⟨shift_{1}(r_{2}),?⟩) .

Hence, by induction

g(r_{2}) = S_{n−1}(p_{S}[?/⟨2, q_{2}, ⟨r_{2},?⟩⟩]) ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ}(p̂_{S} ∪ {(2, r_{2})}) .

This analysis of the possible form of r_{2} concludes the proof of the claim. (Claim) Given the claim, it is easy to show that

S ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ} .

The query ? clearly satisfies the invariant Σ. In addition, for all n ≥ 0,

S_{n}(?,?) ⊑ S_{n+1}(?,?) .

Hence,

S = ⨆_{n}{S_{n}(?,?)} ∈ ^{(σ→τ→υ)→(σ→τ)→σ→υ} .

Now we are finally ready to prove that S satisfies its characteristic equation.

Lemma A.6 For all e_{1}, e_{2}, e_{3} in appropriate domains,

apply(S(?,?), e_{1}, e_{2}, e_{3}) = apply(apply(e_{1}, e_{3}), apply(e_{2}, e_{3}))

Proof. As in Lemma A.1, we first prove the lemma holds for finite subtrees; the proof relies on the fact that the inputs e_{1}, e_{2}, and e_{3} direct the application process from the root of a tree to the given subtree (see Lemma A.7 below). Given that, we can prove the full lemma via the continuity of apply.

Lemma A.7 Let p_{S} and q_{1} be queries satisfying the invariant Σ and let e_{1}, e_{2}, e_{3} be finite elements in appropriate domains such that \overline{q_{1}} ⊑ e_{1}, ⨆ p̂_{S}(2) ⊑ e_{2}, and ⨆ p̂_{S}(3) ⊑ e_{3}. Then

apply(S(p_{S}, q_{1}), e_{1}, e_{2}, e_{3}) = apply(apply(e_{1}@q_{1}, e_{3}), apply(e_{2}, e_{3})).

Proof. The proof proceeds by induction on the form of e′_{1} =^{df} e_{1}@q_{1}:

1. e′_{1} ∈ : If e′_{1} =⊥, then

apply(S(p_{S}, q_{1}), e_{1}, e_{2}, e_{3}) = ⊥
= apply(⊥, apply(e_{2}, e_{3}))
= apply(apply(e′_{1}, e_{3}), apply(e_{2}, e_{3}))

If e′_{1} = error_{1} or e′_{1} = error_{2} the same reasoning holds.

2. e′_{1} ∈ : Then,

apply(S(p_{S}, q_{1}), e_{1}, e_{2}, e_{3}) = apply(e′_{1}, e_{1}, e_{2}, e_{3})
= e′_{1}
= apply(e′_{1}, apply(e_{2}, e_{3}))
= apply(apply(e′_{1}, e_{3}), apply(e_{2}, e_{3}))

3. e′_{1} = ⟨1, p, f_{1}⟩: Then,

apply(S(p_{S}, q_{1}), e_{1}, e_{2}, e_{3}) = apply((\underline{λ}r_{1} ∈ R(q_{1}) . · · ·)(q_{1}[?/⟨1, p⟩]), e_{1}, e_{2}, e_{3}) .

The argument e_{1} is asking for the value of its first argument at position p. But e_{1}’s first argument is e_{3}. The tree S(p_{S}, q_{1}) does the translation. For the remainder of this proof, let d_{1} =^{df} \overline{q_{1}}, d_{2} =^{df} ⨆ p̂_{S}(2), and d_{3} =^{df} ⨆ p̂_{S}(3). In addition, let r_{3} be the response by e_{3} to the query p. Hence, r_{3} ⊑ e_{3} and r_{3} ∈ R(p). We need to distinguish two subcases:

(a) d_{3}@p ≠ ⊥: That is p_{S} already contains the response r_{3} to querying e_{3} at position p. Let r_{1} denote q_{1}[?/⟨1, p⟩]. Then, by the definition of S,

… = apply(S(p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], r_{1} . ⟨r_{3},?⟩), e_{1}, e_{2}, e_{3})
= apply(apply(f_{1}(r_{3}), e_{3}), apply(e_{2}, e_{3}))  (by induction hypothesis)
= apply(apply(⟨1, p, f_{1}⟩, e_{3}), apply(e_{2}, e_{3}))  (by definition of apply)
= apply(apply(e′_{1}, e_{3}), apply(e_{2}, e_{3}))

(b) d_{3}@p = ⊥: Let r_{1} denote q_{1}[?/⟨1, p⟩]. Then

… = apply(⟨3, p, \underline{λ}s ∈ R(p) . S(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨3, p, ⟨s,?⟩⟩⟩⟩], r_{1} . ⟨s,?⟩)⟩,
e_{1}, e_{2}, e_{3})
= apply(S(p_{S}[?/⟨1, q_{1}, ⟨r_{1}, ⟨3, p, ⟨r_{3},?⟩⟩⟩⟩], r_{1} . ⟨r_{3},?⟩),
e_{1}, e_{2}, e_{3})
= apply(apply(f_{1}(r_{3}), e_{3}), apply(e_{2}, e_{3}))  (by induction hypothesis)
= apply(apply(⟨1, p, f_{1}⟩, e_{3}), apply(e_{2}, e_{3}))  (by definition of apply)
= apply(apply(e′_{1}, e_{3}), apply(e_{2}, e_{3}))

The cases for (e_{3}@p) ∈ are simpler.

4. e′_{1} = ⟨2, p, f_{1}⟩: Hence,

apply(S(p_{S}, q_{1}), e_{1}, e_{2}, e_{3}) = apply((\underline{λ}r_{1} ∈ R(q_{1}) . · · ·)(q_{1}[?/⟨2, p⟩]), e_{1}, e_{2}, e_{3}) .

Let r_{1} = q_{1}[?/⟨2, p⟩]. Then,

apply(S(p_{S}, q_{1}), e_{1}, e_{2}, e_{3}) = apply(T (p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], q_{2}), e_{1}, e_{2}, e_{3})
= apply(⟨2, q_{2}, \underline{λ}r_{2} ∈ R(q_{2}) . · · ·⟩, e_{1}, e_{2}, e_{3})

where q_{2} = encode(d_{2}, p) and shift_{1}(q_{2}) = p. Since q_{2} is a legitimate query about e_{2}, \overline{q_{2}} ⊑ e_{2}.

To complete the proof for e′_{1} = ⟨2, p, f_{1}⟩, we invoke the following claim (labeled ‡), which we will prove later.

For any queries p′_{S} and q′_{2} satisfying the invariant T

apply(T (p′_{S}, q′_{2}), e_{1}, e_{2}, e_{3}) =

\{ \begin{matrix}w & w ∈ \\ apply(S(p′_{S}[?/⟨2, q′_{2}, ⟨q′_{2}[?/w],?⟩⟩], & w ∈ \\ d′_{1} . ⟨shift_{1}(q′_{2}[?/w]),?⟩), e_{1}, e_{2}, e_{3}) \\ apply(S(p′_{S}[?/⟨2, q′_{2}, ⟨q_{2}[?/⟨i + 1, p′′⟩],?⟩⟩], & w = ⟨i, p′′, ·⟩ \\ d′_{1} . ⟨shift_{1}(q′_{2}[?/⟨i + 1, p′′⟩]),?⟩), e_{1}, e_{2}, e_{3}) \end{matrix} (‡)

where e′_{2} =^{df} e_{2}@q′_{2} and w =^{df} apply(e′_{2}, e_{3}).

The hypothesis of claim ‡ is clearly where p′_{S} = p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩] and q′_{2} = q_{2}. In this case, we can rewrite the claim as:

apply(T (p_{S}[?/⟨1, q_{1}, ⟨r_{1},?⟩⟩], q_{2}), e_{1}, e_{2}, e_{3}) =
w  w ∈
apply(apply(f_{1}(p[?/w]), e_{3}), apply(e_{2}, e_{3}))  w ∈
apply(apply(f_{1}(p[?/⟨i, p′′⟩]), e_{3}), apply(e_{2}, e_{3})) w = ⟨i, p′′, ·⟩

where e′_{2} =^{df} e_{2}@q_{2} and w =^{df} apply(e′_{2}, e_{3}).

Given the claim (‡), the final step in the proof for the case e′_{1} = ⟨2, p, f_{1}⟩ is to verify that the right side of the preceding equation equals

apply(apply(e′_{1}, e_{3}), apply(e_{2}, e_{3})) .

By the definition of apply, we know that

apply(apply(e′_{1}, e_{3}), apply(e_{2}, e_{3}))
= apply(apply(⟨2, p, f_{1}⟩, e_{3}), apply(e_{2}, e_{3}))
= apply(⟨1, p, \underline{λ}r_{1} ∈ R(p) . apply(f_{1}(r_{1}), e_{3})⟩, apply(e_{2}, e_{3})) ,

independent of w. In addition,

apply(e_{2}, e_{3}) ⊒ apply(q_{2}[?/e′_{2}], e_{3})
= apply(encode(e_{2}, p)[?/e′_{2}], e_{3})
= p[?/apply(e′_{2}, e_{3})]
= p[?/w],

implying that

apply(e_{2}, e_{3})@p = w.

Given this fact, we can verify the compound equation by performing a case split on w:

(a) w ∈ : Since apply(e_{2}, e_{3})@p = w,

apply(⟨1, p, \underline{λ}r′ . apply(f_{1}(r′), e_{3})⟩, apply(e_{2}, e_{3})) = w

(b) w ∈ : Since apply(e_{2}, e_{3})@p = w,

apply(⟨1, p, \underline{λ}r′ ∈ R(p) . apply(f_{1}(r′), e_{3})⟩, apply(e_{2}, e_{3})) =
apply(apply(f_{1}(p[?/w]), e_{3}), apply(e_{2}, e_{3}))

(c) w = ⟨i, p′′, ·⟩: Since apply(e_{2}, e_{3})@p = ⟨i, p′′, ·⟩,

apply(⟨1, p, \underline{λ}r′ ∈ R(p) . apply(f_{1}(r′), e_{3})⟩, apply(e_{2}, e_{3})) =
apply(apply(f_{1}(p[?/⟨i, p′′⟩]), e_{3}), apply(e_{2}, e_{3}))

To complete the proof for e′_{1} = ⟨2, p, f_{1}⟩, we still need to prove the claim (‡). The proof proceeds by a nested induction on e′_{2} =^{df} e_{2}@q′_{2}. We perform a case analysis on the form of e′_{2} and w =^{df} apply(e′_{2}, e_{3}), which is summarized in the following table:

e′_{2} ∈  e′_{2} ∈  e′_{2} = ⟨1, p′, ·⟩ e′_{2} = ⟨i + 1, p′′, ·⟩
w ∈  easy empty  A  empty
w ∈  empty easy  A  empty
w = ⟨i, p′′, ·⟩ empty empty  A  B

The cases marked easy are easy to prove, the cases marked empty are vacuously true, and the cases marked A and B need additional explanation:

A: Since e′_{2} = ⟨1, p′, ·⟩, we can immediately deduce that

apply(T (p′_{S}, q′_{2}), e_{1}, e_{2}, e_{3}) =
apply((\underline{λ}r_{2} ∈ R(q′_{2}) . · · ·)(q′_{2}[?/⟨1, p′⟩]), e_{1}, e_{2}, e_{3})

If \overline{p′} ⊑ d′_{3} =^{df} ⨆ p̂′_{S}(3), then p′_{S} already contains the response s by e_{3} to the query p′. Moreover, it is not bottom or an error value. Hence,

… = apply(T (p′_{S}[?/⟨2, q′_{2}, ⟨q′_{2}[?/⟨1, p′⟩],?⟩⟩], q′_{2}[?/⟨1, p′, ⟨s,?⟩⟩]), e_{1}, e_{2}, e_{3}) .

The rest follows from the inductive hypothesis because the T above is invoked with new values of p′_{S} and q′_{2} (as determined in the recursion equations defining T) that correspond to a smaller value of e′_{2} On the other hand, if d′_{3}@p′ = ⊥, p′_{S} does not contain e_{3}’s response to p′. Therefore, T generates the query p′ to probe e_{3}:

apply(T (p′_{S}, q′_{2}), e_{1}, e_{2}, e_{3}) =

apply(⟨3, p′, \underline{λ}s ∈ R(p′) .

T (p′_{S}[?/⟨2, q′_{2}, ⟨q′_{2}[?/⟨1, p′⟩], ⟨3, p′, ⟨s,?⟩⟩⟩⟩], q′_{2}[?/⟨1, p′, ⟨s,?⟩⟩])⟩,

e_{1}, e_{2}, e_{3})

Now, if e_{3}@p′ ∈ , then w ∈ and apply(T (p′_{S}, q′_{2}), e_{1}, e_{2}, e_{3}) = w. Otherwise, let s = p′[?/e_{3}@p′]. Then,

… =
apply(T (p′_{S}[?/⟨2, q′_{2}, ⟨q′_{2}[?/⟨1, p′⟩], ⟨3, p′, ⟨s,?⟩⟩⟩⟩], q′_{2}[?/⟨1, p′, ⟨s,?⟩⟩]),
e_{1}, e_{2}, e_{3})

and the rest follows by the inductive hypothesis as above.

B: In this case, the claim follows immediately since

apply(T (p′_{S}, q′_{2}), e_{1}, e_{2}, e_{3}) =

apply(S(p′_{S}[?/⟨2, q′_{2}, ⟨q′_{2}[?/⟨i + 1, p′⟩],?⟩⟩], d′_{1} . ⟨shift_{1}(q′_{2}[?/⟨i + 1, p′⟩]),?⟩),

e_{1}, e_{2}, e_{3})

by the definition of T, where d′_{1} =^{df} ⨆ p̂′_{S}(1).

The preceding case analysis completes the proof of claim (‡).

5. e′_{1} = ⟨i + 3, p, f_{1}⟩ for i ≥ 1: The proof of this case follows the same outline as the proof of Lemma A.1.

B Equations for catch and error

Lemma B.1 For all variables x_{1}, …, x_{n}, for all evaluation contexts E, and for all 1 ≤ j ≤ n,

T [[λ^{∗}x_{1}, …, x_{n} . E[x_{j}]]] = ⟨j,?, f⟩

for an appropriate branching function f .

Proof. Let d = T [[λ^{∗}x_{1}, …, x_{n} . E[x_{j}]]]. We procced by induction on the structure of the evaluation context E[ ]. There are three possible forms for E[ ]

1. E = [ ]: By (β), for all d_{i} in appropriate domains apply(d, d_{1}, …, d_{n}) = d_{j}. Thus, since d_{j} could be error_{1}, d cannot be ⊥ or a constant. Similarly, d also cannot be error_{1}, because d_{j} could be ⊥. Thus, d must be of the shape ⟨i,?, f⟩ for some i and f . Assume i ≠ j. Then, for d_{i} =⊥ and d_{j} = error_{1} we have that

apply(d, d_{1}, …, d_{n}) = apply(⟨i,?, f⟩, d_{1}, …, d_{n}) =⊥≠ error_{1} = d_{j},

which means that we have again derived a contradiction. We conclude that

T [[λ^{∗}x_{1}, …, x_{n} . x_{j}]] = ⟨j,?, f⟩

for some function f .

2. E = apply(s, E′): Observe that for all d_{i} in appropriate domains,

apply(d, d_{1}, …, d_{n})
= apply(T [[λ^{∗}x_{1}, …, x_{n} . apply(s, E′[x_{j}])]], d_{1}, …, d_{n})
= apply(T [[λ^{∗}x_{1}, …, x_{n} . apply(s, apply(apply(λ^{∗}x_{1}, …, x_{n} . E′[x_{j}],
x_{1}, …, x_{n})))]],
d_{1}, …, d_{n})
= apply(T [[s]], apply(T [[λ^{∗}x_{1}, …, x_{n} . E′[x_{j}]]], d_{1}, …, d_{n}))
= apply(⟨1,?, f_{s}⟩, apply(⟨j,?, f′⟩, d_{1}, …, d_{n})) .

The last step is an immediate consequence of the inductive hypothesis for some function f′ and the definition of strict, unary functions. As above, if d_{j} = error_{1}, the right-hand side is error_{1}, and thus d cannot be ⊥ or a constant. Conversely, if d_{j} =⊥ then the right-hand side is ⊥, and therefore d cannot be error_{1}. If d is ⟨i,?, f⟩, then i = j since the negation leads to a contradiction as in the base case.

3. E = apply(E′, M): With a short calculation we can see that the argument from the previous case applies here, too:

apply(d, d_{1}, …, d_{n})
= apply(T [[λ^{∗}x_{1}, …, x_{n} . apply(E′[x_{j}], M)]], d_{1}, …, d_{n})
= apply(T [[λ^{∗}x_{1}, …, x_{n} . apply(apply(λ^{∗}x_{1}, …, x_{n} . E′[x_{j}], x_{1}, …, x_{n}), M)]],

d_{1}, …, d_{n})
= apply(T [[apply(λ^{∗}x_{1}, …, x_{n} . E′[x_{j}], d_{1}, …, d_{n})]], T [[M[x_{1}/d_{1}] … [x_{n}/d_{n}]]])
= apply(apply(⟨j,?, f′⟩, d_{1}, …, d_{n}), T [[M[x_{1}/d_{1}] … [x_{n}/d_{n}]]])

where the last step follows from the inductive hypothesis for some function f′.

4. E = apply(catch, T [[λ^{∗}y_{1}, …, y_{m} . E′]]): Finally, the case of catch applications is a straightforward modification of the second case:

apply(d, d_{1}, …, d_{n})
= apply(T [[λ^{∗}x_{1}, …, x_{n} . apply(catch, λ^{∗}y_{1}, …, y_{m} . E′[x_{j}])]], d_{1}, …, d_{n})
= apply(T [[λ^{∗}x_{1}, …, x_{n} . apply(catch,
apply(λ^{∗}x_{1}, …, x_{n}, y_{1}, …, y_{m} . E′[x_{j}], x_{1}, …, x_{n}))]],
d_{1}, …, d_{n})
= apply(catch, apply(T [[λ^{∗}x_{1}, …, x_{n}, y_{1}, …, y_{m} . E′[x_{j}]]], d_{1}, …, d_{n}))
= apply(⟨1,?, fcatch⟩, apply(⟨j,?, f′⟩, d_{1}, …, d_{n}))

where the final step follows from the inductive hypothesis for some function f′.

This analysis covers all the possible forms for E[ ], completing the proof.

References

1. Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics. Revised Edition. Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, 1984.

2. Berry, G. Séquentialité de l’evaluation formelle des λ-expressions. In Proc. 3rd International Colloquium on Programming, 1978.

3. Berry, G. Modèles complètement adéquats et stables des lambda-calculus typé. Ph.D. dissertation, Université Paris VII, 1979.

4. Berry, G. and P-L. Curien. Sequential algorithms on concrete data structures. Theor. Comput. Sci. 20, 1982, 265–321.

5. Berry, G. and P-L. Curien. Theory and practice of sequential algorithms: the kernel of the applicative language cds. In Algebraic Methods in Semantics, edited by J. Reynolds and M.Nivat. Cambridge University Press. London, 1985, 35–88.

6. Berry, G., P-L. Curien, and P.-P. Lévy. Full-abstraction of sequential languages: the state of the art. In Algebraic Methods in Semantics, edited by J. Reynolds and M.Nivat. Cambridge University Press. London, 1985, 89–131.

7. Cartwright, R. and A. Demers. The topology of program termination. In Proc. Symposium on Logic in Computer Science, 1988, 296–308.

8. Curien, P-L. Categorical Combinators, Sequential Algorithms, and Functional Programming. Research Notes in Theoretical Computer Science. Pitman, London. 1986. Birkhäuser, Revised Edition, to appear.

9. Curien, P.-L.. Observable algorithms on concrete data structures. In Proc 7th Symposium on Logic in Computer Science, 1992, to appear.

10. Felleisen, M. The theory and practice of first-class prompts. In Proc. 15th ACM Symposium on Principles of Programming Languages, 1988, 180–190.

11. Felleisen, M. and R. Hieb. The revised report on the syntactic theories of sequential control and state. Technical Report 100, Rice University, June 1989. Theor. Comput. Sci., 1992, to appear.

12. Felleisen, M., D.P. Friedman, E. Kohlbecker, and B. Duba. A syntactic theory of sequential control. Theor. Comput. Sci. 52(3), 1987, 205–237. Preliminary version in: Proc. Symposium on Logic in Computer Science, 1986, 131–141.

13. Jim, T. and A. Meyer. Full abstraction and the context lemma. In Proc. International Conference on Theoretical Aspects of Computer Software (TACS). Lecture Notes in Computer Science 526. Springer Verlag, Berlin, 1991, 131–151.

14. Kahn, G. and G. Plotkin. Structures des donnés concrètes (Domaines Concrètes). IRIA Report 336. 1978.

15. Meyer, A. R. and K. Sieber. Towards a fully abstract semantics for local variables. In Proc. 15th ACM Symposium on Principles of Programming Languages, 1988, 191– 203.

16. Milner, R. Fully abstract models of typed λ-calculi. Theor. Comput. Sci. 4, 1977, 1–22.

17. Mulmuley, K. Full Abstraction and Semantic Equivalences. Ph.D. dissertation, Carnegie Mellon University, 1985. MIT Press, Cambridge, Massachusetts, 1986.

18. Plotkin, G.D. LCF considered as a programming language. Theor. Comput. Sci. 5, 1977, 223–255.

19. Rose, J.R. and G.L. Steele Jr. C*: An extended C language for data parallel programming. In Proc. Second International Conference on Supercomputing. International Supercomputing Institute, Inc. (Santa Clara, 1987) Volume II, 2-16. Also available as: Technical Report No. PL87-5, Thinking Machines Corporation, 1987.

20. Scott, D. S. Domains for denotational semantics. In Proc. International Conference on on Automata, Languages, and Programming, Lecture Notes in Mathematics 140, Springer-Verlag, Berlin, 1982, ??–??.

21. Scott, D.S. Lectures on a Mathematical Theory of Computation. Techn. Monograph PRG-19, Oxford University Computing Laboratory, Programming Research Group, 1981.

22. Sitaram, D. and M. Felleisen. Reasoning with continuations II: Full abstraction for models of control. In Proc. 1990 ACM Conference on Lisp and Functional Programming, 1990, 161–175.

23. Steele, G.L., Jr. Common Lisp—The Language. Digital Press, 1984.

24. Steele, G.L., Jr. and G.J. Sussman. The revised report on Scheme, a dialect of Lisp. Memo 452, MIT AI-Lab, 1978.

25. Stoughton, A. Fully Abstract Models of Programming Languages. Research Notes in Theoretical Computer Science. Piman, London. 1986.

26. Vuillemin, J. Proof techniques for recursive programs. IRIA Report. 1973.