Axiomatizing Higher Level Delimited Continuation
Yukiyoshi Kameyama
Institute of Information Sciences and Electronics
University of Tsukuba
Tsukuba, Japanand Japan Science and Technology Agency

kam@is.tsukuba.ac.jp
ABSTRACTIn our previous work we gave a sound and complete axiomatization of the control operators for delimited continuations,shift and reset by Danvy and Filinski and their variants.
Since the calculus allows only one use of shift and reset, anext step is to investigate the calculus with many different
shift’s and reset’s. In this work, we study the calculus
with higher-level delimited continuation operators, and givea sound and complete axiomatization of the calculus withlevel-1 and level-2 control operators for delimited continuations.
Due to lack of space, we leave the detailed proof to a
separate draft available at:
http://logic.is.tsukuba.ac.jp/~kam/level2-proof.ps

1.

INTRODUCTION

We are interested in precise semantics of control operators such as callcc in Scheme and SML/NJ. Such semantics
is often given by a set of equations (axioms) which characterize the operational behavior of control operators. In
our previous work [6], we axiomatized the control operatorsfor delimited continuations. Specifically, we gave sound andcomplete axiomatizations to the following two calculi:• shift and reset by Danvy and Filinski [1]• callcc, abort and reset
These two theories are equivalent in the sense that wehave a natural interpretation from one theory to the other.
For the latter case, the theory consists of (1) the axioms incomputational lambda calculus by Moggi [7], (2) the axioms
for callcc and abort by Sabry and Felleisen [10], and (3) afew simple and natural axioms which characterizes the reset
operator. Moreover, we showed the latter theory is conservative over the theory for callcc and abort, hence, the extra
expressiveness of delimited continuations is exactly that expressed by the delimiter (as one expects.)

Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, torepublish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee.
Copyright 2002 ACM X-XXXXX-XX-X/XX/XX ...$5.00.

While the shift and reset operators give programmers more
freedom to control their programs, a problem arises when
one wants to combine two programs each of which has different use of shift and reset.
To see this, let us consider the following situation. We are
to prove the correctness of partial evaluator, which receives asource program and after some binding-time analysis, which
evaluates static parts of the program and produces a residue
program. Several partial evaluators use the shift and reset
operators to perform so called let-insertion (see for example
Thiemann [11]). If the source program of partial evaluator
already contains the shift and reset operators and those operators are static in the sense that they must be evaluated at
the specialization time, then a conflict may arise. The twodifferent uses of shift and reset operators might interact sothat shift in the source program may capture a continuation
up to a reset operator for let-insertion, which would resultin a wrong answer.
A solution of this problem already exists in Danvy andFilinski’s work [1]. Namely, they proposed an infinite number of shift and reset operators indexed by a natural numbern > 0, and each level-n shift operator captures the continuation up to the (closest) reset operator of level-n or higher.
To explain it in the evaluation-context semantics, let E1 be
an arbitrary evaluation-context, and E2 be an evaluationcontext with level less than n, and m ≥ n. Then we have:
E1 [hE2 [ξn c.M ]im ]evaluates to
E1 [hM {c := λf.hE2 [f ]in }im ]where h im is the level-m reset operator, ξn c.M is the level-n
shift operator, and {c := · · · } is the usual capture-avoiding
substitution. It is easy to see the shift operator captures thedelimited continuation up to the corresponding reset operator. A subtle point here is that level-n shift cannot escapefrom level-m reset if m ≥ n, thus each shift cannot freely select its corresponding reset. Rather, higher-level operators
dominate lower-level operators, thus the hierarchy of control
operators.
Surprisingly, this hierarchy of shift and reset has a (relatively) simple and uniform functional CPS-transform which
Danvy and Filinski called CPS-hierarchy. The CPS-hierarchy
may be viewed as a composition of n CPS-translations, thus
inserting n continuation parameters. In order to consider
level-n control operators, we need n+1 continuation parameters, for instance, the standard shift operator (level-1 shift)needs the CPS-hierarchy for two continuation parameters.
For details about CPS-hierarchy, see Danvy and Filinski [1]and Danvy and Yang [2].
The use of level-n delimited control operators is not restricted to program manipulations. A certain kinds of control mechanism such as backtracking can be written concisely with shift and reset, and to build a large programfrom small modules, one needs to ensure each use of shift
and reset does not interfere. The hierarchy of level-n control
operators can give a (partial) solution to such a situation.
Note, however, since higher levels dominate lower levels,
each use of shift and reset cannot be completely independent, thus we cannot freely compose two program modules
both using shift and reset. The hierarchy of level-n shift
and reset operators is useful in the case where Danvy andYang [2] mention other applications of higher level delimited continuations, hierarchical backtracking and quantifier
alternation.
One may consider other variations for delimited- (or sometimes called partial-) continuation operators, such as Felleisen’s
prompt [3] and Hieb et al’s subcontinuations [9]. There arealso extensions of these operators which allows multiple usesof control operators [4], [5]. These proposals are certainly
useful and easier to use than higher-level shift and reset.
However, an important merit of Danvy and Filinski’s operators is that they have a simple, functional CPS-transform,
while other proposals do not have such simple (and functional) CPS-transform as far as we know. To our view, the
CPS-transform best describe the precise semantics of control operators, thus, we can build a solid foundation on topof them.
In this work, we first discuss the difficulty of axiomatizing
the level-n delimited continuations, then extend our previous result to the level-2 world, namely, we give a soundand complete axiomatization of the calculus with level-1 andlevel-2 control operators for delimited continuations.

