Reasoning with Continuations II: Full Abstraction for Models of Control

Two Corrections

Dorai Sitaram Matthias Felleisen

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

July 29, 1992

1 Environments for Pcf_{v}

The original paper [1] defines the domain of environments for call-by-value Pcf as typerespecting maps from the set of variables to domains (cf. [1, page 166]):

ρ ∈ Env implies ρ(x^{t}) ∈ _{t}.

Kurt Sieber [Universität des Saarlandes; personal communication: June 29, 1990] discovered that this definition is wrong as the following example demonstrates. Clearly,

(if0 x 1 1 ) ≃ 1

because x must be bound by some surrounding λ x.-abstraction, which in turn implies that it cannot represent a diverging computation. On the other hand, an environment could map x to bottom and then the denotations of the two expressions would differ.

Solution. The correct way to solve this problem is to restrict the set of environments to type-respecting finite maps from variables to non-bottom elements of the appropriate domain:

ρ ∈ Env implies ρ(x^{t}) ∈ _{t} \ {⊥}

provided x^{t} is in the domain of ρ. It is easy to check that this set forms a Scott-domain under the usual ordering on finite functions, i.e., environments with the same domain are ordered component-wise and the empty environment is below every other environment.

An alternative solution, employed by Riecke [2], is to change the language and to include a syntactic construct for declaring recursive objects:

μx.M.

It is then possible to bind a diverging computation to a variable.

2 The CPS model for Pcf_{v}-C

The original paper [1] assigns the following semantics to Y (cf. [1, page 170]):

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κ)), …

Thomas Streicher [Universität München; personal communication: June 29, 1992] points out that the set {a_{i}} is not necessarily a directed set and, hence, does not necessarily have a least upper bound. For a counter-example take

fnk = \{ \begin{matrix}1 & (kX) = 0 \\ 0 & (kX) = 1 \\ ⊥ & otherwise \end{matrix}

for some element X . Then, taking κ = \underline{λ}x.0, we get

a_{0} = f⊥κ  = 1
a_{1} = f⊥(\underline{λ}n.fnκ) = 0
a_{2} = f⊥κ  = 1
…

One procedure that denotes the above function is

         (Y (lambda f.
              (call/cc (lambda (k)
                 (if0 (% (k X))
                      (abort 1)
                      (if0 (sub1 (% (k X)) (abort 0) Omega)))))))

A context that creates an appropriate continuation is

                              let x = [ ] in 0

The above code shows that the problematic procedure passed to Y is not a true second-order procedure but a procedure that manipulates its continuation in a non-standard way.

Solution 1. If we restrict the input to fix_{cps} to functions f such that

fxκ = κ(fxI)

for all inputs x and continuations κ, then it is easy to show that the series a_{i} is ascending:

a_{0} = f⊥κ
= κ(f⊥I)
a_{i+1} = f⊥(\underline{λ}n.fn ⋯)
= (\underline{λ}n.fn ⋯)(f⊥I)
= f(f⊥I) ⋯  [continuations for f are non-strict]
⊒ κ(f⊥I) ⋯
= a_{i}

To enforce this solution on the syntactic level, we require that Y can only be applied to procedures of the form λf.λx. · · ·. If applied to any other procedure, Y diverges. While this solution is feasible and covers all relevant cases, it is overly restrictive.

Solution 2. An alternative solution relies on the syntactic (operational) definition of Y :

(Y f) = f(λx.(Y f)x).

A direct translation of this equation into a semantic constraint for fix_{cps} yields the following:

(fix_{cps}f) = f(\underline{λ}x.(\underline{λ}κ.(fix_{cps}f)(\underline{λ}g.(gx)κ))),

i.e., fix_{cps} is the least element M satisfying the equation

M = \underline{λ}f.f(\underline{λ}x.(\underline{λ}κ.(Mf)(\underline{λ}g.(gx)κ))).

Thus, fix_{cps} is determined by a simple fixpoint equation on an ordinary domain. By solving this equation iteratively, we get the desired solution:

fix_{cps} = ⨆_{i}((\underline{λ}F.\underline{λ}f.f(\underline{λ}x.(\underline{λ}κ.(F f)(\underline{λ}g.(gx)κ))))^{i}⊥)

Acknowledgement. We gratefully acknowledge discussions with Amr Sabry and Thomas Streicher on the topic of fixpoints in CPS models.

References

1. 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.

2. Riecke, J.G.. Fully abstract translations between functional languages. In Proc. 18th ACM Symposium on Principles of Programming Languages, 1991, 245-254.