Reasoning with Continuations II: Full Abstraction for Models of Control

Dorai Sitaram and Matthias Felleisen^{∗}

Department of Computer Science

Rice University Houston, TX 77251-1892

Abstract

A fully abstract model of a programming language assigns the same meaning to two terms if and only if they have the same operational behavior. Such models are well-known for functional languages but little is known about extended functional languages with sophisticated control structures. We show that a direct model with error values and the conventional continuation model are adequate for functional languages augmented with first- and higher-order control facilities, respectively. Furthermore, both models become fully abstract on adding a control delimiter and a parallel conditional to the programming languages.

1 The Control Structure of Lisp

Many programming languages, in particular Lisp [17, 24] and Scheme [22, 26], contain sophisticated control structures with constructs for labeling the control state at an arbitrary point for later reuse. Since Lisp is an expression-oriented language, a jump to a labeled control state—just like a procedure—may also pass a parameter so that it is possible to communicate results between control points. In most Lisp systems, control points have a special status, distinct from all other values. The Scheme dialect treats its control points—referred to as continuations—as ordinary, first-class procedural objects and even uses the same syntax for continuation invocations and procedure calls.

For many programming tasks, control facilities are an important means of abstraction. They avoid the cumbersome encoding of control mechanisms through boolean predicates and tests, and explicate the purpose of otherwise unreadable programming patterns. Moreover, by incorporating explicit statements about the control behavior, a program provides clues to the compiler for possible optimizations. However, control constructs also invalidate some common laws of reasoning that hold for functional programming languages like pure Lisp [6, 18, 27]. More technically, the operational equivalence relation for the functional subset of Lisp is not a subset of the operational equivalence relation for Lisp with control facilities. Given the importance of operational equivalence laws for reasoning about programs, this raises two crucial questions:

1. How can we reason with control facilities?

2. How can we relate the reasoning system for functional languages to the system for extended languages with control facilities?

Talcott’s [27, 28] and our own [6, 7, 11] results on functional languages with first-class control abstractions provide a partial answer to the first question.^{1} There is a small number of fundamental laws for the operational equivalence relation of such languages that play a crucial role in equivalence proofs of Lisp-like programs with continuations. Based on these laws, it is possible to manipulate such programs with the same algebraic elegance as functional programs. Our work [6, 7, 11] on conservative extensions of Plotkin’s [20] λ_{v}-calculus for pure Lisp also contributes to an answer for the second question. It shows that all equational proofs in the syntactic theory of functional languages carry over to the extended framework with control mechanisms.

∗The work of both authors was partially supported by NSF and DARPA.

0

1The recent work by Aiken et al [1] on program transformations in the presence of errors can also be viewed as addressing this problem although their main concern is quite different.

Unfortunately, both pieces of research are only incomplete answers to the above questions. Reasoning directly about operational equivalence is a powerful approach but suffers from the sensitivity of the relation to language extensions. This approach also ignores the existing mathematical models for functional languages and the potential for exploiting traditional mathematical techniques for reasoning about programs. Our extended λ_{v}- calculus, on the other hand, is necessarily a weak reasoning tool because it accomodates language extensions. It particularly lacks an induction principle, which automatically comes with denotational models.

In this paper we present another step toward a reasoning system for languages with control structure. Following Plotkin’s [21] approach, we analyze extensions of a typed functional language with Lisp-style control facilities and their natural models. Adjusting the programming languages so that these models become fully abstract leads to the surprising re-discovery of first-class prompts: We had earlier suggested the inclusion of prompts in languages with control structures but for entirely different reasons [8, 23]. The full abstraction theorem for the conventional continuation model also verifies a conjecture by Meyer and Riecke [18:65].

The following section introduces Pcfv-c, an extension of a call-by-value variant of Pcf [21] with a sophisticated control structure. It also contains a formal discussion on the above-mentioned problematic relationship between the operational equivalence relations of Pcfv and the extended languages, providing a comprehensive overview of the expressive power of the various control constructs [9]. The third section describes the properties of a denotational semantics for Pcfv and the related notions of denotational equivalence, adequacy and full abstraction. The fourth and fifth sections present direct and continuation models for first- and higher-order control structures, respectively. In both cases, full abstraction fails for the original languages, but language extensions can fix both instances of the problem. The last section interprets our results with respect to programming language design.

2 Pcfv-c

Pcfv-c is an extension of call-by-value Pcf [21] with control facilities. Pcfv, the programming language of computable functions, is a variant of the typed λ-value-calculus with ground constants, conditionals, and fixpoint combinators.

Figure 1 describes the types and syntax of Pcfv. Subscripts on terms indicate the types of the terms; superscripts indicate the types of variables. The language includes the numeral n for each natural number n. As usual, λ-abstractions introduce bound variables; those variables in a term that are not bound are free. A term with no free variables is closed. Pcfv programs are closed Pcfv terms of ground type. The notation M[x:=N] denotes the substitution of all occurrences of a free variable x in M with the term N. Finally, a context C[ ] is a term with a “hole” where a subterm should be; C[M] is the term where the hole is filled with a subterm M of appropriate type, with the context possibly capturing free variables in M. We adopt the usual conventions governing the use of concrete syntax for λ-expressions [2].

Figure 1 also specifies the primitive transition rules (⟶) of an abstract machine for Pcfv. The numerals represent numbers. The functional constants 1+ and 1− have the behavior of “add 1” and “subtract 1.” A thunk is a procedure with a dummy argument: we use 0 to discharge a thunk. The constant ef is a conditional function. The constant 0 also acts as false, every other ground value being true. The form if is syntactic sugar relative to ef based on thunks:

if M N P ≡ (ef M (λd.N) (λd.P)) 0 ,

where d is not free in N, P. The combinators Y^{s→t} create recursive functions of type s → t.

In contrast to the original Pcf, the abstractions in our variant are call-by-value and evaluation proceeds left-to-right. On evaluation, a program is searched for a redex, i.e., a subterm that matches the left-hand side of some primitive machine rule.

Types:

t ::= ι  (ground type)
| t → t (procedure type)

