Fully Abstract Semantics for

Observably Sequential Languages

Robert Cartwright  Pierre-Louis Curien  Matthias Felleisen

Department of Computer Science Rice University Houston, TX 77251-1892

Rice University Technical Report # 93-219 To appear in Information and Computation 1994

Fully Abstract Semantics for Observably Sequential Languages

Robert Cartwright^{∗}

Department of Computer Science, Rice University, Houston, TX 77005

Pierre-Louis Curien^{†}

Ecole Normale Supérieure, LIENS-CNRS, 45 rue d’Ulm, 75230 Paris, France

Matthias Felleisen^{‡}

Department of Computer Science, Rice University, Houston, TX 77005

Abstract

One of the major challenges in denotational semantics is the construction of a fully abstract semantics for a higher-order sequential programming language. For the past fifteen years, research on this problem has focused on developing a semantics 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 to procedures. Since we believe that these facilities play a crucial role in sequential computation, this paper focuses on a sequential extension of PCF, called SPCF, that includes two classes of control operators: a possibly empty set of error generators and a collection of catch and throw constructs. For each set of error generators, the paper presents a fully abstract semantics for SPCF. If the set of error generators is empty, the semantics interprets all procedures—including catch and throw—as Berry-Curien sequential algorithms. If the language contains error generators, procedures denote manifestly sequential functions. The manifestly sequential functions form a Scott domain that is isomorphic to a domain of decision trees, which is the natural extension of the Berry-Curien domain of sequential algorithms in the presence of errors.

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 have the same meaning (denotation). 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.

∗Supported in part by NSF grant CCR 91-22518.

†Supported in part by Esprit BRA CLICS, and a visit at DEC SRC, Palo-Alto.

‡Supported in part by NSF grants CCR 89-17022, CCR 91-22518, and a visit at Carnegie Mellon University.

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. Unfortunately, it is difficult to prove that two phrases are observationally equivalent because the proof must address all possible program contexts. Denotational equivalence is more tractable because it can be analyzed using the algebraic and topological structure of denotations.

As a result, one of the primary goals of programming language theory is the construction of denotational semantics for practical languages where denotational equivalence and observational equivalence coincide. A semantics with this property is called fully abstract.

Denotational equivalence implies observational equivalence because a denotational semantics is compositional. But the converse rarely holds for practical programming languages; some observationally equivalent phrases inevitably have different meanings. The following example shows why a conventional continuous function semantics is not fully abstract for higher-order sequential languages. Consider the 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 phrase and i denotes an arbitrary natural number. By a proof technique due to Plotkin [24], p_{i} is observationally equivalent to the procedure p defined by p(f) = Ω. In essence, the procedures p_{i} diverge for all inputs because the only possible inputs f are sequential procedures.

Nevertheless, the conventional semantics 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. The application of p_{i} to parallel-and yields the answer i instead of ⊥ because divergent subcomputations are ignored by parallel-and. Consequently, the conventional semantics for language L 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 [21, 30]. 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 [30, 29]. Indeed, all commonly used deterministic languages are sequential.

In rough terms, a language is sequential if it can be implemented without time-slicing among multiple threads of control. The technical usage of the term sequential in this paper should not be confused with the informal uses of term in the context of parallel processing. In informal usage, languages are classified as “sequential” or “parallel” based on the intended implementation strategy rather than the semantic properties of the language. In fact, practical parallel languages are either sequential in the technical sense or they are nondeterministic. Deterministic parallel languages like C*, *Lisp, and some parallel dialects of Fortran support parallelism in program execution through “data-parallel” operations or “hierarchical” parallelism where every task executed in parallel must terminate for the entire computation to terminate. The functions computable using these two forms of parallelism are sequential.

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 by a semantics.

Parallel functions like parallel-and increase the expressiveness of deterministic languages, but the price paid in execution efficiency for using these operations is exorbitant. Moreover, the additional expressiveness is not useful in practice, because it applies only to computations that are unbounded. For this reason, parallel functions have not been included in any practical language.

1.1 History of Previous Work

Milner [22], Plotkin [24], and Sazonov [26] were the first researchers to study the full abstraction problem for sequential languages. They focused on constructing a fully abstract semantics for PCF, a call-by-name functional language based on the typed λ-calculus. Plotkin and Sazonov observed that the continuous function semantics for PCF is not fully abstract using essentially the same counterexample as given above. Milner and Plotkin developed different strategies for eliminating the discrepancy between the continuous function semantics and the observable behavior of PCF.

Milner eliminated parallel functions from the semantics by constructing Scott domains from equivalence classes of observationally equivalent terms. Milner showed that his semantics is fully abstract, and that it is unique up to isomorphism among fully abstract, extensional semantics. But Milner’s construction of a semantics is not regarded as “denotational” because it fails to identify any algebraic structure within programs. Plotkin extended PCF by adding parallel deterministic operations, eliminating the discrepancy between the continuous function semantics and the procedures definable in the language. Unfortunately, neither Milner’s nor Plotkin’s result showed how to construct a fully abstract denotational semantics for a sequential language like PCF.

In a subsequent investigation of sequential languages, Berry and Curien [3, 4, 6, 8] constructed a semantics for PCF with more restrictive domains for procedure denotations. Berry introduced the stable function space construction, which eliminated many—but not all—parallel functions.^{2} To address this problem and to produce a semantic characterization of sequentiality, Berry and Curien [4, 5] proposed interpreting procedures as sequential algorithms over concrete domains [18]. Roughly speaking, a concrete domain is a domain that is isomorphic to a domain consisting of potentially infinite trees. A sequential algorithm is a continuous function plus a strategy for evaluating its arguments. While this approach eliminates all parallel functions, the resulting semantics is not extensional because it contains different sequential algorithms that compute the same function. 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 semantics for PCF is not fully abstract.

2Indeed, it even introduces new distinctions, which are impossible in the continuous function space construction. This observation is due to Jim and Meyer [16]; for details on this observation, we refer to their paper.

Berry and Curien did show, however, that the concrete domains and sequential algorithms form a Cartesian-closed category and they developed a language called CDS0 for which the sequential algorithm semantics is fully abstract. CDS0 differs from conventional functional languages like PCF because it relies on sequential algorithms—represented as decision trees—rather than PCF-like procedures as higher order data objects. Hence, higher order data objects in CDS0 are not extensional.

Mulmuley [23] generalized Milner’s work by showing how to construct a fully abstract semantics for PCF as a quotient of a conventional semantics based on lattices instead of cpos. He defined a retraction on the conventional semantics that equates all parallel functions with the “overdefined” element top (⊤). Jung and Stoughton [17] recently extended Mulmuley’s work by directly constructing a projection from the inductively reachable subalgebra of the continuous function semantics to the fully abstract semantics for PCF. However, like Milner’s original fully abstract semantics, both Mulmuley’s and Jung and Stoughton’s semantics are “syntactic” in flavor because they rely on a quotient construction based on observational equivalence and definability. For more details on the history of the full abstraction problem for sequential languages, we refer the reader to three extensive surveys [6, 9, 32].

1.2 Summary of Results

This paper integrates recent work by Cartwright and Felleisen [7] and by Curien [10] on fully abstract semantics for simple, sequential extensions of PCF. It solves an important form of the full abstraction problem, namely the construction of a fully abstract semantics for a realistic functional language extending PCF. The key insight underlying this work is the invention of a new form of function space: the domain of manifestly sequential functions. The manifestly sequential functions form a projective subspace [19] of the continuous functions—provided that the domain and codomain meet certain topological constraints.

By drawing on their intuitions as programmers, Cartwright and Felleisen [7] invented the manifestly sequential functions to construct a fully abstract denotational semantics for a sequential extension of PCF called SPCF. Curien [10] recognized that the manifestly sequential functions were an extensional refinement of the sequential algorithms that he and Berry had developed in an attempt to construct a fully abstract semantics for PCF. His paper showed that the framework of “concrete data structure” (cds) domains can easily be extended to accommodate manifestly sequential functions without invalidating any of the framework’s important properties.^{3}

This paper presents a new framework for defining the category of manifestly sequential domains and functions called sequential data structures. The paper subsumes both original presentations by the authors. In the framework of sequential data structures, manifestly sequential functions are represented as decision trees, formalized as sets of paths. Sequential data structures are similar to the concrete data structures that Berry and Curien used to define sequential algorithms, but they are simpler and make the tree structure of elements explicit.

3The term manifestly sequential was coined by the authors in the process of writing this paper. Cartwright and Felleisen [7] defined the manifestly sequential functions in the context of two error elements. They called these functions error-sensitive functions. Manifest sequentiality is a generalization of the original notion of error-sensitivity that is applicable to domains with a single error element.

The paper is organized as follows. Section 2 contains the mathematical preliminaries for the remainder of the paper. Section 3 describes the syntax and semantics of PCF. In Section 4, we compare PCF to realistic functional languages. Unlike practical functional languages (Common Lisp, Scheme), 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. Extending PCF to include these facilities naturally leads to a fully abstract semantics using manifestly sequential functions represented by decision trees. Section 5 introduces suitable domains and functions for constructing such a semantics and Section 6 contains the proof that this collection of domains and functions forms an appropriate category. Section 7 is devoted to the proof of full abstraction for SPCF. Finally, Section 8 presents an operational semantics and an adequacy theorem for SPCF. The adequacy proof uses a strong normalization argument for bounded recursion, simplifying Curien’s original proof [10]. The appendix relates the sequential data structures presented in this paper to the original concrete data structures used by Berry and Curien.

2 Mathematical Preliminaries

Before we present the syntax and semantics of PCF and SPCF, we need to introduce some definitions and notation.

Sets. We use standard mathematical notation and terminology for sets and functions. terminology. In particular, denotes the set of natural numbers. The indices i, …, n range over a (subset of) . The expression \underline{λ}x. · · · x ⋯ denotes the mathematical function f defined by the equation f(x) = ⋯ x ⋯, where the domain and codomain (range) of f are determined by context. If A and B are sets, then the equations

A \ B = {a | a ∈ A, a ∉ B}
A ⊎ B = {⟨a, 1⟩, ⟨b, 2⟩ | a ∈ A, b ∈ B}

define the set difference A \ B between A and B and the discriminated union A ⊎ B of the sets A and B.

Partial Orders and Domains. A partial order is a pair (D, ⊑) where D is a set and ⊑ is a binary relation on D that is reflexive, transitive, and antisymmetric. In contexts where no confusion can arise, we abuse notation and use the symbol D to refer to the partial order. If x ⊑ y, we say x approximates y or y dominates x. If x ⊑ y and x ≠ y, then we write x y and say x is strictly below y.

An upper bound of X ⊆ D is an element of D that dominates all elements x ∈ X. A least upper bound of X is an upper bound that approximates all other upper bounds. Since the partial order D is antisymmetric, a least upper bound of X is unique; it is denoted ⨆ X. The least upper bound of a pair x, y of elements in D is denoted x ⊔ y. The notions of lower bound and greatest lower bound are defined similarly; ⊓X is the least upper bound of X ⊆ D and x ⊓ y is the greatest lower bound of the pair x, y ∈ D. A subset X ⊆ D is bounded if it has an upper bound. If a pair x, y ∈ D is bounded, we say it is consistent and write x ↑ y. A non-empty subset X of a partial order D is directed if every pair of elements from X has an upper bound in X.

A complete partial order (cpo) is a partial order (D, ⊑) such that D has a least element ⊥ and every directed subset X of D has a least upper bound. An element y of a cpo D is finite if for every directed X ⊆ D such that y ⊑ ⨆ X, there exists an element x ∈ X such that y ⊑ x.

A cpo is flat if x ⊑ y if and only if x =⊥ or x = y. A cpo is consistently-complete if every bounded pair of elements has a least upper bound. A cpo D is algebraic if for every x ∈ D the set of finite elements below x is directed and its least upper bound is x:

x = ⨆{d ⊑ x | d is finite }.

It is ω-algebraic if it is algebraic and the set of finite elements is countable.

A function f : D ⟶ D′ for cpos (D, ⊑) and (D′, ⊑′) is continuous if it preserves limits of directed sets:

f(⨆ X) = ⨆{f(x) | x ∈ X}

for any directed set X. A function f : D_{1} ×… × D_{n} ⟶ D is strict in argument position k, 1 ≤ k ≤ n, if for all x_{1} ∈ D_{1}, …, x_{k−1} ∈ D_{k−1}, x_{k+1} ∈ D_{k+1}, …, x_{n} ∈ D_{n}:

f(x_{1},…, x_{k−1}, ⊥_{k}, x_{k+1},…, x_{n}) =⊥ .

A Scott domain (or simply domain) is an ω-algebraic, consistently-complete cpo. _{⊥} is the flat domain of natural numbers with least element ⊥.

Paths.^{4} If Σ is an arbitrary set, called the alphabet, then Σ^{∗} denotes the set of finite paths over Σ. The empty path is denoted ϵ.

Every path p ∈ Σ^{∗} can be interpreted as a partial function from to Σ that satisfies the following two conditions:

• There exists n ∈ such that p(n) is undefined.

• If p(i + 1) is defined, then p(i) is defined.

We often write p@i instead of p(i); this notation corresponds to interpreting p as a sequence of tokens

p@0 · p@1 ·. . . · p@n

where · is a separator delimiting the boundaries between tokens. The notation |p| denotes the length of a path, i.e., |p| = n + 1 if p@n is defined and p@(n + 1) is undefined. It is also convenient to identify the elements of Σ with the paths of length 1.

Σ^{∗} forms a partial order under prefix ordering ⊑ defined by the rule: q ⊑ p if q ⊆ p as partial functions. In other words, q ⊑ p when p and q satisfy the following condition: if q(n) is defined, then p(n) is defined and p(n) = q(n).

4In the literature, a path is usually called a word or a list, but the reader will see that for our purposes it is more appropriate to use the terminology “path”.

If p ∈ Σ^{∗} is a path and a a member of the alphabet, then p · a is the path that extends p with a: (p · a)@|p| = a. Similarly, a · p is the path that shifts p to the right and places a at the beginning: (a · p)@i + 1 = p@i for all i > 0 and (a · p)@0 = a. The symbol · also stands for path concatenation. Since paths over Σ are not tokens, this convention does not cause any ambiguity.

Given two subsets, Φ and Υ, of an alphabet Σ, such that Φ∪Υ = Σ, the set of alternating paths, denoted by (Φ, Υ)^{∗}, is the set of paths p in Σ^{∗} that satisfy the following conditions:

1. if p@(2n + 1) is defined, then p@(2n + 1) ∈ Υ; and

2. if p@2n is defined, then p@2n ∈ Φ.

In particular, ϵ ∈ (Φ, Υ)^{∗}. An alternating path p is called non-repetitive in Φ if it satisfies the following additional condition:

3. if p@i, p@j are in Φ and p@i = p@j then i = j.

It is non-repetitive in Υ if it satisfies the same condition relative to Υ.

Categories. A category C is 4-tuple ⟨Obj_{C}, ⟶_{C}, ∘, id_{C}⟩ where

1. Obj_{C} is a collection of objects;

2. ⟶_{C} is a family of collections A ⟶_{C} B of arrows called homsets, one for each pair of objects A, B ∈ Obj_{c};

3. ∘ is a composition operation on arrows (⋃ ⟶_{C}) such that (i) f ∘ g is an arrow in A ⟶_{C} C if f is in B ⟶_{C} C and g is in A ⟶_{C} B; and (ii) the operation is associative:

(f ∘ g) ∘ h = f ∘ (g ∘ h) ;

4. id_{C} is a collection of arrows id^{A} ∈ A ⟶_{C} A, one for each object A ∈ Obj_{C} such that id^{A} is the identity with respect to the composition operation:

id^{A} ∘ f = f ∘ id^{A} = f.

When no confusion can arise, subscripts and superscripts are dropped in the notation for categories.

An object 1 in a category C is terminal if there exists exactly one arrow 1^{A} in A ⟶ 1 for each object A. The object A_{1} × A_{2} is a product of the two objects A_{1}, A_{2} if

1. there exist arrows π_{i} in A_{1} × A_{2} ⟶ A_{i} for i = 1, 2; and

2. for any object B and any arrows f_{1} in B ⟶ A_{1}, f_{2} in B ⟶ A_{2}, there exists an arrow ⟨f_{1}, f_{2}⟩ in B ⟶ A_{1} × A_{2}, the pair of f_{1} and f_{2}, such that

π_{1} ∘ ⟨f_{1}, f_{2}⟩ = f_{1}
π_{2} ∘ ⟨f_{1}, f_{2}⟩ = f_{2}
⟨π_{1} ∘ f, π_{2} ∘ f⟩ = f .

The last equation forces the arrow ⟨f_{1}, f_{2}⟩ to be unique.

In the sequel, we will work with multiple products of the shape 1 × A_{n} ×… × A_{1}, n > 0, with corresponding arrows π_{i}^{n} ∈ 1 × A_{n} ×… × A_{1} ⟶ A_{i}, 1 ≤ i ≤ n such that:

1 × A_{n} ×… × A_{2} × A_{1} = (… (1 × A_{n}) ×…) × A_{1}
π_{i}^{n} = π_{2} ∘ \underbrace{π_{1} ∘… ∘ π_{1}}_{i−1} .

A category C is cartesian if (i) it has a terminal object and (ii) a product object for any two objects.

An object [A ⇒ B] in a cartesian category C is the exponent of the objects A and B if for any object C :

1. there is a bijection Λ from C × A ⟶ B to C ⟶ [A ⇒ B] with inverse Λ^{−1} such that for all f in C × A ⟶ B and g in C ⟶ [A ⇒ B]:

Λ^{−1}(Λ(f)) = f
Λ(Λ^{−1}(g)) = g

2. for any object D and any two arrows f in C × A ⟶ B and g in D ⟶ C:

Λ(f) ∘ g = Λ(f ∘ ⟨g ∘ π_{1}, π_{2}⟩) .

The bijection Λ is called the currying operator. The Λ-inverse of the identity arrow for the exponent object A ⇒ B is called the application arrow:

App = Λ^{−1}(id^{A⇒B}).

It is easy to show that the preceding conditions on Λ are equivalent to the following two equations:

f = Λ^{−1}(id) ∘ ⟨Λ(f) ∘ π_{1}, π_{2}⟩ = App ∘ ⟨Λ(f) ∘ π_{1}, π_{2}⟩
f = Λ(Λ^{−1}(id) ∘ ⟨f ∘ π_{1}, π_{2}⟩) = Λ(App ∘ ⟨f ∘ π_{1}, π_{2}⟩) .

A cartesian category is cartesian-closed if it has exponents for any two objects. The category Dom, consisting of (Scott) domains as objects and continuous functions as arrows, is cartesian-closed.

A cartesian-closed category is cpo-enriched if:

• the collection of arrows (homset) A ⟶ B between every two objects A and B forms a cpo with respect to a supplementary approximation ordering ⊑_{A⟶B};

• arrow composition ∘ is continuous with respect to the approximation ordering on arrows; and

• the currying constructor Λ(·) and the pairing constructor ⟨·, ·⟩ are monotonic with respect to the approximation ordering on arrows.

The continuity of function composition implies the continuity of the pairing constructor and currying operator. The category Dom is cpo-enriched.

3 PCF: Syntax and Semantics

PCF is a functional language consisting of the typed λ-calculus augmented by numerals, procedures to increment and decrement numbers, a conditional procedure, and a family of fixed-point operators. The first two subsections of this section introduce the syntax and semantics of PCF. The last subsection introduces the notions of full abstraction and sequentiality.

3.1 PCF Syntax

The set of PCF types consists of a single ground type (o), denoting the set of observable values, and an infinite collection of procedure types (σ → τ), denoting sets of procedural values.

Definition 3.1 (PCF Types) The following grammar generates the set of PCF types:^{5}

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

The meta-variables τ, τ_{1}, τ′, ν, σ,… range over PCF types; τ_{1} → τ_{2} → … → τ_{n} abbreviates τ_{1} → (τ_{2} → … → τ_{n}). It is easy to show that all types τ have the shape

τ_{1} → τ_{2} → … → τ_{n} → o

for some types τ_{1},…, τ_{n}. The arity of a type τ with shape

τ_{1} → τ_{2} → … → τ_{n} → o

is n.

An unchecked PCF phrase M is either a numeral (^{⌈}n^{⌉} for n ≥ 0), a typed variable (x^{τ}), a λ-abstraction, or one of two types of applications.

Definition 3.2 (Unchecked PCF Phrases) The following grammar generates the set of unchecked PCF phrases:

M ::= c | x | (λx.M) | (M M) | (f M)
c ::= Ω | ^{⌈}0^{⌉} | ^{⌈}1^{⌉} | …
f ::= add1 | sub1 | if0 | Y^{τ}
x ::= x^{τ} | y^{τ} | ….

The meta-variables L, M, N, L′, M′, N′, L_{1}, M_{1}, N_{1},… range over phrases.

5We follow the usual practice of using meta-variables for sets as if they were members of a set and vice versa.

As is customary in functional languages, λ-abstraction is the only binding form in PCF: λx.M binds x in M. A variable that is not bound by a surrounding λ-abstraction is free. A phrase in which all variables are bound is closed. Phrases are identified if they are interconvertible by consistent renaming of bound variables, e.g., λx.x ≡ λy.y. Thus, an assertion stating that λx.M has the property “x is not a member of some finite set of variables” means that λx.M is an appropriate member of the equivalence class. The description of the operational semantics requires the standard notion of capture-free substitution: M[N/x] denotes the substitution of all free occurrences of x in M by N . Finally, the standard syntactic conventions of the λ-calculus apply, e.g., λxyz.M abbreviates λx.(λy.(λz.M)) and (M N L) abbreviates ((M N) L).

Many important semantic properties of languages rely on notion of a context, which is a program phrase with holes. The set of contexts is generated by an extension of the grammar for unchecked PCF phrases.

Definition 3.3 (Contexts) The language of PCF contexts is generated by the grammar for the set of unchecked PCF phrases augmented by the production:

M ::= [ ]_{0} | [ ]_{1} …

where the symbol [ ]_{i}, i ∈ is called a hole.

The notation C[ ] designates an arbitrary context with a single hole [ ]. Filling all occurrences of the hole [ ] in the context C[ ] with a phrase M yields the phrase C[M] in which λ-abstractions in C may capture free variables in M . A context with m disjoint sets of holes, written:

C \underbrace{[ ],…, [ ]}_{m},

can be filled with m terms: C[M_{1},…, M_{m}].

Filling a context with a context, written as C[C′[ ]] yields another context.

A (typed) PCF phrase is an unchecked PCF phrase that also conforms to the type constraints imposed by the typed λ-calculus. Every (typed) PCF phrase M has a unique type τ. Each variable x^{σ} has type σ. Similarly, each constant c in the language has a designated type τ_{c}. Within a (typed) PCF 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.

Definition 3.4 (PCF Phrases, Programs, Program Contexts) Let M be an unchecked PCF phrase and let A be a list of typed variables, called a type environment, that contains the free variables of M . The relation “A proves that M is a PCF phrase of type τ,” written A ⊢ M : τ, is the least relation generated by the following axioms and inference rules:

A ⊢ x^{τ} : τ  A, x^{τ} ⊢ M : τ′ ; \overline{A ⊢ λx^{τ} .M : τ → τ′}  A ⊢ M : τ′ → τ; A ⊢ M′ : τ′ ; \overline{A ⊢ (MM′) : τ} A ⊢ ^{⌈}n^{⌉} : o  A ⊢ M : o ; \overline{A ⊢ (add1 M) : o}  A ⊢ M : o ; \overline{A ⊢ (sub1 M) : o} A ⊢ Ω : o A ⊢ M : o ; \overline{A ⊢ (if0 M) : o → o → o}  A ⊢ M : τ → τ ; \overline{A ⊢ (Y^{τ} M) : τ} .

If A ⊢ M : τ holds, it is called a typing for M. Since the choice of A does not affect the type inference process, we often just say M has type τ. The significance of the type environment A is explained in the definition of the semantics of PCF.

A (typed) PCF phrase is an unchecked PCF phrase that has some type τ. A PCF program is a closed PCF phrase of type o. The hole of a context C[ ] has type τ if C[x^{τ}] is a typed phrase. Given the PCF phrases M and N of type τ, a program context C[ ] for M and N is a context such that C[M] and C[N] are programs.

A PCF phrase M of type τ has arity n if τ has arity n.

The semantics of PCF phrases is easy to explain informally. Numerals denote numbers, Ω represents a diverging computation of type o, λ-abstractions denote call-by-name procedures, juxtapositions denote procedure applications, and the procedural constants add1, sub1, if0, and Y^{σ} have their usual meanings. Hence, the procedures add1 and sub1 increment and decrement their integer inputs, respectively; 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 of procedures of type σ → σ.

The following phrases frequently appear in the analysis of PCF and warrant special notation:

Ω^{o} = Ω
Ω^{σ→τ} = λx^{σ} . Ω^{τ}
Y_{0}^{σ} = λx^{σ⟶σ} . Ω^{σ}
Y_{n+1}^{σ} = λf^{σ⟶σ} . (f (Y_{n}^{σ} f)) .

The phrase Ω^{τ} is a divergent phrase of type o. The phrase Y_{i}^{σ} approximates the Y^{σ} combinator: for f of type σ → σ, Y_{i}^{σ}f is the i-fold application of f to Ω^{σ}. Roughly speaking, Y^{σ} is the least upper bound of {Y_{i}^{σ} | i ∈ }.

3.2 PCF Semantics

A denotational semantics for a language based on the typed λ-calculus assigns meaning to types and phrases by mapping them to appropriate mathematical entities. These entities form a cartesian-closed cpo-enriched category that interprets the divergent term Ω^{σ} as the least element in the corresponding domain of arrows and interprets the fixed-point combinator Y^{σ} as the least upper bound of the approximations Y_{i}^{σ}.

Definition 3.5 (Semantics for languages based on the typed λ-calculus) Let L be a language consisting of the typed λ-calculus augmented by a set of constants including the divergent constant Ω, and the Y^{σ}-combinator for each type σ. A semantics for L is determined by a triple ⟨C, C^{o}, C[[ · ]]⟩ where C is cartesian-closed cpo-enriched category, C^{o} is an object in C, and C[[ · ]] is a function mapping each constant c of type τ in L, except Y^{τ}, to an arrow in 1 ⟶ C^{τ} such that the following conditions are satisfied:

• The homset ⊥^{1⟶C^{o}} is a flat Scott domain.

• Ω is interpreted as the least element ⊥^{1⟶C^{o}} in the Scott domain 1 ⟶ C^{o}:

C[[ Ω ]] =⊥^{1⟶C^{o}} .

• For any three objects A, B and C:

Λ(⊥^{C×A⟶B}) = ⊥^{C⟶[A⇒B]}
⟨⊥^{A⟶B}, ⊥^{A⟶C}⟩ = ⊥^{A⟶B×C} .

Given C^{o}, the family of objects C^{τ} in the category C is inductively defined by the equation:

C^{σ→τ} = C^{σ} ⇒ C^{τ} .

The meaning function C[[ · ]] is extended from constants to typed phrases excluding Y^{τ} as follows. Let A ⊢ N : τ be (the conclusion of) a proof that N is a typed phrase for some type environment A = x_{n}^{τ_{n}},…, x_{1}^{τ_{1}}, n ≥ 0. Then the meaning of N is an arrow in

1 × C^{τ_{n}} ×… × C^{τ_{1}} ⟶ C^{τ}

inductively defined by the following equations:

C[[ A ⊢ c : τ ]]  = C[[ c]] ∘ 1^{1×C^{τn}×...×C^{τ_{1}}}
C[[ A ⊢ x_{i}^{τ} : τ ]]  = π_{i}^{n}
C[[ A ⊢ λx^{τ} . M : τ′]] = Λ(C[[ A, x^{τ} ⊢ M : τ′]])  x^{τ} is not in A
C[[ A ⊢ (M_{1} M_{2}) : τ′]] = App ∘ ⟨C[[ A ⊢ M_{1} : τ → τ′]] , C[[ A ⊢ M_{2} : τ ]]⟩ .

The type environment A plays a crucial role in the extension of C[[ · ]] to typed phrases containing free variables, because it determines which projection function is used to select each variable x_{i}^{τ}.

Given the meaning function C[[ · ]] for typed phrases excluding Y^{τ}, let the extension of C[[ · ]] to Y^{τ} be defined by:

C[[ A ⊢ Y^{τ} : (τ → τ) → τ ]] = ⨆ {C[[ A ⊢ Y_{n}^{τ} : (τ → τ) → τ ]] | n ∈ } .

For the sake of notational economy, we refer to the semantics determined by the triple ⟨C, C^{o}, C[[ · ]]⟩ simply by the symbol C. For closed typed terms M, we often abbreviate C[[ A ⊢ M : τ ]] by C[[ A ⊢ M ]] or by C[[ ⊢ M ]], since the type of M can be reconstructed from the types of the constants that appear in M.

The semantics of a program P is C[[ ⊢ P ]], an arrow in 1 ⟶ C^{o}.

A semantics validates the (β) and (fix) axioms of the typed λ-calculus with Y as well as its inference rules [8].

Lemma 3.6 Let C be a semantics for PCF. Then for all PCF phrases M and N , contexts C[ ] , appropriate type environments A, and variables x^{τ}:

C[[ A ⊢ C[((λx^{τ} . M) N)] ]] = C[[ A ⊢ C[M[N/x^{τ}]] ]]

and

C[[ A ⊢ C[(Y M)] ]] = C[[ A ⊢ C[(M (YM))] ]] .

The conventional semantics for PCF based on continuous functions is an instance of the general definition. It is based on the cpo-enriched category Dom whose objects are Scott domains and whose arrow sets A ⟶ B are the sets of continuous functions from domain A to domain B.

Definition 3.7 (Dom Semantics of PCF, Adequate Semantics, PCF-like Languages) The cpo-enriched cartesian-closed category of the conventional semantics for PCF is Dom. The ground type o is interpreted as _{⊥}:

Dom^{o} = _{⊥}.

The semantics assigns the following meaning to constants:

Dom[[ Ω^{o}]] = \underline{λ}ρ : 1 . ⊥
Dom[[^{⌈}n^{⌉}]] = \underline{λ}ρ : 1 . n

