<p>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 <em>language</em> 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 <em>free variables</em> of the program $M$.
<em>Types</em> 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 <em>configuration</em> is a pair $(M, \sigma)$ such that $M$ is a
program and $\sigma$, the <em>continuation map</em>, ranged over by
$\sigma, ...$, maps each $k \in \FV{M}$ of type $\CONT{\alpha}$ to an appropriately typed program.
Then
<em>reductions</em> 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 <em>values</em>, and
$E[\cdot]$ over the usual call-by-value <em>reduction contexts</em>. The two new constants give rise to the following evaluation contexts: $\CALLCC\ E[\cdot]$, $\THROW\ E[\cdot]\ M$
and $\THROW\ V\ E[\cdot]$.</p>

<p>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.</p>

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

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

<p>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
  $$</p>

<p>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.</p>

<hr>

<ol>
<li><p>J. G. Riecke, H. Thielecke, <a href="https://www.cs.bham.ac.uk/~hxt/research/exn-and-cont.ps" rel="nofollow">Typed Exceptions and Continuations Cannot Macro-Express Each Other</a> (Postscript file).</p></li>
<li><p>R. Harper, B. F. Duba, D. MacQueen, <a href="http://www.cs.cmu.edu/~rwh/papers/callcc/popl91.pdf" rel="nofollow">Typing First-Class Continuations in ML</a>.</p></li>
<li><p>H. Thielecke, <a href="http://www.cs.bham.ac.uk/~hxt/research/Logiccolumn8.pdf" rel="nofollow">Continuations, functions and jumps</a>.</p></li>
</ol>

CC BY-SA 3.0
2015-08-14T19:48:27.440Z
2015-08-15T11:28:24.727Z
2015-08-15T11:28:24.727Z
Martin Berger
<p>In <a href="https://en.wikipedia.org/w/index.php?title=Lambda_calculus&amp;oldid=675419259#Reduction" rel="nofollow noreferrer">lambda calculus</a> or in <a href="https://en.wikipedia.org/w/index.php?title=Combinatory_logic&amp;oldid=672097334#Reduction_in_combinatory_logic" rel="nofollow noreferrer">combinatory logic</a> 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 <a href="https://en.wikipedia.org/wiki/Normalization_property_(abstract_rewriting)" rel="nofollow noreferrer">the normalization property</a> or <a href="https://en.wikipedia.org/wiki/Confluence_(abstract_rewriting)" rel="nofollow noreferrer">confluence</a>.</p>

<p><strong>How could one formally define reductions for the <a href="https://en.wikipedia.org/wiki/Call-with-current-continuation" rel="nofollow noreferrer">call/cc</a> <em>(call with the current continuation)</em> operator</strong> in terms of a rewrite system?</p>

<p>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.</p>

<p>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 <a href="https://stackoverflow.com/q/24711643/1333025">depends on the evaluation order</a>).</p>

CC BY-SA 3.0
2015-08-14T20:02:02.200Z
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](https://en.wikipedia.org/wiki/Lambda-mu_calculus).
cody
CC BY-SA 3.0
2015-08-14T20:12:33.297Z
@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
CC BY-SA 3.0
2015-08-14T20:16:10.023Z
@cody You're right, corrected.
Petr
<lambda-calculus><term-rewriting-systems><normalization><continuations>
What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?
Petr
# What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?

(Asked by: username_0 on 2015-08-14)

In [lambda calculus](https://en.wikipedia.org/w/index.php?title=Lambda_calculus&oldid=675419259#Reduction) or in [combinatory logic](https://en.wikipedia.org/w/index.php?title=Combinatory_logic&oldid=672097334#Reduction_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](https://en.wikipedia.org/wiki/Normalization_property_(abstract_rewriting)) or [confluence](https://en.wikipedia.org/wiki/Confluence_(abstract_rewriting)).

**How could one formally define reductions for the [call/cc](https://en.wikipedia.org/wiki/Call-with-current-continuation) *(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](https://stackoverflow.com/q/24711643/1333025)).

**Tags:** lambda-calculus, term-rewriting-systems, normalization, continuations

> **Comments:**
> **username_1**: 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](https://en.wikipedia.org/wiki/Lambda-mu_calculus).  
> **username_2**: @username_1 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.  
> **username_0**: @username_1 You're right, corrected.  

---

## 1 answers

### Answer by username_2 on 2015-08-14. Score: 10 | Accepted answer

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](https://www.cs.bham.ac.uk/~hxt/research/exn-and-cont.ps) (Postscript file).
2. R. Harper, B. F. Duba, D. MacQueen, [Typing First-Class Continuations in ML](http://www.cs.cmu.edu/~rwh/papers/callcc/popl91.pdf).
3. H. Thielecke, [Continuations, functions and jumps](http://www.cs.bham.ac.uk/~hxt/research/Logiccolumn8.pdf).


---