Syntax:

M ::= V | (M_{s→t}M_{s})_{t}  (terms)
V ::= c | x^{t} | (λx^{s}.M_{t})_{s→t}  (values)
c ::= b | f  (constants)
b ::= n_{ι}  (basic constants)
f ::= 1+_{ι→ι} | 1−_{ι→ι} | ef_{ι→s→s→s} | Y_{((s→t)→(s→t))→(s→t)}^{s→t} (functional constants)

Behavior:

\begin{matrix}1+ n & ⟶ & n + 1 \\ 1− n + 1 & ⟶ & n \end{matrix} \begin{matrix}ef n + 1 & ⟶ & λx, y.x \\ ef 0 & ⟶ & λx, y.y \end{matrix}  \begin{matrix}(λx.M)V ⟶ M[x:=V] \\ YV ⟶ λx.V (YV)x \end{matrix}

Figure 1: Call-by-value Pcfv.

This search is guided by recognizing an evaluation context, a special kind of context, given by the following grammar:

E[ ] ::= [ ] | V E[ ] | E[ ]M.

The appropriate machine rule transforms the redex, giving a new program. This single evaluation step is defined as

E[M] > E[M′], if M ⟶ M′.

The stepping procedure is continued until the program reduces to a ground constant. The evaluation process is abstracted by the partial function eval from programs to ground constants:

eval(M) = b iff M >^{∗} b.

Programs that fail to yield a value are called nonterminating or diverging. For any value V, Ω ≡ (Y (λfx.fx) V) is a diverging term.

A starting point for reasoning with terms is the ability to identify language terms that have the same behavior.

Definition 2.1 For Pcfv terms M and N of type t, M operationally approximates N, M _{∼}_{v} N, if for all contexts C[ ], eval(C[M]) = b implies eval(C[N]) = b. M is operationally equivalent to

N, M ≃_{v} N, if M _{∼}_{v} N and N _{∼}_{v} M.

For an example of operationally equivalent terms, consider M_{1} ≡ λf.Ω and M_{2} ≡ λf.f 0 Ω.

Take any program context C[ ] enclosing M_{i}. The evaluation of the program may never place M_{i} in a function position, in which case the programs C[M_{1}] and C[M_{2}] clearly cannot give different results. If M_{1} shows up in a function position, then so does M_{2} and both programs are guaranteed to diverge. Thus the two terms M_{i} are interchangeable in any program context, and hence M_{1} ≃_{v} M_{2}.

Our first control extension is the abortexpression of the form AM. Many programming languages provide this feature, which goes by various names: error, stop, abort, exit, and halt. An Aexpression stops the evaluation of a program and returns the value of its sub-expression as the result of the entire program. Thus, the sub-expression of A must be of ground type, whereas the type of the A-expression itself is arbitrary:

M ::= … | (AM_{ι})_{t}.

We call this extended language Pcfv+A. The additional stepping rule is

E[AM] > M.

The evaluation function eval_{a} and the operational equivalence relation ≃_{a} for Pcfv+A are defined along the same lines as for Pcfv. However, the addition of A invalidates some of the operational equivalences in Pcfv, showing that functional languages cannot express abort [9].

Proposition 2.2 ≃_{v} ≃_{a} Proof. The terms M_{1} and M_{2} above, which are operationally equivalent in Pcfv, are inequivalent in Pcfv+A, since the context [ ](λx.Ax) distinguishes the two.

Our second control extension, the K-expression of the form KM, provides more interesting possibilities for control manipulations than A. The programming language Scheme [22, 26] provides the equivalent of K-expressions with the procedure callwith-current-continuation or call/cc. A limited version of K is provided by the goto-construct and labels of Algol-like languages, the catch/throw or errset/error mechanism of traditional Lisp systems, and the exception handlers of ML [19].

A K-expression applies its sub-expression to an abstraction of the surrounding context or the rest of the computation, the continuation. This continuation is a procedural object that can be called anywhere in the program, just like any other procedure. When it is invoked, evaluation reinstates the captured context in place of the current one, and fills it with the continuation’s argument. It is easy to simulate other non-local control actions in terms of K [5, 12, 14, 15, 26].

A K-expression can occur anywhere inside a program; thus it can have any type s. Also, the program can invoke the continuation anywhere, but the latter’s argument must be of the same type as the K-expression. Further, the K-subexpression returns a value of the type of the K-expression. Given this, we have the following extension of Pcfv’s syntax: ^{2}

M ::= … | (KM_{(s→t)→s})_{s}.

Assuming A-expressions in the state transition language, the additional stepping rule for K is:

E[KM] > E[Mλx.AE[x]].

The evaluation function and operational equivalence relation for Pcfv+K are eval_{k} and ≃_{k}, respectively. Once again, operational equivalences are not necessarily preserved when Pcfv is extended to Pcfv+K.

Proposition 2.3 ≃_{v} ≃_{k}

Proof. The same counterexample as for Proposition 2.2 holds. The distinguishing context is now K(λa.[ ]a).

The full language Pcfv+A+K, which we shall call Pcfv-c, is also a non-conservative extension of Pcfv+A, i.e., K adds true expressive power [9]. The evaluation function and operational equivalence relation for Pcfv-c are eval_{c} and ≃_{c}, respectively.

Proposition 2.4 ≃_{a} ≃_{c}

Proof. Let

equal? = λxy.if x (if y 1 0 ) (if y 0 1 ).

Consider the terms

M_{u} ≡ λf.equal? (fλk.k 1 Ω) (fλk.k u Ω),

for u = 0, 1. The only way these terms can differ is by invoking the variables k without evaluating the Ω’s, so that the equality test takes place. An abort could be used to elude the Ω, but the first argument of equal?, which is the same for both terms, is the first and only site where the abort may happen. Thus, owing to left-to-right evaluation, the terms are operationally equivalent in Pcfv+A. In Pcfv+K, on the other hand, the context [ ](λx.Kx) distinguishes them.

Finally, K-expressions provide the power of abort in a certain sense. Hence, operational equivalences are not affected by extending Pcfv+K to Pcfv-c.