Dom[[ add1 ]] = \underline{λ}ρ : 1 . \underline{λ}m . \{ \begin{matrix}m + 1 & m ∈ \\ ⊥ & m = ⊥ \end{matrix}

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

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

where 1 in Dom is the trivial, one-element domain.

A semantics for PCF that assigns the same meaning as the Dom semantics to the ground type o and to all PCF programs is called adequate.

For any language L based on typed λ-calculus that extends PCF (differs from PCF only by extending the set of constants), a semantics for L is PCF-like if it assigns a flat super-domain of _{⊥} to the base type and the same meaning as the Dom semantics to PCF programs.

3.3 Full Abstraction and Sequentiality

Given the preceding definition of a PCF-like language, we are finally ready to give a rigorous definition of denotational and observational equivalence, the two equivalence relations on typed phrases discussed at the beginning of the paper.

Definition 3.8 (Denotational and Observational Equivalence and Approximation, Full Abstraction) In a PCF-like programming language with semantics C, let M and M′ be phrases that have the same type (i.e., A ⊢ M : τ and A ⊢ M′ : τ for some list of typed variables A). Then

• M denotationally approximates M′, written M ⊑ M′ if

C[[ A ⊢ M : τ ]] ⊑ C[[ A ⊢ M′ : τ ]].

• M is denotationally equivalent to M′, written M ≡ M′, if

C[[ A ⊢ M : τ ]] = C[[ A ⊢ M′ : τ ]].

• M observationally approximates M′, written M ∼ M′, if C assigns approximating meanings to the programs C[M] and C[M′] for all program contexts C[ ] for M and M′:

C[[ ⊢ C[M] ]] ⊑ C[[ ⊢ C[M′] ]] .

• M is observationally equivalent to M′, written M ≃ M′, if C assigns the same meaning to the programs C[M] and C[M′] for all program contexts C[ ] for M and M′:

C[[ ⊢ C[M] ]] = C[[ ⊢ C[M′] ]].

A semantics C is (equationally) fully abstract if for all pairs of typed phrases M and M′ of the same type, M ≃ M′ iff M ≡ M′; it is inequationally fully abstract if the proposition also holds for approximations: M ∼ M′ iff M ⊑ M′.

In the presence of two different semantics C and C′ for a language, we attach identifying subscripts to the denotational equivalence and approximation relations, e.g., ≡_{C}, ⊑_{C′}.

Denotational and observational equivalence are different in character. While the former relation depends on the choice of the semantics, the latter does not as long as the semantics is adequate. More precisely, if C′ is an adequate semantics for PCF distinct from C, it still determines the same observational equivalence relation ≃ but possibly a different denotational equivalence relation. The two relations are distinct in the Dom semantics of PCF.

The lack of full abstraction for the Dom semantics of PCF is due to the presence of parallel functions in the domain of continuous functions, e.g., parallel-and. Yet, PCF can only define sequential functions, which evaluate their arguments in some specified order and diverge when they begin to evaluate a diverging argument. The procedures p_{i} defined in the introduction exploit this discrepancy: they behave differently only on inputs that are not sequential. Hence they are denotationally distinct and observationally equivalent.

Finally, we can precisely define what it means for the language to be sequential.

Definition 3.9 (Sequential Language) A PCF-like language with semantics C is sequential if the following condition holds. Let C be a context with k holes of ground type and no free variables and M_{1},…, M_{k} be closed phrases such that C[[ C[M_{1},…, M_{k}] ]] ≠⊥ and C[[ C[Ω,…, Ω] ]] =⊥. Then there exists j ∈ , 1 ≤ j ≤ k, called a (syntactic) sequentiality index of C, such that

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

for all phrases M′_{i} (of correct type).

This definition is based on Vuillemin’s definition [33] of sequentiality for first-order functions. Plotkin [24:Activity Lemma] and Berry [6:Theorem 3.6.4] proved that PCF is sequential, using an adequate^{6} operational semantics for PCF. Plotkin’s proof is direct, while Berry’s proof is obtained as a corollary of a general syntactic sequentiality theorem [2, 6 : Theorem 3.6.2, 1 : Theorem 14.4.8].

We conclude the section with two useful examples of PCF procedures. The following two equations specify two versions of the binary addition procedure:

+_{l} = Y(λf^{o→o→o} . (λxy . if0 x y (add1 (f (sub1 x) y))))
+_{r} = Y(λf^{o→o→o} . (λ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 Dom semantics of PCF, these two procedures denote exactly the same function, namely, binary addition. However, the two procedures clearly employ distinct strategies to inspect their arguments. Although this difference is not observable in PCF, it is observable in many practical languages. In the context of PCF, these two procedures can be distinguished only by inspecting the program text. But in more practical languages, control operators can be used to determine the evaluation order of procedures without inspecting their text. The next section focuses on the conflict between PCF and more practical languages.

4 Observing Sequentiality

As a pedagogic language, PCF lacks several constructs that are essential in practice. For example, PCF does not have any provision for generating run-time errors or handling exceptions. Although this design choice simplifies the definition of the language, we believe that it has diverted people from discovering fully abstract semantics for simple, sequential extensions of PCF. In the following subsections, we explain why the addition of two simple control mechanisms to PCF is important from the perspective of language design and how their presence facilitates the construction of a fully abstract semantics.

6An operational semantics of a PCF-like language is adequate if the evaluator diverges on a program precisely when the program denotes bottom (see Definition 3.7).

4.1 Using Errors, Programmers Can Observe the Order of Evaluation

Since PCF excludes negative numbers, the predecessor operation for numbers diverges when applied to zero. While this design decision avoids the complication of generating and propagating error values in the semantics, it withholds important information from the programmer that is readily available in real implementations. A programmer who mistakenly tries to take the predecessor of zero would like to be informed of this fact instead of seeing his program diverge for the sake of a “simpler” semantics. The inclusion of error values in the language has a dramatic impact on the underlying semantics because it permits programmers to observe the evaluation order of subexpressions in programs by conducting simple experiments.

To report run-time errors in PCF, we can add error constants, e_{1}, e_{2},…, e_{n}, n > 1, of ground type to the language and demand that all procedures in the extended language be manifestly sequential. An operation is manifestly sequential if it propagates any errors that it encounters in evaluating its arguments. In PCF with errors, a programmer can observe the evaluation order among subexpressions by exploiting the manifest sequentiality of all program operations. Specifically, let C[M_{1},…, M_{m}] be a terminating PCF program such that C[Ω,…, Ω] diverges. To find out which of the m distinguished subexpressions is evaluated first, the programmer can evaluate the expression C[e_{1},…, e_{m}] assuming m errors are available. The result e_{i} indicates which expression M_{i} was evaluated first. The same observation can be made with only two errors at the cost of conducting m experiments. Experiment i replaces M_{j} for j ≠ i by e_{1} and M_{i} by e_{2}. The index of the experiment that yields the answer e_{2} identifies which subexpression is evaluated first.

Using this form of experimentation, a programmer can distinguish procedures that denote the same function over _{⊥} such as the addition procedures +_{l} and +_{r} defined in Section 3. The expression (+_{l} e_{1} e_{2}) produces e_{1} because +_{l} evaluates its left argument first; (+_{r} e_{1} e_{2}) returns e_{2} because +_{r} evaluates its right argument first.

4.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 exploit the order of evaluation among the arguments in a procedure application. Since knowledge of the evaluation order can lead to shorter, more expressive, and faster programs, many practical languages include a non-local control operator that can propagate ordinary data values along the evaluation path that an error value would take.

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

(Catch e (add1 (e ^{⌈}0^{⌉})))

returns ^{⌈}0^{⌉} by popping the control stack back through the lexical binding of e in the form (Catch e …) after encountering the subexpression (e ^{⌈}0^{⌉}). With such a Catch construct, a procedure that multiplies the elements of a list of numbers can escape from the recursive traversal of the list if it determines that the list contains ^{⌈}0^{⌉}; see Figure 1 for the code.

product = (λl . (Catch e (Y(λπ . (λl . (if0 (null? l) ^{⌈}1^{⌉} (if0 (car l) (e ^{⌈}0^{⌉}) (∗ (car l) (π (cdr l))))))) l)))

Figure 1: The Function product in PCF with Lists

More importantly for our purposes, a program can use Catch to determine the order of evaluation of a procedure’s arguments. For example, the procedure

G = (λf . (Catch x (f (x ^{⌈}0^{⌉}) (x ^{⌈}1^{⌉}))))

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

To equip PCF with non-local control, we add a family of procedures catch^{τ} of type τ → o to PCF where τ = τ_{1} → … τ_{k} → o. If f is a procedure of type τ, then (catch^{τ} f) returns ^{⌈}i − 1^{⌉} if f evaluates the ith argument first and returns ^{⌈}k + n^{⌉} if f is a constant procedure with result ^{⌈}k^{⌉}. Equivalently, (catch^{τ} f) is ^{⌈}i − 1^{⌉} if

(f \underbrace{Ω … Ω}_{i−1} e_{j} \underbrace{Ω … Ω}_{k−i})

returns e_{j} for j = 1, 2. If τ = o, catch^{τ} is degenerate: it always returns the value of its argument (^{⌈}k^{⌉}).

In the context of PCF, the family of catch procedures has the same expressive power as Scheme’s Catch construct [7:39–40], which is equivalent to call/cc restricted to continuations of type o → τ for some τ. We use the catch procedures in our extension of PCF because the catch procedures have a simpler definition and they facilitate proving the representability lemma (see Section 7). We designate our sequential extension of PCF by the name SPCF.

Definition 4.1 (SPCF ) Let be a set of error constants. The language SPCF( ) is PCF augmented by the set of constants ∪ {catch^{τ} }:

c ::= e  (e ∈ )
f ::= catch^{τ} .

The typing rules for the new constants are

A ⊢ e : o for all constants e ∈ A ⊢ catch^{τ} : τ → o

SPCF is an abbreviation for SPCF( ) when the set of error constants can be deduced from context.

Since the behavior of the procedure catch^{τ} depends only on the arity (see Definition 3.1) of the type τ, it suffices to decorate catch with the arity k instead of its complete type. We will frequently exchange the type superscript τ in favor of its arity k, using catch^{k} to denote any procedure catch^{τ} where τ has the form (τ_{1} → … τ_{k} → o).

4.3 Observably Sequential Programming Languages

Once we accept the idea that PCF should be extended to include error values and control operators like catch, we need to identify the technical properties that distinguish the extension from PCF. To this end, we introduce the notions of manifest sequentiality and observable sequentiality.

Definition 4.2 (Manifestly Sequential and Observably Sequential Languages) A sequential PCF-like language L (see Definition 3.7) with semantics C is manifestly sequential^{7} if there exists a non-empty set of error elements ⊆ C^{o} \ {⊥} denoted by a corresponding set of closed expressions L_{}such that for any context C[ ]_{1} … [ ]_{k} with sequentiality index j and any E ∈ L_{},

C[[ ⊢ C[M′_{1},…, M′_{j−1}, E, M′_{j+1},…, M′_{k}] ]] = C[[ ⊢ E]] .

A sequential PCF-like language L is observably sequential if for any context C[ ]_{1} … [ ]_{k} with sequentiality index j, j is unique and there exists a program context D[ ] such that

C[[ ⊢ D[λx_{1} … x_{k}.C[x_{1},…, x_{k}]] ]] = C[[ ⊢ ^{⌈}j^{⌉}]] .

SPCF is observably sequential and manifestly sequential (provided that is non-empty). We will prove this fact after we define the semantics of SPCF in Section 7 (Theorem 7.5).

4.4 Procedure Denotations Have Explicit Computational Structure

Conventional semantic definitions for languages like SPCF rely on passing continuations, which are functions representing control contexts. In a continuation-passing semantics, the meaning of a phrase is a functions of it free variables and its control context. In essence, the function denoted by a phrase takes a “hidden” argument not manifest in the program syntax, namely a continuation representing the control context. In a continuation semantics, control operators like Catch are interpreted as functions that “grab” the continuation argument and pass it to other higher order arguments. For sequential languages, continuation-passing semantics are not fully abstract because they rely on continuous function spaces containing parallel functions (as well as control delimiters) [30]. Consequently, to construct a fully abstract semantics for SPCF, we must devise a more restrictive collection of domains that exclude parallel functions. The domains used in continuation semantics contain too many elements.

7If contains at least two elements, a weaker property of languages called error-sensitivity is equivalent to manifest sequentiality. A PCF-like language L with semantics C is error-sensitive if there exists a nonempty set of error elements ⊆ C^{o} denoted by a corresponding set of closed expressions L_{}such that if ⊥= C[[ ⊢ C[Ω] ]] C[[ ⊢ C[M] ]] for any M then for all E ∈ L_{}, C[[ ⊢ C[E] ]] = C[[ ⊢ E]]. In the presence of at least two errors, error-sensitivity implies sequentiality. We use the stronger notion of manifest sequentiality in this paper to address the case where there is only one element.

The informal operational semantics of SPCF, notably the behavior of the catch^{k} operators, 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^{⌉})).  (1)

It has type o → (o → (o → (o → o))), i.e., it is 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.

By supplying error values as arguments, a programmer can determine the schedule that p uses to evaluate its arguments. The results of these experiments can be expressed in the form of equations as follows:

(p Ω  e_{i}  Ω Ω) = e_{i}
(p Ω ^{⌈}0^{⌉} e_{i} Ω) = e_{i}
(p Ω ^{⌈}n + 1^{⌉} Ω e_{i}) = e_{i}.

The equations demonstrate that p evaluates its arguments in a specific order and that the graph of the function denoted by p contains the schedule information.

The presence of error elements forces a function to follow a unique schedule. In the presence of errors, no function is strict in more than one piece of accessible, unexplored information. Consequently, we can represent functions by decision-trees (schedules) without sacrificing extensionality! For example, p can be represented 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 is 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}⊥↦⊥ \\ e_{1} ↦ e_{1} \\ … \\ 0 ↦ ⟨3, \{ \begin{matrix}⊥↦⊥ \\ e_{1} ↦ e_{1} \\ … \\ 0 ↦ 1 \\ 1 ↦ 2 \\ … \end{matrix} ⟩ \\ 1 ↦ ⟨4, \{ \begin{matrix}⊥↦⊥ \\ e_{1} ↦ e_{1} \\ … \\ 0 ↦⊥ \\ 1 ↦⊥ \\ 2 ↦ 0 \\ 3 ↦ 1 \\ … \end{matrix} ⟩ \\ … \end{matrix} ⟩

Since p must be manifestly sequential, its branching functions map ⊥ to ⊥ and e_{i} to e_{i}.

Rotating the preceding picture produces a tree with decision points as internal nodes and alternative outcomes as branches:

[figure: ?_{2}; 0; 1; 2; …; ?_{3}; 1; 0; 2; 1; 3; 2; …; ?_{4}; ⊥; 0; ⊥; 1; 0; 2; …]

For readability, each argument index i has been replaced by the symbol ?_{i} in the rotated picture. A node with the label ?_{i} represents the querying of the ith argument. This notation emphasizes that the respective indices are queries about an argument; it will be generalized in the next subsection to a representation where procedures can play the role of arguments. The edges below a node with label ?_{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 ∪ {⊥, e_{1},…}), then p has completed its computation; otherwise, it continues to query its argument(s).

The most important property of these trees is that they are extensional when the set of errors is non-empty. Every manifestly sequential function has a unique decision-tree representation.

4.5 Higher-order Procedures Explore and Output Trees Sequentially

Given that we want procedures to denote decision trees, our next task is to 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. Like a Lisp procedure, a higher-order procedure can inspect a node in an input tree only after inspecting its predecessors. We express queries about procedural inputs as patterns that identify nodes in decision trees. Thus, a query is a pair consisting of a path-pattern and an argument index. A path-pattern 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.^{8} If g is the actual argument under inspection, the response to a query is the label of the specified node in g.

The crucial semantic restriction on the process is that it is sequential and propagates error values: it cannot ignore infinite loops or errors in inputs. If computing an output node requires inspecting an input node that is ⊥ or e_{i}, the computed output node must be ⊥ or e_{i}, respectively.

To illustrate what happens when a function explores a higher order input (a tree), let us examine the behavior of the procedure

F = λg.(add1 (g Ω ^{⌈}0^{⌉} ^{⌈}2^{⌉} e_{1})) : (o → o → o → o → o) → o.

Since this procedure has only one argument, all the queries in the denotation of F have the form ⟨Q, 1⟩. When (the denotation of) 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, F ’s initial query is Q_{1} =? to determine the root of g. If the value of g is the procedure p described in the preceding subsection, g answers this question with the response ?_{2}, which is just the label of the root of p. Now F knows that g initially demands information about its second argument. To find out more about g, the procedure 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 ⟨Q_{2}, 1⟩ where

[figure: Q_{2} =; ?_{2}; 0; ?]

As with Q_{1}, Q_{2} is a pattern identifying the node of g that F wants to inspect; it lies just below the root of g on the edge labeled 0. Matching the pattern Q_{2} against p yields the label ?_{3}, which is a query about p’s third argument. Thus, as long as the input demands more information about its arguments, its responses will simply answer the queries (about g) with queries (about the arguments of g).

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

8According to this convention, the queries ?_{1}, ?_{2}, … should be written as ⟨1,?⟩, ⟨2,?⟩, …, respectively.

To make our examples more readable, we elected to use the more compact notation ?_{i} instead of ⟨i,?⟩.

[figure: Q_{3} =; ?_{2}; 0; ?_{3}; ?; 2]

Matching this pattern against p yields the leaf value 3, which is the final answer of p along this path. This response from p completes the subcomputation (g Ω 0 2 e_{1}). F subsequently adds 1 to the result of the subcomputation, yielding the final answer 4.

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

Figure 2: A Fragment of Procedure F

If F were a black box, a programmer could determine the schedule for F by applying F to error-laden arguments. A portion of the schedule for F (which is infinite), including the cases discussed above, is captured by the following equations:

(F (λwxyz . e_{1}))  = e_{1}
(F (λwxyz . e_{2}))  = e_{2}
(F (λwxyz . (if0 x e_{1} e_{2}))  = e_{1}
(F (λwxyz . (if0 x (if0 (sub1 (sub1 y)) e_{1} e_{2}) e_{3})) = e_{1}
(F (λwxyz . (if0 x (if0 (sub1 (sub1 y)) 3 e_{2}) e_{3})) = 4
(F (λwxyz . (if0 z e_{1} e_{2})))  = e_{1}
(F (λwxyz . (if0 z e_{2} e_{3})))  = e_{1}

The last pair of experiments shows that F produces the constant output e_{1} for a procedure argument that is strict in its fourth position. It also shows why it is necessary in some cases to repeat an experiment using different errors.

In a domain of decision trees representing schedules, we must be able to represent the schedule for F by a tree with queries to inputs as internal nodes, final answers as leaves, and possible answers from inputs as edges. Figure 2 shows the portion of tree denoted by F , captured in the equations above. It also includes a leaf showing that F diverges if its procedure argument g immediately demands its fourth argument. The other branches in the tree representing F have been omitted.

Finally, 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]

As we will see in Section 6 below, the catch procedure denotes a similar tree or manifestly sequential function.

4.6 SPCF Defines Manifestly Sequential Functions

In summary, the analysis of PCF from the perspective of language design shows that adding control operators to PCF produces a more general form of computation in which functions have a natural representation as decision trees. Moreover, if the domain of computation includes error elements, the decision tree representation is extensional. The remainder of the paper is devoted to constructing a fully abstract semantics for the family of languages SPCF( ), which extend PCF by the control operators catch^{τ} and the error elements .

This work expands and generalizes the work by Berry and Curien [4] on semantics for sequential languages based on sequential algorithms over concrete data structures. The next section presents a new framework derived from concrete data structures—called sequential data structures—suitable for defining both Berry and Curien’s sequential algorithms and our manifestly sequential functions. This construction yields a cartesian-closed category of manifestly sequential domains and manifestly sequential functions, which forms the basis for defining fully abstract semantics for the languages SPCF( ).

5 Sequential Data Structures with Errors

The definition of a suitable semantics for SPCF presumes the existence of a category of domains where the arrows are functions represented by decision-trees as described in the preceding section. In denotational semantics, domains are usually constructed as the ideal completions of finitary bases. The completion process adds infinite elements as limit points for directed sets of finite elements[27]. Our construction of domains of trees follows the same general pattern, but relies on smaller bases consisting exclusively of prime elements.^{9} This construction is less general than the usual one, but it yields a simpler representation for domain elements in terms of the original basis.

To formulate decision trees as a Scott domain, we need to identify the finite pieces of information used to build decision trees. For reasons that will become clear later, we have elected to represent trees as sets of paths. Each path consists of an alternating sequence of addresses and data items. Every path begins with an address.^{10} Each address on a path identifies which son below the current tree node is being selected. A tree is a set of paths ending in data items that satisfies two constraints. First, the set is closed under the prefix ordering on paths ending in data items. Second, all common prefixes between paths end in data items. Hence, the first point of disagreement between any two incomparable paths is an address.

9Kanneganti, Cartwright, and Felleisen [19] developed an alternate characterization of the same categorical framework using a topological formulation of the function space construction.

A framework of addresses, data items, and paths governing the construction of trees is called a sequential data structure. We will subsequently show that the set of trees determined by a sequential data structure form a Scott domain.

Definition 5.1 (Sequential Data Structure, Path, Query, Response) A sequential data structure (sds) M is a 3-tuple (A, D, P) consisting of three countable sets:

• a set A of addresses;

• a set D of data; and

• a prefix-closed set P of non-empty, alternating paths in (A,D)*, i.e.,

1. P ⊆ (A, D)^{∗} (see Section 2 (Paths));

2. ϵ ∉ P;

3. (prefix-closure) if p ∈ P, p′ ∈ (A, D)^{∗}, p′ ≠ ϵ, and p′ ⊑ p (where ⊑ is the prefix-ordering on paths) implies p′ ∈ P.

A path ending in an address is also called query, and a path ending in a datum is called response; Que_{M} and Res_{M} denote the sets of queries and responses for a sequential data structure M, respectively.

A simple example that illustrates the concept of an sds is the following structure, which generates the natural numbers as “trees”:

N = ({?}, , {?, ? · n | n ∈ }).

N uses a single address, ?. At this address a path of N contains a single number, if it contains any datum at all. Similarly, an sds T for truth values has the following definition:

T = ({?}, {tt, ff }, {?,? · tt,? · ff }).

A slightly more interesting example is the sds N × T, which represents the cartesian product of N and T:

N × T = ({?_{1},?_{2}}, ∪ {tt, ff }, {?_{1},?_{2},?_{1} · n,?_{2} · tt,?_{2} · ff | n ∈ }).

Depending on the first address, a path in N × T indicates the presence of a truth value or the presence of a number in a pair. Since a path contains exactly one address and since one address is associated with truth values and the other with numbers, a path never represents a complete pair but one of the two components. In contrast, the following sds N ⊗ T is the basis for the strict product of the two sds’s:

10To construct a cartesian-closed category, we must construct a collection of objects that is closed under cartesian products. Hence, we need to construct a domain of tuples of decision trees, which are forests. Par abus de langage we continue to speak of trees.

N ⊗ T = ({?}, × {tt, ff }, {?,? · (n, tt),? · (n, ff ) | n ∈ }).

Here a path has an address for a pair of data components, namely, a truth value and a number.

As a last example, consider the sds N^{4} → N whose trees are the denotations of procedures of type o → o → o → o → o like the procedure p defined in equation (1). In general such a procedure may just output a result or it may inspect its input. In the first case, the procedure’s representation is basically a single datum (n ∈ ) but, to formulate this description as an sds-path, it is prefixed with an address (?). Intuitively, a path of the shape ? · n represents a procedure that “fills” the only output address (?) with a natural number (n). In the second case, the procedure’s paths must include a strategy for exploring the arguments. A straightforward representation of a strategy is a series of query-response pairs, where the query indicates which part of the argument is inspected and the response indicates the anticipated response. In the sds N^{4} → N, the argument is a four-tuple of numbers and hence provides four possible choices for inspection, all of which have numbers as the only possible responses. The symbols ?_{1},?_{2},?_{3}, and ?_{4} denote queries and numbers specify responses.

The representation of a non-constant procedure is a set of paths that all start with the address ?. Each path describes a strategy for exploring the input addresses ?_{1},?_{2},?_{3}, and ?_{4}, which are data items in the representation of the procedure. The path returns an “answer” in when it has gathered sufficient information about the contents of the input addresses. The paths are identical to the paths in the tree representation for p sketched in Subsection 4.4, except that they are preceded by the address ?. Thus, some paths in the denotation of the procedure p are ?·?_{2} · 0·?_{3} · 1 · 2 and ?·?_{2} · 1·?_{4} · 2 · 0.

The formal specification of the sds N^{4} → N = (A_{→}, D_{→}, P_{→}) for representations of procedures like p is as follows:

A_{→} = {?} ∪
D_{→} = {?_{1},?_{2},?_{3},?_{4}} ∪

P_{→} = \{ \begin{matrix}?, \\ ? · n, \\ ?·?_{i_{1}}, \\ ?·?_{i_{1}} · n_{1}, \\ ?·?_{i_{1}} · n_{1} · n, \\ ?·?_{i_{1}} · n_{1}·?_{i_{2}}, \\ ?·?_{i_{1}} · n_{1}·?_{i_{2}} · n_{2}, \\ ?·?_{i_{1}} · n_{1}·?_{i_{2}} · n_{2} · n, \\ ?·?_{i_{1}} · n_{1}·?_{i_{2}} · n_{2}·?_{i_{3}}, \\ ?·?_{i_{1}} · n_{1}·?_{i_{2}} · n_{2}·?_{i_{3}} · n_{3}, \\ ?·?_{i_{1}} · n_{1}·?_{i_{2}} · n_{2}·?_{i_{3}} · n_{3} · n, \\ ?·?_{i_{1}} · n_{1}·?_{i_{2}} · n_{2}·?_{i_{3}} · n_{3}·?_{i_{4}}, \\ ?·?_{i_{1}} · n_{1}·?_{i_{2}} · n_{2}·?_{i_{3}} · n_{3}·?_{i_{4}} · n \end{matrix} |  \begin{matrix}n, n_{1}, n_{2}, n_{3}, n_{4} ∈ , \\ \{i_{1}, i_{2}, i_{3}, i_{4}\} = \{1, 2, 3, 4\} \end{matrix} \}

Equivalently, a path is a member of the context-free language (specified in extended BNF):

p ::= r | q
r ::= ? · [?_{i} · n]^{∗} · m | ? · [?_{i} · n]^{∗}·?_{j}
q ::= ? · [?_{i} · n]^{∗}

where m, n ∈ , i, j ∈ {1, 2, 3, 4} and no address (?,?_{i}) occurs more than once in a path.

The formal definition of N^{4} → N also clarifies how a query of the sds N becomes a datum in the specification of a procedure space, and, conversely, how a datum in N becomes an address in the procedure space.

Given the preceding definition of sds’s, we can restate our informal definition of a tree as follows. A tree is a set of responses such that all the response predecessors of a response are included and such that all non-empty intersections of elements are responses (and hence included). In the domain of trees determined by an sds, the finite elements are precisely the finite trees, including the empty one.

To accommodate error values in computations involving trees, we need to include error elements in the domain of trees determined by an sds. The following definition formalizes the definition of trees and tree domains that possibly contain error values.

Definition 5.2 ((Manifestly) Sequential Domain, Tree) Let M = (A, D, P) be an sds, and let

= {e_{1}, e_{2},…}

be a possibly empty set of error values, or errors for short, disjoint from D. An error response is a path r = q · e consisting of a query q ∈ Que_{M} extended with an element e ∈ . Since ∩ D = ∅, error responses and responses are disjoint. An observable response r is either a response or an error response:

ResM^{e} = Res_{M} ∪ {q : e | q ∈ Que_{M}, e ∈ }.

A tree x over M relative to is a set of observable responses closed under the prefix ordering and greatest lower bounds:

prefix-closed: x ⊆ ResM^{e} such that if r ∈ x and r′ ⊑ r for some r′ ∈ Res_{M}, then r′ ∈ x;

glb-closed: if r, r′ ∈ x, then r ⊓ r′ = ϵ or r ⊓ r′ ∈ ResM^{e} (and, by prefix-closure, is therefore in x).

A tree that does not contain error responses is called error-free. The set of trees over M relative to is denoted by (M), and is ordered by set-inclusion. A partial order that is isomorphic to (M) for some M is called the sequential domain generated by M. _{0}(M) is the set of finite sets of paths (finite trees). We call these domains manifestly sequential if the underlying set of errors is non-empty.

Convention The symbol ⊥ is used interchangeably with ∅ for the least element in domains.

To provide some intuition about sequential domains, let us describe the domains generated by the example sds’s presented earlier in this section. Unless noted otherwise, this discussion of examples assumes that the set of errors is empty.

The domain (N) generated by N has as its universe the set {⊥, {? · n} | n ∈ }. It is clearly isomorphic to the flat domain _{⊥} of natural numbers. If the set of errors is nonempty, (N) contains all the error elements, which are incomparable to numbers and each other but dominate bottom. The composite symbol _{⊥}^{e} denotes the domain generated by N when errors are present.

The domain (T) is flat like (N); it is isomorphic to _{⊥}, the flat domain of truth values. Again, if there are errors, each of them dominates ⊥ and is incomparable to all other elements.

The domain (N × T) consists of the set

{⊥, {?_{1} · n}, {?_{2} · t}, {?_{1} · n,?_{2} · t} | n ∈ , t ∈ {tt, ff }}

under the relation ⊆. It is isomorphic to the cartesian product domain _{⊥} × _{⊥}. This example illustrates how independent information appears on distinct paths in a tree and how a missing path in a tree signifies lack of information (bottom). Consider the trees {?_{1} · 1,?_{2} · tt} and {?_{2} · tt}; the former represents the pair (1, tt) and the latter corresponds to the pair (⊥, tt).

The domain (N ⊗ T) over the sds N ⊗ T is clearly isomorphic to the strict product domain _{⊥} ⊗ _{⊥}. The elements of (N ⊗ T) are {⊥, {? · (n, t)} | n ∈ , t ∈ {tt, ff }}. In other words, every element of (N ⊗ T) other than ⊥ is the single query ? followed by a pair (n, t) where n ∈ and and t ∈ {tt, ff}.

In the absence of errors, the domain (N^{4} → N) does not correspond to a standard function domain construction. It is isomorphic to Berry and Curien’s domain of sequential algorithms [8:ch. 2]. As we have already pointed out, sets of paths in N^{4} → N are most easily understood as trees (technically forests). Unlike the trees of the preceding examples whose maximal depth was two, the elements of (N^{4} → N) may be up to ten levels deep. Two examples of error-free trees over this structure are

Π_{l}^{1} = {?·?_{1},?·?_{1} · n · n | n ∈ }
Π_{s}^{1} = {?·?_{1}}

Both “algorithms” attempt to provide a datum for their single output address ? and, for this purpose, inspect the first component of their argument. The first algorithm returns the response it gets for its query and thus computes the projection function of four-tuples for the first position. The second one is an approximation to the first: it diverges after the inspection of the argument yields an error-free response. These examples serve to illustrate some concepts in the following discussion. While (N^{4} → N) is not isomorphic to a traditional domain construction, it is nevertheless a Scott domain as are all domains over an sds.

Proposition 5.3 The (observably) sequential domain (M) over an sds M is a Scott domain; the corresponding set of finite trees _{0}(M) comprises the finite elements of (M).

Proof. It is easy to verify that the union of a bounded set of trees is a tree, that is, that the union is also prefix- and glb-closed. Hence, the proof of the proposition is a variation of the proof for the standard meta-theorem on ideal constructions [27].

After establishing what the domains for the semantics of SPCF are, we turn to functions between domains. Specifically, we must formalize the notion of a manifestly sequential function, which we sketched in the previous section. We begin by introducing some auxiliary terminology and notation.

Definition 5.4 (Open and Answered Query) Let M = (A, D, P) be an sds. Given a tree x in the domain (M), a query q ∈ Que_{M} is:

• answered in x, written q ∈ Answered(x), if q ⊑ r for some r ∈ x;

• open in x, written q ∈ Open(x), if q is not answered in x and q = r · a, for some r ∈ x and a ∈ A.

To illustrate this terminology, consider the domain elements Π_{l}^{1}, Π_{s}^{1} in (N^{4} → N):

Open(Π_{l}^{1}) = ∅  Answered(Π_{l}^{1})  = {?,?·?_{1} · n | n ∈ }
Open(Π_{s}^{1}) = {?·?_{1} · n | n ∈ } Answered(Π_{s}^{1})  = {?}.

Next we turn to the definition of the sequential and manifestly sequential functions between domains determined by sds’s. Our definitions of these terms are motivated by constraints on the meaning of contexts imposed by sequential and manifestly sequential languages.

Definition 5.5 (Sequential and Manifestly Sequential Functions) Let M_{1}, M_{2} be sds’s and let (M_{1}), (M_{2}) be the corresponding domains relative to an error set . A function f : (M_{1}) ⟶ (M_{2}) is:

• monotonic if x ⊑ y implies f(x) ⊑ f(y);

• continuous if r ∈ f(x) implies r ∈ f(y) for some finite y ⊑ x.^{11}

A monotonic, continuous function f : (M_{1}) ⟶ (M_{2}) is:

• sequential if q′ ∈ Open(f(x)) and q′ ∈ Answered(f(z)) for some finite z ⊒ x implies that there exists q ∈ Open(x), called a sequentiality index of f at (x, q′), such that for all y ⊒ x, q′ ∈ Answered(f(y)) implies q ∈ Answered(y); • manifestly sequential if f is sequential, is non-empty, and for any sequentiality index

11This notion of continuity is weaker than the usual definition based on directed sets, but in tandem with monotonicity it is equivalent to the usual definition (which implies monotonicity).

q at (x, q′), f(x ∪ {q · e}) = f(x) ∪ {q′ · e} for e ∈ ;^{12}

For ≠ ∅, we let (M_{1} ⇒ M_{2}) denote the collection of manifestly sequential functions from (M_{1}) to (M_{2}). If = ∅, then no function f : (M_{1}) ⟶ (M_{2}) is manifestly sequential because manifest sequentiality requires ≠ ∅. In this case we let (M_{1} ⇒ M_{2}) denote the collection of sequential functions from (M_{1}) to (M_{2}).

To explain the concept of manifest sequentiality and its relationship to sequentiality, let us examine a series of examples. First, we observe that a continuous, monotonic function may not have a sequentiality index for a given pair of input value and output query. Let f : (N × T) ⟶ (T) be defined as follows:

f({?_{1} · 0} ∪ X) = {? · tt}
f({?_{2} · tt} ∪ X) = {? · tt}
f({?_{1} · m,?_{2} · ff }) = {? · ff } for m ≥ 1
f(⊥) = ⊥

where X ⊇ ∅ is any set such that the input is a proper tree. The function is not sequential because f does not have a sequentiality index at (⊥,?): f can produce output by looking at either ?_{1} or ?_{2} and thus neither of them is a sequentiality index. A uniprocessor implementation of non-sequential function must rely on time-slicing to prevent a diverging input from forcing the implementation to diverge.

The identity function id : (N) ⟶ (N) (relative to = {e}) is manifestly sequential. The query ? is the sequentiality index for (⊥,?). No other pair can have a sequentiality index, and thus id is sequential. The sequentiality index of the identity function from (N^{4} ⟶ N) to itself (over the empty set of errors) for (⊥,?) is ?. For (x,?·?_{1} · n) (with ?·?_{1} · n ∈ Open(x)), it is ?·?_{1} · n. Again, the function is sequential. Indeed, all identity functions are manifestly sequential functions. Moreover, the composition of two manifestly sequential functions is manifestly sequential.

Proposition 5.6 Let M, M_{1}, M_{2} and M_{3} be sds’s and let (M), (M_{1}), (M_{2}), and (M_{3}) be the corresponding domains relative to . Then

1. the identity function id^{(M)} : (M) ⟶ (M) is (manifestly) sequential: sequential for all and manifestly sequential for ≠ ∅;

2. if f : (M_{1}) ⟶ (M_{2}) and g : (M_{2}) ⟶ (M_{3}) are (manifestly) sequential

functions, then the composite function h(x) = g(f(x)) is (manifestly) sequential.

q′ : e_{i} ∈ f(y).

12If contains at least two elements, then the weaker notion of error-sensitivity is equivalent to manifest sequentiality. Given a monotonic, continuous function f : (M_{1}) ⟶ (M_{2}), the input z ∈ (M1) is a threshold for query q′ if q′ ∈ Answered(f(z)) yet q′ ∈ Open(f(y)) for all y z. For e_{i} ∈ , an e_{i}-variant of z ∈ (M1) is an element of the form y ∪ {q · e_{i}} such that y ⊑ z, Open(y) ⊆ Open(z) ∪ {q}. The function f is error-sensitive if for all finite x, y, z ∈ (M1) such that x z ∈ (M1), z is threshold for q′, and y is an e_{i}-variant of z:

Proof. The first part of the proposition follows from a generalization of the argument just given for the id function on the domain (N^{4} ⟶ N). To verify the second part, we must prove that g ∘ f is monotonic, continuous, and (manifestly) sequential. The first two properties are easy to verify. To prove sequentiality, assume q′ ∈ Open(g(f(x))) and q′ ∈ Answered(g(f(z))) for some z ⊒ x. Then, by the (manifest) sequentiality of g, there is a (unique) sequentiality index q^{∗} for (f(x), q′). Clearly, q^{∗} ∈ Open(f(x)) and q^{∗} ∈ Answered(f(z)). Hence, by the (manifest) sequentiality of f, there is a (unique) sequentiality index q for (x, q^{∗}). It is easy to check that q is a (unique) sequentiality index of g ∘ f for (x, q′). Finally, to verify manifest sequentiality, observe that

g(f(x ∪ {q · e})) = g(f(x) ∪ {q^{∗} · e}) by the manifest sequentiality of f
= g(f(x)) ∪ {q′ · e}  by manifest sequentiality of g

which concludes the proof.

A more interesting example of a sequential function is the addition function from (N× N) to (N) relative to the empty error set:

+ : \{ \begin{matrix}(N × N) & ⟶ & (N) for = ∅ \\ \{?_{1} · n_{1},?_{2} · n_{2}\} & ↦ & \{? · n | n = n_{1} + n_{2}\} \\ \{?_{1} · n\} & ↦ & ⊥ \\ \{?_{2} · n\} & ↦ & ⊥ \\ ⊥ & ↦ & ⊥ \end{matrix}

for n ∈ . At the input ⊥ and the output query ?, the function has two sequentiality indices, namely, ?_{1} and ?_{2}. Only if both addresses of the input tree contain a datum will + produce a response distinct from ⊥.

In contrast, a manifestly sequential function f has unique sequentiality indices and a non-empty error set .

Proposition 5.7 Let M_{1}, M_{2} be sds’s and let (M_{1}) and (M_{2}) be the respective domains relative to . Let f : (M_{1}) ⟶ (M_{2}) be an manifestly sequential function. Then all sequentiality indices are unique.

Proof. Let x ∈ (M_{1}) be a tree such that q′ is open for f(x) and answered in f(z) for some z ⊒ x. Assume q_{1} and q_{2} are sequentiality indices. Then, by manifest sequentiality,

f(x ∪ {q_{1} : e}) = f(x) ∪ {q′ : e}

for e ∈ . Since q′ is answered in f(x) ∪ {q′ : e} and x ∪ {q_{1} : e} ⊒ x, sequentiality implies that q_{2} is answered in x∪{q_{1} : e}. But given that q_{2} was open in x, this means that q_{1} = q_{2}, as desired.

Notation: Based on this lemma, it makes sense to introduce the notation si_{f}(x, q′) for the sequentiality index of an observably sequential function f at (x, q′).

As a result, the evaluation strategy for f is uniquely determined by the graph of the function. Moreover, that strategy can be effectively extracted from the graph by inspecting the behavior of f on inputs containing errors. There are two manifestly sequential addition functions. Left addition is defined by the graph:

+_{l} : \{ \begin{matrix}(N × N) & ⟶ & (N) for ≠ ∅ \\ \{?_{1} · n_{1},?_{2} · n_{2}\} & ↦ & \{? · n | n = n_{1} + n_{2}\} \\ \{?_{1} · n\} & ↦ & ⊥ \\ \{?_{1} · e_{i}\} & ↦ & \{? · e_{i}\} \\ \{?_{1} · e_{i},?_{2} · x\} & ↦ & \{? · e_{i}\} \\ \{?_{2} · x\} & ↦ & ⊥ \\ \{?_{1} · n,?_{2} · e_{i}\} & ↦ & \{? · e_{i}\} \\ ⊥ & ↦ & ⊥ \end{matrix}

where n ∈ , e_{i} ∈ , and x ∈ ∪ . When +_{l} inspects its input it always inspects the first component of the pair first. If the first component is e_{i}, manifest sequentiality forces +_{l} to return e_{i}. If the first component is a number, then +_{l} inspects the second component and returns the appropriate result when the value of the second component is determined. The reader may want to construct the graph of “right addition”, +_{r}, and compare it with the graph of +_{l}.

The preceding definitions of manifestly sequential domains and functions and Proposition 5.6 have laid the groundwork for constructing a category SEQ( ) suitable for defining the semantics of of SPCF.

6 The Manifestly Sequential Cartesian-Closed Category

In this section we show that manifestly sequential domains and functions form a cpoenriched cartesian-closed category SEQ( ) provided ≠ ∅. We begin by defining the category SEQ( ) consisting of (manifestly) sequential domains and functions relative to an error set .

Definition 6.1 (SEQ( )) The category of (manifestly) sequential objects and functions over an error set is defined as follows:

1. the collection of objects is { (M) | M is an sds}, the set of (manifestly) sequential domains over sds’s relative to ;

2. the collection of arrows between the objects (M_{1}) and (M_{2}) is (M_{1} ⇒ M_{2}),^{13} the set of (manifestly) sequential functions relative to ;

3. the composition operation for arrows is the usual function composition;

4. for each object the identity arrow is the identity function.

We use the notation SEQ( ) to refer to this category.

13This definition of homset is independent of the choice of the sds’s M_{1} and M_{2} representing _{1} and _{2}, where _{1} = (M_{1}) and _{2} = (M_{2}).

By Proposition 5.6, the preceding definition formalizes a category. More importantly, most of these categories, specifically, all those generated over non-empty error sets, are cartesian-closed categories.

Theorem 6.2 1. If ≠ ∅, then SEQ( ) is a cartesian-closed category.

2. SEQ(∅) is not cartesian-closed.

Proof. For non-empty sets of error values , we prove in the following two subsections that the category is cartesian (Lemma 6.6) and cartesian-closed (Lemma 6.22). Berry and Curien [4: Theorem 3.4.6] showed that the category of concrete domains and sequential functions is not cartesian-closed. In the Appendix, we prove that SEQ(∅) is equivalent to the Berry and Curien’s original category of (filiform) concrete domains and sequential functions, which implies the second part of the theorem.

An alternative way of defining a cpo-enriched cartesian-closed category for SPCF exploits the bijection between an exponent object (M_{1} ⇒ M_{2}) in SEQ( ) (see Definition 6.21) and the corresponding manifestly sequential function space (M_{1} ⇒ M_{2}) when ≠ ∅. The category Seq( ) has the same objects as SEQ( ) but it uses the set (M_{1} ⇒ M_{2}) instead of (M_{1} ⇒ M_{2}) as the homset (M_{1}) ⟶ (M_{2}) where the composition of such algorithms is defined in terms of Berry and Curien’s abstract algorithms (see Definition A.3). This category is important because it relates our work to the original work of Berry and Curien on sequential algorithms. When = ∅, Seq( ) contains more arrows than SEQ( ) because many functions are represented by more than one decision tree. The additional arrows make Seq( ) cartesian-closed at the cost of sacrificing extensionality. Appendix A defines the category Seq( ) and discusses its relationship to both SEQ( ) and Berry and Curien’s original category.

Theorem 6.3 Seq( ) is cartesian-closed for all sets of error values .

Proof. Appendix A contains the equivalence proof between Seq(∅) and the Berry-Curien cartesian-closed category of filiform concrete data structures. The rest follows from Theorem 6.2.

The rest of this section is dedicated to proving the two lemmas cited in the proof of Theorem 6.2. The first subsection shows that the category SEQ( ) is cartesian. The second subsection defines the exponent of two sds’s, proves an extensionality theorem for elements of the exponent, and uses this result to prove that the category SEQ( ) is cartesian-closed if is non-empty. In these two subsections, is a fixed but unspecified, non-empty set of error values. The results of the first subsection hold for all possible error sets, but those of the second subsection are sensitive to the cardinality of .

6.1 SEQ( ) is Cartesian

We begin by identifying the terminal object in SEQ( ) and defining the product construction on objects of SEQ( ).

Definition 6.4 (Terminal sds, Object, Arrow) The terminal sds is the triple (∅, ∅, ∅). The terminal object 1 is the domain containing the single element ⊥ (∅). If A is an object in SEQ( ), then the arrow 1^{A} : A ⟶ 1 is the constant function whose graph is {(x, ⊥) | x ∈ A}.

The construction of a product in SEQ( ) relies on the notion of a product sds, which is basically a “disjoint union” of two sds’s.

Definition 6.5 (Product sds, Object, Arrow) Let M_{1} = (A_{1}, D_{1}, P_{1}) and M_{2} = (A_{2}, D_{2}, P_{2}) be two sds’s. The product sds of M_{1} and M_{2} is M_{1} × M_{2} = (A, D, P) where

A = A_{1} ⊎ A_{2}
D = D_{1} ⊎ D_{2}
P = {⟨b_{1}, i⟩ ·. . . · ⟨b_{n}, i⟩ | b_{1} ·. . . · b_{n} ∈ P_{i} for i ∈ {1, 2}}

The product object of (M_{1}) and (M_{2}) is the domain (M_{1} × M_{2}). The projection functions π_{i}^{×} : (M_{1} ×M_{2}) ⟶ (M_{1}) remove the disjoint union tag from each component of a path from the respective domain and ignore other paths:

π_{i}^{×}(x) = {a_{1} · d_{1} ·. . . · a_{n} · d_{n} | ⟨a_{1}, i⟩ · ⟨d_{1}, i⟩ ·. . . · ⟨a_{n}, i⟩ · ⟨d_{n}, i⟩ ∈ x}
∪
{a_{1} · d_{1} ·. . . · a_{n} · e | ⟨a_{1}, i⟩ · ⟨d_{1}, i⟩ ·. . . · ⟨a_{n}, i⟩ · e ∈ x}.

If (M) is an object and f_{i} : (M) ⟶ (M_{i}), i ∈ {1, 2}, are functions, then the pair ⟨f_{1}, f_{2}⟩ is the function that combines the results of both functions:

⟨f_{1}, f_{2}⟩(x) = inj_{1}(f_{1}(x)) ∪ inj_{2}(f_{2}(x))

where the injection functions inj_{i} : (M_{i}) ⟶ (M_{1} × M_{2}), i ∈ {1, 2}, put an appropriate tag on each element of each path:

inj_{i}(x) = {⟨a_{1}, i⟩ · ⟨d_{1}, i⟩ ·. . . · ⟨a_{n}, i⟩ · ⟨d_{n}, i⟩ | a_{1} · d_{1} ·. . . · a_{n} · d_{n} ∈ x}
∪
{⟨a_{1}, i⟩ · ⟨d_{1}, i⟩ ·. . . · ⟨a_{n}, i⟩ · e | a_{1} · d_{1} ·. . . · a_{n} · e ∈ x}.

The second components in the unions defining the projection and the injection functions above are included to make the functions manifestly sequential.

It is easy to verify that the preceding definition constitutes a product construction for SEQ( ). Specifically, the projection and pairing functions are manifestly sequential functions and satisfy the required equations.

Lemma 6.6 Let f_{1} : (M) ⟶ (M_{1}) and f_{2} : (M) ⟶ (M_{2}) be manifestly sequential functions. Then π_{1}^{×}, π_{2}^{×}, and ⟨f_{1}, f_{2}⟩ are manifestly sequential functions that satisfy the following equations:

π_{1}^{×} ∘ ⟨f_{1}, f_{2}⟩ = f_{1}
π_{2}^{×} ∘ ⟨f_{1}, f_{2}⟩ = f_{2}
⟨π_{1}^{×} ∘ f, π_{2}^{×} ∘ f⟩ = f

where f ranges over (M) ⟶ (M_{1} × M_{2}).

Proof. The functions π_{1}^{×}, π_{2}^{×}, and ⟨f_{1}, f_{2}⟩ for appropriate f_{1}, f_{2} are clearly monotonic and continuous. The sequentiality index of π_{i}^{×} for (x, a_{1} · d_{1} ·. . . · a_{n}) is ⟨a_{1}, i⟩ · ⟨d_{1}, i⟩ ·. . . · ⟨a_{n}, i⟩. Similarly, the sequentiality index of the function ⟨f_{1}, f_{2}⟩ for (x, ⟨a′_{1}, i⟩ · ⟨d′_{1}, i⟩ ·. . . · ⟨a′_{n}, i⟩) is the sequentiality index of f_{i} for (x, ·a′_{1}d′_{1} … a′_{n}). The function is manifestly sequential because f_{1} and f_{2} are manifestly sequential.

The rest of the proof is a straightforward calculation based on the preceding definitions. For any x,

(π_{1}^{×} ∘ ⟨f_{1}, f_{2}⟩)(x) = π_{1}^{×}(inj_{1}(f_{1}(x)) ∪ inj_{2}(f_{2}(x)))
= π_{1}^{×}(inj_{1}(f_{1}(x))) ∪ π_{1}^{×}(inj_{2}(f_{2}(x)))
= π_{1}^{×}(inj_{1}(f_{1}(x)))
= f_{1}(x).

Hence, π_{1}^{×} ∘ ⟨f_{1}, f_{2}⟩ = f_{1}. Similarly, for all x,

(⟨π_{1}^{×} ∘ f, π_{2}^{×} ∘ f⟩)(x) = inj_{1}(π_{1}^{×}(f(x))) ∪ inj_{2}(π_{2}^{×}(f(x)))
= (f(x) \ inj_{2}(f(x))) ∪ (f(x) \ inj_{1}(f(x)))
= f(x) ,

implying that ⟨π_{1}^{×} ∘ f, π_{2}^{×} ∘ f⟩ = f.

We have thus shown that SEQ( ) is a cartesian category.

6.2 SEQ( ) is Cartesian-Closed

The construction of exponent objects in SEQ( ) relies on the extensional representation of manifestly sequential functions as trees. The first part of this section explains that representation and identifies its important technical properties. The second part uses these properties to prove that SEQ( ) is cartesian-closed provided is non-empty. For a general treatment of the case = ∅ we refer to Curien’s monograph [8] and Appendix A.

6.2.1 An Extensional Representation of Functions as Trees

The informal description of the decision tree representation for functions in the preceding two sections referred to the strategy that a function uses to explore its argument. Roughly speaking, a strategy is a sequence of queries and responses between the function and its argument (which may be a tuple). The application of a function follows a particular strategy as long the argument yields the anticipated responses. If the actual response differs from the expected response, the function must use an alternate strategy (consistent with the explored prefix of the previous strategy) or diverge.

Technically, a strategy for a (finite) argument value x is a non-repetitive, alternating sequence of queries and responses, starting with a query, such that x is the collection of all responses in the sequence. In such a sequence, each response q · d is immediately preceded by the query q. Conversely, each query p·a is preceded (but not necessarily immediately) by the the response p. These two properties capture the idea that a function can only explore a path in its argument after it has explored all approximations to the path. In addition, an observable response whose last element is an error value cannot appear in a strategy. Otherwise, a function could check for the presence of error values in its input and output a non-error value, violating the manifest sequentiality condition. If the exploration of the argument x encounters an error value, the application process must place the same error value in the output tree at the appropriate position. This part of the application process is encoded into the application function (see Definition 6.10 below). The formal definition of a strategy follows.^{14}

Definition 6.7 (Path Sequences) Let M = (A, D, P) be an sds. A path sequence s over M is a path p_{1} ·. . . · p_{n} over the alphabet (Que_{M} ∪ Res_{M}) such that:

1. s ∈ (Que_{M}, Res_{M})^{∗}, and s is non-repetitive in Que_{M} (which implies that the path is also non-repetitive in Res_{M});

2. for all i ≥ 1 such that 2i+1 ≤ |s|, there exists d ∈ D such that s @ (2i + 1) = s @ (2i)·d;

3. s @ 0 ∈ A (that is, s @ 0 has length 1); and

4. for all i ≥ 1 such that 2i ≤ |s| there exists an j such that 2j + 1 < 2i and s @ (2i) = s @ (2j + 1) · a for some a ∈ A.

A path sequence over M is a path constructed from tokens that are paths. For this reason, a path sequence can be interpreted as the linearization of a tree. This idea is formalized in the next lemma.

Lemma 6.8 If s is a path sequence over M, then {s @ (2i + 1) | 2i + 1 ≤ |s|} ∈ (M).

Proof. Let T stand for the set in question. We must show that T is prefix-closed and glbclosed. By conditions 2 and 4 in the preceding definition, and by induction induction on the position in s, T contains all response predecessors of its elements, i.e., T is prefix-closed. Next assume that q ·d, q ·d′ ∈ T. Then q ·d = s @ (2i + 1) for some i and q ·d′ = s @ (2j + 1) for some j . By condition 2, q = s @ (2i) = s @ (2j), and i = j by condition 1. This implies that d = d′. Hence, T is also glb-closed, proving the lemma.

Notation Given the preceding lemma, it makes sense to introduce the notation ||s|| (pronounced “tree of s”) to denote the tree {s @ (2i + 1) | 2i + 1 ≤ |s|}.

After a successful (possibly void) exploration of its argument based on some strategy, the function may construct a path in its output. Thus, a path in an element of an exponent object alternates between pieces of a strategy and pieces of output information. Since an output path, like any other path, is an alternating path of addresses and data, a path in a “functional tree” is a sequence starting with an address a on an output path, continued with a strategy, eventually followed by a datum that could be associated with a on the output path. The path can then continue with a new output address, followed by a (portion of a) strategy eventually followed by an output datum, and so on. This representation of functions is formalized in the following construction.

14The set of path sequences over M can be formulated as an sds with QueM and ResM as the sets of addresses and responses. This observation is the basis for a factorization of the function space construction into a construction of path sequences and an affine function space. One can show that the two ways of constructing the function space yield isomorphic results, an idea that naturally leads to the construction of a model of affine and possibly linear logic. This decomposition is explored in forthcoming papers by Lamarche [20] and by the second author [11].

Definition 6.9 (Exponent sds) Let M_{1} = (A_{1}, D_{1}, P_{1}) and M_{2} = (A_{2}, D_{2}, P_{2}) be sds’s. Let Res_{1} = Res_{M_{1}}, Que_{1} = Que_{M_{1}}, and S_{1} be the set of path sequences over M_{1}. The exponent sds M_{1} ⇒ M_{2} is (A, D, P) where

A = Res_{1} ⊎ A_{2} D = Que_{1} ⊎ D_{2} P = \{p ∈ (A, D)^{∗} | π\overrightarrow{1}(p) ∈ S_{1}, π\overrightarrow{2}(p) ∈ P_{2} p @ 0 ∈ A_{2}, if p @ (i + 1) ∈ A_{2} then p @ i ∈ D_{2}, if p @ (i + 1) ∈ Res_{1} then p @ i ∈ Que_{1}\} .

The corresponding recursive functions π\overrightarrow{1}, π\overrightarrow{2} : P ⟶ P are defined as follows:

π\overrightarrow{i}(ϵ) = ϵ;  π\overrightarrow{i}(p · ⟨x, i⟩) = π\overrightarrow{i}(p) · x;  π\overrightarrow{i}(p · ⟨x, j⟩) = π\overrightarrow{i}(p) if i ≠ j

for x ∈ A_{2} ∪ D_{2} ∪ Res_{1} ∪ Que_{1} and i, j ∈ {1, 2}. The extensions of these functions to paths in domain elements propagate errors:

π\overrightarrow{i}(p · e) = π\overrightarrow{i}(p) · e.

Note: In the set comprehension defining P, the two last conditions imply each other; they are both mentioned for clarity.

To ensure that the exponent construction is well-defined, we need to confirm that P is a valid set of paths. First, it does not contain the empty path since π\overrightarrow{2}(p) ∈ P_{2} forces p ≠ ϵ. Second, it is prefix-closed because S_{1} and P_{2} are prefix-closed. Note that the construction precisely captures the idea that a procedure cannot examine a node in a decision tree unless it has already examined its ancestors. Technically, if p · ⟨q, 1⟩ is a response in the exponent, then q ∈ Open(||π\overrightarrow{1}(p)||).

A simple example of an exponent sds is N ⇒ N :

A = {⟨?, 2⟩, ⟨? · n, 1⟩ | n ∈ }
D = {⟨n, 2⟩, ⟨?, 1⟩ | n ∈ }
P = \{ \begin{matrix}⟨?, 2⟩, ⟨?, 2⟩ · ⟨n, 2⟩, ⟨?, 2⟩ · ⟨?, 1⟩ \\ ⟨?, 2⟩ · ⟨?, 1⟩ · ⟨? · n, 1⟩, ⟨?, 2⟩ · ⟨?, 1⟩ · ⟨? · n, 1⟩ · ⟨m, 2⟩ \end{matrix} | m, n ∈ \} .

Similarly, the sds N^{4} → N described in the previous section is an exponent modulo the renaming of addresses and data.

The shape of a tree over an exponent sds satisfies three simple constraints, which we exploit in drawing trees schematically:

[figure: ⟨a_{0}, 2⟩; ⟨q_{0}, 1⟩/⟨d_{0}, 2⟩; Top of a tree; ⟨q, 1⟩; …; ⟨r_{1}, 1⟩; ⟨r_{n}, 1⟩; Query and Responses; ⟨d, 2⟩; …; ⟨a_{1}, 2⟩; ⟨a_{n}, 2⟩; Datum and Addresses]

The top of the tree is always an initial address from M_{2} followed by a either a datum from M_{2} or a one-element query from M_{1}. The root of a proper subtree may be labeled with a query q. It may then have as many sons as there are legal responses r_{1} through r_{n}; the responses are used as labels for the outgoing edges from a query node. Similarly, a node may be labeled with a datum d from M_{2} and the outgoing edges may then be labeled with as many addresses a_{1} through a_{n} from M_{2} as can possibly follow on a legal path in M_{2}. The trees in Section 4 omit the top part, which can always be restored, and do not require the datum/address shape because the corresponding functions are always fully uncurried.

[figure: ⟨⟨?, 2⟩, 2⟩; ⟨?, 1⟩; ⟨? · 0, 1⟩; ⟨? · 1, 1⟩; …; …; …; ⟨⟨?, 1⟩, 2⟩; ^{⟨? · n, 1⟩  …}; ⟨n, 2⟩; ⟨⟨? · 0, 1⟩, 2⟩; ⟨n + 1, 2⟩; ⟨⟨? · 1, 1⟩, 2⟩; …; ⟨m + n, 2⟩; ^{⟨⟨? · m, 1⟩, 2⟩  …}]

Figure 3: Left Addition: +_{l}

Figure 3 shows left-addition as an example of a tree in N ⇒ N ⇒ N. A more interesting example of a function tree over (N ⇒ N) ⇒ N ⇒ N, including its SPCF text, is displayed in Figure 4. The tree tests whether its input is a strict function, and if so returns the function sub1 when the argument maps 0 to 1 and 1 to 2. For non-strict inputs, the function returns whatever the input returns.

A path p in a decision tree of an exponent sds has a natural interpretation as a piece of an algorithm. Such a path has the shape:

⟨a_{1}, 2⟩ · s_{1}^{∗} · ⟨d_{1}, 2⟩ · ⟨a_{2}, 2⟩ ·. . . · ⟨d_{n−1}, 2⟩ · ⟨a_{n}, 2⟩ · s_{n}^{∗} · ⟨d_{n}, 2⟩ · ⟨a_{n+1}, 2⟩ · s_{n+1}^{∗}

[figure: ⟨⟨?, 2⟩, 2⟩; ⟨⟨?, 2⟩, 1⟩; …; ⟨⟨0, 2⟩, 2⟩; ⟨⟨?, 2⟩⟨0, 2⟩, 1⟩; ⟨⟨n, 2⟩, 2⟩; ⟨⟨?, 2⟩⟨n, 2⟩, 1⟩; …; ⟨⟨?, 2⟩⟨?, 1⟩⟨? · 0, 1⟩, 1⟩; ⟨⟨?, 2⟩⟨?, 1⟩, 1⟩; ⟨⟨?, 2⟩⟨?, 1⟩⟨? · 1, 1⟩, 1⟩; ⟨⟨?, 2⟩⟨?, 1⟩⟨? · 0, 1⟩⟨1, 2⟩, 1⟩; ⟨⟨?, 1⟩, 2⟩; ⟨⟨?, 2⟩⟨?, 1⟩⟨? · 1, 1⟩⟨2, 2⟩, 1⟩; ⟨⟨0, 2⟩, 2⟩; ⟨⟨? · 1, 1⟩, 2⟩; ⟨⟨1, 2⟩, 2⟩; ⟨⟨? · 2, 1⟩, 2⟩; …; ⟨⟨n − 1, 2⟩, 2⟩; ⟨⟨? · n, 1⟩, 2⟩]

λfx.(if0 (catch f) (if0 (sub1 (f ^{⌈}0^{⌉})) (if0 (sub1 (sub1 (f ^{⌈}1^{⌉}))) (sub1 x) Ω) Ω) (f Ω))

Figure 4: A Tree in ((N ⇒ N) ⇒ (N ⇒ N))

where each segment s_{i}^{∗}, for 1 ≤ i ≤ n, is a tagged portion of a strategy:

s_{i}^{∗} = ⟨q_{i,1}, 1⟩ · ⟨r_{i,1}, 1⟩ ·. . . · ⟨q_{i,m_{i}}, 1⟩ · ⟨r_{i,m_{i}}, 1⟩

for some m_{i} ≥ 0. When stripped of its tags, each s_{i}^{∗} is a portion

s_{i} = q_{i,1} · r_{i,1} ·. . . · q_{i,m_{i}} · r_{i,m_{i}}

of a path sequence such that for all i, 1 ≤ i ≤ n + 1, the composite sequence s_{1} … s_{i} is a path sequence (over M_{1}). For example the right-most path in the tree of Figure 4, the pieces are:

⟨a_{1}, 2⟩ = ⟨⟨?, 2⟩, 2⟩
s_{1}^{∗}

=

query  response
⟨⟨?, 2⟩, 1⟩  ⟨⟨?, 2⟩ · ⟨?, 1⟩, 1⟩
⟨⟨?, 2⟩ · ⟨?, 1⟩ · ⟨? · 0, 1⟩, 1⟩ ⟨⟨?, 2⟩ · ⟨?, 1⟩ · ⟨? · 0, 1⟩ · ⟨1, 2⟩, 1⟩
⟨⟨?, 2⟩ · ⟨?, 1⟩ · ⟨? · 1, 1⟩, 1⟩ ⟨⟨?, 2⟩ · ⟨?, 1⟩ · ⟨? · 1, 1⟩ · ⟨2, 2⟩, 1⟩

⟨d_{1}, 2⟩ = ⟨⟨?, 1⟩, 2⟩
⟨a_{2}, 2⟩ = ⟨⟨? · n, 1⟩, 2⟩
s_{2}^{∗} = ϵ
⟨d_{2}, 2⟩ = ⟨⟨(n − 1), 2⟩, 2⟩
s_{3}^{∗} = ϵ

With the initial address a_{1}, the path p announces that the function attempts to construct an output path starting with a_{1}. If it can now successfully explore the argument according to strategy s_{1}, the function will add the datum d_{1} to the output path, finishing the first possible approximation to the response. Then the process starts over with the announcement that the function will place a datum at address a_{2} if the strategy s_{1}s_{2} can be pursued successfully, and so on. If at any point in the exploration of the argument a match yields no value at all, the process stops. Similarly, if the match produces an error value, the function must place the same error value on the output path behind the “announced” address and then the process terminates. The following definition formalizes the idea of “applying” a tree from the domain over an exponent sds to an argument tree.

Definition 6.10 (Application) Let M_{1} ⇒ M_{2} be the exponent sds of M_{1} and M_{2}. The application of some tree t ∈ (M_{1} ⇒ M_{2}) to some tree x ∈ (M_{1}), written as t ⋆ x, is defined as follows:

t ⋆ x = \{π\overrightarrow{2}(p) ∈ Res_{M_{2}} | ||π\overrightarrow{1}(p)|| ⊑ x, p ∈ t\} ∪ \{π\overrightarrow{2}(p) · e ∈ ResM_{2}^{e} | ||π\overrightarrow{1}(p)|| ∪ \{q · e\} ⊑ x, p · ⟨q, 1⟩ ∈ t\}.

The formal definition of application captures the intuitive ideas presented in the preceding sections about manifestly sequential functions. When a decision tree is interpreted as a function, it inspects the argument tree one step at a time, with missing information resulting in a bottom output and erroneous information being propagated. It constructs distinct paths in the output tree independently, but each path is constructed sequentially. If a path occurs in the output, it is due to precisely one path.

Lemma 6.11 If t ∈ (M_{1} ⇒ M_{2}) and x ∈ (M_{1}), then t ⋆ x ∈ (M_{2}).

Proof. Each element of t ⋆ x is clearly an observable response over M_{2} by the definition of the application operator. Based on the fact that t is prefix- and glb-closed, it is easy to verify that t ⋆ x satisfies the same properties.

We can now show that application is “functional”, i.e., for fixed t and varying x, t ⋆ x uniquely determines t. This extensionality property holds only when the set of errors is non-empty.

Theorem 6.12 (Extensionality) Let t, t′ ∈ (M_{1} ⇒ M_{2}). Then:

1. if = ∅, t ⋆ x = t′ ⋆ x for all x ∈ (M_{1}) does not imply that t = t′; 2. if contains a single element, t = t′ iff t ⋆ x = t′ ⋆ x for all x ∈ (M_{1});

3. if contains more than one element, t ⊑ t′ iff t ⋆ x ⊑ t′ ⋆ x for all x ∈ (M_{1}).

Proof. Part 1 is obvious: the trees for the two addition procedures +_{l} and +_{r} introduced in Section 3 are distinct but they compute the same sequential function over the natural numbers. The tree for +_{l} is given in Figure 3 in Subsection 6.2.1. In contrast, the tree for +_{r} has the following form:

[figure: ⟨⟨?, 2⟩, 2⟩; ⟨?, 2⟩; …]

For the remaining cases, the left to right direction is obvious. For the converse, we first prove Part 3 by contra-position and return to Part 2 below. Assume t ⋢ t′, i.e., there exists p such that p ∈ t and p ∉ t′. Let p^{∗} be the maximal path approximating p that also approximates some p′ ∈ t′. To prove the claim we will derive a witness x from p^{∗} such that t ⋆ x ⋢ t′ ⋆ x. Clearly, the witness must dominate x_{0} = ||π\overrightarrow{1}(p^{∗})||. To determine the rest of the witness, we need to distinguish two cases:

1. p^{∗} is empty or is a response: Since p^{∗} is maximal in t′ in the direction of p, it suffices to understand how p extends p^{∗} in order to construct the witness:

path in t  witness x  path in t ⋆ x, not in t′ ⋆ x
p^{∗} · ⟨r, 1⟩ · ⟨q, 1⟩  x = x_{0} ∪ \{r, q · e\}  π\overrightarrow{2}(p^{∗}) · e
p^{∗} · ⟨r, 1⟩ · ⟨d, 2⟩  x = x_{0} ∪ \{r\}  π\overrightarrow{2}(p^{∗}) · d
p^{∗} · ⟨r, 1⟩ · e  x = x_{0} ∪ \{r\}  π\overrightarrow{2}(p^{∗}) · e
p^{∗} · ⟨a, 2⟩ · ⟨q, 1⟩  x = x_{0} ∪ \{q · e\}  π\overrightarrow{2}(p^{∗}) · a · e
p^{∗} · ⟨a, 2⟩ · ⟨d, 2⟩  x = x_{0}  π\overrightarrow{2}(p^{∗}) · a · d
p^{∗} · ⟨a, 2⟩ · e  x = x_{0}  π\overrightarrow{2}(p^{∗}) · a · e

Given a witness, it is easy to prove that the path in the last column is indeed in t ⋆ x but not in t′ ⋆ x. For an example, consider the first line. If π\overrightarrow{2}(p^{∗}) · e ∈ t′ ⋆ x then either

• there exists a response r′ ∈ t′ such that π\overrightarrow{2}(r′) = π\overrightarrow{2}(p^{∗}) · e and ||π\overrightarrow{1}(r′)|| ⊑ x (error generation); or

• there exists a response r′ = p′ · ⟨q′, 1⟩ ∈ t′ such that ||π\overrightarrow{1}(p′)|| ∪ \{q′ · e\} ⊑ x and π\overrightarrow{2}(p^{∗}) = π\overrightarrow{2}(p′) (error propagation).

In either case, ||π\overrightarrow{1}(p^{∗})|| ↑ ||π\overrightarrow{1}(r′)|| and the outputs are comparable, so that p^{∗} and r′ are comparable as well by the following lemma (6.13). First, assume p^{∗} ⊑ r′. Since ||π\overrightarrow{1}(r′)|| ⊑ x, it is moreover true that p^{∗} · ⟨r, 1⟩ ⊑ r′ because x can only respond in one way to the question at the end of p^{∗}. But this contradicts the maximality of p^{∗} in t′ in the direction of p. Second, assume p^{∗} ⊑ r′, which is only possible in the error propagation case since π\overrightarrow{2}(p^{∗}) π\overrightarrow{2}(r′) in the error generation case. Now, for some r ∈ Res_{M_{2}}, r′ · ⟨r, 1⟩ ⊑ p^{∗}, which implies that r ∈ ||π\overrightarrow{1}(p^{∗})|| ⊑ x and thus contradicts q′ : e ∈ x. — The proofs for other cases proceed in similar fashion.

2. p^{∗} is a query: Now p^{∗} has extensions in both t and t′ and the subcases accordingly account for this fact:

path in t path in t′ witness x  path in t ⋆ x, not in t′ ⋆ x
p^{∗} · ⟨q, 1⟩ p^{∗} · ⟨q′, 1⟩ x = x_{0} ∪ \{q · e\}  π\overrightarrow{2}(p^{∗}) · e
where q ≠ q′
p^{∗} · ⟨q, 1⟩ p^{∗} · ⟨d′, 2⟩ x = x_{0} ∪ \{q · e\}  π\overrightarrow{2}(p^{∗}) · e
p^{∗} · ⟨q, 1⟩ p^{∗} · e′ x = x_{0} ∪ \{q · e | e ≠ e′\} π\overrightarrow{2}(p^{∗}) · e (†)
p^{∗} · ⟨d, 2⟩ p^{∗} · ⟨q′, 1⟩ x = x_{0}  π\overrightarrow{2}(p^{∗}) · d
p^{∗} · ⟨d, 2⟩ p^{∗} · ⟨d′, 2⟩ x = x_{0}  π\overrightarrow{2}(p^{∗}) · d
where d ≠ d′
p^{∗} · ⟨d, 2⟩ p^{∗} · e′  x = x_{0}  π\overrightarrow{2}(p^{∗}) · d
p^{∗} · e  p^{∗} · ⟨q′, 1⟩ x = x_{0}  π\overrightarrow{2}(p^{∗}) · e
p^{∗} · e  p^{∗} · ⟨d′, 2⟩ x = x_{0}  π\overrightarrow{2}(p^{∗}) · e
p^{∗} · e  p^{∗} · e′  x = x_{0}  π\overrightarrow{2}(p^{∗}) · e
where e ≠ e′

Again, we only illustrate with an example the kind of proofs that are required to show that the path in the last column is not in t′ ⋆ x. Consider the fourth line. For t′ ⋆ x to contain π\overrightarrow{2}(p^{∗}) · d, there must be a response r′ ∈ t′ such that π\overrightarrow{2}(r′) = π\overrightarrow{2}(p^{∗}) · d and ||π\overrightarrow{1}(r′)|| ⊑ x. By Lemma 6.13, p^{∗} · ⟨d, 2⟩ ⊑ r′ since π\overrightarrow{2}(p^{∗}) π\overrightarrow{2}(r′). Then we should have that p^{∗} = p^{∗} · ⟨q′, 1⟩ ⊓ p^{∗} · ⟨d, 2⟩ is in t′. But p^{∗} is a query and thus cannot be a member of the tree t′. Hence, π\overrightarrow{2}(p^{∗}) · d ∉ t′ ⋆ x.

The proof of Part 2 is similar to the proof of Part 3, except for the case marked with (†) because there is no second element in = {e′} that can be used to extend q. Thus, for example, in N ⇒ N, ⟨?, 2⟩ · ⟨?, 1⟩ ⋢ ⟨?, 2⟩ · e′ yet ⟨?, 2⟩ · ⟨?, 1⟩ ⋆ x = ∅ ⊑ ⟨?, 2⟩ · e′ ⋆ x for any x. But the following equivalent formulation of part 2 holds:

2′. If contains a single element, t ⋢ t′ implies t ⋆ x ≠ t′ ⋆ x, for some x ∈ (M_{1}).

With the exception of the case marked (†), all cases work as before. For case (†), π\overrightarrow{2}(p^{∗})·e′ ∈ t′ ⋆ x_{0} but π\overrightarrow{2}(p^{∗}) · e′ ∉ t ⋆ x_{0}, i.e., t′ ⋆ x_{0} ⋢ t ⋆ x_{0}.

To complete the proof of the extensionality theorem, we need to verify the following lemma, which we use again later.

Lemma 6.13 Let t ∈ (M_{1} ⇒ M_{2}) and let p, p′ ∈ t. If ||π\overrightarrow{1}(p)|| ↑ ||π\overrightarrow{1}(p′)|| and π\overrightarrow{2}(p) ⊑ π\overrightarrow{2}(p′), then p ⊑ p′ or p′ ⊑ p. Moreover, if π\overrightarrow{2}(p) π\overrightarrow{2}(p′) then p p′.

Proof. Assume ||π\overrightarrow{1}(p)|| and ||π\overrightarrow{1}(p′)|| are consistent and π\overrightarrow{2}(p) ⊑ π\overrightarrow{2}(p′). Let s = p ⊓ p′. Assume that neither s = p nor s = p′, i.e., p, p′ are incomparable, and consider the following cases:

s = s′ · ⟨q, 1⟩· Then for some r and r′, s · ⟨r, 1⟩ ⊑ p and s · ⟨r′, 1⟩ ⊑ p′ with r ≠ r′. But this contradicts the consistency of ||π\overrightarrow{1}(p)|| and ||π\overrightarrow{1}(p′)||.

s = ϵ or s = s′ · ⟨d, 2⟩· Here, for some addresses a, a′, s · ⟨a, 2⟩ ⊑ p and s · ⟨a′, 2⟩ ⊑ p′ with a ≠ a′. But again, this leads to a contradiction: if this were true, π\overrightarrow{2}(p) could not possibly approximate π\overrightarrow{2}(p′).

Since both cases turn out to be impossible, p and p′ must be comparable. If in addition π\overrightarrow{2}(p) π\overrightarrow{2}(p′) then clearly, p p′ by the definition of the projection function.

The extensionality theorem confirms that each tree uniquely represents a function. It gives rise to the definition of a mapping from the domain over the exponent sds to the set of functions between the respective domains.

Definition 6.14 (Fun) Let t ∈ (M_{1} ⇒ M_{2}). Then Fun(t) = \underline{λ}x : (M_{1}) . t ⋆ x.

In fact, for a tree t, Fun(t) is always a manifestly sequential function.

Lemma 6.15 Fun : (M_{1} ⇒ M_{2}) ⟶ (M_{1} ⇒ M_{2})

Proof. Let t ∈ (M_{1} ⇒ M_{2}). Clearly, Fun(t) is a monotonic and continuous function. As for sequentiality, assume that for some x and for some z ⊒ x, q′ ∈ Open(t ⋆ x) and q′ ∈ Answered(t ⋆ z). Let q′ = r′ · a (where, possibly, r′ = ϵ) and let q′ · d_{z} ∈ t ⋆ z for some d_{z} from M_{2}. By the definition of the application operator, there must be

1. p_{z} ∈ t such that π\overrightarrow{2}(p_{z}) = r′ · a · d_{z} and ||π\overrightarrow{1}(p_{z})|| ⊑ z; or,

2. q_{z} · ⟨q_{e}, 1⟩ ∈ t such that π\overrightarrow{2}(q_{z}) · e = r′ · a · d_{z} and ||π\overrightarrow{1}(q_{z})|| ∪ \{q_{e} · e\} ⊑ z.

The rest of the proof concentrates on the first case; the arguments can easily be modified for the second one.

Choose p and q_{x} such that

p · ⟨a, 2⟩ ·. . . · ⟨q_{x}, 1⟩ ·. . . · ⟨d_{z}, 2⟩ = p_{z},

where q_{x} ∈ Open(x) is the first such open query. The path fragment between ⟨a, 2⟩ and ⟨d_{z}, 2⟩ must contain a query q_{x} ∈ Open(x). Otherwise, ||π\overrightarrow{1}(p · ⟨a, 2⟩ ·. . . · ⟨d_{z}, 2⟩)|| ⊑ x and π\overrightarrow{2}(p · ⟨a, 2⟩ ·. . . · ⟨d_{z}, 2⟩) = q′ · d_{z} ∈ t ⋆ x, which contradicts q′ ∈ Open(t ⋆ x).

It is easy to show that ||π\overrightarrow{1}(p)|| ⊑ x. If p ≠ ϵ, then π\overrightarrow{2}(p) = r′, and r′ ≠ ϵ. Since r′ ∈ t ⋆ x, there must be some path p′ such that π\overrightarrow{2}(p′) = r′ and ||π\overrightarrow{1}(p′)|| ⊑ x. By Lemma 6.13, p′ and p_{z} are comparable. If p′ p, then π\overrightarrow{2}(p′) r′ because p ends in ⟨d, 2⟩ when r′ ends in d; otherwise, if p p′, then r′ · a ⊑ π\overrightarrow{2}(p′). Thus, p′ = p. If p = ϵ, then ||π\overrightarrow{1}(p)|| =⊥⊑ x.

The query q_{x} is the sequentiality index of Fun(t) for (x, q′). To prove this claim, let y ∈ (M_{1}) be such that y ⊒ x and q′ ∈ Answered(t ⋆ y). By the same arguments as for z, t must contain some path p_{y} with

p · ⟨a, 2⟩ ·. . . · ⟨q_{y}, 1⟩ ·. . . · ⟨d_{y}, 2⟩ = p_{y}

for some first q_{y} ∈ Open(x). The path p is the prefix for both p_{z} and p_{y} because at most one path in t can produce the output path r′. It follows from a simple inductive argument that any query following ⟨a, 2⟩ in front of q_{y} on p_{y} must be identical to the respective query on p_{z} due to the tree structure of t and that the following responses must be identical because they are in x.

Since all queries between ⟨a, 2⟩ and q_{y} are answered in x, all corresponding responses are identical to the respective responses on p_{z}. Since t is a tree, the queries must be identical, too. Hence, q_{y} = q_{x}, which proves that q_{x} is the sequentiality index.

The manifest sequentiality of Fun(t) follows immediately from the preceding portion of the proof and the definition of application.

The proof of the preceding lemma also indicates how to find a tree from a manifestly sequential function f. Every path in the functional tree corresponding to f contributes one path to an output, if any, by exploring some finite piece of the input according to the strategy of f. The strategy is an alternating sequence of (unique) sequentiality indices and their responses mixed with output addresses and data. Collecting all of the paths for a function f in a set yields a tree.

Definition 6.16 (Tree, Path_{f}(x, p)) Let f : (M_{1} ⇒ M_{2}) be a sequential and manifestly sequential function between the domains (M_{1}) and (M_{2}). Let x be in _{0}(M_{1}), and let p = a_{1}d_{1} … a_{n}d_{n} be in f(x) with, possibly, d_{n} ∈ .

The finite element Path_{f}(x, p) = {p_{0},…, p_{m}} is inductively defined as follows:

1. p_{0} = \{ \begin{matrix}⟨a_{1}, 2⟩ · ⟨d_{1}, 2⟩ & if a_{1} · d_{1} ∈ f(⊥) \\ ⟨a_{1}, 2⟩ · e & if a_{1} · e = p and p ∈ f(⊥) \\ ⟨a_{1}, 2⟩ · ⟨si_{f}(⊥, a_{1}), 1⟩ & otherwise \end{matrix}

2. if p_{i} = q_{i} · ⟨q, 1⟩, π\overrightarrow{2}(p_{i}) = a_{1} · d_{1} ·. . . · a_{j} and there is an r = q · d from Res_{M_{2}} in x then

p_{i+1} = \{ \begin{matrix}q_{i+1} · ⟨d_{j}, 2⟩ & if π\overrightarrow{2}(p_{i}) · d_{j} ∈ f(||π\overrightarrow{1}(q_{i+1})||) \\ q_{i+1} · e & if π\overrightarrow{2}(p_{i}) · e ∈ f(||π\overrightarrow{1}(q_{i+1})||) \\ q_{i+1} · ⟨si_{f}(||π\overrightarrow{1}(q_{i+1})||, π\overrightarrow{2}(q_{i+1})), 1⟩ & otherwise \end{matrix}

where q_{i+1} = p_{i} · ⟨r, 1⟩;

3. if p_{i} = q_{i} · ⟨d_{j}, 2⟩, π\overrightarrow{2}(p_{i}) = a_{1} · d_{1} ·. . . · a_{j} · d_{j}, and j < n then

p_{i+1} = \{ \begin{matrix}q_{i+1} · ⟨d_{j+1}, 2⟩ & if π\overrightarrow{2}(q_{i+1}) · d_{j+1} ∈ f(||π\overrightarrow{1}(p_{i})||) \\ q_{i+1} · e & if π\overrightarrow{2}(q_{i+1}) · e ∈ f(||π\overrightarrow{1}(p_{i})||) \\ q_{i+1} · ⟨si_{f}(||π\overrightarrow{1}(p_{i})||, π\overrightarrow{2}(q_{i+1})), 1⟩ & otherwise \end{matrix}

where q_{i+1} = p_{i} · ⟨a_{j+1}, 2⟩.

The tree for f is the lub of all such finite elements:

Tree(f) = ⨆{Path_{f}(x, p) | x ∈ _{0}(M_{1}), p ∈ f(x)}.

The proof that Tree(f) is a well-defined element of (M_{1} ⇒ M_{2}) requires a simple lemma about Path_{f}(x, p).

Lemma 6.17 Let f ∈ (M_{1} ⇒ M_{2}), let x ∈ _{0}(M_{1}), and let p ∈ f(x). Then

1. Path_{f}(x, p) ∈ _{0}(M_{1} ⇒ M_{2});

2. ||π\overrightarrow{1}(Path_{f}(x, p))|| is the minimal finite element x′ ⊑ x such that p ∈ f(x′), and hence, p ∈ Path_{f}(x, p) ⋆ x.

Proof. For Part 1, first note two invariants of the elements p_{0},…, p_{m} in Path_{f}(x, p):

1. p_{i} ∈ Res_{M_{2}} for all i;

2. if p_{i}, p_{i+1} ∈ Path_{f}(x, p) then p_{i} is the immediate predecessor of p_{i+1}.

Hence, Path_{f}(x, p) is a prefix-closed chain of paths, and therefore is an element. By the finiteness of p and x, Path_{f}(x, p) is finite.

Part 2 first claims that that there is a unique input threshold for every output path. The proof follows Berry’s proof that sequential functions are stable [8:Proposition 2.4.7]. If x ↑ y then f(x ⊓ y) = f(x) ⊓ f(y): Assume x ↑ y. Clearly f(x ⊓ y) ⊑ f(x) ⊓ f(y). Thus, assume that

f(x ⊓ y) f(x) ⊓ f(y).

This means that there exists a path p such that p ∈ f(x), p ∈ f(y), and p ∉ f(x ⊓ y). Let q′ be the first open query for f(x ⊓ y) below p. By the sequentiality of f ,

q = si_{f}(x ⊓ y, q′)

is defined. By assumption, there are d_{x} and d_{y} such that q · d_{x} ∈ x and q · d_{y} ∈ y. Since x ↑ y, d_{x} = d_{y}. But therefore q · d_{x} ∈ x ⊓ y, which contradicts q ∈ Open(x ⊓ y). Hence, f(x ⊓ y) = f(x) ⊓ f(y).

“Stability” implies the existence of a unique threshold: By continuity there exists a finite x_{0} ⊑ x such that p ∈ f(x_{0}). Let x_{0}, x_{1} be two minimal elements such that p ∈ f(x_{0}) and p ∈ f(x_{1}). Then p ∈ f(x_{0} ⊓ x_{1}), which can only mean x_{0} = x_{1} by minimality. Hence, there is a least threshold for every p in f(x).

The proof that p ∈ f(π\overrightarrow{1}(Path_{f}(x, p))) relies on further invariants of the construction of the paths p_{1},…, p_{m}:

1. ||π\overrightarrow{1}(p_{i})|| ⊑ x for all i;

2. π\overrightarrow{2}(p_{i}) ⊑ p for all i; 3. if π\overrightarrow{2}(p_{i}) ∈ Res_{M_{2}} then ||π\overrightarrow{1}(p_{i})|| is the minimal element x′ ⊑ x such that π\overrightarrow{2}(p_{i}) ∈

f(x′);

4. if π\overrightarrow{2}(p_{i}) ∈ Que_{M_{2}} then p_{i} = q_{i} · ⟨q, 1⟩ and q = si_{f}(||π\overrightarrow{1}(q_{i})||, π\overrightarrow{2}(q_{i})).

The first two invariants are obvious. The third and fourth follow from simple arguments: First, if a_{1}d_{1} ∉ f(⊥), then a_{1} ∈ Open(f(⊥)). Since a_{1}d_{1} ∈ f(x) and ⊥⊑ x, si_{f}(⊥, a_{1}) is defined. If a_{1}d_{1} ∈ f(⊥) then ⊥ is clearly the minimal element below x such that this is the case. Second, if p_{i} was constructed via clause 2 of Definition 6.16, and π\overrightarrow{2}(p_{i}) · d_{j} ∉ f(||π\overrightarrow{1}(q_{i+1})||) then π\overrightarrow{2}(p_{i}) ∈ Open(f(||π\overrightarrow{1}(q_{i+1})||)). Since π\overrightarrow{2}(p_{i}) · d_{j} ∈ f(x) and ||π\overrightarrow{1}(q_{i+1})|| ⊑ x, si_{f}(||π\overrightarrow{1}(q_{i+1})||, π\overrightarrow{2}(q_{i+1})) is defined. However, if π\overrightarrow{2}(p_{i}) · d_{j} ∈ f(||π\overrightarrow{1}(q_{i+1})||) then ||π\overrightarrow{1}(q_{i+1})|| is a minimal element below x such that this is the case. The argument below shows that there is only one minimal element. Finally, if p_{i} was constructed via clause 3, the arguments proceeds as for clause 2.

Now it suffices to show that p_{m} outputs p. The lack of a successor for p_{m} is due to one of two reasons:

1. p_{m} = q_{m} ·⟨q, 1⟩ and q ·e ∈ x (it is impossible that q ∈ Open(x)). But then π\overrightarrow{2}(q_{m})·e ∈ f(||π\overrightarrow{1}(q_{m})||), π\overrightarrow{2}(q_{m}) · e ∈ f(x), and hence, p = π\overrightarrow{2}(q_{m}) · e.

2. p_{m} = q_{m} · d_{j} and j ≮ n: immediately, π\overrightarrow{2}(p_{m}) = p.

In either case, p ∈ Path_{f}(x, p) ⋆ x.

Two distinct paths Path_{f}(x, p) and Path_{f}(x′, p′) cannot interfere with each other. Thus, the collection of all such finite elements forms a valid tree. Moreover, the tree “implements” f when interpreted as a “functional tree”.

Lemma 6.18 1. Tree : (M_{1} ⇒ M_{2}) ⟶ (M_{1} ⇒ M_{2}).

2. If f ∈ (M_{1} ⇒ M_{2}), let x ∈ (M_{1}), then f(x) = Tree(f) ⋆ x.

Proof. Part 1 requires a proof that Tree(f) is not only prefix-closed, as shown in the preceding lemma, but is also glb-closed. It suffices to show that two finite elements Path_{f}(x_{1}, p_{1}) and Path_{f}(x_{2}, p_{2}) in the tree cannot contain paths whose glb is a query. Thus, assume that there is a query q that has two incompatible completions to responses in Path_{f}(x_{1}, p_{1}) and Path_{f}(x_{2}, p_{2}). There are nine possible cases, each of which falls into one of three classes with d_{1} ≠ d_{2}, q_{1} ≠ q_{2}, e_{1} ≠ e_{2}:

q · e_{2} q · ⟨d_{2}, 2⟩ q · ⟨q_{2}, 1⟩
q · e_{1}  A  A  B
q · ⟨d_{1}, 2⟩ A  A  B
q · ⟨q_{1}, 1⟩ B  B  C

We concentrate on one example from each class:

A: Let q · ⟨d_{1}, 2⟩ ∈ Path_{f}(x_{1}, p_{1}) and q · ⟨d_{2}, 2⟩ ∈ Path_{f}(x_{2}, p_{2}). By Lemma 6.17,

π\overrightarrow{2}(q · ⟨d_{1}, 2⟩) ∈ f(||π\overrightarrow{1}(q · ⟨d_{1}, 2⟩)||)
π\overrightarrow{2}(q · ⟨d_{2}, 2⟩) ∈ f(||π\overrightarrow{1}(q · ⟨d_{2}, 2⟩)||).

But by the definition of the projection functions,

f(||π\overrightarrow{1}(q · ⟨d_{1}, 2⟩)||) = f(||π\overrightarrow{1}(q)||) = f(||π\overrightarrow{1}(q · ⟨d_{2}, 2⟩)||) .

Therefore,

π\overrightarrow{2}(q) · d_{1} ∈ f(||π\overrightarrow{1}(q)||)

and

π\overrightarrow{2}(q) · d_{2} ∈ f(||π\overrightarrow{1}(q)||) .

Hence, π\overrightarrow{2}(q), a query, is in f(||π\overrightarrow{1}(q · ⟨d_{2}, 2⟩)||), which proves that the latter is not a tree, contradicting the basic assumptions of the lemma.

B: Let q · ⟨d_{1}, 2⟩ ∈ Path_{f}(x_{1}, p_{1}) and q · ⟨q_{2}, 1⟩ ∈ Path_{f}(x_{2}, p_{2}). Then

π\overrightarrow{2}(q) · d_{1} ∈ f(||π\overrightarrow{1}(q · ⟨d_{1}, 2⟩)||) = f(||π\overrightarrow{1}(q)||),
q_{2} = si_{f}(||π\overrightarrow{1}(q)||, π\overrightarrow{2}(q)).

But the two consequences simultaneously demand that

π\overrightarrow{2}(q) · d_{1} ∈ Answered(f(||π\overrightarrow{1}(q)||))

and

π\overrightarrow{2}(q) ∈ Open(f(||π\overrightarrow{1}(q · ⟨q_{2}, 1⟩)||)) = Open(f(||π\overrightarrow{1}(q)||)),

that is, we have a contradiction.

C : Let q · ⟨q_{1}, 1⟩ ∈ Path_{f}(x_{1}, p_{1}) and q · ⟨q_{2}, 1⟩ ∈ Path_{f}(x_{2}, p_{2}). Since si_{f} is a function for manifestly sequential functions

q_{1} = si_{f}(||π\overrightarrow{1}(q)||, π\overrightarrow{2}(q)) = q_{2},

which contradicts the assumption.

The other cases in the three classes have similar proofs. In summary, a case analysis shows that the intersection of two responses from distinct finite elements Path_{f}(x_{1}, p_{1}) and Path_{f}(x_{2}, p_{2}) is a response, and that therefore, Tree(f) ∈ (M_{1} ⇒ M_{2}).

To prove part 2, we must show Tree(f) ⋆ x and Tree(f) ⋆ x ⊆ f(x), and vice versa. The proof of the first proposition is easy. Assume p ∈ f(x). By continuity, there exists a finite x_{0} ⊑ x such that p ∈ f(x_{0}). By Lemma 6.17, p ∈ Path_{f}(x_{0}, p) ⋆ x_{0} and, hence, p ∈ Tree(f) ⋆ x_{0}. By monotonicity, p ∈ Tree(f) ⋆ x.

To prove Tree(f)⋆x ⊆ f(x), we must consider two cases. Let p ∈ Tree(f)⋆x. In the first case, r ∈ Tree(f), π\overrightarrow{2}(r) = p, and ||π\overrightarrow{1}(r)|| ⊑ x. By the construction of paths in Tree(f),

p = π\overrightarrow{2}(r) ∈ f(||π\overrightarrow{1}(r)||).

By monotonicity, p ∈ f(x). In the second case, q · ⟨q′, 1⟩ ∈ Tree(f), π\overrightarrow{2}(q) · e = p, and ||π\overrightarrow{1}(q)|| ∪ \{q′ · e\} ⊑ x. Now the construction of q · ⟨q′, 1⟩ implies that

q′ = si_{f}(||π\overrightarrow{1}(q)||, π\overrightarrow{2}(q)),

which means π\overrightarrow{2}(q) ∈ Open(f(x)). But then

p = π\overrightarrow{2}(q) · e ∈ f(||π\overrightarrow{1}(q)|| ∪ \{q′ · e\})

by error propagation. The conclusion, p ∈ f(x), follows again by monotonicity. Together the two cases imply Tree(f) ⋆ x = f(x).

In summary, we have shown that there exists a bijection between the set (M_{1} ⇒ M_{2}) of manifestly sequential functions and the (carrier of the) domain over the exponent sds M_{1} ⇒ M_{2}.

Theorem 6.19 1. For every manifestly sequential function f ∈ (M_{1} ⇒ M_{2}),

Fun(Tree(f)) = f.

2. For every domain element t ∈ (M_{1} ⇒ M_{2}),

Tree(Fun(t)) = t.

Proof. To prove part 1, we observe that for all x,

Fun(Tree(f))(x) = Tree(f) ⋆ x = f(x)

by Lemma 6.18. By extensionality, Fun(Tree(f)) = f.

To prove part 2, we observe that for all x,

Tree(Fun(t)) ⋆ x = Fun(t)(x) = t ⋆ x

by Lemma 6.18 and Definition 6.14. By the Extensionality Theorem for trees (6.12), Tree(Fun(t)) = t.

Together with the third part of the Extensionality Theorem, the theorem implies that the function space (M_{1} ⇒ M_{2}) itself with the usual, pointwise ordering is a Scott domain provided the error set contains at least two elements. Notation We write f ⊑_{e} g iff for all x, f(x) ⊑ g(x).

Corollary 6.20 If contains at least two elements, then Fun : (M_{1} ⇒ M_{2}) ⟶ (M_{1} ⇒ M_{2}) is an order-isomorphism. Hence, ( (M_{1} ⇒ M_{2}), ⊑_{e}) is a Scott domain.^{15}

Proof. By Theorem 6.19, Fun is a bijection. Under the additional assumption of the corollary, t ⊑ t′ iff t ⋆ x ⊑ t′ ⋆ x for all x (by Extensionality) iff Fun(t)(x) ⊑ Fun(t′)(x) for all x (by Lemma 6.18).

15Interestingly the Berry-Curien stable ordering for this space coincides with the pointwise ordering [11].

6.2.2 The Exponent Object

The fact that the decision tree representation for manifestly sequential functions is extensional and that the tree domain is isomorphic to the function space of manifestly sequential functions provides the background for the definition of the exponent object and its related arrows, Λ and Λ^{−1}. The following definition is “operational” in that it defines currying and uncurrying as renaming operations for paths in the trees.

Definition 6.21 (Exponent Object, Λ) Let M_{i} be sds’s, and let (M_{i}) be their respective domains for i ∈ {0, 1, 2}. (M_{1} ⇒ M_{2}) is the exponent object for (M_{1}) and (M_{2}). For arbitrary (M_{2}), Λ : [ (M_{0} × M_{1}) ⟶ (M_{2})] ⟶ [ (M_{0}) ⟶ (M_{1} ⇒ M_{2})] and its inverse Λ^{−1} are defined as follows:

Λ(f) = Fun(Λ_{t}(Tree(f)))

where Λ_{t} : ((M_{0} × M_{1}) ⇒ M_{2}) ⟶ (M_{0} ⇒ (M_{1} ⇒ M_{2}))

Λ_{t}(x) = {Λ_{t}(p) | p ∈ x}

and Λ_{t}(p · ⟨p_{0}, 1⟩) = Λ_{t}(p) · ⟨π_{1}^{×}(p_{0}), 1⟩

if for some a ∈ A_{0}, p_{0} = ⟨a, 1⟩…
Λ_{t}(p · ⟨p_{1}, 1⟩) = Λ_{t}(p) · ⟨⟨π_{2}^{×}(p_{1}), 1⟩, 2⟩
if for some a ∈ A_{1}, p_{1} = ⟨a, 2⟩…
Λ_{t}(p · ⟨y, 2⟩) = Λ_{t}(p) · ⟨⟨y, 2⟩, 2⟩
Λ_{t}(p · e)  = Λ_{t}(p) · e
Λ^{−1}(g) = Fun(Λ_{t}^{−1}(Tree(g)))

where Λ_{t}^{−1} : (M_{0} ⇒ (M_{1} ⇒ M_{2})) ⟶ ((M_{0} × M_{1}) ⇒ M_{2})

Λ_{t}^{−1}(x) = {Λ_{t}^{−1}(p) | p ∈ x}

and Λ_{t}^{−1}(p · ⟨p_{0}, 1⟩)  = Λ_{t}^{−1}(p) · ⟨inj_{1}(p_{0}), 1⟩

Λ_{t}^{−1}(p · ⟨⟨p_{1}, 1⟩, 2⟩) = Λ_{t}^{−1}(p) · ⟨inj_{2}(p_{1}), 1⟩
Λ_{t}^{−1}(p · ⟨⟨y, 2⟩, 2⟩) = Λ_{t}^{−1}(p) · ⟨y, 2⟩
Λ_{t}^{−1}(p · e)  = Λ_{t}^{−1}(p) · e

To verify that the definition is correct, it suffices to check the appropriate equations with simple calculations.

Lemma 6.22 Let f ∈ (M_{0} × M_{1}) ⟶ (M_{2}) and let g ∈ (M_{0}) ⟶ (M_{1} ⇒ M_{2}). Then Λ(f) and Λ^{−1}(g) are manifestly sequential functions, and

1. Λ^{−1}(Λ(f)) = f;

2. Λ(Λ^{−1}(g)) = g;

3. Λ(f)(x_{0}) ⋆ x_{1} = f(inj_{1}(x_{0}) ∪ inj_{2}(x_{1})) for all x_{0} ∈ (M_{0}) and x_{1} ∈ (M_{1}); and

4. Λ(f) ∘ g = Λ(f ∘ ⟨g ∘ π_{1}, π_{2}⟩), for any g of correct type.

Proof. The validity of claims 1 and 2 clearly follows from the validity of analogous claims about Λ_{t}(Tree(f)) and Λ_{t}^{−1}(Tree(g)) due to Theorem 6.19, which, in turn, follow from the respective claims for paths. Finally, Λ_{t} and Λ_{t}^{−1} are obviously bijections for paths, i.e., for all paths p over (M_{0}×M_{1}) ⇒ M_{2}, Λ_{t}^{−1}(Λ_{t}(p)) = p; and for all paths p over M_{0} ⇒ (M_{1} ⇒ M_{2}), Λ_{t}(Λ_{t}^{−1}(p)) = p. The proof is by induction on the length of p.

The proof of claim 3 requires the verification of the following properties of a response p over (M_{0} × M_{1}) ⇒ M_{2} and its curried version Λ_{t}(p):

π_{1}^{×}(||π\overrightarrow{1}(p)||) = ||π\overrightarrow{1}(Λ_{t}(p))||
π_{2}^{×}(||π\overrightarrow{1}(p)||) = ||π\overrightarrow{1}(π\overrightarrow{2}(Λ_{t}(p)))||
π\overrightarrow{2}(p) = π\overrightarrow{2}(π\overrightarrow{2}(Λ_{t}(p)))

Again, a proof by an induction on the length of the response p verifies the three claims. The rest follows easily:

Λ(f)(x_{0}) ⋆ x_{1}
= Fun(Λ_{t}(Tree(f)))(x_{0}) ⋆ x_{1}
= Λ_{t}(Tree(f)) ⋆ x_{0} ⋆ x_{1}
= (\{π\overrightarrow{2}(r) | r ∈ Λ_{t}(Tree(f)), ||π\overrightarrow{1}(r)|| ⊑ x_{0}\}
∪ \{π\overrightarrow{2}(p) · e | p · ⟨q, 1⟩ ∈ Λ_{t}(Tree(f)), ||π\overrightarrow{1}(p)|| ∪ \{q · e\} ⊑ x_{0}\}) ⋆ x_{1}
= \{π\overrightarrow{2}(π\overrightarrow{2}(r)) | r ∈ Λ_{t}(Tree(f)), ||π\overrightarrow{1}(r)|| ⊑ x_{0}, ||π\overrightarrow{1}(π\overrightarrow{2}(r))|| ⊑ x_{1}\}
∪ \{π\overrightarrow{2}(π\overrightarrow{2}(p)) · e |
p · ⟨⟨q, 1⟩, 2⟩ ∈ Λ_{t}(Tree(f)), ||π\overrightarrow{1}(p)|| ⊑ x_{0}, ||π\overrightarrow{1}(π\overrightarrow{2}(p))|| ∪ \{q · e\} ⊑ x_{1}\}
∪ \{π\overrightarrow{2}(π\overrightarrow{2}(p)) · e |
p · ⟨q, 1⟩ ∈ Λ_{t}(Tree(f)), ||π\overrightarrow{1}(p)|| ∪ \{q · e\} ⊑ x_{0}, ||π\overrightarrow{1}(π\overrightarrow{2}(p))|| ⊑ x_{1}\}
= \{π\overrightarrow{2}(π\overrightarrow{2}(Λ_{t}(r))) | r ∈ Tree(f), ||π\overrightarrow{1}(Λ_{t}(r))|| ⊑ x_{0}, ||π\overrightarrow{1}(π\overrightarrow{2}(Λ_{t}(r)))|| ⊑ x_{1}\}
∪ \{π\overrightarrow{2}(π\overrightarrow{2}(Λ_{t}(p))) · e |

p · ⟨q, 1⟩ ∈ Tree(f), ||π\overrightarrow{1}(Λ_{t}(p))|| ⊑ x_{0}, ||π\overrightarrow{1}(π\overrightarrow{2}(Λ_{t}(p)))|| ∪ \{π_{2}^{×}(q) · e\} ⊑ x_{1}\}

∪ \{π\overrightarrow{2}(π\overrightarrow{2}(Λ_{t}(p))) · e |

p · ⟨q, 1⟩ ∈ Tree(f), ||π\overrightarrow{1}(Λ_{t}(p))|| ∪ \{π_{1}^{×}(q) · e\} ⊑ x_{0}, ||π\overrightarrow{1}(π\overrightarrow{2}(Λ_{t}(p)))|| ⊑ x_{1}\}

= \{π\overrightarrow{2}(r) | r ∈ Tree(f), π_{1}^{×}(||π\overrightarrow{1}(r)||) ⊑ x_{0}, π_{2}^{×}(||π\overrightarrow{1}(r)||) ⊑ x_{1}\}
∪ \{π\overrightarrow{2}(p) · e |
p · ⟨q, 1⟩ ∈ Tree(f), π_{1}^{×}(||π\overrightarrow{1}(p)||) ⊑ x_{0}, π_{2}^{×}(||π\overrightarrow{1}(p)||) ∪ \{π_{2}^{×}(q) · e\} ⊑ x_{1}\}
∪ \{π\overrightarrow{2}(p) · e |
p · ⟨q, 1⟩ ∈ Tree(f), π_{1}^{×}(||π\overrightarrow{1}(p)||) ∪ \{π_{1}^{×}(q) · e\} ⊑ x_{0}, π_{2}^{×}(||π\overrightarrow{1}(p)||) ⊑ x_{1}\}
= \{π\overrightarrow{2}(p) | p ∈ Tree(f), ||π\overrightarrow{1}(r)|| ⊑ inj_{1}(x_{0}) ∪ inj_{2}(x_{1})\}
∪ \{π\overrightarrow{2}(p) · e | p · ⟨q, 1⟩ ∈ Tree(f), ||π\overrightarrow{1}(p)|| ∪ \{q · e\} ⊑ inj_{1}(x_{0}) ∪ inj_{2}(x_{1})\}

= Tree(f) ⋆ (inj_{1}(x_{0}) ∪ inj_{2}(x_{1}))
= f(inj_{1}(x_{0}) ∪ inj_{2}(x_{1}))

By claim 3, currying and uncurrying as defined are just the set-theoretic currying and uncurrying functions, hence the equation of claim 4 holds in SEQ since it holds in the category of sets.

7 Full Abstraction for SPCF

Both SEQ( ) and Seq( ) can serve as the basis of a fully abstract semantics for SPCF. Unfortunately, working with the elements in the domains of either category imposes a heavy notational overhead. To overcome this problem, we introduce some additional notation.

Consider the meaning of add1 in SEQ( ). It is the arrow f : 1 ⟶ (N ⇒ N), and in Seq( ) it is the arrow f′ : 1 ⟶ (N ⇒ N) where

f′ ⋆ x = f(x) = A = {⟨?, 2⟩ · ⟨?, 1⟩, ⟨?, 2⟩ · ⟨?, 1⟩ · ⟨?n, 1⟩ · ⟨?m, 2⟩ | m, n ∈ , m = n + 1}

for the unique element x in 1. Similarly, the procedure if0 is the arrow that produces the following element

\{ \begin{matrix}⟨⟨⟨?, 2⟩, 2⟩, 2⟩ · ⟨?, 1⟩, \\ ⟨⟨⟨?, 2⟩, 2⟩, 2⟩ · ⟨?, 1⟩ · ⟨? · 0, 1⟩ · ⟨⟨?, 1⟩, 2⟩, \\ ⟨⟨⟨?, 2⟩, 2⟩, 2⟩ · ⟨?, 1⟩ · ⟨? · 0, 1⟩ · ⟨⟨?, 1⟩, 2⟩ · ⟨⟨? · m, 1⟩, 2⟩ · ⟨⟨⟨? · m, 2⟩, 2⟩, 2⟩, \\ ⟨⟨⟨?, 2⟩, 2⟩, 2⟩ · ⟨?, 1⟩ · ⟨? · n, 1⟩ · ⟨⟨?, 1⟩, 2⟩, \\ ⟨⟨⟨?, 2⟩, 2⟩, 2⟩ · ⟨?, 1⟩ · ⟨? · n, 1⟩ · ⟨⟨?, 1⟩, 2⟩ · ⟨⟨? · m, 1⟩, 2⟩ · ⟨⟨⟨? · m, 2⟩, 2⟩, 2⟩ \end{matrix} | n > 0 \}

in (N ⇒ N ⇒ N ⇒ N) upon application to the single element of 1. To simplify the definition of SPCF’s semantics and the proofs about the semantics, we first introduce some notational abbreviations before we specify some trees that are common to both semantics.

Since all SPCF types τ have the shape

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

the interesting domains are generated by sds’s of the shape

M = M_{1} ⇒ … M_{k} ⇒ N

where M_{i} is the sds that corresponds to τ_{i} and N is the sds that generates _{⊥}^{e}, the flat domain of natural numbers and errors (cmp. the examples following Definition 5.1). By the definition of the exponent construction, all paths over (M) start with the initial address

⟨… ⟨?, \underbrace{2⟩,…, 2⟩}_{k} .

Below we use ⟨?⟩ as an abbreviation for this address, unless k = 0. Similarly, a maximal path in (M) ends in e ∈ or in

⟨… ⟨? · n, \underbrace{2⟩,…, 2⟩}_{k},

= (M_{1} ⇒ … M_{k} ⇒ N) where M_{i} = M_{i,1} ⇒ … M_{i,k_{i}} ⇒ N

⟨?⟩ = ⟨… ⟨?, \underbrace{2⟩,…, 2⟩}_{k}
⟨n⟩ = ⟨… ⟨? · n, \underbrace{2⟩,…, 2⟩}_{k}
⟨p, i⟩ = ⟨… ⟨p, 1⟩, \underbrace{2⟩,…, 2⟩}_{i−1}  π_{i}(p) = π\overrightarrow{1}(\underbrace{π\overrightarrow{2}(… π\overrightarrow{2}}_{i−1}(p) …)
⟨?, i⟩ = ⟨⟨?⟩, i⟩

Figure 5: Abbreviations for domain elements in an SPCF domain

for n ∈ . We will use ⟨n⟩ to denote this datum. Finally, the intermediate queries and responses of a path in (M) are about elements in (M_{1}) through (M_{k}) and, for domain (M_{i}) have the shape

⟨… ⟨p, 1⟩, \underbrace{2⟩,…, 2⟩}_{i−1},

for 1 ≤ i ≤ k. The abbreviation ⟨p, i⟩ will stand for the above. For the very first query about the ith argument, we use ⟨?, i⟩ instead of ⟨⟨?⟩, i⟩. To extract the path p from ⟨p, i⟩ we use the function π_{i}, which is the composition of π\overrightarrow{1} with the (i − 1)-fold composition of π\overrightarrow{2}.

Warning: When encountering the abbreviations below, the reader should keep in mind that the implicit parameter k is a context-sensitive entity.

Using the newly introduced abbreviations, we turn to the definition of trees that characterize the denotations of add1, sub1, if0, and catch.

Definition 7.1 (A, S, I, C ) Let M_{1},…, M_{k} be arbitrary sds’s. Then the constants

A, S ∈ (N ⇒ N)
I ∈ (N ⇒ N ⇒ N ⇒ N)
C_{k} ∈ ((M_{1} ⇒ … ⇒ M_{k} ⇒ N) ⇒ N)

are defined as follows:

A = { ⟨?⟩ · ⟨?, 1⟩, ⟨?⟩ · ⟨?, 1⟩ · ⟨?n, 1⟩ · ⟨m⟩ | m, n ∈ , m = n + 1 }
S = { ⟨?⟩ · ⟨?, 1⟩, ⟨?⟩ · ⟨?, 1⟩ · ⟨?n, 1⟩ · ⟨m⟩ | m, n ∈ , m + 1 = n }

I = \{ \begin{matrix}⟨?⟩ · ⟨?, 1⟩, \\ ⟨?⟩ · ⟨?, 1⟩ · ⟨? · 0, 1⟩ · ⟨?, 2⟩, \\ ⟨?⟩ · ⟨?, 1⟩ · ⟨? · 0, 1⟩ · ⟨?, 2⟩ · ⟨? · m, 2⟩ · ⟨m⟩, \\ ⟨?⟩ · ⟨?, 1⟩ · ⟨? · n, 1⟩ · ⟨?, 3⟩, \\ ⟨?⟩ · ⟨?, 1⟩ · ⟨? · n, 1⟩ · ⟨?, 3⟩ · ⟨? · m, 3⟩ · ⟨m⟩ \end{matrix} | n, m ∈ , n > 0\}

C_{k} = \{ \begin{matrix}⟨?⟩ · ⟨?, 1⟩, \\ ⟨?⟩ · ⟨?, 1⟩ · ⟨⟨?⟩ · ⟨?, i⟩, 1⟩ · ⟨i − 1⟩, \\ ⟨?⟩ · ⟨?, 1⟩ · ⟨⟨n⟩, 1⟩ · ⟨k + n⟩ \end{matrix} | n, i ∈ , 1 ≤ i ≤ k\}

While the definitions for A and S are obvious, those for I and C_{k} deserve some additional explanation. I represents a function that contains the following evaluation strategy. First, it announces that it will fill the only address ? in the output space and then probes its first argument. If it is 0, it probes the second argument and puts its answer at the end of the output path; if not, it probes the third argument and continues as before. As for C_{k}, it also probes its first argument. If the argument is a constant function that would return n, C_{k} returns k + n. If the argument represents a function that is strict in its ith argument, then C_{k} returns i − 1.

We are now ready to define the semantics of SPCF.

Definition 7.2 (Seq and SEQ Semantics of SPCF ) Let be a set of error values.

If ≠ ∅, the underlying cartesian-closed category of SPCF’s SEQ semantics is SEQ( ). The ground type o is interpreted as the domain _{⊥}^{e}:

C^{o} = (N).

The SEQ semantics assigns the following meaning to constants:

SEQ[[ e ]] = \underline{λ}ρ : 1.e  for e ∈
SEQ[[^{⌈}n^{⌉}]] = \underline{λ}ρ : 1.n
SEQ[[ add1 ]] = \underline{λ}ρ : 1.A
SEQ[[ sub1 ]] = \underline{λ}ρ : 1.S
SEQ[[ if0 ]] = \underline{λ}ρ : 1.I
SEQ[[ catch_{k}]] = \underline{λ}ρ : 1.C_{k}

The meaning of terms in the SEQ semantics are functions that map n-tuples or environments to elements in the appropriate domain. To avoid notational clutter, we use tuple notation for environments: if M’s free variables are among x_{1}^{τ_{1}} … x_{k}^{τ_{k}}, we write

SEQ[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ M ]]⟨x_{1},…, x_{k}⟩

for

SEQ[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ M ]]ρ

where x_{i} = π_{1}^{×}(\underbrace{π_{2}^{×}(… π_{2}^{×}}_{i−1}(ρ) …)) for arbitrary x_{i} ∈ SEQ^{τ_{i}}.

For arbitrary , the underlying cartesian-closed category of SPCF’s Seq semantics is Seq( ). The ground type o is interpreted as _{⊥}^{e}:

C^{o} = (N).

The Seq semantics assigns the following meaning to constants:

Seq[[ e ]] = {⟨?, 2⟩ · e}
Seq[[^{⌈}n^{⌉}]] = {⟨?, 2⟩ · ⟨n, 2⟩})
Seq[[ add1 ]] = {⟨b_{1}, 2⟩ ·. . . · ⟨b_{n}, 2⟩ | b_{1} ·. . . · b_{n} ∈ A}
Seq[[ sub1 ]] = {⟨b_{1}, 2⟩ ·. . . · ⟨b_{n}, 2⟩ | b_{1} ·. . . · b_{n} ∈ S}
Seq[[ if0 ]] = {⟨b_{1}, 2⟩ ·. . . · ⟨b_{n}, 2⟩ | b_{1} ·. . . · b_{n} ∈ I}
Seq[[ catch_{k}]] = {⟨b_{1}, 2⟩ ·. . . · ⟨b_{n}, 2⟩ | b_{1} ·. . . · b_{n} ∈ I}

The meaning of terms in the Seq semantics are algorithms that input n-tuples and output elements in the appropriate domain. Again, we use ordinary tuple notation for these environments.

We use Seq^{}[[ · ]] when we need to distinguish between two Seq semantics based on different error sets.

For ≠ ∅, we interchangeably use the SEQ and Seq semantics for SPCF since

Fun(Seq[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ M ]]) = SEQ[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ M ]]

for all SPCF terms M whose free variables are among x_{1}^{τ_{1}} … x_{k}^{τ_{k}}. Similarly, for a term that does not explicitly mention error, it does not matter which error set we choose to determine its Seq semantics.

Lemma 7.3 For all SPCF(∅) terms M (that is, a term that does not contain error constants) whose free variables are among x_{1}^{τ_{1}} … x_{k}^{τ_{k}} then for any ,

Seq^{}[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ M ]] = Seq^{∅}[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ M ]].

Proof. The proof proceeds by induction on the structure of M .

Moreover, SPCF is PCF-like.

Proposition 7.4 If M is a PCF program, then

Dom[[ ∅ ⊢ M ]] ⊥= Seq[[ ∅ ⊢ M ]]⋆ ⊥= SEQ[[ ∅ ⊢ M ]] ⊥ .

Proof. The theorem follows from the operational adequacy theorem (Theorem 8.13 in the following section), from Plotkin’s operational adequacy theorem for the continuous semantics [24:Theorem 3.1], and a simple check that the two versions of the operational semantics agree on PCF.

Next we can show that SPCF is sequential and propagates errors as expected, i.e., that it is an observably sequential programming language. The proof relies on the results in the preceding section and on Lemma 3.6, which states that a semantics based on cartesian-closed categories satisfies (β).

Theorem 7.5 SPCF is sequential, manifestly sequential (if ≠ ∅), and observably 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 3.9:

(i): SEQ[[ ⊢ C[M_{1},…, M_{k}] ]] ∈ ∪ ;

(ii): SEQ[[ ⊢ C[Ω,…, Ω] ]] =⊥.

We must show that there is an argument position j that forces divergence. Since the semantics satisfies the equation β, we have:

SEQ[[ ⊢ C[M_{1},…, M_{k}] ]] ⊥
= SEQ[[ ⊢ ((λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.C[x_{1},…, x_{k}]) M_{1} … M_{k}) ]] ⊥
= SEQ[[ ⊢ (λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.C[x_{1},…, x_{k}]) ]] ⊥ ⋆SEQ[[ M_{1} ]] ⊥ ⋆… ⋆ SEQ[[ M_{k}]] ⊥

Now consider the possible denotations of the k-ary procedure

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

The denotation of such a procedure is either a decision tree of the shape

{⟨?⟩ · ⟨d⟩}

for d ∈ ∪ or a decision tree that contains the path

⟨?⟩ · ⟨?, j⟩

for some j ≤ k. Clearly, the first case contradicts assumption (ii). The second case specifies that the k-ary procedure first probes its j th argument. But this fact implies that

SEQ[[ ⊢ C[M′_{1},…, M′_{j},…, M′_{k}] ]]
= SEQ[[ ⊢ λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.C[x_{1},…, x_{k}] ]] ⊥
⋆SEQ[[ ⊢ M′_{1} ]] ⊥ ⋆… ⋆ SEQ[[ ⊢ M′_{j}]] ⊥ ⋆… ⋆ SEQ[[ ⊢ M′_{k}]] ⊥
= ⊥

for M′_{j} = Ω and arbitrary M′_{i}, i ≠ j. More concisely, the program diverges if the expression M_{j} in j th hole diverges—regardless of the expressions in the other holes. Hence, j is the desired sequentiality index.

The proof that SPCF programs also propagate errors that occur at the sequentiality index proceeds in precisely the same manner. And finally, given λx_{1} … x_{k}.C[x_{1},…, x_{k}], the context D[ ] = (add1 (catch [ ])) produces the sequentiality index. Hence, SPCF satisfies the conditions of Definition 4.2, which shows that it is a manifestly sequential and observably sequential language.

After establishing the basic properties of SPCF’s semantics, we are ready to prove that the semantics are fully abstract.

Theorem 7.6 (Full Abstraction) For all error sets ,

1. M ⊑_{Seq} N iff M ∼ N and M ≡_{Seq} N iff M ≃ N;

2. if ≠ ∅, M ⊑_{SEQ} N iff M ∼ N and M ≡_{SEQ} N iff M ≃ N.

Note. We concentrate on the proof of the theorem’s second part, indicating differences to the proof of the first part as we proceed. Proof. The left to right direction follows from the compositional definition of the semantics. For the right to left direction, assume M⋢_{SEQ}N (both are closed and of type τ). We will prove that M≁N.

By the Discriminator Lemma (7.7), there exists a finite, error-free discriminator F of type τ → o such that F ⋆ SEQ[[ ⊢ M ]] ⊥⋢ F ⋆ SEQ[[ ⊢ N ]] ⊥. It follows from the Representability Lemma (7.8) that there is a term D such that SEQ[[ ⊢ D]] = F (Seq[[ ⊢ D]] = F). Thus,

SEQ[[ ⊢ (D M) ]] ⋢ SEQ[[ ⊢ (D N) ]],

(Seq[[ ⊢ (D M) ]] ⋢ Seq[[ ⊢ (D N) ]]) which implies M ≁ M′ as desired.

For open terms, it suffices to point out that if x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} are all the free variables in M and N , then M ∼ N implies λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.M ∼ λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.N, which by the preceding arguments for closed terms is equivalent to λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.M ⊑_{SEQ} λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.N and hence, M ⊑_{SEQ} N [24].

Lemma 7.7 (Discriminator) If f, g are elements in SEQ^{τ} (Seq^{τ}) and f ⋢ g then for some finite, error-free F ∈ ^{τ→o}, F ⋆ f ⊑ F ⋆ g. Moreover, by monotonicity, f ⊑ g if and only if for all finite F ∈ ^{τ→o}, F ⋆ f ⊑ F ⋆ g.

Proof. Assume f ⋢ g. From this it follows that there is some minimal response r ∈ f such that r ∉ g: for any r′ ⊑ r, r′ ∈ g. Let r_{1},…, r_{n} be the prefixes of r such that r_{1} ⊑ … ⊑ r_{n} = r, let q_{i} be the query that is the immediate predecessor of r_{i}, and set

F^{∗} = ⟨?, 2⟩ · ⟨q_{1}, 1⟩ · ⟨r_{1}, 1⟩ ·. . . · ⟨q_{n}, 1⟩ · ⟨r_{n}, 1⟩ · ⟨0, 2⟩.

Then if r does not end in an error, F is the prefix-closure of F^{∗}, i.e., F = {r ⊑ F^{∗}} . As a function, F explores its argument and determines whether the argument contains r. If so, the argument dominates f and F returns 0 (F ⋆ f = {? · 0}); otherwise it is undefined or propagates errors (F ⋆ g =⊥ or F ⋆ g = {? · e}).

If r = q · e, the discriminator is the prefix-closure of the shorter path

F^{&} = ⟨?, 2⟩ · ⟨q_{1}, 1⟩ · ⟨r_{1}, 1⟩ ·. . . · ⟨q_{n}, 1⟩.

Again F checks whether r ∈ f but, if so, it returns e (F ⋆ f = {? · e}). If F does not find r, it is undefined or propagates a different error.

Thus, in both cases, F ⋆ f ⋢ F ⋆ g, which is what the the lemma claims.

Lemma 7.8 (Representability) Let τ = τ_{1} → … → τ_{k} → o for k ≥ 0. If x is a finite tree in SEQ^{τ} (Seq^{τ}) , then there is a closed SPCF phrase M such that SEQ[[ ⊢ M ]] ⊥= x (Seq[[ ⊢ M ]]⋆ ⊥= x).

Proof. Due to its length, we have subdivided the proof into several parts.

Generalizing the Claim. The proof of the lemma is a lexicographic induction on the depth of the type τ and the cardinality of the element x, where the depth of ground type o is 1, the depth of τ_{1} → … τ_{k} → o is 1 + max{depth(τ_{i}) | 1 ≤ i ≤ k}. The term M that we shall construct will have the shape

λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.L

for some term L. Given the knowledge of how to construct L′ for some x′ below x, we will need to construct a term L that is like L′ except for the code that accounts for the differences between x and x′. Put differently, we will need to keep track of places in the code that are due to occurrences of ⊥ in some tree x′ so that we know how to modify the code for extensions of x′ that replace these occurrences of ⊥. To accomplish this bookkeeping task, we will use a partitioning of M into contexts and holes filled with Ω. The generalized induction hypothesis is as follows:

Given a finite tree x in the semantic domain associated with the type τ = τ_{1} → … τ_{k} → o, and an arbitrary finite set Q of open queries, i.e., Q ⊆ Open(x), there exists a term

M = λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.L

such that there is an injection from Q to the set of contexts with a single hole, satisfying the following condition:

If q ∈ Q is associated with C[ ], then

M = C[Ω^{o}]

and for all terms N (of ground type) whose free variables are among x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, for all finite x_{i} ∈ SEQ^{τ_{i}} (where 1 ≤ i ≤ k),

SEQ[[ ⊢ C[N] ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} = \{ \begin{matrix}SEQ[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ N ]]⟨x_{1},…, x_{k}⟩ \\ if ||π_{i}(q)|| ⊑ x_{i}, for all i \\ x ⋆ x_{1} ⋆… ⋆ x_{k} \\ if ||π_{i}(q)|| ⋢ x_{i}, for some i \end{matrix} (‡)

Given an element x and its term M , we say that M can grow in the direction of all q ∈ Q.

The condition (‡) has a simple intuitive explanation: If M is applied to arguments that have responses to all the queries on the path from the root of x to the occurrence of ⊥ represented by C[ ], then the only relevant part of the code is the filler of the hole; otherwise, the application has the same meaning as an application of x to the arguments. The condition implies that M represents x. To see this, set N = Ω. Since M = C[Ω] the claim clearly holds if for some i, ||π_{i}(q)|| ⋢ x_{i}. Thus, assume ||π_{i}(q)|| ⊑ x_{i}, for all i. Then

SEQ[[ ⊢ M ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k}
= SEQ[[ ⊢ C[Ω] ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k}
= SEQ[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ Ω ]]⟨x_{1},…, x_{k}⟩
= ⊥ .

On the other hand, it is also straightforward to see that

x ⋆ x_{1} ⋆… ⋆ x_{k} =⊥ .

For the application to contain ? · n or ? · e, the element x would have to have a path r such that ||π_{i}(r)|| ⊑ x_{i} for all i and (π\overrightarrow{2})^{k}(q) =? (π\overrightarrow{2})^{k}(r), which by a k-fold application of Lemma 6.13 would imply q r in contradiction to q ∈ Open(x). By extensionality we may conclude that

SEQ[[ M ]] ⊥= x.

Base Case. If x is empty, a valid representation is

M = λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.Ω.

The only open query, q = ⟨?⟩, for x maps to λx_{1}^{τ_{1}} … x_{k}^{τ_{k}}.[ ]. The injection obviously satisfies condition (‡).

Induction Step. If x is not empty and Q ⊆ Open(x), we can pick an x′ that is immediately below x, i.e., there is some x′ such that for some query q′ ∈ Open(x′) and datum d,

x = x′ ∪ {q′ · d}.

Let Q^{−} = {q ∈ Q | q′ ⊑ q} and let Q^{+} = Q \ Q^{−} ∪ {q′}. By inductive hypothesis, some term M′ represents x′ relative to the set Q^{+}, q′ is associated with a unique context C[ ] that satisfies condition (‡) and, in particular, M′ = C[Ω]. Clearly, to turn into M, M′ must grow in the direction of q′. But, to determine the precise replacement for the Ω term in the hole of C[ ], we need to give consideration to the two possible origins of the datum d.

Induction Step: Numbers and Errors. First, if d = ⟨n⟩ or d = e, set

M = C[^{⌈}n^{⌉}] or M = C[e],

respectively. To prove the appropriateness of this choice, we concentrate on the first case; the proof for the error case proceeds in an analogous fashion.

Since q′ · ⟨n⟩ is maximal in x, any q ∈ Q is also in Q^{+}. By the inductive hypothesis for x′ and Q^{+}, there is a context C′ with two holes such that: (i) C[ ] = C′[ ]_{1}[Ω]_{2} and therefore M′ = C′[Ω]_{1}[Ω]_{2}; and (ii) q is associated with the context C′[Ω]_{1}[ ]_{2}. We claim that for x and Q, q is associated with C′[^{⌈}n^{⌉}]_{1}[ ]_{2}.

Associating C′[^{⌈}n^{⌉}]_{1}[ ]_{2} with q satisfies (‡). We analyze each of the two parts of the constraint individually. Let N be an expression of ground type whose free variables are among x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}. Let x_{1} ∈ SEQ^{τ_{1}}, …, x_{k} ∈ SEQ^{τ_{k}} be the denotations of these variables.

1. Suppose that ||π_{i}(q)|| ⊑ x_{i} for all i. We need to prove that for all N ,

SEQ[[ ⊢ C′[^{⌈}n^{⌉}]_{1}[N]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} = SEQ[[ ⊢ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ N ]]⟨x_{1},…, x_{k}⟩.

By inductive hypothesis for x′ and Q^{+}, mapping q to C′[Ω]_{1}[ ]_{2} satisfies (‡) and, thus,

SEQ[[ ⊢ C′[Ω]_{1}[N]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} = SEQ[[ ⊢ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ N ]]⟨x_{1},…, x_{k}⟩

for arbitrary N . By induction on the types τ_{1} through τ_{k}, whose depth is smaller than τ’s depth, we can find terms P_{1}, …, P_{k} denoting x_{1}, …, x_{k}. Hence,

SEQ[[ ⊢ (C′[Ω]_{1}[N]_{2} P_{1} … P_{k}) ]] ⊥ .
= SEQ[[ ⊢ C′[Ω]_{1}[N]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k}
= SEQ[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ N ]]⟨x_{1},…, x_{k}⟩

Thus, for N, N′ with free variables among x_{1}^{τ_{1}} … x_{k}^{τ_{k}}, then, by monotonicity,

SEQ[[ ⊢ C′[N′]_{1}[N]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} = n

if SEQ[[ ⊢ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ N ]]⟨x_{1},…, x_{k}⟩ = n ≠⊥.

If N denotes ⊥ in the given environment, the equation also implies that

SEQ[[ ⊢ C′[Ω]_{1}[Ω]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} =⊥,

By the sequentiality of SPCF (see Theorem 7.5), the second hole of C′[ ]_{1}[ ]_{2} is the syntactic sequentiality index of the program. Hence,

SEQ[[ ⊢ (C′[N′]_{1}[N]_{2} P_{1} … P_{k}) ]] ⊥= SEQ[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ N ]]⟨x_{1},…, x_{k}⟩ =⊥

for any N′ and, in particular, for N′ = ^{⌈}n^{⌉}. In conclusion, for all possible N ,

SEQ[[ ⊢ (C′[^{⌈}n^{⌉}]_{1}[N]_{2} P_{1} … P_{k}) ]] ⊥= SEQ[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ N ]]⟨x_{1},…, x_{k}⟩,

which is the desired conclusion.

2. Suppose that ||π_{i}(q)|| ⋢ x_{i} for some i. In this case, the goal is to prove

SEQ[[ ⊢ C′[^{⌈}n^{⌉}]_{1}[N]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} = x ⋆ x_{1} ⋆… ⋆ x_{k}.

Depending on whether or not the information in the arguments demands the evaluation of the contents of the first hole, which is associated with q′, we must distinguish two subcases:

(a) If ||π_{i}(q′)|| ⊑ x_{i} for all i, then by inductive hypothesis for x′ and Q^{+}, the association of q′ with C′[ ]_{1}[Ω] satisfies condition (‡):

SEQ[[ ⊢ C′[^{⌈}n^{⌉}]_{1}[Ω]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} = SEQ[[ x_{1}^{τ_{1}} … x_{k}^{τ_{k}} ⊢ ^{⌈}n^{⌉}]]⟨x_{1},…, x_{k}⟩
= {? · n}
= (x′ ∪ {q′ · ⟨n⟩}) ⋆ x_{1} ⋆… ⋆ x_{k}
= x ⋆ x_{1} ⋆… ⋆ x_{k}.

The proof goal now follows from monotonicity.

(b) Assume ||π_{i}(q′)|| ⋢ x_{i} for some i. By the inductive hypothesis for x′ and Q^{+} the association of q′ with C′[ ]_{1}[Ω] as well as the association of q with C′[Ω][ ]_{2} satisfy condition (‡). Thus,

\begin{aligned}SEQ[[ C′[Ω]_{1}[N]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} & = & x′ ⋆ x_{1} ⋆… ⋆ x_{k} & (∗) \\ SEQ[[ ⊢ C′[L]_{1}[Ω]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} & = & x′ ⋆ x_{1} ⋆… ⋆ x_{k} & (∗∗) \end{aligned}

for all N and L (whose free variables are among x_{1}^{τ_{1}}, …, x_{k}^{τ_{k}}). Moreover, by a simple argument,

x′ ⋆ x_{1} ⋆… ⋆ x_{k} = (x′ ∪ {q′ · ⟨n⟩}) ⋆ x_{1} ⋆… ⋆ x_{k}
= x ⋆ x_{1} ⋆… ⋆ x_{k}

The rest depends on the result of x ⋆ x_{1} ⋆… ⋆ x_{k}:

i. x ⋆ x_{1} ⋆… ⋆ x_{k} ≠⊥: Equation (∗) implies the result by monotonicity.

ii. x ⋆ x_{1} ⋆ … ⋆ x_{k} =⊥: By instantiating N and L in equations (∗) and (∗∗) appropriately, we can determine three equations about the program:

SEQ[[ ⊢ C′[Ω]_{1}[e]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} = ⊥
SEQ[[ ⊢ C′[e]_{1}[Ω]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} = ⊥
SEQ[[ ⊢ C′[Ω]_{1}[Ω]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} = ⊥

By manifest sequentiality and the first two equations, neither hole in the context C′[ ]_{1}[ ]_{2} can be a sequentiality index. By sequentiality and the third equation, for all L and N :

SEQ[[ ⊢ C′[L]_{1}[N]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} =⊥,

In particular, for all N ,

SEQ[[ ⊢ C′[^{⌈}n^{⌉}]_{1}[N]_{2} ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} =⊥= x ⋆ x_{1} ⋆… ⋆ x_{k}.

This concludes the proof that for any q ∈ Q, we have a context that satisfies (‡), which shows that the inductive claim holds for M, x, and the injection of queries from Q to contexts.

Induction Step: Subtrees. Second, d = ⟨q^{∗}, i⟩, i.e., d is a query about the ith argument. Let q_{1},…, q_{m+n} be all the queries in Q that dominate q′ · ⟨q^{∗}, i⟩; they are the ones that contribute to the construction of M . By the construction of the exponent sds, all of these queries extend q′ · ⟨q^{∗}, i⟩ with a response:

q_{1} = q′ · ⟨q^{∗}, i⟩ · ⟨r_{1}, i⟩

…

q_{m} = q′ · ⟨q^{∗}, i⟩ · ⟨r_{m}, i⟩
q_{m+1} = q′ · ⟨q^{∗}, i⟩ · ⟨r_{m+1}, i⟩

…

q_{m+n} = q′ · ⟨q^{∗}, i⟩ · ⟨r_{m+n}, i⟩

[figure: root of x; ⊥; …; ⊥; ⊥; …; ⊥; q′; ⟨q^{∗}, i⟩; r_{1}; r_{m}; r_{m+1}; r_{m+n}; } Q^{−}]

Figure 6: The Induction Step (Subtrees) of the Representability Lemma

The possible responses to ⟨q^{∗}, i⟩ fall into two distinct classes: q_{1},…, q_{m} and q_{m+1},…, q_{m+n}. The first m responses are query responses, that is, the ith argument demands more information about its possible inputs. Assuming that

τ_{i} = σ_{1} → … σ_{l} → o for l ≥ 0,

the responses have the shape

r_{1} = q^{∗} · ⟨p_{1}, i_{1}⟩

…

r_{m} = q^{∗} · ⟨p_{m}, i_{m}⟩

where p_{1},…, p_{m} are queries for arguments i_{1},…, i_{m}, respectively, and 1 ≤ i_{1},…, i_{m} ≤ l. The responses in the second set are final responses. They correspond to cases in which the ith argument does not demand more information about its arguments and simply returns an answer in . They have the form:

r_{m+1} = q^{∗} · ⟨a_{1}⟩

…

r_{m+n} = q^{∗} · ⟨a_{n}⟩

where a_{1},…, a_{n} ∈ . The picture in Figure 6 provides a concise overview of the situation.

Now we need to construct a term N^{∗} such that C[N^{∗}] denotes x. By the inductive hypothesis for x′ (and Q^{+}), we know that if x_{1},…, x_{k}, the arguments to M , dominate the information in q′, then the meaning of M is the meaning of N^{∗} and the query q^{∗} is open or answered in x_{i}. The program should then probe the ith argument and determine which of the m + n responses x_{i} dominates, if any. Based on this probe, N^{∗} can perform a dispatch according to the answer and diverge by evaluating Ω. Thus, a rough outline of N^{∗} is

let w = “probe argument x_{i}” in

(if0 “w indicates r_{1} ∈ x_{i}” Ω  ; [1]

… ;

(if0 “w indicates r_{m} ∈ x_{i}” Ω  ; [m]
(if0 “w indicates r_{m+1} ∈ x_{i}” Ω  ; [m + 1]

… ;

(if0 “w indicates r_{m+n} ∈ x_{i}” Ω  ; [m + n]

Ω) …)) …) ;

where the expression (let w = L in K) abbreviates ((λw.K) L). The first m + n new Ω terms in C[N^{∗}] correspond to the m + n new open queries in whose direction M can grow. Specifically, the Ω term on line [j] indicates where M must grow for a tree y that extends x in the direction of the query q′ · ⟨q^{∗}, i⟩⟨r_{j}, i⟩ for j, 1 ≤ j ≤ m + n.

A naïve way of probing x_{i} is to apply it to the arguments ||π_{1}(q^{∗})||,…, ||π_{l}(q^{∗})||, that is, the information in q^{∗} about the arguments of x_{i}. Since σ_{i}, the type of ||π_{i}(q^{∗})||, is smaller than τ, the inductive hypothesis implies that there is a term A_{i} that represents ||π_{i}(q^{∗})||. Hence a syntactic representation of the probe expression would be the application

(x_{i}^{τ_{i}} A_{1} … A_{l}).

As long as x_{i} dominates a final response, say, r_{m+j} for 1 ≤ j ≤ n, the naïve way of probing x_{i} works. The probe will evaluate to a_{j} (in ), and it is easy to dispatch to the right branch in the following if0-expression. However, if x_{i} contains some query response, say, r_{j} = q^{∗} · ⟨p_{j}, i_{j}⟩, then it ends up issuing a query asking for more information about its i_{j}th argument. Since the expression A_{i_{j}} only encodes the information embedded in q^{∗}, i.e., p_{j} ∈ Open(π_{i_{j}}(q^{∗})), this last action will cause the entire probe to diverge.

To get around the “over-exploration” of arguments to x_{i}, we need to define variants B_{1},…, B_{l} of the arguments A_{1},…, A_{l} such that each variant B_{h} initiates a non-local exit from the application (x_{i}^{τ_{i}} B_{1} … B_{l}) whenever x_{i} asks for information in the direction of any of the responses r_{1},…, r_{m}. In SPCF the catch operator, when applied to an appropriate procedure, can simulate a non-local exit. Thus, to implement our ideas in SPCF, the expression (x_{i}^{τ_{i}} B_{1} … B_{l}) needs to be parameterized such that it demands its j th argument precisely when x_{i} dominates r_{j}. Call the resulting procedure N^{@}. Then by applying the catch operator to N^{@}, the program can determine which query or which final response x_{i} dominates and can thus branch to the correct line in N^{∗}.

Expressed formally, we must define a λ-abstraction

N^{@} = λy_{1}^{o}… y_{m}^{o}.(x_{i}^{τ_{i}} B_{1} … B_{l})

that satisfies the following condition:

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ N^{@} ]]⟨x_{1},…, x_{k}⟩ = \{ \begin{matrix}\{⟨?⟩ · ⟨?, j⟩\} & if r_{j} ∈ x_{i} \\ & for some j, 1 ≤ j ≤ m \\ \{⟨?⟩ · ⟨a⟩\} & if q^{∗} · ⟨a⟩ ∈ x_{i}, a ∈ \end{matrix}

Then:

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ (catch N^{@}) ]]⟨x_{1},…, x_{k}⟩ = \{ \begin{matrix}\{? · (j − 1)\} & if r_{j} ∈ x_{i} \\ \{? · (a + m)\} & if q^{∗} · ⟨a⟩ ∈ x_{i} \\ \{? · e\} & if q^{∗} · e ∈ x_{i} \\ ⊥ & otherwise \end{matrix}

The last two parts are implied by sequentiality and manifest sequentiality.

The key to constructing N^{@} is defining the expressions B_{1},…, B_{l}. Each expression B_{h} must evaluate the variable y_{j}^{o} if r_{j} ∈ x_{i}. In addition, each expression B_{h} must satisfy the constraint ||π_{h}(q^{∗})|| ⊑ SEQ[[ y_{1}^{o},…, y_{s}^{o} ⊢ B_{h}]]⟨y_{1},…, y_{s}⟩ for arbitrary y_{1},…, y_{s}. Since the construction of the expression is complicated, we assume for the moment that we can construct the argument expressions B_{1},…, B_{l} and continue with the rest of the construction of N^{@}.

Given the expression N^{@}, N^{∗} is easy to construct. Since the application (catch N^{@}) yields an encoding of the index j of x_{i}’s response r_{j} (if any), N^{∗} can branch to the correct line representing the query q_{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

N^{∗} = let w = (catch N^{@}) in
(if0 w Ω  ; [1]

…

(if0 (sub1^{m−1} w) Ω  ; [m]
(if0 (sub1^{a_{1}+m} w) Ω  ; [m + 1]

…

(if0 (sub1^{a_{n}+m} w) Ω  ; [m + n]

Ω) …)) …)

where the expression (sub1^{b} L) abbreviates the b-fold application of sub1 to the argument expression L.

Beyond the construction of M the inductive hypothesis also demands the definition of an injection from Q to the set of contexts derived from M such that the injection satisfies (‡). If q ∈ Q^{+} then we can exploit the inductive hypothesis for x′ and Q^{+} and use the injection from Q^{+} to contexts for M′ to find an appropriate context for q and M; the proof that this association works is only a minor variant of the proof in the first subcase of the induction step. Otherwise, by assumption, q is one of q_{1},…, q_{m+n}. Say, q = q_{m+j} for 1 ≤ j ≤ n and r_{m+j} = q^{∗} · ⟨a_{j}⟩. If C_{m+j} is the context whose hole contains the Ω term on line m + j of N^{∗}, i.e., C[N^{∗}] = C[C_{m+j}[Ω]], then C[C_{m+j}[ ]] is the context associated with q.

We will concentrate on a query that ends in a final response to simplify the presentation: q_{m+j} for 1 ≤ j ≤ n and r_{m+j} = q^{∗} · ⟨a_{j}⟩. For a response that ends in a query (r_{j} for 1 ≤ j ≤ m), the proof proceeds in essentially the same manner.

Associating C[C_{m+j}[ ]] with q satisfies (‡). We analyze each of the two parts of condition (‡) separately. Let N be a term with free variables in x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, and let x_{1} ∈ SEQ^{τ_{1}}, …, x_{k} ∈ SEQ^{τ_{k}} be the denotations of these variables.

1. Suppose that ||π_{h}(q′ · ⟨q^{∗}, i⟩ · ⟨r_{m+j}, i⟩)|| ⊑ x_{h} for all h, which clearly means ||π_{h}(q′)|| ⊑ x_{h} and at index i implies

||π_{i}(q′ · ⟨q^{∗}, i⟩ · ⟨r_{m+j}, i⟩)|| = ||π_{i}(q′)|| ∪ {r_{m+j}} ⊑ x_{i}.

We must show that the meaning of C[C_{m+j}[N]] is the meaning of N:

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ C[C_{m+j}[N]] ]]⟨x_{1},…, x_{k}⟩

= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ N ]]⟨x_{1},…, x_{k}⟩

By the inductive hypothesis for x′ and Q^{+}, q′ is associated with C[ ] and satisfies (‡). Since ||π_{h}(q′)|| ⊑ x_{h} for all h by assumption,

SEQ[[ ⊢ C[C_{m+j}[N]] ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k}
= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ C_{m+j}[N] ]]⟨x_{1},…, x_{k}⟩.

Also by assumption, r_{m+j} = q^{∗} · ⟨a_{j}⟩ for a_{j} ∈ and thus,

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ (catch N^{@}) ]]⟨x_{1},…, x_{k}⟩ = {? · (a_{j} + m)}.

The rest is a straightforward calculation:

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ C_{m+j}[N] ]]⟨x_{1},…, x_{k}⟩

= SEQ[[x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢

(if0 w Ω … (if0 (sub1^{m−1} w) Ω (if0 (sub1^{a_{1}+m} w) Ω … (if0 (sub1^{a_{j}+m} w) N … (if0 (sub1^{a_{n}+m} w) Ω) …) …)) …)]]⟨x_{1},…, x_{k}, {? · (a_{j} + m)}⟩

= SEQ[[x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢

(if0 (sub1^{a_{j}+m} w) N … (if0 (sub1^{a_{n}+m} w) Ω) …)]]⟨x_{1},…, x_{k}, {? · (a_{j} + m)}⟩

= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢ N ]]⟨x_{1},…, x_{k}, {? · (a_{j} + m)}⟩
= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ N ]]⟨x_{1},…, x_{k}⟩ because w^{o} is not free in N .

