# What is the formal definitions of the reduction related to the “call/cc” (call with the current continuation) operator?

In lambda calculus or in combinatory logic we formally define reduction/expansion rules for terms (and in their typed variants reductions must preserve the type). Then we can talk about properties of such systems, in particular about the normalization property or confluence.

How could one formally define reductions for the call/cc (call with the current continuation) operator in terms of a rewrite system?

The semantics of the operator allows to abandon the current evaluation context and return to the point where the continuation was captured, effectively allowing the evaluation state to become explicit.

I'd be interested in such a definition that'd allow to formally talk about confluence of such a system (and showing it doesn't hold, as the behavior of the operator depends on the evaluation order).

• Note that normalization in this field usually refers to only existence of normal forms and not unicity. That property is usually called confluence, and indeed googling "classical calculus confluence" gives many results, including the Wikipedia article on the $\lambda\mu$-calculus. – cody Aug 14 '15 at 20:02
• @cody I recommend not to use the $\lambda\mu$-approach to the operational semantics of continuations/jumps, because it's really complicated. The $\lambda\mu$-calculus is the only calculus I know whose semantics gets much easier when translated into the $\pi$-calculus. – Martin Berger Aug 14 '15 at 20:12
• @cody You're right, corrected. – Petr Aug 14 '15 at 20:16


Note that (1) does not use continuation maps to define the CBV semantics of $\CALLCC$ and $\THROW$. Instead a run-time value is introoduced. The two approaches are equivalent.

As to evaluation order, $\CALLCC$ enriches the power of contexts and can distinguish programs by application that are indistinguishable in the absence of continuations:

$$\newcommand{\ARGFC}{\PROGRAM{argfc}} \ARGFC = \CALLCC\ \lambda k.(\THROW\ {k}\ {\lambda x.(\THROW\ {k}\ {\lambda y.x}}))$$

This is the classic example of calling a function once, but returning twice. e.g. in $$(\lambda x.(x\; 1);(x\; 2))\ \ARGFC = 1$$ and $$(\lambda x.\lambda y.(x\; 1);(y\; 2))\ \ARGFC\ \ARGFC = 2$$

with $M;N$ being the sequential composition of $M$ and $N$, binding more tightly than $\lambda$-abstraction. The reason is that continuations carry information about contexts that may be returned (jumped) to later.

1. J. G. Riecke, H. Thielecke, Typed Exceptions and Continuations Cannot Macro-Express Each Other (Postscript file).

2. R. Harper, B. F. Duba, D. MacQueen, Typing First-Class Continuations in ML.

3. H. Thielecke, Continuations, functions and jumps.