Proposition 2.5 ≃_{k} ⊆ ≃_{c}

Proof. The only extra construct in Pcfv-c is A. From the proof for Proposition 2.3, we note that an A-expression can be simulated in Pcfv+K by enclosing the program with Kλa.[ ], and using the variable a in place of the aborting construct.

3 Models, Adequacy, and Full Abstraction

A denotational model for a language like Pcfv provides a collection of domains, an interpretation for the constant symbols, and a meaning function for the language terms. A domain is a partially ordered (⊑) collection of elements. In subsequent sections, we use one primitive domain _{⊥} and the following domain constructions: function domains (→, with functions notated by \underline{λ}), strict function domains (→_{s}, with functions notated by \underline{λ}^{s}), disjoint union (⊕), and lifting (·_{⊥}). Appendix A gives a brief description of domains, domain constructions, and their salient properties.

2Bruce Duba [private communication] and Tim Griffin [13] independently formulated similar typing rules for A and K.

Each type t maps to a domain _{t}, starting with the ground domain _{ι}. The domain for the arrow type s → t is built from the domains for s and t using appropriate domain constructions. The interpretation 𝔄 maps the constant terms of the language to elements in the appropriate domains. The semantic functional 𝔄̂, an extension of the interpretation, maps each term of type t to a denotation, usually a function that maps some auxiliary arguments to a value in _{t}. For example, the semantic function for a direct model has only an environment as an auxiliary argument; in the continuation model, the arguments include a continuation argument. Finally, the meaning function for programs maps programs to ground values:

ˆ𝔄̂ : Programs → _{ι}.

A minimum requirement on a model is that it not contradict and faithfully implement the operational semantics. This property is called adequacy.

Definition 3.1 [Adequacy] A model is adequate if for any program M,

eval(M) = b iff ˆ 𝔄̂[[M]] = 𝔄[[b]].

Analogous to operational approximation and equivalence, we can define notions of approximation and equivalence among terms based on their denotations.

Definition 3.2 For terms M and N of type t, M denotationally approximates N, M ⊑ N, if 𝔄̂[[M]] ⊑ 𝔄̂[[N]]. M is denotationally equivalent to N, M ≡ N, if M ⊑ N and N ⊑ M.

A meaning function is compatible if M ⊑ N implies C[M] ⊑ C[N] for all contexts C. For such a meaning function, it follows from adequacy that denotationally equivalent terms are also operationally equivalent.

Lemma 3.3 Let 𝔄̂ be the compatible semantic function of an adequate model. Then, for terms M and N, (1) M ⊑ N implies M _{∼} N, and (2) M ≡ N implies M ≃ N.

Proof. (1) Suppose M ⊑ N, but M _{≁} N. Then there is a context C[ ] such that eval(C[M]) = b and eval(C[N]) ≠ b. By adequacy, this gives C[M] ⋢ C[N], which is a contradiction since, by compatibility, M ⊑ N implies C[M] ⊑ C[N]. (2) The second claim follows from the first.

If operational equivalence also implies equivalence in the model, the model is fully abstract.

Definition 3.4 [Full Abstraction] A model is fully abstract for a language if for any two terms M, N in the language,

M_{∼}N iff M ⊑ N.

Given that the operational semantics and the model are constructed independently, full abstraction should not be expected automatically.

4 Direct Models for Pcfv+A

Plotkin [21] showed that a simple extension of call-by-name Pcf has a fully abstract direct model. It is part of programming language folklore that this result extends to the call-by-value variant of Pcf, Pcfv, as well as its simple control extension Pcfv+A. We confirm this by constructing the appropriate models for Pcfv and Pcfv+A.

We begin with the model for Pcfv (Figure 2). Its ground domain _{ι} is the traditional cpo of natural numbers, _{⊥} . The arrow type s → t maps to the lifted strict function domain _{s} →_{s} _{t}. The lift operation reflects the fact that there are diverging terms of all types; the strictness of the function spaces accounts for the call-by-value behavior of procedures. The interpretation 𝔄 maps the constants of Pcfv to their standard denotations, i.e., 1 to 1, 1+ to the “add one” function, etc. The semantic functionals 𝔄̂_{t} : Terms_{t} → Env → _{t} extend 𝔄 to all Pcfv-terms. Env is the set of environments, which are type-respecting maps from variables to elements in the domains.

It is straightforward to show that this model is adequate. This result was also obtained by Breazu-Tannen et al [3] and Riecke [personal communication].

Theorem 4.1 (Adequacy) For any program M in Pcfv,

eval(M) = b iff ˆ 𝔄̂[[M]] = 𝔄[[b]].

Domains:

\begin{aligned}_{ι} & = & _{⊥} \\ _{s→t} & = & [ _{s} →_{s} _{t}] _{⊥} \end{aligned}

Semantic functions:

ˆ𝔄̂ : Programs → _{ι}
ˆ𝔄̂[[M]] = 𝔄̂[[M]]⊥
𝔄̂ : Terms_{t} → Env → _{t}
𝔄̂[[b]]ρ = 𝔄[[b]]
𝔄̂[[x]]ρ = ρ[[x]]
𝔄̂[[λx.M]]ρ = lift(\underline{λ}^{s}v.𝔄̂[[M]]ρ[x/v])
𝔄̂[[Y]]ρ = fix_{cbv}
𝔄̂[[MN]]ρ = apply(𝔄̂[[M]]ρ, 𝔄̂[[N]]ρ)
fix_{cbv} : _{((s→t)→(s→t))→(s→t)}
fix_{cbv}(⊥) = ⊥
fix_{cbv}(lift(f)) = fix(f) where fix(f) = ⨆_{i=0}^{∞} {a_{i}} for a_{0} = ⊥, a_{i+1} = apply(f, a_{i})
apply : _{s→t} × _{s} → _{t}
apply(⊥, v) = ⊥
apply(lift(f), v) = fv

Figure 2: The direct model for call-by-value Pcfv.