2. Suppose that ||π_{l}(q′ · ⟨q^{∗}, i⟩ · ⟨r_{m+j}, i⟩)|| ⋢ x_{l} for some l. Now we must show that the meaning of C[C_{m+j}[N]] is independent of N:

SEQ[[ ⊢ C[C_{m+j}[N]] ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k} = x ⋆ x_{1} ⋆… ⋆ x_{k}.

We distinguish two subcases:

(a) If for any h (unrelated to l) ||π_{h}(q′)|| ⋢ x_{h} then by the inductive hypothesis for x′ and Q^{+}, for any K ,

SEQ[[ ⊢ C[K] ]] ⊥ ⋆x_{1} ⋆… x_{k} = x′ ⋆ x_{1} ⋆… ⋆ x_{k}.

By instantiating with C_{m+j}[L],

SEQ[[ ⊢ C[C_{m+j}[N]] ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k}
= x′ ⋆ x_{1} ⋆… ⋆ x_{k}
= (x′ ∪ {q′ · ⟨q^{∗}, i⟩}) ⋆ x_{1} ⋆… ⋆ x_{k}
= x ⋆ x_{1} ⋆… ⋆ x_{k}

The last two steps hold because ||π_{h}(q′)|| ⋢ x_{h} and therefore q′ · ⟨q^{∗}, i⟩ does not contribute anything to the final output of the application.

(b) If ||π_{h}(q′)|| ⊑ x_{h} for all h then obviously, ||π_{i}(q′ · ⟨q^{∗}, i⟩ · ⟨r_{m+j}, i⟩)|| ⋢ x_{i}. Moreover, the inductive hypothesis for x′ and Q^{+} implies that for any term in the hole of C[ ], and in particular for C_{m+j}[L],

SEQ[[ ⊢ C[C_{m+j}[N]] ]] ⊥ ⋆x_{1} ⋆… ⋆ x_{k}

= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ C_{m+j}[N] ]]⟨x_{1},…, x_{k}⟩.