2.

DIFFERENCES BETWEEN LEVEL-1 ANDLEVEL-2 AXIOMATIZATION

One may think extending the axiomatization of level-1 tolevel-2 can be done straightforwardly. But there are several
differences between level-1 operators and level-n (n > 1)
operators and these differences made our task harder than
one might expect initially. Let us explain them in order.
Firstly, the level-2 abortive operator A2 cannot be considered as a constant (value). In the case of the level-1 abortive
operator A1 , the equation (λx.A1 x)M = A1 M is valid, so
introducing this operator as a term constructor is equivalent to have it as a value corresponding to λx.A1 x. On theother hand, (λx.A2 x)M = A2 M is in general not valid withrespect to the CPS-semantics (for instance, let M be A1 N
then the left hand side is equal to A1 N (since λx.A2 x is avalue) while the right hand side is equal to A2 N (since A2 isstronger than A1 ). As a conclusion, we should take care of
the difference between A2 and λx.A2 x. (We also note that,the term λx.A2 x appears in several places in our proof.)
Secondly, and more importantly, the callcc-lift axiom does
not extend naturally to the case of level-2. To see this, let
us recall the axiom for level-1:
E0 [callccM ] = callcc(λk.E0 [M (λf.k(E0 [f ]))])
where E0 is a pure evaluation context (level-0 evaluation
context), k 6∈ F V (E0 [M ]) and f 6∈ F V (kE0 [ ]). This axiom(or its variant) has been the central axiom to characterize

the role of callcc operator. However, its level-2 counterpart:E1 [callcc2 M ] = callcc2 (λk.E1 [M (λf.k(E1 [f ]))])
is not valid when we take E1 to be a level-1 evaluation context1 . For instance, let E1 be A1 [ ] (where A1 is the level-1
abort operator), thenLHS=

A1 (callcc2 M ) = callcc2 M

RHS

=
=

callcc2 (λk.E1 [M (λf.k(A1 f ))])
callcc2 (λk.E1 [M (λf.A1 f )])=E1 [M (λf.A1 f )]The results are completely different. Lack of the callcc-lift
axiom brings a big difficulty in obtaining a complete axiomatization.
A rescue for this problem is given by Murthy’s “telescope”
axiom [8]. A level-2 instance of this axiom is:
C2 (λγ.M ) = C1 (λx.C2 (λy.M {γ := λv.yhxvi1 }))where we used the C-operator instead of callcc since the axioms looks simpler for the case of C-operator than callcc2
The role of this axiom is to split a single occurrence of leveln control operator (C2 in this case) to a sequence of n control
operators of level 1, 2, · · · , n.
Combining the telescope axiom with the level-1 C-lift axiom (which is valid), we can simulate the level-2 version of
C-lift axiom as:
hE[C2 (λγ.M )]i1=

hE[C1 (λk.C2 (λγ.M {γ := λv.γhkvi1 }))]i1==

hC1 (λk.(C2 (λγ.M {γ := λv.γhk(A1 (E[v]))i1 })))i1
hC1 (λk.C2 (λγ.M {γ := λv.γhE[v]i1 }))i1=

hC2 (λγ.M {γ := λv.γhE[v]i1 })i1=C2 (λγ.M {γ := λv.γhE[v]i1 })where E is a level-0 evaluation context.
We can easily see that the outer context hE[ ]i1 was captured and passed to the parameter γ. This rewriting has
the same effect as C-lift except that we cannot lift C2 stepby step, but we must lift it to the next reset operator at atime.

3. HIGHER LEVEL SHIFT AND RESET
Our source language is a type-free lambda calculus with
control operators with the call-by-value semantics. Our axiomatization should go through for the typed case, but it isleft for future work. In this paper, we restrict ourselves tolevel-2 only. The grammar of the source calculus is givenby:(terms) M, N::=

V | M N | hM i1 | hM i2(values) V::=

x | λx.M | C1 | C2

where h ii is the reset operator and Ci is a variant of the shiftoperator (similar to Felleisen’s operator). The original shiftoperator proposed by Danvy and Filinski can be defined1
Here level-i context is an evaluation context in which there
are no reset operators of level-i + 1 or higher which enclose
the hole.
2
This choice is only superficial, since a similar but more
complex axiom holds for callcc.

by Ci . The index i indicates the level, with i = 1 being
the base level. We abbreviate Ci (λx.M ) as Ci x.M , and if
x 6∈ F V (M ), it is also abbreviated as Ai M .
The informal semantics of these control operators is given
using evaluation contexts as follows (we assume i > j here):E[hV ii ]

→

E[V ]

[Cj V ]ii ]→E[hV (λf.Aj (E j−1 [f ]))ii ]E[hE j−1 [Aj V ]ii ]