Proof. We define two auxiliary functions: eval_{r} and η. The partial function eval_{r}, from terms and syntactic environments (maps from variables to tuples) to tuples of terms and environments, defines an equivalent operational semantics for Pcfv. The semantic function η on these tuples is then:

\begin{aligned}η(c; ∅) & = & 𝔄[[c]], \\ η(λx.M; r) & = & f \end{aligned}

where apply(f, η(a))

= \{ \begin{matrix}η(eval_{r}(M)r[x/a]) \\ if eval_{r}(M)r[x/a] converges, \\ ⊥ otherwise. \end{matrix}

We can then show that η satisfies:

𝔄̂[[M]](η ∘ r)

= \{ \begin{matrix}η(eval_{r}(e)r) & if eval_{r}(e)r converges, \\ ⊥ & otherwise. \end{matrix}

A specialization of this result to complete programs proves the theorem:

1. Assume eval(M) = b. Then, eval_{r}(M)∅ = b; ∅, and so

ˆ𝔄̂[[M]] = 𝔄̂[[M]]⊥ = 𝔄[[b]].

2. Assume ˆ 𝔄̂[[M]] = 𝔄[[b]]. Then, 𝔄̂[[M]]⊥ = 𝔄[[b]] ≠ ⊥. Thus eval_{r}(M)∅ converges, and η(eval_{r}(M)∅) = 𝔄[[b]]. Now, since b; ∅ is the only tuple mapped by η to 𝔄[[b]], we have eval_{r}(M)∅ = b; ∅, and eval(M) = b.

From Lemma 3.3, since 𝔄̂ is compatible, it follows that denotationally equivalent call-by-value Pcfv-terms are also operationally equivalent. However, the converse is not true: from Plotkin’s treatment of Pcf, we can easily derive a counterexample for Pcfv. Consider N_{u} (u = 0, 1):

N_{u} = λx.if (x (λd. 1 ) (λd.Ω))

(if (x (λd.Ω) (λd. 1 )) (if (x (λd. 0 ) (λd. 0 )) Ω u) Ω)

Ω.

Although N_{0} ≃_{v} N_{1}, N_{0} ≢ N_{1}, for applying the denotation of N_{u} to

\underline{por} = \underline{λ}^{s}m, n. \{ \begin{matrix}1 & if m0 > 0 or n0 > 0 \\ 0 & if m0 = 0 and n0 = 0 \\ ⊥ & otherwise \end{matrix}

\begin{aligned}′_{ι} & = & _{ι} \\ ′_{s→t} & = & [ ′_{s} →_{s} _{t}] _{⊥} \\ _{ι} & = & ′_{ι} ⊕ _{ι} \\ _{s→t} & = & ′_{s→t} ⊕ _{ι} \end{aligned}

Semantic functions (As in Figure 2, with the following changes):

ˆ𝔄̂ : Programs → ′_{ι}
ˆ𝔄̂[[M]] = strip(𝔄̂[[M]]⊥)
𝔄̂ : Terms_{t} → Env → _{t}
𝔄̂[[AM]]ρ = inR(strip(𝔄̂[[M]]ρ))
fix_{cbv} : ′_{(s→)→(s→t)} → _{s→t}
fix_{cbv}(⊥) = ⊥
fix_{cbv}(lift(f)) = fix(f) where fix(f) = ⨆_{i=0}^{∞} {a_{i}} for a_{0} = ⊥, a_{i+1} = apply(f, a_{i}) = f(a_{i})
apply : _{s→t} × _{s} → _{t}
apply(⊥, v) = ⊥
apply(inL(f), inL(v)) = fv
apply(inL(f), inR(v)) = inR(v)
apply(inR(f), inL(v)) = inR(f)
apply(inR(f), inR(v)) = inR(f)
strip : _{t} → _{t}
strip(inL(v)) = v
strip(inR(v)) = v

Figure 3: The extended direct model for Pcfv+A.

yields differing results.

A deterministically parallel operator that eliminates the counterexample is parallel-if:

M ::= … | (pif M_{ι} M_{ι} M_{ι})_{ι}.

The construct pif is like if, but can also give a result if the sub-expression in the test position diverges. The choice of pif rather than por as the new Pcfv-construct facilitates the proof of full abstraction below. The stepping rules for pif are:

E[pif M N P] > \{ \begin{matrix}E[N] & {if M >^{∗} n and \atop n > 0} \\ E[P] & if M >^{∗} 0 \\ E[c] & {if N >^{∗} c and \atop P >^{∗} c} \end{matrix}

The clause for pif-expressions in the meaning func-

tion 𝔄̂ is:

𝔄̂[[pif M N P]]ρ

= \{ \begin{matrix}𝔄̂[[N]]ρ & if 𝔄̂[[M]]ρ > 0 \\ 𝔄̂[[P]]ρ & if 𝔄̂[[M]]ρ = 0 \\ 𝔄̂[[N]]ρ & if 𝔄̂[[N]]ρ = 𝔄̂[[P]]ρ \\ ⊥ & otherwise \end{matrix}

A parallel disjunction function on thunks is defined as:

por = λab.pif (a 0 ) 1 (pif (b 0 ) 1 0 ).

It is easy to verify that 𝔄̂[[por]]⊥ = \underline{por} and that the terms N_{u} are operationally inequivalent in Pcfv with pif.

The direct model is fully abstract with respect to Pcfv with pif. The same result for Plotkin’s related model of partial functions was independently obtained by Sieber [personal communication].

Theorem 4.2 For Pcfv+pif terms M, N, (1)

M _{∼} N iff M ⊑ N, and (2) M ≃ N iff M ≡ N.

Proof. The proof uses Plotkin’s [21] method of defining terms for the finite elements of the domains.

The direct model is easily extended to accommodate Pcfv+A [10]. Each domain is augmented with exception values to correspond to denotations of abort terms of that type. Since the exception values are always ground, they can be represented by _{ι}. The domains and the semantic functionals for Pcfv+A are shown in Figure 3.

The direct model is adequate for Pcfv+A, but is not fully abstract. As for Pcfv, Pcfv+A requires a parallel-if construct. The operational semantics of pif slightly differs from the one above to accommodate the presence of aborts:

E[pif M N P] > \{ \begin{matrix}E[N] & {if M >^{∗} n and \atop n > 0} \\ E[P] & if M >^{∗} 0 \\ c & {if E[N] >^{∗} c and \atop E[P] >^{∗} c} \end{matrix}

Equality of the branches now also requires that their control actions are identical; aborts in the test-position are delimited. The 𝔄̂-clause for pif remains the same as above but is interpreted in the larger model. Unlike in the functional case, pif is not sufficient for full abstraction.

Proposition 4.3 The extended direct model is not fully abstract for Pcfv+A+pif.

Proof. Consider the Pcfv+A terms

M_{u} = λf.equal? (f λd.A 5 ) (f λd.A 5 + u),

where u is either 0 or 1. The only way the terms could potentially differ in Pcfv+A+pif is by applying f’s argument, but delimiting the abort. Since the only delimiter available is the testposition of a pif, and since the only deductions possible from this position is whether the delimited test-value was zero or non-zero, the terms cannot be distinguished in Pcfv+A+pif.

However, the model distinguishes them by applying the denotation of M_{0} and M_{1} to

\underline{λ}^{s}m.inL(strip(m0)).

To fix this problem, we augment the language with a control delimiter or prompt [8, 23]. A prompt-expression, %M, runs its sub-expression M as an independent program insofar as control action is concerned. Aborts cannot extend beyond the dynamically closest prompt. Since a promptexpression is treated as a program, it is always of ground type:

M ::= … | (%M_{ι})_{ι}.

The additional stepping rule for Pcfv+A+pif with prompts is

E[%M] > E[V] if M >^{∗} V.

The clause that extends the semantic functional ℭ̂ to include prompt-expressions is:

𝔄̂[[%M]]ρ = inL(strip(𝔄̂[[M]]ρ)).

The terms M_{u} in Proposition 4.3 are operationally inequivalent in Pcfv+A+pif with prompts. For, taking the context C[ ] = [ ](λf.%(f 0 )), we have C[M_{0}] and C[M_{1}] evaluating to different results.

Theorem 4.4 The extended direct model is adequate and fully abstract for Pcfv+A+pif+%.

Proof. The proof is a modification of the proofs of Theorems 4.1 and 4.2 that accounts for the exception elements.

5 Adequacy and Full Abstraction of the CPS Model

The typed direct model does not easily extend to Pcfv-c with its higher-order continuations. The traditional model for such languages is the CPS (continuation-passing style) model [25]. The ground domain _{ι} remains the traditional cpo of natural numbers, but the domains for arrow types are no longer simple function spaces. Instead, a Pcfv-c procedure maps to a function that maps the argument denotation and a denotation representing the rest of the computation—a continuation function—to an answer. This scheme accounts for control operations in the procedure body that can affect the rest of the computation. Initially, we assume non-strict function spaces for all the domains; Figure 4 displays the actual solution that emerges for reasons discussed below.

\begin{aligned}_{ι} & = & _{⊥} \\ _{ι→t} & = & _{ι} →_{s} _{t} → _{ι} \\ _{s→t} & = & _{s} → _{t} → _{ι}, s ≠ ι \end{aligned}  \begin{aligned}_{ι} & = & _{ι} →_{s} _{ι} \\ _{s→t} & = & _{s→t} → _{ι} \end{aligned}

Semantic functions:

ˆℭ̂ : Programs → _{ι}
ˆℭ̂[[M]] = ℭ̂[[M]]⊥(\underline{λ}^{s}x.x)
ℭ̂ : Terms_{t} → Env → _{t} → _{ι}
ℭ̂[[b]]ρκ = κℭ[[b]]
ℭ̂[[x]]ρκ = κ(ρ[[x]])
ℭ̂[[λx.M]]ρκ = κ(\underline{λ}v, κ′.ℭ̂[[M]]ρ[x/v]κ′)
ℭ̂[[Y]]ρκ = κ fix_{cps}
ℭ̂[[MN]]ρκ = ℭ̂[[M]]ρ(\underline{λ}m.ℭ̂[[N]]ρ(\underline{λ}n.mnκ))
ℭ̂[[A M]]ρκ = ℭ̂[[M]]ρ(\underline{λ}^{s}v.v)
ℭ̂[[K M]]ρκ = ℭ̂[[M]]ρ(\underline{λ}m.m(jκ)κ)
j : _{s} → _{s→ι}
j(κ) = \underline{λ}v, κ′.κv
fix_{cps} : _{((s→t)→(s→t))→(s→t)}
fix_{cps} = \underline{λ}f, κ. ⨆_{i=0}^{∞} \{a_{i}\}, where a_{0} = f⊥κ, a_{1} = f⊥(\underline{λ}n.fnκ), a_{2} = f⊥(\underline{λ}n.fn(\underline{λ}n.fnκ)), …

Figure 4: The CPS model for Pcfv-c.

The CPS model is adequate for Pcfv, Pcfv+A, Pcfv+K and Pcfv-c.

Theorem 5.1 (Adequacy of CPS) For any program M in Pcfv-c,

eval(M) = b iff ℭ̂[[M]]⊥(\underline{λ}^{s}x : _{ι} .x) = ℭ[[b]].

Proof. The proof is similar to the one for the direct model.

By Lemma 3.3, since the CPS meaning function is compatible, terms that are denotationally equivalent in our four languages are also operationally equivalent. Unfortunately, but not surprisingly, the model is not fully abstract for any of these languages.

Proposition 5.2 The CPS model is not fully abstract for plain Pcfv.

Proof. Full abstraction breaks down in three distinct ways in the naïve (fully non-strict) CPS model for Pcfv:

1. The simple model for Pcfv assigns non-strict functions to apparently non-strict procedures.^{3} As a result, call-by-value procedures that are operationally equivalent like

e_{1} = (λd. 0 )

and

e_{2} = (λd.if d 0 0 )

have distinct meanings in the model:

ℭ̂[[e_{1}]]⊥κ = κ\underline{λ}d, κ′.κ′0

versus

ℭ̂[[e_{2}]]⊥κ = κ\underline{λ}^{s}d, κ′.κ′0.

If κ = \underline{λ}m.m⊥_{ι}(\underline{λ}x.x), the former evaluates to 0 and the latter to ⊥.

2. Consider the terms from Section 4:

3Olivier Danvy and Andrzej Filinski pointed out this problem with the naïve model and provided the idea for the counterexample.

N_{u} = λx.if (x (λd. 1 ) (λd.Ω))

(if (x (λd.Ω) (λd. 1 )) (if (x (λd. 0 ) (λd. 0 )) Ω u) Ω)

Ω, for u = 0, 1.

We have N_{0} ≃_{v} N_{1}, but N_{0} ≢ N_{1}. Applying the denotations of N_{u} to the continuation κ_{1} = \underline{λ}m.m(\underline{por}_{c})(\underline{λ}x : _{ι} .x) produces 0 and 1, respectively. The function \underline{por}_{c} is the CPS version of parallel-or:

\underline{por}_{c} = \underline{λ}m, κ.κ\underline{λ}n, κ. \{ \begin{matrix}κ1 & {if m0\underline{λ}x.x > 0 \atop or n0\underline{λ}x.x > 0} \\ κ0 & {if m0\underline{λ}x.x = 0 \atop and n0\underline{λ}x.x = 0} \\ ⊥ & otherwise. \end{matrix}

3. Recall M_{1} = λf.Ω and M_{2} = λf.f 0 Ω from above. M_{1} and M_{2} are operationally but not denotationally equivalent in Pcfv. In particular, let

\begin{matrix}κ_{0} = \underline{λ}m : _{(ι→(ι→ι))→ι}. \\ m(\underline{λ}v : _{ι}, κ : _{ι→ι}.v)(\underline{λ}x : _{ι}.x). \end{matrix}

Then we have

ℭ̂[[M_{1}]]⊥κ_{0} = ⊥,

whereas

ℭ̂[[M_{2}]]⊥κ_{0} = 0.

We can eliminate the first problem by using strict spaces for those function domains that originate from a ground domain (see Figure 4). The second counterexample shows that the model can express deterministic parallelism. The continuation κ_{0} in the third counterexample is clearly the equivalent of an aborting action. Thus, adding A, for example, suffices to eliminate this problem (Propositions 2.2 and 2.3). Control extensions to Pcfv do not eliminate the first problem but they do remove counterexamples of the second kind. In the following propositions, we gradually work out the control specific deficiencies of our Pcfv extensions.

Proposition 5.3 There is a control-specific counterexample to full abstraction of the CPS model for Pcfv+A.

Proof. Consider the terms M_{u} (u = 0, 1) from the proof of Proposition 2.4:

M_{u} = λf.equal?(fλk.k 1 Ω)(fλk.k u Ω).

Recall that M_{0} ≃_{a} M_{1}, but M_{0} ≢ M_{1}. For, taking

κ_{0} = \underline{λ}m.m(\underline{λ}f, κ.f(jκ)(\underline{λ}^{s}x.x)),

we have ℭ̂[[M_{0}]]⊥κ_{0} = 0 and ℭ̂[[M_{1}]]⊥κ_{0} = 1.

The function (jκ) corresponds to a procedural value that substitutes one continuation for another, but there is no expression in the language that has this denotation. This is exactly the property of continuation objects provided by K. Hence, adding K to the language makes the terms M_{u} operationally inequivalent (Proposition 2.4). The choice between A and K suggested by Proposition 5.2 is thus illusory: the proper language for a CPS model must have a K-like facility, whether or not it has an A. Indeed, it is easy to see that the control facility must give first-class access to continuations. Still, not even the addition of K suffices to recover full abstraction.

Proposition 5.4 There is a control-specific counterexample to full abstraction of the CPS model for Pcfv-c and Pcfv+K.

Proof. Consider the Pcfv-c terms

M_{u} = λz.equal? (z λd.A 1 ) (z λd.A u),

where u is either 0 or 1. Distinguishing these terms operationally requires that z apply its argument, and, since the first z-argument aborts, the second z-argument has no opportunity to affect the answer. In short, M_{0} ≃_{c} M_{1}.

On the other hand, let

κ_{0} = \underline{λ}m.m[\underline{λ}f, κ_{1}.(κ_{1}(f0(\underline{λ}^{s}x.x)))](\underline{λ}^{s}x.x).

Then, ℭ̂[[M_{u}]]⊥κ_{0} = ℭ[[u]] and hence, M_{0} ≢ M_{1}.

Pcfv+K has essentially the same counterexample, but since it does not have abort, the Aexpressions in the M_{u} have to be replaced by invocations of an appropriate continuation, e.g.,

M′_{u} = λz.K(λa.equal?(zλd.a 1 )(zλd.a u)).

The continuation κ_{0} in the above proof first runs the thunk f in an identity continuation before passing the result on to κ_{1}, the continuation that came along with f. This makes the result of calling f available for immediate examination, even if it involved an abort or a continuation invocation. In other words, the model has a facility to run a sub-computation as an independent program whose control actions are isolated from the enclosing program. On finishing the sub-computation, its result is used to resume the rest of the computation. Pcfv-c cannot simulate this control delimiting action since aborts or continuation invocations are irrevocable.

To fix the problem posed by Proposition 5.4, we augment Pcfv-c with a control delimiter or prompt, as for Pcfv+A (Section 4). In this setting, a prompt-expression delimits all control actions that it dynamically encloses, including aborts, context captures by K-expressions, or context switches on continuation invocations. The operational semantics of the prompt is the same as the one given in Section 4. The clause that extends the semantic functional ℭ̂ to include prompt-expressions is:

ℭ̂[[%M]]ρκ = κ(ℭ̂[[M]]ρ\underline{λ}^{s}x.x).

The operator that eliminates the second counterexample in the proof of Proposition 5.2 is once again a parallel disjunction procedure por based on pif, introduced in Section 4. The ℭ̂-clause for pifexpressions is:

ℭ̂[[pif M N P]]ρκ

= \{ \begin{matrix}ℭ̂[[N]]ρκ & if ℭ̂[[M]]ρ\underline{λ}^{s}x.x > 0, \\ ℭ̂[[P]]ρκ & if ℭ̂[[M]]ρ\underline{λ}^{s}x.x = 0, \\ ℭ̂[[N]]ρκ & if ℭ̂[[N]]ρκ = ℭ̂[[P]]ρκ, \\ ⊥ & otherwise. \end{matrix}

The operational semantics of pif is identical to the one for Pcfv+A+pif. Also as above, the addition of pif is orthogonal to the addition of prompt.

By augmenting Pcfv-c with pif and prompt, we arrive at a language for which the CPS model is fully abstract. The proof follows Plotkin’s plan [21] and essentially consists in showing that there are Pcfv-c terms for defining all finite elements. In our case, this includes elements from both the value and the continuation domains.

Definition 5.5 [Definability]

1. A value v ∈ _{s} is -definable if there is a Pcfv-c term V such that for all ρ, κ:

ℭ̂[[V]]ρκ = \{ \begin{matrix}⊥ & if v = ⊥_{ι} : _{ι}, \\ κv & otherwise. \end{matrix}

2. A continuation κ ∈ _{s} is -definable if there is a Pcfv-c program evaluation context E[ ] such that for all ρ, M:

ℭ̂[[E[M]]]ρ(\underline{λ}^{s}x.x) = ℭ̂[[M]]ρκ.

To prove full abstraction of the CPS model, we need to show that all finite elements can be defined in Pcfv-c.

Lemma 5.6 For all types s,

1. v ∈ _{s} is -definable;

2. κ ∈ _{s} is -definable.

Proof. The proof is by induction on s, with the following strengthening of the hypothesis: for each type s, we prove that a collection of values in _{s→ι} and _{(s→ι)→ι} are also definable, and then use this fact in the induction step.

Thus, we need to show that for every finite v, v′ ∈ s, κ, κ′ ∈ _{s}:

1. v is -definable;

2. v ⇒ (⊥ ⇒ ⊥) ⇒ 1 is -definable, if it exists; and

3. (v ⇒ (⊥ ⇒ ⊥) ⇒ 1) ⊔ (v′ ⇒ (⊥ ⇒ ⊥) ⇒ 0) is -definable, if it exists.

and also,

1. κ is -definable;

2. j(κ) ⇒ (⊥ ⇒ ⊥) ⇒ 1 is -definable; and

3. (j(κ) ⇒ (⊥ ⇒ ⊥) ⇒ 1) ⊔ (j(κ′) ⇒ (⊥ ⇒ ⊥) ⇒ 0) is -definable, if it exists.

The notation a ⇒ b denotes a one-step function in the appropriate domain. The transformation j on continuations is specified in Figure 4.

From this lemma, it follows that operational equivalent terms are also denotationally equivalent.

Theorem 5.7 (Full Abstraction of CPS) For terms M and N in Pcfv-c (1) M _{∼} N iff M ⊑ N, and (2) M ≃ N iff M ≡ N.

Proof. The proof is standard, based on Lemma 5.6 [21].

6 Enhancing Control Structures

In our study of models for Pcfv with control extensions, we looked at both a simple aborting facility and a higher-order control facility, using a direct and a CPS model, respectively. In each case, the model is not fully abstract as it has more capabilities than the language. Both direct and CPS models can

• express deterministic parallelism; and

• restrict the actions of control constructs.

To get full abstraction, we could either restrict the model or further extend the language. Taking the latter recourse, we need to incorporate a facility for deterministic parallelism (pif) and a control delimiter (prompt) into the language. Some of the above language extensions are already present in Lisp and Scheme, though not always in their most general form. In traditional Lisp, the first-order combination of prompt and A occurs as errset and error. Common Lisp [24] no longer provides a facility like errset, i.e., it misses a control delimiter for error; its catch mechanism is sufficient as a prompt for control actions by throw. Scheme has higherorder continuations based on call/cc but also lacks a control delimiter.^{4} Neither programming language has deterministic parallelism.

Purely functional languages reflect their conventional direct model accurately but for the nonsequential pif. To establish an analogous relationship, languages with control require a control delimiter to express all sequential aspects of their models. This extension is also supported by practical evidence. Our own investigation of control delimiters found them to yield several useful programming paradigms for languages like Scheme [8, 23]; Danvy and Filinski [4] describe other interesting uses of prompt and related concepts. Recently, Hieb and Dybvig [16] argued for an extension of prompt, called spawn, as a crucial programming tool for concurrent systems with control operators. Thus, on the strength of both denotational completeness and practical utility, the prompt merits consideration for inclusion in sequential languages with control facilities, whether first- or higherorder.

In conclusion, with the right extensions, a Lispor Scheme-like language not only increases its power as a programming language, but, just like purely functional languages, becomes a genuine mathematical reasoning system based on the fully abstract model.

Acknowledgment. We are grateful to Robert Cartwright and Albert Meyer for helpful discussions on this topic.

References

[1] Aiken A., J.H. Williams, and E.L. Wimmers. Program transformation in the presence of errors. In Proc. 17th ACM Symposium on Principles of Programming Languages, pages 210– 217, 1990.

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

[3] V. Breazu-Tannen, C. Gunter, and A. Scedrov. Computing with coercions. In Proc. 1990 ACM Conference on Lisp and Functional Programming, 1990, this volume.

[4] O. Danvy and A. Filinski. Abstracting control. In Proc. 1990 ACM Conference on Lisp and Functional Programming, 1990, this volume.

[5] R.K. Dybvig and R. Hieb. Engines from continuations. Journal of Computer Languages (Pergamon Press), 14(2):109–124, 1989.

[6] M. Felleisen. The Calculi of Lambda-v-CS-Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Indiana University, 1987.

[7] M. Felleisen. λ-v-CS: An extended λ-calculus for Scheme. In Proc. 1988 Conference on Lisp and Functional Programming, pages 72– 84, 1988.

[8] M. Felleisen. The theory and practice of first-class prompts. In Proc. 15th ACM Symposium on Principles of Programming Languages, pages 180–190, 1988.

4With side-effects and an eval function, it is possible to simulate prompt in Scheme [23].

[9] M. Felleisen. On the expressive power of programming languages. In Proc. European Symposium on Programming. Lecture Notes in Computer Science, 1990. To appear.

[10] M. Felleisen and R.S. Cartwright. Extended direct semantics. Technical Report 105, Rice University, January 1990.

[11] M. Felleisen, D.P. Friedman, E. Kohlbecker, and B. Duba. A syntactic theory of sequential control. Theor. Comput. Sci., 52(3):205–237, 1987. Preliminary version: Reasoning with Continuations, Proc. Symposium on Logic in Computer Science, 1986, 131–141.

[12] D.P. Friedman, C.T. Haynes, and E. Kohlbecker. Programming with continuations. In P. Pepper, editor, Program Transformations and Programming Environments, pages 263–274. Springer-Verlag, Heidelberg, 1985.

[13] T. Griffin. A formulæ-as-types notion of control. In Proc. 17th ACM Symposium on Principles of Programming Languages, 1990, to appear.

[14] C.T. Haynes and D.P. Friedman. Embedding continuations in procedural objects. ACM Transactions on Programming Languages and Systems, 9(4):245–254, 1987.

[15] C.T. Haynes, D.P. Friedman, and M. Wand. Obtaining coroutines from continuations. Journal of Computer Languages (Pergamon Press), 11(3/4):109–121, 1986.

[16] R. Hieb and R.K. Dybvig. Continuations and concurrency. In Second ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 128–136, 1990.

[17] J. McCarthy et al. Lisp 1.5 Programmer’s Manual. The MIT Press, Cambridge, second edition, 1965.

[18] A.R. Meyer and J.R. Riecke. Continuations may be unreasonable. In Proc. 1988 Conference on Lisp and Functional Programming, pages 63–71, 1988.

[19] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, Cambridge, Massachusetts and London, England, 1990.

[20] G.D. Plotkin. Call-by-name, call-by-value, and the λ-calculus. Theor. Comput. Sci., 1:125–159, 1975.

[21] G.D. Plotkin. LCF considered as a programming language. Theor. Comput. Sci., 5:223– 255, 1977.

[22] J. Rees and W. Clinger. The revised^{3} report on the algorithmic language Scheme. SIGPLAN Notices, 21(12):37–79, 1986.

[23] D. Sitaram and M. Felleisen. Control delimiters and their hierarchies. Lisp and Symbolic Computation, 3(1):67–99, 1990.

[24] G.L. Steele Jr. Common Lisp—The Language. Digital Press, 1984.

[25] C. Strachey and C.P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Technical Report PRG-11, Oxford University Computing Laboratory, Programming Research Group, 1974.

[26] G.J. Sussman and G.L. Steele Jr. Scheme: An interpreter for extended lambda calculus. Memo 349, MIT AI Lab, 1975.

[27] C. Talcott. The Essence of Rum—A Theory of the Intensional and Extensional Aspects of Lisp-type Computation. PhD thesis, Stanford University, 1985.

[28] C. Talcott. Rum: An intensional theory of function and control abstractions. In Proc. 1987 Workshop on Foundations of Logic and Functional Programming. Springer Lecture Notes 306, 1988.

A Domains and their Properties

A domain is a partially ordered collection of elements. The ordering relation (⊑) is generally a complete partial order. The following describes the domain constructions and properties used in the paper.

Domain constructions:

⊥ : This is the traditional cpo of natural numbers.

→ : This is a function cpo consisting of the continuous (i.e., lub-preserving) functions from the cpo to the cpo . The ordering is that induced by pointwise ordering. We shall use “meta-lambda” (\underline{λ}) to notate elements in the function domains, e.g.,

\underline{λ}x : .1 = \{(x, 1) | x ∈ \}.

→_{s} : This is the strict and continuous function cpo. We shall use \underline{λ}^{s} to notate strict functions, e.g.,

\begin{matrix}\underline{λ}^{s}x : .1 = \{(⊥_{}, ⊥)\} \\ ∪ \{(x, 1) | x ∈ \ \{⊥_{}\} \}. \end{matrix}

⊕ : This is the disjoint union cpo of cpos and , and is given by:

⊕  = {(a, 0) | a ∈ \ {⊥_{}} }
∪ {(b, 1) | b ∈ \ {⊥_{}} }
∪ {⊥_{⊕} }.

The ordering is inherited from the constituent domains, with ⊥_{⊕} being the new bottom element. We use inL(a) and inL(b) to refer to the elements (a, 0) and (b, 1) respectively.

⊥: This is the lift of the cpo , given by:

{(a, 0) | a ∈ } ∪ {⊥}.

Again, the ordering is inherited from the original domain, with the new bottom being the least element. We use lift(a) to refer to the non-⊥ element (a, 0) ∈ _{⊥}.

Domain properties

Finite elements: A domain element d ∈ is finite if for all directed subsets X ⊆ , d ⊑ ⊔X implies d ⊑ e for some e ∈ X.

Prefinite elements: A prefinite element d ⇒ e in → is an element such that:

(d ⇒ e)x = \{ \begin{matrix}e & if x ⊒ d, \\ ⊥ & otherwise. \end{matrix}

By Plotkin, the finite elements of a function domain are the lubs of finite sets of prefinite elements.

Algebraicity: A domain is algebraic if for any x ∈ , the set {d | d is finite ∧ d ⊑ x} is directed with x as its lub.

Consistent completeness: A domain is consistently complete if two elements with an upper bound also have a least upper bound.

The domain of natural numbers, _{⊥} , is consistently complete and algebraic. Further, the domains constructions for (strict) function cpo, disjoint union, and lifting preserve consistent completeness and algebraicity. Thus, all our domains are consistently complete algebraic cpos.