The rest of this case depends on the response of x_{i} to the query q^{∗}, if any: i. If q^{∗} ∈ Open(x_{i}) then

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ C_{m+j}[N] ]]⟨x_{1},…, x_{k}⟩

= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢ (if0 w Ω …) ]]⟨x_{1},…, x_{k}, ⊥⟩
= ⊥

because SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ (catch N^{@}) ]]⟨x_{1},…, x_{k}, ⊥⟩ =⊥. ii. If q^{∗} · e ∈ x_{i} (for e ∈ ), then

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ C_{m+j}[N] ]]⟨x_{1},…, x_{k}⟩

= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢ (if0 w Ω …) ]]⟨x_{1},…, x_{k}, {? · e}⟩
= {? · e}

because SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ (catch N^{@}) ]]⟨x_{1},…, x_{k}⟩ = {? · e} if q^{∗} · e ∈ x_{i}. iii. If q^{∗}·⟨a⟩ ∈ x_{i}, then two cases are possible. First, a = a_{h} for some h, 1 ≤ h ≤ n

but h ≠ j. Then because SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ (catch N^{@}) ]]⟨x_{1},…, x_{k}⟩ = {? · (a_{j} + m)},

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ C_{m+j}[N] ]]⟨x_{1},…, x_{k}⟩

= SEQ[[x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢

(if0 w Ω … (if0 (sub1^{m−1} w) Ω (if0 (sub1^{a_{1}+m} w) Ω … (if0 (sub1^{a_{j}+m} w) N … (if0 (sub1^{a_{n}+m} w) Ω) …) …)) …)]]