→

E[V ]

E[hE

j−1

Here we give a Plotkin-style CPS-translation, that is, forthe translation of a function, the continuation parametercomes after the argument of the function.
[ ] :[V ] =

Term → Target Term
λk.kV ∗

[M N ] =[ hM i1 ] =λk.[[M ] (λm.[[N ] (λn.mnk))
λkγ.[[M ] θ1 (λv.kvγ)[ hM i2 ] =λkγδ.[[M ] θ1 θ2 (λv.kvγδ)

( )∗

:

Value → Target Termx∗(λx.M )∗==x
λx.[[M ]C1 ∗=λxk.x(λvk 0 .kv)θ1∗=

λxkγ.x(λvk 0 γ 0 .kvγ)θ1 θ2

jwhere E is an evaluation context (in call-by-value), and E
is a level-j evaluation context defined below.
The first line says delimiting a value does nothing. The
second line explains how Cj works; it captures the continuation up to (delimited by) the reset operator whose level isthe same as or higher than j. Unlike the shift operator, butlike callcc, the operator Cj inserts an occurrence of Aj in thecaptured continuation. The third line says that Aj aborts
the current continuation up to the reset operator whose levelis the same as j or higher.
The evaluation contexts used above are defined as follows:E= [ ] | EM | V E | hEij

Ei=[ ] | E i M | V E i | hE i ij for j ≤ i

We can also consider the shift operator. The operationalsemantics of the control operator S is given by:
E[hE j−1 [Sj V ]ii ] → E[hV (λf.hE i−1 [f ]ij )ii ]Then the real shift operator is given by ξi c.M ≡ Si (λc.M ).
The two operators C and S can be defined by each other:

4.

Si

=

λz.Ci (λk.z(λx.hkxii ))Ci=

λz.Si (λk.z(λx.Si (λd.kx)))

CPS-TRANSLATIONA CPS-translation is a syntactic translation from the source
calculus given in the previous section to the target calculus,
the pure type-free lambda calculus without control operators.
The strength of shift and reset operators due to Danvy andFilinski is their semantics is precisely given by a functional
CPS-translation. Unlike ordinary CPS-translations, their
CPS-translation takes more than one continuation parameters in order to interpret level-n control operators. Moreprecisely, if the source calculus has up to level-n control operators, we need a CPS-transform with n + 1 continuation
parameters.
In our case, we have up to level-2 control operators, so
we need CPS-hierarchy with three continuation parameters,
which are denoted by k, γ, and δ. These three continuation
parameters are called the (standard) continuation parameter, the meta- continuation parameter, and the meta-metacontinuation parameter, respectively.
In summary, the CPS-translation here translates a termin the source calculus (with control operators) to a termin the target calculus, and the resulting term takes threeparameters k, γ, δ. For readability we present here a CPStranslation where all the η-redexes are reduced, so some resulting terms may not take three parameters.

C2

where we used abbreviations as θ1 = λxγ.γx and θ2 =λxδ.δx.

5.

AXIOMS

The set of axioms for λC 2 is given in Figure 1 where we
introduce an abbreviation hM i0 ≡ M to state the axiom
C-elim uniformly.
In order to read the axioms, recall that we abbreviate
Ci (λx.M ) as Ci x.M . Note also that the indices i and j range
over {1, 2} only, hence, we do not consider the case for j = 0
in, e.g., the axiom reset-lift-2 (such an instance is not sound).
Most axioms are level-i extension of those for level-1 in ourprevious work [6]. (1) The axiom βΩ is valid only for level-0
contexts. To compensate the weakness of this axiom, we
have two axioms, reset-lift and reset-lift-2. (2) The axiom
C-lift is only applicable to level-0, as we explained before.
(3) Most other axioms but telescope are natural extensions
from the axioms for level-1. However, there are subtle differences, for instance, the axiom C-elim needs an occurrenceof a reset operator if it is applied to level-2. In the C-abortaxiom, the argument of k is restricted to a value V , while
its level-1 counterpart allows an arbitrary term. The axiom
such as reset-reset and C-top were not included in the level-1
axiomatization because their level-1 instances are derivablefrom other axioms. Since it is not known to us if their level-2
instances are derivable or not, we included these axioms. (4)The axiom reset-C and telescope did not exist in the level-1
for the obvious reason.
The telescope axiom (written in terms of the shift operator) was first proposed by Murthy [8]. We should also
remark that Murthy gave a type system and based on thetyping he derived many sound equations, most of which arevery similar to ours, but he did not mention completeness.
The precise relationship between his axioms and ours is notclear at present, since he gave axioms based on the Si operator and also he worked in a typed setting. However, boththeories look quite similar; in a sense, our present work could
be understood as proving the completeness of (some variation of) Murthy’s axioms.
The main result of this paper is that our theory for level-2
is sound and complete with respect to the CPS-translation.
Theorem 1(Soundness & Completeness). Let M1

(λx.M )V = M {x := V }λx. V x = Vβv
ηv , if x 6∈ F V (V )(λx.E 0 [x])M = E 0 [M ]βΩ , if x 6∈ F V (E 0 )hV ii = Vh(λx.M )hN ii ii = (λx.hM ii )hN ii

reset-value
reset-lifth(λx.M )hN ij ii = h(λx.hM ii )hN ij ii

reset-lift-2, i > j

Ci k.hM ii = Ci k.M
Ci k.khM ii−1 = hM ii−1

C-resetC-elim, if k 6∈ F V (M )Ci k.C[E i [kV ]] = Ci k.C[kV ]0C-abort, if k is not captured by C
0

E [C1 M ] = C1 k.M (λf.k(E [f ]))C-lift, if k 6∈ F V (E 0 [M ]) and f 6∈ F V (kE 0 )hhM ii ij = hM imax(i,j)
hCi k.M ij = Ci k.M

reset-reset
reset-C, if i > j

hCi k.M ii = hM {k := λx.Ci k0 .x}ii
C2 γ.M = C1 k.C2 γ.M {γ := λf.γhkf i1 }C-toptelescope

Figure 1: Axioms of λC 2 (i, j range over {1, 2})
and M2 be terms in the source calculus. Then we have:
λC 2 ` M1 = M2 if and only if λβη ` [ M1 ] = [ M2 ]T
We can prove the soundness by calculation. In the next
section we give a very brief summary of completeness proof.
The details can be found in the accompanying draft.

6.

COMPLETENESS PROOF

As in our previous work, we first analyze the structureof the target calculus then define the translation from thetarget to the source. The target calculus is the closure of
the image of the CPS-translation which is closed by the βηreductions.

T −1 (λk.Q) =C1 (λk.Q−1 (Q))−1

(W1 W2 ) =−1Q (λγ.R) =W −1 (W1 )W −1 (W2 )C2 (λγ.R−1 (R))

Q−1 (T K) =K−1 (K)T −1 (T )−1

(KW ) =

K−1 (K)W −1 (W )R−1 (λδ.S) =R−1 (QG) =S −1 (S)G −1 (G)hQ−1 (Q)i1

R−1 (GW ) =G −1 (G)W −1 (W )Q

−1

S (RH) =S −1 (HW ) =H−1 (H)hR−1 (R)i2
H−1 (H)W −1 (W )W −1 (x) =W (λx.T ) =xλx.T −1 (T )−1

K−1 (k) =k(term) T::=

λk.Q | W W

K(preterm-1) Q(preterm-2) R

::=
::=

λγ.R | T K | KW
λδ.S | QG | GW

(λx.Q) =G −1 (γ) =λx.hQ−1 (Q)i1γ

G −1 (λx.R) =λx.hR−1 (R)i2(answer) S::=

RH | HW(value) W(continuation) K

::=
::=

x | λx.T
k | λx.Q(meta-cont.) G(meta-meta-cont.) H

::=
::=

γ | λx.R
δ | λx.S

Terms in the class T are called T -terms. Similarly for Q-,
R-, S-, W -, K-, G-, H-terms. Terms, values, level-0 context(i.e. E 0 ), level-1 context (i.e. E 1 ), and level-2 context (i.e.
E) are mapped to T -, W -, K-, G-, H-terms in the target
calculus. Q- and R-terms do not have intuitive counterpart
in the source calculus. We should note that the meta-metacontinuation variable δ is linear.
The inverse translation from the target language to thesource language is given by:−1

H−1 (δ) =H−1(λx.S) =λx.x
λx.S −1 (S)Since the meta-meta-continuation variable δ is linear, we
can simply ignore it. It can be seen that the above inversion
takes a very uniform form, and we can extend it to level-3
or higher levels.
The remaining proof proceeds as in the previous work. (1)Prove the inverse translation is really an inverse of the CPStranslation (up to the equality in the source calculus), that
is, T −1 ([[M ] ) = M in λC 2 . (2) Prove the β- and η-equality
in the target are preserved by the inverse translation. (3)To prove (2), we need to prove substitutions in the target
calculus is preserved by the inverse translation.
The detailed proof needs a lot of calculations so we leave
the detailed description to a separate draft.

7.

CONCLUSION

We have given the axiomatization of the level-2 delimited
continuation operators, thus we can reason about programswith two different sets of control operators. An obvious next
step is to have level-n axiomatization for arbitrary n > 0.
In the level-2 world, several things are different from thelevel-1 operators, for instance, the operator A cannot be
regarded as a constant (value), and C-lift no longer holds
for C2 . However, once we have obtained the level-2 axioms,
it should be straightforward to formulate axioms of higher
levels (just replace i by higher levels). The only problem
we see is the telescope axiom, but Murthy [8] already gave ageneralized telescope axiom for any level. In summary, going
to level-3 or higher levels seems a straightforward extensionof this paper (the details are yet to be done, though).
Besides going to higher levels, there are two major remaining problems: (1) the set of axioms we give in thispaper may not be optimal in the sense that some axioms
may be derived from others. In fact, for the case of level-1
axiomatization [6], we can derive C-top and reset-reset fromother level-1 axioms. At present, we do not know how toderive the level-2 instances of these axioms from other axioms. (2) we only worked for the C operators, while ouractual aim is to axiomatize the S operator. It is easy justto obtain a sound and complete axiomatization for S using
the translation given in this paper, but obtaining a good axiomatization needs more work. We believe this can be donein the same line as our previous work.
Acknowledgments: The author would like to thankMasahito Hasegawa who improved the axioms and the proofin the previous work, and also pointed out errors in earlier
versions of this abstract. He also thanks to anonymous referees for constructive comments.
This work was supported in part by Grant-in-Aid for Scientific Research No. 13680411, from MEXT of Japan.

8.

REFERENCES[1] O. Danvy and A. Filinski. Abstracting Control. In
Proc. 1990 ACM Conference on Lisp and Functional
Programming, pages 151–160, 1990.
[2] O. Danvy and Z. Yang. An Operational Investigationof the CPS Hierarchy. In ESOP 99, Lecture Notes in
Computer Science 1576, pages 224–242, 1999.
[3] M. Felleisen. The Theory and Practice of First-Class
Prompts. In Proc. 15th Symposium on Principles ofProgramming Languages, pages 180–190, 1988.
[4] C. A. Gunter, D. Remy, and J. G. Riecke. A
Generalization of Exceptions and Control in ML-Like
Languages. In Proc. Functional Programming andComputer Architecture, pages 12–23, 1995.
[5] Y. Kameyama. A Type-Theoretic Study on Partial
Continuations. In Proc. IFIP International Conferenceon Theoretical Computer Science, Lecture Notes in
Computer Science 1872, pages 489–504, 2000.
[6] Y. Kameyama and M. Hasegawa. A Sound andComplete Axiomatization of Delimited Continuations.
In Proc. ACM International Conference on Functional
Programming, pages 177–188, 2003.
[7] E. Moggi. Computational Lambda-Calculus andMonads. In Proc. 4th Symposium on Logic in
Computer Science, pages 14–28, 1989.
[8] C. Murthy. Control Operators, Hierarchies, andPseudo-Classical Type Systems: A-Translation at
Work. In Proc. ACM Workshop on Continuation,
pages 49–71, 1992.
[9] Hieb R., R. Dybvig, and C. W. Anderson.
Subcontinuations. Lisp and Symbolic Computation,
6:453–484, 1993.
[10] A. Sabry and M. Felleisen. Reasoning about Programsin Continuation-Passing Style. Lisp and Symbolic
Computation, 6(3-4):289–360, 1993.
[11] P. Thiemann. Cogen in Six Lines. In Proc.
International Conference on Functional Programming,
pages 180–189, 1996.