5
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – cody Aug 14 '15 at 20:02
  • $\begingroup$ @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. $\endgroup$ – Martin Berger Aug 14 '15 at 20:12
  • $\begingroup$ @cody You're right, corrected. $\endgroup$ – Petr Pudlák Aug 14 '15 at 20:16
9
$\begingroup$

The definition is straightforward and can be found e.g. in (1, 2), see also (3). Here is a short summary, using a typed $\lambda$-calculus as basis. Types are not really needed for the presentation of reductions, but clarify the presentation in my opinion. Let's assume your language is given by the following grammar. $$ \newcommand{\PROGRAM}[1]{\mathsf{#1}} \newcommand{\FV}[1]{\mathsf{fv}(#1)} \newcommand{\DOM}[1]{\mathsf{dom}(#1)} \newcommand{\VERTICAL}{\; \mid\hspace{-3.0pt}\mid \; } \newcommand{\CALLCC}{\PROGRAM{callcc}} \newcommand{\CONT}[1]{\mathsf{Cont}(#1)} \newcommand{\THROW}{\PROGRAM{throw}} \newcommand{\infer}[2]{\frac{\displaystyle{ #1 }}{\displaystyle{ #2 }}} \newcommand{\ZEROPREMISERULE}[1]{\infer{-}{#1}} \newcommand{\FS}{\rightarrow} \newcommand{\RED}{\rightarrow} \newcommand{\ONEPREMISERULE}[2]{\infer{#1}{#2}} \newcommand{\TYPES}[3]{#1 \vdash #2 : #3} \newcommand{\TWOPREMISERULE}[3]{\infer{#1 \quad #2}{#3}} M ::= x \VERTICAL \lambda x.M \VERTICAL MM \VERTICAL ... \VERTICAL \CALLCC \VERTICAL \THROW $$ Here $\CALLCC$ and $\THROW$ are seen as constants although we could also have defined them in different ways. Let us denote by $\FV{M}$ the free variables of the program $M$. Types could be something like this: $$ \alpha\ ::=\ \alpha \FS\alpha \VERTICAL \PROGRAM{Int} \VERTICAL ... \VERTICAL \CONT{\alpha} $$ Here $\CONT{\alpha}$ is the type of continuations with final answer type $\alpha$. The constants $\CALLCC$ and $\THROW$ are values and have the following types. $$ \ZEROPREMISERULE { \TYPES{\Gamma}{\CALLCC}{(\CONT{\alpha} \FS \alpha) \FS \alpha} } \qquad \ZEROPREMISERULE { \TYPES{\Gamma}{\THROW}{\CONT{\alpha} \FS \alpha \FS \beta} } $$ Depending on your use-case, the type variables may be quantified. Reductions are defined with the help of configurations. A configuration is a pair $(M, \sigma)$ such that $M$ is a program and $\sigma$, the continuation map, ranged over by $\sigma, ...$, maps each $k \in \FV{M}$ of type $\CONT{\alpha}$ to an appropriately typed program. Then reductions are of the form $(M, \sigma) \RED (N, \sigma')$. For call-by-value, the reductions are generated as usual, with the following additions for $\CALLCC$ and $\THROW$. $$ \ONEPREMISERULE { k, x\ \text{fresh} } { (E[\CALLCC\ V], \sigma) \RED (E[V\;k], \sigma \cdot k \mapsto \lambda x.E[x]) } \quad \ONEPREMISERULE { \sigma(k) = M } { (E[\THROW\ k\ V], \sigma) \RED (MV, \sigma) } $$ Here $V$ over ranges over values, and $E[\cdot]$ over the usual call-by-value reduction contexts. The two new constants give rise to the following evaluation contexts: $\CALLCC\ E[\cdot]$, $\THROW\ E[\cdot]\ M$ and $\THROW\ V\ E[\cdot]$.

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.