⟨x_{1},…, x_{k}, {? · (a_{h} + m)}⟩

= SEQ[[x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢

(if0 (sub1^{a_{h}+m} w) Ω … (if0 (sub1^{a_{n}+m} w) Ω) …)]]⟨x_{1},…, x_{k}, {? · (a_{j} + m)}⟩

= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢ Ω ]]⟨x_{1},…, x_{k}, {?p(a_{h} + m)}⟩
= ⊥ .

Second, a may be distinct from a_{1},…, a_{n} such that, without loss of generality, a < a_{n}. Again, one of the test expressions will diverge:

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ C_{m+j}[N] ]]⟨x_{1},…, x_{k}⟩
= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢ (if0 w Ω …) ]]⟨x_{1},…, x_{k}, {? · a}⟩
= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢ (if0 (sub1^{a_{j}+m} w) Ω …) ]]⟨x_{1},…, x_{k}, {? · a}⟩
for a_{j} > a
= ⊥

If a > a_{n}, then the evaluation will reach the else branch of the last if0expression, which will force divergence again.

iv. If q^{∗} · ⟨p^{∗}, 1⟩ ∈ x_{i} for some query p^{∗}, we must also consider two cases. First, p^{∗} may be one of p_{1},…, p_{m}, e.g., p^{∗} = p_{h} for h, 1 ≤ h ≤ m. This implies that

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ (catch N^{@}) ]] = {? · (h − 1)}.

A simple calculation now shows that

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ C_{m+j}[N] ]]⟨x_{1},…, x_{k}⟩
= SEQ[[x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢

(if0 w Ω …

(if0 (sub1^{h−1} w) Ω (if0 (sub1^{a_{1}+m} w) Ω … (if0 (sub1^{a_{j}+m} w) N … (if0 (sub1^{a_{n}+m} w) Ω) …) …)) …)]] ⟨x_{1},…, x_{k}, {? · (h − 1)}⟩

= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, w^{o} ⊢ (if0 (sub1^{h−1} w) Ω …) ]]

⟨x_{1},…, x_{k}, {? · (h − 1)}⟩

= ⊥

Second, p^{∗} may be distinct from any of the p_{1},…, p_{m}, in which case

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ (catch N^{@}) ]]⟨x_{1},…, x_{k}⟩ =⊥,

and therefore

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ C_{m+j}[N] ]]⟨x_{1},…, x_{k}⟩ =⊥ .

For all four cases the result that C_{m+j}[N] evaluates to in the environment ⟨x_{1},…, x_{k}⟩ is the required one:

x ⋆ x_{1} ⋆… ⋆ x_{k} = (x′ ∪ {q′ · ⟨q^{∗}, i⟩}) ⋆ x_{1} ⋆… ⋆ x_{k}

= \{ \begin{matrix}⊥ & if q^{∗} ∈ Open(x_{i}) \\ \{? · e\} & if q^{∗} · e ∈ x_{i} \\ ⊥ & if q^{∗} · ⟨a⟩ ∈ x_{i}, a ≠ a_{j} \\ ⊥ & if q^{∗} · ⟨p^{∗}, 1⟩ ∈ x_{i} \end{matrix}

Given that N was arbitrary we were able to show that the association of C_{m+j}[ ] with q = q′ · ⟨q^{∗}, i⟩ · ⟨r_{m+j}, i⟩ satisfies (‡).

Constructing B_{1},…, B_{l}. To complete the proof of the lemma, we must

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

• prove that the expression N^{@}, constructed from B_{1},…, B_{l}, satisfies the correctness conditions identified above.

Let h be an index in the range 1,…, l. The type of B_{h} has the form

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

for some integer t ≥ 0. Its construction falls into one of two cases. In the first case, no query response r_{j} (1 ≤ j ≤ m) asks for more information about the hth argument. In this case, we simply define B_{h} as the closed expression representing the tree ||π_{h}(q^{∗})||, which exists by the induction hypothesis because the type σ_{h} of B_{h} is smaller than τ.

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^{∗} · ⟨p_{1}, h⟩, …, r_{s} = q^{∗} · ⟨p_{s}, h⟩, and that the variables y_{1}^{o},…, y_{s}^{o} correspond to these responses. From the assumptions, p_{1},…, p_{s} ∈ Open(||π_{h}(q^{∗})||). Now our goal is to construct a procedure B_{h} that requests information about y_{j}^{o} if x_{i} inquires about p_{j} (1 ≤ j ≤ s). Thus, B_{h} must be a procedure of type σ_{h} but its body must also depend on the parameters y_{1}^{o},…, y_{s}^{o}. If E_{h} is the body of B_{h}, the latter has the following shape:

B_{h} = λz_{1}^{ν_{1}} … z_{t}^{ν_{t}}.(E_{h} z_{1}^{ν_{1}} … z_{t}^{ν_{t}} y_{1}^{o} … y_{s}^{o}).

In other words, E_{h} is procedure of type

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

that acts like ||π_{h}(q^{∗})|| with respect to the first t arguments and contains a query for y_{j}^{o} if the first t arguments dominate the information in the path p_{j} (1 ≤ j ≤ s).

Semantically speaking, we need to (1) inject ||π_{h}(q^{∗})|| from the domain for σ_{h} into σ′_{h} and (2) extend ||π_{h}(q^{∗})|| at the positions p_{1},…, p_{s} so that it issues a query for argument t + 1,…, t + s, respectively:

1. Every z tree of type σ_{h} directly corresponds to a tree in σ′_{h}. By changing every initial address on a path in z from

⟨… ⟨?, \underbrace{2⟩,…, 2⟩}_{t} to ⟨… ⟨?, \underbrace{2⟩,…, 2⟩}_{s+t}

and every final datum from

⟨… ⟨? · n, \underbrace{2⟩,…, 2⟩}_{t} to ⟨… ⟨? · n, \underbrace{2⟩,…, 2⟩}_{s+t},

we get a tree in the extended domain. We use the notation z^{σ′_{h}} for the result of injecting z. Since the tree in the extended domain does not contain any queries about the arguments t + 1,…, t + s, it is immediate that ||π_{h}(q^{∗})||^{σ_{h}} and ||π_{h}(q^{∗})||^{σ′_{h}} relate to each other as follows:

||π_{h}(q^{∗})||^{σ_{h}} ⋆ z_{1} ⋆… ⋆ z_{t} = ||π_{h}(q^{∗})||^{σ′_{h}} ⋆ z_{1} ⋆… ⋆ z_{t} ⋆ y_{1} ⋆… ⋆ y_{s}

for all z_{1},…, z_{t} and y_{1},…, y_{s}.

2. Given the tree ||π_{h}(q^{∗})||^{σ′_{h}}, we can form a tree that grafts appropriate subtrees at (the paths in the extended domain) p_{1},…, p_{s} onto the tree:

e_{h} = ||π_{h}(q^{∗})||^{σ′_{h}} ∪ {p_{1}^{σ′_{h}} · ⟨?, t + 1⟩,…, p_{s}^{σ′_{h}} · ⟨?, t + s⟩}.

Interpreted as a function, e_{h} obviously has the desired behavior. The inductive hypothesis implies that there is a representing term E_{h} for e_{h} because σ′_{h} is smaller than τ.

The meaning of B_{h} depends on the values of y_{1}^{o},…, y_{s}^{o} in the environment. Let y⃗ = ⟨y_{1},…, y_{s}⟩ be a vector of s arbitrary values in _{⊥}^{e}. Then we claim that B_{h} denotes the tree

(||π_{h}(q^{∗})|| ∪ {p_{j} · y_{j} | if y_{j} ∈ })^{σ_{h}}

That is, if none of the variables y_{1}^{o},…, y_{s}^{o} denotes an error value, B_{h} denotes ||π_{h}(q^{∗})||. If some variable y_{j}^{o} stands for an error value y_{j}, the error value is propagated and is grafted onto the end of the query p_{j} ∈ Open(||π_{h}(q^{∗})||). We refer to the meaning of B_{h} relative to

y⃗ as by⃗ ; h.

To prove that the denotation of B_{h} is the above tree, assume that z_{1} ∈ SEQ^{ν_{1}},…, z_{t} ∈ SEQ^{ν_{t}} and y_{1},…, y_{s} ∈ _{⊥}^{e} are arbitrary:

SEQ[[ y_{1}^{o} … y_{s}^{o} ⊢ B_{h}]]⟨y_{1},…, y_{s}⟩ ⋆ z_{1} ⋆… ⋆ z_{t}
= SEQ[[ y_{1}^{o} … y_{s}^{o}z_{1}^{ν_{1}} … z_{t}^{ν_{t}} ⊢ (E_{h} z_{1}^{ν_{1}} … z_{t}^{ν_{t}} y_{1}^{o} … y_{s}^{o}) ]]⟨y_{1},…, y_{s}, z_{1},…, z_{t}⟩
= e_{h} ⋆ z_{1} ⋆… ⋆ z_{t} ⋆ y_{1} ⋆… ⋆ y_{s}
= (||π_{h}(q^{∗})|| ∪ {p_{1} · ⟨?, t + 1⟩,…, p_{s} · ⟨?, t + s⟩})^{σ′_{h}} ⋆ z_{1} ⋆… ⋆ z_{t} ⋆ y_{1} ⋆… ⋆ y_{s}

= \{ \begin{matrix}\{? · y_{1}\} & if ||π_{g}(p_{1})|| ⊑ z_{g} for 1 ≤ g ≤ t, y_{1} ∈ \\ … \\ \{? · y_{s}\} & if ||π_{g}(p_{s})|| ⊑ z_{g} for 1 ≤ g ≤ t, y_{s} ∈ \\ ||π_{h}(q^{∗})|| ⋆ z_{1} ⋆… ⋆ z_{t} ⋆ y_{1} ⋆… ⋆ y_{s} & otherwise \end{matrix}

= (||π_{h}(q^{∗})|| ∪ {p_{j} · y_{j} | if y_{j} ∈ })^{σ_{h}} ⋆ z_{1} ⋆… ⋆ z_{t},

which, by extensionality, implies SEQ[[ y_{1}^{o} … y_{s}^{o} ⊢ B_{h}]]⟨y_{1},…, y_{s}⟩ = by⃗ ; h.

After constructing and analyzing B_{h}, we must show that the denotation of

N^{@} = λy_{1}^{o}… y_{m}^{o}.(x_{i}^{τ_{i}} B_{1} … B_{l})

is such that

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ N^{@} ]]⟨x_{1},…, x_{k}⟩ = \{ \begin{matrix}\{⟨?⟩ · ⟨a⟩\} & if q^{∗} · ⟨a⟩ ∈ x_{i}, a ∈ \\ \{⟨?⟩ · ⟨?, j⟩\} & if r_{j} ∈ x_{i} \\ & for some j, 1 ≤ j ≤ m. \end{matrix}

To prove this claim, assume that x_{i} contains a response to q^{∗}, say, r_{j}. Let y_{1},…, y_{m} be l arbitrary values from _{⊥}^{e} and let y⃗_{1},…, y⃗_{l} be vectors containing the values from y_{1},…, y_{m} of all the free variables among y_{1}^{o},…, y_{m}^{o} for the expressions B_{1},…, B_{l}, respectively. Then:

SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ N^{@} ]]⟨x_{1},…, x_{k}⟩ ⋆ y_{1} ⋆… ⋆ y_{m}

= SEQ[[ x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ (x_{i} B_{1} … B_{l}) ]]⟨x_{1},…, x_{k}, y_{1},…, y_{m}⟩
= x_{i} ⋆ by⃗_{1} ; 1 ⋆… ⋆ by⃗_{l} ; l
= \{(π\overrightarrow{2})^{l}(r_{j}) | r_{j} = q^{∗} · ⟨a⟩, a ∈ \} ∪ \{(π\overrightarrow{2})^{l}(q_{j}) · y_{h_{j}} | r_{j} = q^{∗} · ⟨p_{j}, h_{j}⟩, if y_{h_{j}} ∈ \}

because by⃗ ; 1 ⊒ ||π_{1}(q^{∗})||, …, by⃗ ; l ⊒ ||π_{l}(q^{∗})||

= {? · a | r_{j} = q^{∗} · ⟨a⟩, a ∈ } ∪ {? · y_{h_{j}} | r_{j} = q^{∗} · ⟨p_{j}, h_{j}⟩, y_{h_{j}} ∈ }

since p_{j} · y_{j} ∈ by⃗_{h_{j}} ; h_{j} if y_{h_{j}} ∈ and p_{j} ∈ Open(by⃗_{h_{j}} ; h_{j}) if y_{h_{j}} ∈ _{⊥}

= \{ \begin{matrix}\{⟨?⟩ · ⟨a⟩\} ⋆ y_{1} ⋆… ⋆ y_{m} & if r_{j} = q^{∗} · ⟨a⟩ \\ \{⟨?⟩ · ⟨?, j⟩\} ⋆ y_{1} ⋆… ⋆ y_{m} & if r_{j} = q^{∗} · ⟨p_{j}, h_{j}⟩ \end{matrix}

By extensionality, the denotation of N^{@} satisfies the desired condition. This observation completes the proof of the lemma for the semantics based on SEQ.

With minor adjustments, the proof is valid for a semantics based on Seq as long as the set of error values is not empty. As for the non-extensional semantics Seq^{∅}, the proof proceeds as above. Since an error-free x is represented by a term M in SPCF(∅), and since by Lemma 7.3 terms in SPCF(∅) of type τ denote the same tree in Seq^{τ} independently of the underlying error set, it is also true that Seq^{∅}[[ M ]]⋆ ⊥= x, i.e., M denotes x in the intensional semantics.

8 An Adequate Operational Semantics for SPCF

Although the denotational semantics of a programming language is an elegant tool for reasoning about the phrases of the language, an operational semantics offers a better basis for the derivation of an implementation. Moreover, when defined via the reductions of a calculus, an operational semantics also provides a simple equational theory that is useful for proving many observational equivalences.

To equip SPCF with an operational semantics, we follow Plotkin’s program [25]—as extended by Felleisen, Friedman and Hieb [13, 14, 15]—on relating λ-calculi and abstract machines. More specifically, we define an extension of the typed λ-calculus and, based on it, a deterministic text rewriting machine for SPCF programs. We then prove an adequacy theorem for SPCF, i.e., we show that for any program P, the meaning of P is n or e if and only if P reduces to ^{⌈}n^{⌉} or e, respectively. Based on this adequacy result, the full abstraction theorem can now be formulated as follows: given two SPCF phrases M and N, Seq[[ M ]] ⊑ Seq[[ N ]] if and only if for for any program context C[ ] for M and N , C[M] evaluates to w implies C[N] evaluates to w where w is either a numeral or an error element.^{16}

16The results presented in this section account for the fact that (sub1 ^{⌈}0^{⌉}) denotes bottom but it does not rely on it. It is easy to adapt the proofs for a version of SPCF in which (sub1 ^{⌈}0^{⌉}) returns ^{⌈}0^{⌉} or signals an error.

8.1 Operational Semantics

The description of the operational semantics relies on the notion of an evaluation context [13] for two separate purposes. First, the notion of an evaluation context is useful for defining notions of reduction that capture the behavior of error elements and control facilities like catch in a context-free manner. Second, given a reduction system, a standard reduction of a program is the repeated reduction of the redex that occurs in the hole of the evaluation context. This definition yields a deterministic textual rewriting machine because every SPCF program (that is not a value) has a unique partitioning into an evaluation context and a (proper) redex.

Definition 8.1 (Evaluation Contexts) The set of evaluation contexts is the following subset of the set of contexts:

E ::= [ ] | (f E) | (E M) | catch (λx_{1} … x_{n}.E) for n ≥ 0

If E[ ] is an evaluation context, then (E[ ])[N/x] denotes the context that results from capture-free substitution of all free x by N in the subterms of E[ ].

The set of evaluation contexts is a subset of the set of contexts (see Definition 3.3). Generally speaking, the hole of an evaluation context can only occur where a reduction must take place due to the strictness properties of the primitive procedures and procedure application in SPCF. There are four specific situations that meet these criteria (in SPCF). First, a hole can clearly occur to the right of a primitive procedure because all primitives are strict. Second, in an application the only position that must be evaluated is the function position: hence, an evaluation context may have a hole in the function position of an arbitrary application. Third, since catch must determine whether or not its argument is constant or strict in some position, it must clearly evaluate its argument and, if the argument reduces to a procedure, the body of the argument’s value.^{17} To reflect the second part of this idea, an evaluation context may also have a hole in the procedure body of the argument to catch. Finally, to provide a base case for the inductive definition, we also include the plain hole in the set of evaluation contexts.

For the specification and analysis of the operational semantics we need to extend the substitution and context-filling operation to evaluation contexts. It is crucial that these operations, i.e., filling an evaluation context with an evaluation context or replacing a free variable by an arbitrary term in an evaluation context, yield not only arbitrary contexts but evaluation contexts.

Lemma 8.2 If E and E′ are evaluation contexts, then so are E[E′[ ]] and (E[ ])[N/x].

17Operationally speaking, catch acts like a (strict) let-expression for which the evaluator creates the values for the variables on the fly. The values are tags that mark the evaluation context of the let-expression.

When one of the tags is touched during the evaluation of the body, the portion of the evaluation context between the markers and the occurrence of the tag needs to be erased. To avoid the introduction of an additional syntactic object, we employ variables as tags and use the notation catch λx_{1} … x_{m}. to mark the evaluation context at the appropriate place. In an abstract machine with an explicit control stack, like the CEK [13] machine, this implementation technique corresponds to marking the control stack (K) and binding the variables of the catch argument to these tags. When an environment lookup produces a tag, the control stack is erased to an appropriate extent.

Proof. The proofs are simple inductions on the structure of E.

Given the definition of evaluation contexts, we can now turn to the definition of the SPCF calculus. The calculus is an extension of the PCF calculus. First, the basic set of axioms contains the usual laws for procedure application (β) and for primitives (Y, add1, sub1, if0/0, if0/1). Second, the laws for catch and error elements reflect the denotational semantics. Accordingly a term signals an error if the error occurs in a position that must be evaluated. Put formally, an error element erases any surrounding evaluation context. Similarly, when a bound variable occurs in an evaluation context (in the procedure body), a catch application will signal that the procedure is strict in this argument. An application of catch to a procedure whose body is a numeral can be replaced by an appropriate result. Finally, there is no reduction for Ω^{o} because it represents the provably diverging program.

Definition 8.3 (SPCF Reductions, Calculus) The nine basic notions of reduction for SPCF are the following nine relations between SPCF phrases:

add1 ^{⌈}n^{⌉} ⟶ ^{⌈}n + 1^{⌉}  (add1)
sub1 ^{⌈}n + 1^{⌉} ⟶ ^{⌈}n^{⌉}  (sub1)
if0 ^{⌈}0^{⌉} ⟶ λxy.x  (if0/0)
if0 ^{⌈}n + 1^{⌉} ⟶ λxy.y  (if0/1)
YM ⟶ M(Y M)  (fix)
(λx.M) N ⟶ M[N/x]  (β)
E[e] ⟶ e, E ≠ [ ], e ∈ (error)
catch (λx_{1} … x_{m}.^{⌈}n^{⌉}) ⟶ ^{⌈}m + n^{⌉}  (return)
catch (λx_{1} … x_{m}.E[x_{i}]) ⟶ ^{⌈}i − 1^{⌉}  where i ≤ m  (catch)

Additional Constraints: First, in (error), E[e] must be of ground type. Second, the last rule assumes that given a term of the shape E[x_{i}], the occurrence of x_{i} in the hole of E is a free occurrence. Terminology: As always, we refer to the left hand side of one of the above rules as “redex”. E[e] is called an error redex; other redexes are proper redexes.

The SPCF calculus is the equational theory generated from the nine axioms above using the inference rules:

\begin{matrix}M ⟶ N ; \overline{M = N} & M = N ; \overline{C[M] = C[N]} & M = N N = L ; \overline{M = L} \\ \overline{M = M} & M = N ; \overline{N = M} \end{matrix}

where C[ ] is an arbitrary context. We write SPCF ⊢ M = N if M and N are provably equal.

Calculating with terms preserves their types. This property is important for many of the subsequent definitions though we will not explicitly mention it.^{18} Lemma 8.4 If A ⊢ M : τ and SPCF ⊢ M = N then A′ ⊢ N : τ.

18The property implies that e can only be the result of a program if it is a part of the original program text.

Proof. It is easy to check that the nine basic axioms have the following, slightly stronger property: If A ⊢ M : τ and M ⟶ N then A ⊢ N : τ. The property obviously holds for all rules except for (error), for which it is explicitly built in. The rest is a straightforward induction.

An operational semantics for a language is a partial function from programs to answers, that is, in our case from closed SPCF terms ofground type to numerals and error elements. Based on the SPCF calculus we can define an evaluation function by saying that if a program is provably equal to a numeral or to an error element, the respective value is the program’s result. With this, it is easy to confirm that the example programs from Section 3, (catch +_{l}) and (catch +_{r}), are equal to distinct outputs:

SPCF ⊢ (catch +_{l}) = ^{⌈}0^{⌉}

and

SPCF ⊢ (catch +_{r}) = ^{⌈}1^{⌉}.

However, Plotkin’s analysis of the λ-calculus as a programming language suggests that such a definition is equivalent to the following, more algorithmic definition: to find the value of a program, it suffices to reduce the leftmost-outermost redex until the program is transformed into a value. Finding the leftmost-outermost redex in SPCF programs requires a partitioning of the program into an evaluation context and a redex. As for PCF, this partitioning process yields a unique pair of context and filler. If the filler is an error element, there may be several choices of splitting the program into an evaluation context and a redex. Otherwise, the pair is unique.

Lemma 8.5 (Unique Evaluation Context) For any SPCF application M, there exists exactly one partitioning of M into an evaluation context E[ ] and a term R where R is either a free variable, Ω, (sub1 0), an error element, or a proper redex.

Proof. The proof is an induction on the structure of M and proceeds by case analysis:

M = (M_{1} M_{2}) : If M_{1} is a λ-abstraction, M is a redex and the empty context serves as the required evaluation context. Otherwise, there exists a unique partitioning of M_{1} into some appropriate E_{1}[ ] and R by the inductive hypothesis. Take M = E[R] as the partitioning where E[ ] = (E_{1}[ ] M_{2}). By the inductive definition of the set of evaluation contexts, there cannot be any other partitioning.

M = (f M_{1}) where f ∈ {add1, sub1, if0}: If M_{1} is a numeral, M is a redex. If M_{1} ∈ , take E = (f [ ]) and R = M_{1}. Otherwise, M_{1} = E_{1}[R] by the inductive hypothesis. As in the preceding case, E[ ] = (f E_{1}[ ]) and R are the desired pieces of M.

M = (Y M_{1}) : M is a redex.

M = (catch (λx_{1} … x_{i}.M_{1}) where i ≥ 0 and M_{1} is not a λ-abstraction: If M_{1} is a numeral or an error element, the argument proceeds as in the preceding case. Otherwise, the inductive hypothesis guarantees that M_{1} = E_{1}[R]. If R is a free variable among x_{1},…, x_{i}, then M is a redex of the right kind. If R is a redex, Ω, an error element, or some different free variable, the required partitioning for M consists of E[ ] = (catch (λx_{1} … x_{i}.E_{1}[ ]) and R.

As a consequence of the Unique Evaluation Context Lemma we can define evaluation for SPCF programs in the traditional way, namely, as leftmost-outermost reduction to a canonical form.

Definition 8.6 (eval_{SPCF} , ↦, Values) The operational semantics of SPCF is the partial relation

eval_{SPCF} : \{ \begin{matrix}Programs & ⟶ ∘ & Values \\ M eval_{SPCF} w & iff & M ↦^{∗} w \end{matrix}

where

w ∈ Values = ∪ {^{⌈}n^{⌉} | n ∈ }

and

M ⟶ M′ ; \overline{E[M] ↦ E[M′]} .

If M ↦ N we say M standard reduces to N; we call ↦ standard reduction.

Due to (error), the relation ↦ is clearly not a function but a proper relation. For example, (add1 (add1 e)) ↦ (add1 e) and (add1 (add1 e)) ↦ e. Hence, it is necessary to prove that eval_{SPCF} is a function. The proposition is an easy consequence of the Unique Evaluation Context Lemma.^{19}

Proposition 8.7 The relation eval_{SPCF} is a partial function.

Moreover, an SPCF program M evaluates either

1. to a numeral,

2. to an error value ( if ≠ ∅),

3. to a stuck state,

4. or has an infinite standard reduction.

Proof. The first part of the proposition is a straightforward consequence of the Unique Evaluation Context Lemma. If a program M is an application it either has a unique successor with respect to standard reduction or reduces to a unique error value. Hence, if M ↦^{∗} w, then w is either a unique numeral or a unique error value.

The second part of the proposition follows from a Uniform Evaluation Lemma (see below). When applied to programs, which are closed and of ground type, the lemma says that for every SPCF program M one of the suggested alternatives holds. The possibilities are mutually exclusive due to the Unique Evaluation Context Lemma.

19The proposition also follows from the Soundness Lemma (see 8.14) in the second subsection.

Uniform evaluation for SPCF means that the reduction rules suffice to show that all SPCF terms M of ground type evaluate according to one of five possibilities: the four mentioned in the previous lemma and a stuck state of the shape E[x] where x is free. The idea generalizes to all types.

Definition 8.8 (Eval_{τ}) The family of sets of SPCF phrases Eval_{τ} is defined by induction on types:

Eval_{o} = \{M | \begin{matrix}M ↦^{∗} ^{⌈}n^{⌉} or \\ M ↦^{∗} e or \\ M ↦^{∗} E[Ω] or \\ M ↦^{∗} E[x_{i}] or \\ ∀N.M ↦^{∗} N ⟹ ∃L.N ↦ L \end{matrix} \}

Eval_{σ→τ} = \{M | \begin{matrix}M ↦^{∗} λx^{σ}.N ∧ N ∈ Eval_{τ} or \\ M ↦^{∗} E[e] or \\ M ↦^{∗} E[Ω] or \\ M ↦^{∗} E[x_{i}] or \\ ∀N.M ↦^{∗} N ⟹ ∃L.N ↦ L \end{matrix} \}

Lemma 8.9 (Uniform Evaluation) For every SPCF term M of type τ, M ∈ Eval_{τ}.

Proof. The proof is an induction on the structure of τ. First assume τ = o, M ↦^{∗} N, and N is irreducible with respect to standard reduction. If N ∈ Values one of the first two clauses of Eval_{o} holds. Otherwise N is an application. In this case Lemma 8.5 says that N = E[R] where R ∈ Vars, R = Ω, R ∈ , or R is a proper redex. The first two cases are covered by clauses 3 and 4 of Eval_{o}. If N = E[e] then N ↦^{∗} e because of its ground type. But this contradicts the assumption that N is irreducible, so it is impossible. The case where R is a redex leads to the same contradiction. Thus, M reduces according to one of the first four clauses or for every reachable term N there is a successor with respect to standard reduction.

Second assume τ = σ → ν. The same analysis applies as in the base case except that irreducible terms are now λ-abstractions and evaluation contexts of type τ filled with e ∈ . By inductive hypothesis, the bodies of λ abstractions are in Eval_{ν}.

The Uniform Evaluation Lemma implies an important lemma on the evaluation of phrases whose root is a catch application. The lemma is crucial for the treatment of catch in the following subsection. It requires the definition of a set of terms that suitably generalizes the set of terms with infinite standard reductions to higher types.

Definition 8.10 (Inf_{τ}) The family of sets of SPCF phrases Inf_{τ} is defined by induction on types:

Inf_{o} = {M | ∀N.M ↦^{∗} N ⟹ ∃L.N ↦ L}
Inf_{σ→τ} = {M | M ↦^{∗} λx^{σ}.N ∧ N ∈ Inf_{τ} , ∀N.M ↦^{∗} N ⟹ ∃L.N ↦ L}

The operator catch discovers when a term belongs to Inf .

Lemma 8.11 Let M be a term of type τ. If (catch M) ∈ Inf_{o}, then M ∈ Inf_{τ}.

Before closing the section, we collect four properties of the reduction and standard reduction relations that are crucial for proofs in the following subsection.

Proposition 8.12 1. If M ⟶ N then M[L/x] ⟶ N[L/x].

2. If M ↦ M′, then E[M] ↦ E[M′].

3. If M ↦ N then M[L/x] ↦ N[L/x].

4. If M ∈ Inf_{τ} and its arity is a, then for all L_{1},…, L_{a} and for all N_{1},…, N_{i} and x_{1},…, x_{i}, (M[N_{1}/x_{1}] … [N_{i}/x_{i}] L_{1} … L_{a}) ∈ Inf_{o}.

Proof. The proof of the first part is straightforward for each notion of reduction. For (error) and (catch) the proof relies on Lemma 8.2, i.e., that substitutions in an evaluation context do not affect its status as evaluation context.

For the second claim, if M = E′[N], N ⟶ N′ and M′ = E′[N′], then E′′ = E[E′[ ]] is an evaluation context by Lemma 8.2 and E[M] = E′′[N]. Hence, by definition of ↦, E[M] ↦ E′′[N′] = E[M′].

The third claim follows from the first one and Lemma 8.2.

Finally, the fourth claim requires a simple induction on the type τ. For τ = o, M ∈ Inf_{o} implies that M has an infinite reduction sequence. By part 3, all substitution instances of M also have an infinite reduction sequence and are thus in Inf_{o}. Thus assume τ = σ → ν. Then either M itself has an infinite standard reduction, in which case the claim is again obviously true, or M standard reduces to some abstraction λx^{σ}.L. In the latter case,

(M[N_{1}/x_{1}] … [N_{i}/x_{i}] L_{1} … L_{a}) ↦^{∗} ((λx^{σ}.L[N_{1}/x_{1}] … [N_{i}/x_{i}]) L_{1} … L_{a})
↦ (L[N_{1}/x_{1}] … [N_{i}/x_{i}][L_{1}/x^{σ}] L_{2} … L_{a})

again by parts 2 and 3 plus (β). By definition L ∈ Inf_{ν} and, hence by inductive hypothesis,

(L[N_{1}/x_{1}] … [N_{i}/x_{i}][L_{1}/x^{σ}] L_{2} … L_{a}) ∈ Inf_{o},

which proves the claim.

8.2 Adequacy

To be useful, an operational semantics must faithfully realize the denotational semantics for programs. Technically, the operational semantics should map a program to a value if and only if the denotational semantics equates the program with the denotation of the value. Since this relationship is similar to the adequacy relationship between different semantics of a language, the corresponding theorem is called Adequacy Theorem.

Theorem 8.13 (Adequacy) Let M be a program of SPCF( ). Then the following equivalences hold:

1. Seq[[ M ]] ⊥= {? · n} iff eval_{SPCF} (M) = ^{⌈}n^{⌉};

2. Seq[[ M ]] ⊥= {? · e} iff eval_{SPCF} (M) = e.

(Seq can be replaced by SEQ if ≠ ∅.)

The if-part of the Adequacy Theorem relies on a standard soundness proof for the reduction rules. Since the rules for catch differ from the rules of more traditional λ-calculi, we formulate the lemma and sketch its proof.

Lemma 8.14 (Soundness) Let M and M′ be terms that are typable with the same variable list A. Then

1. if SPCF ⊢ M = M′, then Seq[[ A ⊢ M ]] = Seq[[ A ⊢ M′]];

2. if M ↦^{∗} M′ then Seq[[ A ⊢ M ]] = Seq[[ A ⊢ M′]].

Note: The type of M is not necessarily o in clause 2: the standard reduction relation applies to terms of higher type, too. Proof. It is a routine exercise to check the basic reduction relations (add1), (sub1), (if0/0), (if0/1), and the respective inference rules. The validity of β- and fix follows from Lemma 3.6 and the results of Section 6. Next, the validation of (return) is simple. Clearly, for any appropriate list of typed variables A and matching environment tuple ρ,

Seq[[ A ⊢ λx_{1}^{τ_{1}},…, x_{k}^{τ_{k}}.^{⌈}m^{⌉}]] ⋆ ρ = {⟨?⟩ · ⟨m⟩}.

Hence, by the semantics of catch,

Seq[[ A ⊢ (catch λx_{1}^{τ_{1}},…, x_{k}^{τ_{k}}.^{⌈}m^{⌉}) ]] ⋆ ρ
= C_{k} ⋆ (Seq[[ A ⊢ λx_{1}^{τ_{1}},…, x_{k}^{τ_{k}}.^{⌈}m^{⌉}]] ⋆ ρ)
= C_{k} ⋆ ({⟨?⟩ · ⟨m⟩}) = {? · (m + k)}
= Seq[[ A ⊢ ^{⌈}m + k^{⌉}]] ⋆ ρ

The validity of the remaining rules, (catch) and (error), follows from a general claim about the denotations of terms of the shape E[x]:

Claim (i): For any evaluation context E and vector of variables x_{1}^{τ_{1}},…, x_{k}^{τ_{k}}, variable list A and matching environment vector ρ, if i ≤ k, then

⟨?⟩ · ⟨i⟩ ∈ Seq[[ A ⊢ λx_{1}^{τ_{1}},…, x_{k}^{τ_{k}}.E[x_{i}] ]] ⋆ ρ.

(Recall that, by convention, x_{i} occurs free in the hole of E.) Given the meaning of catch, it immediately implies the validity of (catch):

Seq[[ A ⊢ (catch λx_{1}^{τ_{1}},…, x_{k}^{τ_{k}}.E[x_{i}]) ]] ⋆ ρ
= C_{k} ⋆ (Seq[[ A ⊢ λx_{1}^{τ_{1}},…, x_{k}^{τ_{k}}.E[x_{i}] ]] ⋆ ρ)
⊒ C_{k} ⋆ {⟨?⟩ · ⟨?, i⟩} = {? · (i − 1)}
= Seq[[ A ⊢ ^{⌈}i − 1^{⌉}]] ⋆ ρ

Together with the validity of (β), the claim also implies (error):

Seq[[ A ⊢ E[e] ]] ⋆ ρ = Seq[[ A ⊢ ((λx^{o}.E[x^{o}]) e) ]] ⋆ ρ by (β)

⊒ {⟨?⟩ · ⟨?, 1⟩} ⋆ {? · e} = {? · e}  by the semantics of application and the claim
= Seq[[ A ⊢ e ]] ⋆ ρ.

Thus, we have reduced our task to the proof of Claim (i), which proceeds as follows:

Seq[[ A ⊢ λx_{1}^{τ_{1}},…, x_{k}^{τ_{k}}.E[x_{i}] ]] ⋆ ρ
= \underbrace{Λ_{t}(… Λ_{t}(}_{k} Seq[[ A, x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ E[x_{i}] ]]) …) ⋆ ρ
= \underbrace{Λ_{t}(… Λ_{t}(}_{k} Seq[[ A, x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} ⊢ E[x_{i}] ]]) …) ⋆ ρ
(ii)  ⊒ \underbrace{Λ_{t}(… Λ_{t}(}_{k}\{⟨?⟩ · ⟨⟨… ⟨⟨?⟩, 2⟩, \underbrace{1⟩,…, 1⟩}_{k−i}, 1⟩,…\}) …) ⋆ ρ
= {⟨⟨?⟩, 2⟩⟨⟨?, i⟩, 2⟩,…} ⋆ ρ
= {⟨?⟩ · ⟨?, i⟩,…}

The step marked with (ii) requires a separate proof. For clarity, we formulate the claim explicitly:

Claim (ii): Let E[ ] be an evaluation context, and let A = x_{1}^{τ_{1}},…, x_{k}^{τ_{k}} be a list of variables. Then

⟨?⟩ · ⟨⟨… ⟨⟨?⟩, 2⟩, \underbrace{1⟩,…, 1⟩}_{k−i}, 1⟩ ∈ Seq[[ A ⊢ E[x_{i}] ]].

We prove Claim (ii) by induction on the structure of evaluation contexts:

1. If E = [ ] then Seq[[ A ⊢ x_{i}]] = π_{k−i+1}^{k}, and this projection clearly contains a path of the appropriate shape. Whence the conclusion immediately follows.

2. If E = (f E_{1}), the result follows from the fact that all primitive functions f consult their first argument, which is E_{1}[x_{i}]: compare Definitions 7.1 and 7.2.

3. If E = (E_{1} N), the conclusion follows from the fact that when an application is evaluated, the procedure, i.e., E_{1}[x_{i}], is consulted first.

4. If E = catch (λy_{1}^{σ_{1}} … y_{m}^{σ_{m}}.E_{1}), then by induction

⟨?⟩ · ⟨⟨… ⟨⟨?⟩, 2⟩, \underbrace{1⟩,…, 1⟩}_{k−i+m}, 1⟩ ∈ Seq[[ A, y_{1}^{σ_{1}},…, y_{m}^{σ_{m}} ⊢ E_{1}[x_{i}] ]]

hence

⟨?⟩ · ⟨⟨… ⟨⟨?⟩, 2⟩, \underbrace{1⟩,…, 1⟩}_{k−i}, 1⟩ = \underbrace{Λ_{t}(… Λ_{t}(}_{m}⟨?⟩ · ⟨⟨… ⟨⟨?⟩, 2⟩, \underbrace{1⟩,…, 1⟩}_{k−i+m}, 1⟩ ) …)
∈ \underbrace{Λ_{t}(… Λ_{t}(}_{m} Seq[[ A, y_{1}^{σ_{1}},…, y_{m}^{σ_{m}} ⊢ E_{1}[x_{i}] ]] ) …)
= Seq[[ A ⊢ λy_{1}^{σ_{1}} … y_{m}^{σ_{m}}.E_{1}[x_{i}] ]]

and

⟨?⟩ · ⟨⟨… ⟨⟨?⟩, 2⟩, \underbrace{1⟩,…, 1⟩}_{k−i}, 1⟩ ∈ Seq[[ A ⊢ catch (λy_{1}^{σ_{1}} … y_{m}^{σ_{m}}.E_{1}[x_{i}]) ]]

follows, since the sequentiality index of catch at (⊥, ⟨?⟩) is ⟨?⟩.

For the only-if part of the Adequacy Theorem, we slightly modify Plotkin’s computability method originally developed for the adequacy theorem for PCF [24]. We proceed in two steps. First, we prove an adequacy theorem for SPCF_{1}, which is SPCF without the Y operators. It has the same operational semantics as SPCF. Second, we lift the adequacy theorem for SPCF_{1} by relating SPCF programs with Y to SPCF_{1} programs with Y_{n} and by relating their evaluations.

To prove adequacy for SPCF_{1}, we first prove that all evaluation sequences are finite. The proof requires a generalization of this claim to closed phrases of all types.

Definition 8.15 (Comp_{τ}) The family of sets of closed SPCF_{1} phrases Comp_{τ} is defined by induction on types:

Comp_{o} = {M | M ↦^{∗} ^{⌈}n^{⌉}, M ↦^{∗} e, M ↦^{∗} E[Ω]}
Comp_{σ→τ} = {M | ∀N ∈ Comp_{σ}.(M N) ∈ Comp_{τ} }.

We say ⊢ M : σ is normalizing if M ∈ Comp_{σ}.

All SPCF_{1} phrases are normalizing.

Lemma 8.16 (Normalization of SPCF_{1}) For every SPCF_{1} program M, M ∈ Comp_{o}.

Proof. For notational convenience, F ranges over numerals, errors, and E[Ω] in this proof. The proof consists of three parts. The first claim shows that a phrase that standard reduces to a normalizing phrase is normalizing.

Claim 1: Let M and M′ be closed phrases of type τ. If M ↦ M′ and M′ ∈ Comp_{τ}, then M ∈ Comp_{τ}.

The proof is an induction on types:

1. Assume τ = o. By assumption, M′ ↦^{∗} F and M ↦ M′. Hence, M ↦^{∗} F.

2. Assume τ = σ → ν. We must show (M P) ∈ Comp_{ν}, for any P ∈ Comp_{σ}. By Lemma 8.12, M ↦ M′ implies (M P) ↦ (M′ P). Since (M′ P) ∈ Comp_{ν} due to the assumptions, the inductive hypothesis implies that (M P) ∈ Comp_{ν}, which is what we had to show. _{Claim1}

Second, we prove that substituting normalizing phrases for all free variables in an open phrase yields a normalizing phrase.

Claim 2: If x_{1} : σ_{1},…, x_{n} : σ_{n} ⊢ M : σ, then N_{1} ∈ Comp_{σ_{1}}, …, N_{n} ∈ Comp_{σ_{n}} implies M[N_{1}/x_{1},…, N_{n}/x_{n}] ∈ Comp_{σ}.

We use the notation M[N⃗/x⃗] to abbreviate M[N_{1}/x_{1},…, N_{n}/x_{n}]. The proof procceds by induction on the structure of M:

1. M = x_{i} . Then M[N⃗/x⃗] = N_{i}, and the conclusion is one of the assumptions.

2. M = e. Then M[N⃗/x⃗] = e, and hence M ∈ Comp_{o}.

3. M = ^{⌈}n^{⌉}. This case is similar to the preceding case.

4. M = Ω. If σ_{1} → … → σ_{m} → o is the type of M, we must prove ΩN_{1} … N_{m} ∈ Comp_{o}. But this holds vacuously since Seq[[ ΩN_{1} … N_{m}]]⋆ ⊥=⊥.

5. M = (f M′) where f ≠ catch. Assume f = sub1. By inductive hypothesis, M′[N⃗/x⃗] ∈ Comp_{o}, i.e.,

(a) M′[N⃗/x⃗] ↦^{∗} ^{⌈}0^{⌉}: then, M ↦^{∗} (sub1 ^{⌈}0^{⌉});

(b) M′[N⃗/x⃗] ↦^{∗} ^{⌈}m + 1^{⌉}: then, M ↦^{∗} (sub1 ^{⌈}m + 1^{⌉}) ↦ ^{⌈}m^{⌉};

(c) M′[N⃗/x⃗] ↦^{∗} e: then, M ↦^{∗} (sub1 e) ↦ e

(d) M′[N⃗/x⃗] ↦^{∗} E′[Ω]: then, M ↦^{∗} (sub1 E′[Ω]) = E[Ω] where E[ ] = (sub1 E′[ ]).

In summary, for all possible cases, M is normalizing.

The treatment of the cases for f = add1 and f = if0 is similar but easier.

6. M = (Y_{n}^{τ} M′). By induction hypothesis, M′[N⃗/x⃗] is normalizing. Call this phrase N . The rest is proved by sub-induction on n. For n = 0, M ↦ Ω^{(τ→τ)}. If L_{1},…, L_{a} (where a is the arity of M ) are normalizing expressions, then (Ω^{τ→τ} L_{1} … L_{a}) ↦ Ω^{o}, which proves that Ω^{τ→τ} is normalizing. For n > 0, (Y_{n} N) ↦ (N (Y_{n−1} N)). Since the sub-induction of this case implies that Y_{n−1} N ∈ Comp_{σ}, N (Y_{n−1} N)) ∈ Comp_{σ} by definition of Comp_{σ}. By Claim 1, M[N⃗/x⃗] ∈ Comp_{σ}.

7. M = λx^{τ} .M′. Assume that σ = τ → ν. Let N be a phrase in Comp_{τ}. Then (M[N⃗/x⃗] N) ↦ M′[x/N][N⃗/x⃗], which, by the inductive hypothesis, is normalizing. Hence, (M[N⃗/x⃗] N) ∈ Comp_{ν} for every N ∈ Comp_{τ}, which is what we had to show.

8. M = (M_{1} M_{2}). By the inductive hypothesis, M_{1}[N⃗/x⃗] and M_{2}[N⃗/x⃗] are normalizing. The rest follows by the definition of Comp at higher types.

9. M = (catch M′). Set N = M′[N⃗/x⃗], which is normalizing by inductive hypothesis. Assume N has type τ and arity a. Since (catch N) is a program, either (catch N) ↦^{∗} F or (catch N) ∈ Inf_{o} by the Uniform Evaluation Lemma. We need to prove that the latter cannot happen. If it does, Lemma 8.11 implies that N ∈ Inf_{τ}. By Proposition 8.12, for all L_{1},…, L_{a}, and in particular normalizing ones, (N L_{1} … L_{a}) ∈ Inf_{o}. But this contradicts the normalizability of N . Hence, M ∈ Comp_{o}. _{Claim 2}

Finally, since closed phrases are just a special case of Claim 3, we have also shown that all SPCF_{1} programs are normalizing.

Based on the Normalization Lemma for SPCF_{1}, it is easy to prove an adequacy lemma.

Lemma 8.17 (Adequacy of SPCF_{1}) For all SPCF_{1} programs M (⊢ M : o),

1. if Seq[[ ⊢ M ]] ⋆ ⊥ = {? · m} then M ↦^{∗} ^{⌈}m^{⌉};

2. if Seq[[ ⊢ M ]] ⋆ ⊥ = {? · e} then M ↦^{∗} e;

3. if Seq[[ ⊢ M ]] ⋆ ⊥ = {} then M ↦^{∗} E[Ω].

Proof. By the Normalization Lemma (8.16), the evaluation of M can only proceed in one of three possible ways:

1. M ↦^{∗} ^{⌈}m^{⌉}: By Soundness, we get Seq[[ M ]]⋆ ⊥= {? · m}.

2. M ↦^{∗} e: By Soundness, Seq[[ M ]]⋆ ⊥= e for any e ∈ .

3. M ↦^{∗} E[Ω]: By Soundness, Seq[[ M ]]⋆ ⊥=⊥.

Now if Seq[[ M ]]⋆ ⊥= m, then M ↦^{∗} m; anything else would contradict the preceding case analysis. The same argument works in the other two cases.

Adequacy for full SPCF is a simple consequence of the preceding lemma.

Proof of Theorem 8.13. The right-to-left direction is a consequence of Lemma 8.14. The left-to-right direction follows from Lemma 8.17, the Adequacy Lemma for SPCF_{1}. The result is lifted to full SPCF as follows. The semantics of (Y M) is the least upper bound of the semantics of the expressions (Y_{n} M) for all n ∈ . Hence for any program M, if Seq[[ ⊢ M ]]⋆ ⊥≠⊥, then by continuity there is some sufficiently large n, such that Seq[[ ⊢ M ]] = Seq[[ ⊢ N ]], where N is the term obtained from M by replacing all the occurrences of Y in M by Y_{n}. By Lemma 8.17, N evaluates to its meaning. To obtain a reduction from M to the answer, it suffices to replace residuals of (Y_{n} L), which are terms of the form (L (… (L Ω) …)), with (Y L). This finishes the proof of the adequacy theorem.

9 Generalizing Observable Sequentiality

Since PCF procedures have multiple sequentiality indices, PCF is clearly neither an observably sequential nor a manifestly sequential programming language (cmp. Definition 4.2). Consequently, the decision tree semantics for PCF is not fully abstract. However, the interesting question is which practical programming languages with non-local control operators are not manifestly sequential or observably sequential. At this point we know of one prominent example: sequential languages with control delimiters [12], also called 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 manifestly sequential 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 % and indexed error constants [30]. The defining equation for % is

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

In PCF′, we can define an addition procedure that does not propagate errors:

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

demonstrating that PCF′ is not a manifestly sequential language. A similar argument also shows that the extended language is not observably sequential. At this point, we do not know how to modify our construction to solve the full abstraction problem for PCF′ and other languages with control delimiters.

Acknowledgements. R. Cartwright and M. Felleisen thank Rama Kanneganti and Dorai Sitaram for helping hone their intuitions about manifest sequentiality, sequential functions, and for numerous discussions about SPCF. Steve Brookes pointed out a mistake in our original definition of syntactic sequentiality. John Gately and Trevor Jim discovered inconsistencies in the first versions of [7] and [10]. The authors gratefully acknowledge comments by Trevor Jim and Robert Harper on an early version of this manuscript. Finally, the authors want to thank the referees for their very careful readings.

A Sequential Data Structures vs. Concrete Data Structures

In this appendix, we connect the sequential data structures introduced in this paper with the concrete data structures of Berry-Curien. We define a category Seq( ) of observable sequential algorithms uniformly for any set of errors. We show that the definition of Seq( ) in Section 6 and the definition of the same category here are equivalent. We also show that the category Seq(∅) is equivalent to Berry-Curien’s category of sequential algorithms. In the process, we introduce filiform data structures, which are intermediate constructions in the gap between concrete data structures and sequential data structures.

A.1 Filiform Data Structures

We begin this subsection by recalling the definition of a concrete data structure. Then we show that filiform concrete data structures correspond through an equivalence of categories to the sequential data structures defined in this paper.

A filiform concrete data structure (fcds for short) is a quadruple (C, V, E, ⊢) where C and V are collections of cells and values, respectively; E is a subset of C × V; and ⊢ is a subset of (E × C) ∪ C. If (c, v) ∈ E, we say that (c, v) is an event, and that c is filled with v. We assume that each cell can be filled: for each c, there is a v such that (c, v) ∈ E. The set ⊢ is called the enabling relation. We write (c_{1}, v_{1}) ⊢ c to assert that ((c_{1}, v_{1}), c) is a member of ⊢ ∩ (E × C), and we say that event (c_{1}, v_{1}) enables cell c. We also say that c_{1} precedes c. We write ⊢ c to assert that c is a member of ⊢ ∩ C. For ⊢ c, we say that c is initial and has an empty enabling. We assume that the precedence relation is well-founded. An fcds is canonical if each cell has a unique enabling. A state of the fcds (C, V, E, ⊢) is a subset x of E that is:

• consistent: if (c, v_{1}) ∈ x and (c, v_{2}) ∈ x, then v_{1} = v_{2}; and

• safe: if (c, v) ∈ x, then x contains an enabling of c.

We assume that fcds’s are stable, which means that given a state x and a cell c filled in x ((c, v) ∈ x for some v), there is exactly one enabling of c in x. Canonical fcds’s are obviously stable. For non-canonical fcds’s, the stability condition must be proved for each domain construction, notably the exponent construction. In contrast, all sequential data structures are canonical and hence stable.

To help explain the connection between fcds’s with sds’s, we introduce the intermediate notion of a filiform data structure. The preceding definition of fcds is a restriction of the general definition of a (stable) concrete data structure (cds). In a general cds, an enabling consists of a finite collection of events. Thus the filiform case corresponds to restricting the maximum cardinality of enablings in a cds to 1. The category of fcds’s and sequential algorithms forms a full cartesian-closed subcategory of the category of stable cds’s and sequential algorithms [8: Theorem 2.6.7]. As a result, we are free to ignore the more general setting of stable cds’s and to take advantage of the special form of fcds’s. In the filiform case, the notions of “filling a cell” and of “enabling a cell” become dual in a loose sense. This fact can be emphasized by changing notation: we can write c ≺ (c, v) when (c, v) ∈ E, and (c_{1}, v_{1}) ≺ c when (c_{1}, v_{1}) ⊢ c. These observations lead to the following definition.

Definition A.1 (Filiform Data Structure) A filiform data structure (fds) (C, E, ≺) consists of a collection C of cells, a collection E of events, and a subset ≺ of (C × E) ∪ (E × C) ∪ C, called the precedence relation where:

• the precedence relation is well-founded; and

• each event e has a unique predecessor.

We write ≺ c to assert that c is a member of ≺ ∩ C. In this case, we say that c is initial and that it has an empty enabling.

The states of the fds are defined as the subsets x of E that are:

• consistent: if c ≺ e_{1}, c ≺ e_{2}, and e_{1} and e_{2} both belong to x, then e_{1} = e_{2}; and

• safe: if e ∈ x, then either the predecessor c of e is initial, or there exists e_{1} ∈ x such that e_{1} ≺ c ≺ e.

We assume that every fds stable: for any state x and any event e ∈ x, the predecessor c of e has at most one predecessor in x. As for fcds’s, we say that an fds is canonical if each cell has at most one predecessor. As before, canonicity implies stability. In addition, the wellfoundedness of ≺ implies that for any state x and any e ∈ x, there exist c_{1}, e_{1} … e_{n−1}, c_{n} such that ≺ c_{1} ≺ e_{1} ≺ … ≺ e_{n−1} ≺ c_{n} ≺ e and e_{1},…, e_{n−1} ∈ x. We call this a proof of e in x.

The notions of fcds and of fds lead to equivalent categories. Although we have not yet defined these categories, the following “textual” correspondence should suffice to justify this claim:

• Given an fcds (C, V, E, ⊢), construct the fds (C, E, ≺), where ≺ c iff ⊢ c; e ≺ c iff e ⊢ c; and c ≺ e iff e = (c, v) for some v.

• Given an fds N = (C, E, ≺), construct the fcds G(N) = (C, E, E′, ⊢), E′ is the set {(c, e) | e ∈ E, c ≺ e}; ⊢ c iff ≺ c; and (c_{1}, e) ⊢ c iff e ≺ c.

These transformations induce order-isomorphisms between the respective sets of states and trees. If we compose the two transformations in either order, we obtain a structure isomorphic to the structure we started with. If we start with an fcds (C, V, E, ⊢), we produce an fcds (C, E, E′, ⊢), whose states are obtained by replacing each (c, v) by (c, (c, v)). Similarly, if we start with an fds (C, E, ≺), we obtain an fds (C, E′, ≺), whose states are obtained by replacing each e by (c, e), where c is the predecessor of e.

As for sds’s (and fcds’s), we write (C, E, ≺) for the set of states of an fds (C, E, ≺), ordered by inclusion.

We now connect sds’s and fds’s. Given an sds M = (A, D, P), we construct the fds F (M) = (Que, Res, ≺), where Que and Res are the sets of queries and responses of M, respectively; ≺ p if and only if |p| = 1; and p_{1} ≺ p_{2} if and only if p_{2} = p_{1} · u for some u. Notice that F (M) is canonical. The following observations give us the ingredients for proving an equivalence of categories:

• The cpos (M) and (F (M)) coincide. This fact follows immediately from the observatins that prefix-closure implies safety, and glb-closure implies consistency.

• Any fds (C, E, ≺) is isomorphic to the image of an sds (A, D, P) under F. We construct (A, D, P) as follows: let A = C, D = E, and let P be the set of all the finite precedence chains starting from an initial cell. Let the inverse mappings ϕ and ψ that define the one-to-one correspondence between (C, E, ≺) and (F (C, E, P)) by defined as follows. The mapping ϕ replaces events e by their unique proof in x; ψ replaces every response with its terminal event. Notice the key role that stability plays in justifying the correspondence.

Since F maps sds’s to canonical fds’s, these observations also imply that fds’s and canonical fds’s define equivalent categories. Berry and Curien chose to work with a non-canonical presentation of the exponent of two canonical cds’s because this choice made it easier to define composition arrows in their category.

The preceding discussion of fcds’s and sds’s can easily be extended to include a given predefined set of errors. We define states relative to just as we did for trees in Section 5, and we call them observable states when is not empty.

The composition of the transformations F from sds’s to fds’s, and G from fds’s to fcds’s, yields a mapping H that can be converted to an equivalence functor.

A.2 A Uniform Definition of Sequential Algorithms

In this subsection, we define categories of sds’s (and fds’s) with arrows that are (manifestly) sequential algorithms. If the set of errors ≠ ∅, then the manifestly sequential algorithms correspond to functions and the methods used in Section 6 suffice. But if = ∅, we need to do more work to define a cartesian-closed category of either trees (using sds’s) or states (using fds’s). We will follow the approach taken by Berry-Curien to define an abstract algorithm between two sds’s, suitable for a simple definition of composition.

In the remainder of this section, we use the following notation. If x is a tree over an sds (with or without error values), we write Enabled(x) for Answered(x) ∪ Open(x).

Definition A.2 (Abstract algorithms) Let M = (A, D, P) and M′ = (A′, D′, P′) be two sds’s. Let Que, Res, Que′, and Res′ abbreviate Que_{M}, Res_{M}, Que_{M′}, and Res_{M′}, respectively. We let u range over D′ ∪ Que ∪ , and w′ range over D′ ∪ . An abstract algorithm from M to M′ is a partial function f from (M) × Que′ to D′ ∪ Que ∪ satisfying the following axioms:

(A0) f(x, q′) defined ⇒ ∃y ≤ x (y finite and f(y, q′) = f(x, q′)),
(A1.1) f(x, q′) = d′ ∈ D′ ⇒ (q′ · d′) ∈ P′,
(A1.2) f(x, q′) = q ∈ Que ⇒ q ∈ Open(x),
(A2.1) f(x, q′) = w′ ∈ D′ ∪ , x ≤ y ⇒ f(y, q′) = w′,
(A2.2) f(x, q′) = q, x ≤ y and q ∈ Open(y) ⇒ f(y, q′) = q,
(A2.3) f(x, q′) = q ⇒ f(x ∪ {q · e}, q′) = e, for any e ∈ .
(A3.1) f(x, q′) defined ⇒ q′ ∈ Enabled(f ∗ x),
(A3.2) f(x, q′) defined, y ⊑ x and q′ ∈ Enabled(f ∗ y) ⇒ f(y, q′) defined.

where

f ∗ x = {(q′ · w′) | f(x, q′) = w′ for w′ ∈ D′ ∪ }.

In the case where is non-empty, we use the term abstract algorithms with errors instead of abstract algorithms.

Let M′′ = (A′′, D′′, P′′) be a third sds, and let g be an abstract algorithm from M′ to M′′. The composition h = g ∘ f is defined as follows:

h(x, q′′) = \{ \begin{matrix}q ∈ Que′′ & if g(f ∗ x, q′′) = q′ and f(x, q′) = q \\ w′′ ∈ D′′ ∪ & if g(f ∗ x, q′′) = w′′ \end{matrix}

The mapping x ↦ f ∗ x defines a manifestly sequential function from (M) to (M′), which we call the function computed by f. When ≠ ∅, the abstract algorithms are equivalent to the manifestly sequential functions defined in Section 6. But abstract algorithms support a uniform construction of Seq( ), independent of .

The proof that the composition is well-defined follows the corresponding proof for Berry and Curien’s abstract algorithms [8: Proposition 2.6.1]. Consequently, we only check the axiom (A2.3) involving errors. If h(x, q′′) = q, then g(f ∗ x, q′′) = q′ and f(x, q′) = q. By (A2.3) applied to f and g, respectively, we have f(x ∪ {q · e}, q′) = e and g((f ∗ x) ∪ {q′ · e}, q′′) = e. From the first equation, we deduce that (q′ · e) ∈ f ∗ (x ∪ {q · e}), implying (f ∗ x) ∪ {q′ · e} ≤ f ∗ (x ∪ {q · e}). The conclusion of the axiom follows from applying (A2.3) and (A2.1) to g.

We can now define a category of sds’s and (abstract) sequential algorithms.

Definition A.3 (Seq( )) The category of (manifestly) sequential objects and algorithms over an error set is defined as follows:

1. the collection of objects is { (M) | M is an sds}, the set of (manifestly) sequential domains over sds’s relative to ;

2. the collection of arrows between the objects (M_{1}) and (M_{2}) is (M_{1} ⇒ M_{2}) (see Definition 6.21), the set of (observably) sequential algorithms relative to ;

3. the composition operation for arrows is defined via the composition of trees when interpreted as abstract algorithms (see Definition A.2);

4. for each object the identity arrow is the identity algorithm.

The main theorem of this appendix states that Seq( ) is cartesian-closed, for any . This fact can be proved uniformly for any by faithfully imitating the proofs of Curien [8]. In this subsection, we merely sketch the proof by partititioning it into two cases: = ∅ and ≠ ∅. In each case, we show that the category Seq( ) is equivalent to a category which we already know to be cartesian-closed.

Theorem A.4 The category Seq( ) is cartesian-closed, for all sets of error values.

Proof. If = ∅, we proceed as follows. The mapping H from sds’s to fcds’s defined in the previous subsection extends to a full and faithful functor from Seq(∅) to the category ALGO of stable cds’s and sequential algorithms, shown to be cartesian closed [8]. The functor H is actually into the full subcategory fALGO of fcds’s. This full subcategory is also cartesian-closed (the product and exponent of two fcds’s is filiform) [8: Theorem 2.6.7]. The arguments given in the last subsection can be easily turned into a formal proof that Seq(∅) is equivalent to fALGO. Hence, it is cartesian-closed.

If ≠ ∅, it is straightforward to show that the abstract algorithms with errors are in one-to-one correspondence with the manifestly sequential functions. The bijection “forgets” an abstract algorithm f and takes “only” the function x ↦ f ∗ x that it computes. The inverse bijection makes the sequentiality indices of a manifestly sequential function explicit. We omit the details.

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és. Thèse d’Etat, 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 J.-J. 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.S. and M. Felleisen. Observable sequentiality and full abstraction. Technical Report 91-167. Rice University Department of Computer Science, 1991. Preliminary version: In Proc. 19th ACM Symposium on Principles of Programming Languages, 1992, 328–342.

8. Curien, P.-L. Categorical Combinators, Sequential Algorithms, and Functional Programming. Research Notes in Theoretical Computer Science. Pitman, London. 1986. Birkhäuser, Revised Edition, 1993.

9. Curien, P.-L. Sequentiality and full abstraction. In Applications of Categories in Computer Science, M.P. Fourman, P.T. Johnstone, and A.M. Pitts (Eds). Cambridge University Press, New York, 1992.

10. Curien, P.-L. Observable algorithms on concrete data structures. In Proc. 7th Symposium on Logic in Computer Science, 1992, 432–443.

11. Curien, P.-L. On the symmetry of sequentiality. In Proc. Mathematical Foundations of Programming Semantics 1993. Springer Lecture Notes in Computer Science, Berlin. To appear.

12. Felleisen, M. The theory and practice of first-class prompts. In Proc. 15th ACM Symposium on Principles of Programming Languages, 1988, 180–190.

13. Felleisen, M. and D.P. Friedman. Control operators, the SECD-machine, and the λ-calculus. In Formal Description of Programming Concepts III , edited by M. Wirsing. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986, 193–217.

14. 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. 102, 1992, 235–271.

15. 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.

16. 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 Heidelberg 1991. 131–151.

17. Jung, A., and A. Stoughton. Studying the fully abstract model of PCF within its continuous function model. In Proc. Conference on Typed Lambda Calculi and Applications. Lecture Notes in Computer Science 664. Springer Verlag, Berlin Heidelberg 1993.

18. Kahn, G. and G. Plotkin. Domaines Concrets. IRIA Report 336. 1978. English translation: Concrete domains, to appear in C. Boehm Festschrift, special volume of Theoretical Computer Science.

19. Kanneganti, R., R. Cartwright, and M. Felleisen. SPCF: its model, calculus, and computational power. In Proc. REX Workshop on Semantics and Concurrency. Lecture Notes in Computer Science 666. Springer Verlag, Berlin Heidelberg 1993. 318– 347.

20. Lamarche, M. Sequentiality, games and linear logic. Unpublished manuscript. Ecole Normale Supérieure, 1992.

21. 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.

22. Milner, R. Fully abstract models of typed λ-calculi. Theor. Comput. Sci. 4, 1977, 1–22.

23. Mulmuley, K. Full Abstraction and Semantic Equivalence. MIT Press, Cambridge, Massachusetts, 1986.

24. Plotkin, G.D. LCF considered as a programming language. Theor. Comput. Sci. 5, 1977, 223–255.

25. Plotkin, G.D. Call-by-name, call-by-value, and the λ-calculus. Theor. Comput. Sci. 1, 1975, 125–159.

26. Sazonov, V.Y. Expressibility of functions in D.Scott’s LCF language. Algebra i Logika 15(3), 1976, 308–330.

27. Scott, D. S. Domains for denotational semantics. In Proc. International Conference on Automata, Languages, and Programming, Lecture Notes in Mathematics 140, Springer Verlag, Berlin, 1982, 577–613.

28. Scott, D.S. Lectures on a Mathematical Theory of Computation. Techn. Monograph PRG-19, Oxford University Computing Laboratory, Programming Research Group, 1981.

29. Sieber, K. Relating full abstraction results for different programming languages. In 10th Conference on Foundations of Software Engineering and Theoretical Computer Science. K.V. Nori and C.E. Veni Madhavan, Eds. Lecture Notes in Computer Science 472. Springer Verlag, Berlin, 1990, 373–387.

30. 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. Corrections posted to the “continuations” email list on September 22, 1992 (also available from titan.cs.rice.edu via anonymous ftp in public/languages as lfp90-sf-correction.{ps,dvi}.Z).

31. Steele, G.L., Jr. and G.J. Sussman. The revised report on Scheme, a dialect of Lisp. Memo 452, MIT AI-Lab, 1978.

32. Stoughton, A. Fully Abstract Models of Programming Languages. Research Notes in Theoretical Computer Science. Pitman, London. 1986.

33. Vuillemin, J. Proof techniques for recursive programs. IRIA Report. 1973.

88 R. Cartwright, P.-L. Curien, M. Felleisen

Notation

Notation  Description  Section

Sets

the set of natural numbers  2
A \ B  set minus  2
A ⊎ B  tagged, disjoint union  2
(\underline{λ}x : A. · · · x ⋯) mathematical function from A to B  2
⟨x, y⟩ cartesian pair of x and y 2

Domains

(D, ⊑) partial order, approximation relation 2
strict partial order (below)  2
⊔  least upper bound  2
x ↑ y  bounded (consistent) elements x and y  2
⊓  greatest lower bound  2
⊥  least element  2
⊥  flat domain of natural numbers  2

Paths

Σ^{∗}  set of paths over alphabet Σ  2
ϵ  empty path  2
a · p  consing a onto path p  2
p · a  consing a onto the end of p  2
q · p  appending q onto p  2
p @ n  nth element in path p  2
(Φ, Ψ)^{∗}  set of alternating paths  2
∘  composition of arrows  2

Categories

id^{A}  identity arrow for object A  2
1  terminal object  2
1^{A}  unique arrow from object A to 1  2
A × B  cartesian product of A and B  2
π_{i}  cartesian projection to the ith component 2
π_{i}^{n}  ith cartesian projection for n fold product 2
A ⇒ B  exponent of A and B  2
Λ, Λ^{−1}  curry function and inverse  2
App  application arrow  2

Notation  Description  Section

PCF syntax

o  PCF ground type (number)  3
τ → σ  PCF procedure type  3
x  PCF variable  3
x^{τ}  typed PCF variable  3
λx.M  PCF procedure  3
(M N)  PCF application  3
(f M)  PCF primitive application  3
⌈n^{⌉}  PCF numeral  3
add1  PCF successor primitive  3
sub1  PCF predecessor primitive  3
if0  PCF zero test primitive  3
Y  PCF fixed-point operator  3
C[ ]  PCF single hole context  3
C[ ]_{1} … [ ]_{n} PCF multiple hole context  3
A ⊢ M : τ  PCF type judgement  3
Ω  Syntactic representation of ⊥  3
Y^{n}  nth approximation of Y  3

Semantics

C  meta-variable for PCF semantics  3
Dom  continuous functions semantics of PCF  3
⊑_{C}  denotational approximation for terms,  3

relative to a semantics C

≡_{C}  denotational equivalence relation for terms, 3

relative to a semantics C

∼  operational approximation  3
≃  operational equivalence  3
+_{l}  left addition  3
+_{r}  right addition  3

SPCF

SPCF set of error values  4
e  element of  4
catch  SPCF catch operation  4
L_{}set of error expressions in PCF-like language 4
E  element of L_{}4

Notation  Description  Section

sdss

M = (A, D, P)  sequential data structure  5
Res_{M}  responses of sds M  5
Que_{M}  queries of sds M  5
N  sds of natural numbers  5
T  sds of booleans  5
N^{4} → N  sds for algorithms from N^{4} to N  5
(M)  domain over sds M  5
0(M)  finite elements in (M)  5
_{⊥}^{e}  flat domain of natural numbers and errors  5
Open(x)  open queries of element x  5
Answered(x)  answered queries in element x  5
(M_{1} ⇒ M_{2})  (observably) sequential functions:  5
(M_{1}) ⟶ (M_{2})
si_{f}(x, q′)  sequentiality index of f at x and q′  5

Function Trees

SEQ( )  category of (observably) sequential domains 6

and functions

Seq( )  category of (observably) sequential domains 6

and functions-as-trees

π_{i}^{×}  projection for cartesian products in SEQ( )  6.1
inj_{i}  injection for cartesian products in SEQ( )  6.1
||s||  domain element determined by s  6.2.1
π\overrightarrow{1}  projection to input sds of exponent  6.2.1
π\overrightarrow{2}  projection to output sds of exponent  6.2.1
⋆  application operation  6.2.1
Fun  isomorphism from exponent to function space 6.2.1
Tree  inverse of Fun  6.2.1
Path_{f}(x, p)  path for simulating f on x with p ∈ f(x)  6.2.1
Λ_{t}, Λ_{t}^{−1}  curry function and inverse for trees  6.2.2

SPCF Semantics

⟨?⟩  initial address for (M_{1} ⇒ … M_{k} ⇒ N)  7
⟨n⟩  initial datum behind ⟨?⟩  7
⟨p, i⟩  path in ith part of (M_{1} ⇒ … M_{k} ⇒ N)  7
π_{i}  = π\overrightarrow{1}(\underbrace{π\overrightarrow{2}(… π\overrightarrow{2}}_{i−1}(p) …)  7
for (M_{1} ⇒ … M_{k} ⇒ N)
A  denotation of add1  7
S  denotation of sub1  7
I  denotation of if0  7
C  denotation of catch  7

Notation  Description  Section

Operational Semantics

E[ ]  evaluation context  8
M ⟶ N  SPCF reduction relation  8
M = N  SPCF calculus  8
M ↦ N  SPCF standard reduction  8
eval_{SPCF}  SPCF evaluator for  8
Eval_{τ}  uniform evaluation set  8
Inf_{τ}  set of terms with infinite evaluation 8
Comp_{τ}  set of tersm with finite evaluation 8

Appendix

(C, V, E, ⊢)  concrete data structure  A.1
(C, E, ≺)  filiform data structure  A.1
∗  application of abstract algorithms A.2

Contents

1 Full Abstraction and Sequentiality 1 1.1 History of Previous Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Summary of Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 Mathematical Preliminaries 5

3 PCF: Syntax and Semantics 9 3.1 PCF Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.2 PCF Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.3 Full Abstraction and Sequentiality . . . . . . . . . . . . . . . . . . . . . . . 14

4 Observing Sequentiality 15 4.1 Using Errors, Programmers Can Observe the Order of Evaluation . . . . . . 16 4.2 Using Control Operators, Programs Can Observe the Order of Evaluation . 16 4.3 Observably Sequential Programming Languages . . . . . . . . . . . . . . . . 18 4.4 Procedure Denotations Have Explicit Computational Structure . . . . . . . 18 4.5 Higher-order Procedures Explore and Output Trees Sequentially . . . . . . 21 4.6 SPCF Defines Manifestly Sequential Functions . . . . . . . . . . . . . . . . 23

5 Sequential Data Structures with Errors 23

6 The Manifestly Sequential Cartesian-Closed Category 31 6.1 SEQ( ) is Cartesian . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 6.2 SEQ( ) is Cartesian-Closed . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

6.2.1 An Extensional Representation of Functions as Trees . . . . . . . . . 34 6.2.2 The Exponent Object . . . . . . . . . . . . . . . . . . . . . . . . . . 48

7 Full Abstraction for SPCF 50

8 An Adequate Operational Semantics for SPCF 68 8.1 Operational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 8.2 Adequacy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74

9 Generalizing Observable Sequentiality 79

A Sequential Data Structures vs. Concrete Data Structures 80 A.1 Filiform Data Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 A.2 A Uniform Definition of Sequential Algorithms . . . . . . . . . . . . . . . . 83

References 85

Notation 88