15. Classical Logic via Continuations and Control Operators

15. Classical Logic via Continuations and Control Operators#

Goal. Understand how control (continuations) corresponds to classical reasoning, and learn to use callcc as an executable model.

You will learn

What a continuation is (“the rest of the computation”)
A precise type for callcc: \(((A \to R) \to A) \to A\)
How classical principles arise as programs with control effects
How to use callcc for early exit and backtracking in real code

Roadmap#

Give the continuation view and the type of callcc.
Implement and test callcc and derived classical principles.
Use the same mechanism for non-local exit and search.
Connect back to the intuitionistic boundary from Chapter 14.

Continuation View of Proofs#

A continuation is a representation of “what happens next”.

If an expression produces a value of type \(A\), we can think of it as receiving a continuation \(k : A \to R\) that consumes an \(A\) and produces a final answer \(R\).

In a CPS (continuation-passing style) evaluator, the evaluation judgment looks like:

\[ \llbracket t \rrbracket\,k \]

meaning “evaluate \(t\) and send its result to \(k\)”.

Key idea

callcc gives you the current continuation as a first-class function. That is exactly what makes classical reasoning computationally possible.

Core Operator `callcc`#

In many typed presentations, callcc has a type like:

\[ \mathrm{callcc} : ((A \to R) \to A) \to A \]

where \(R\) is an “answer type” (the final result type of the whole computation).

Operationally:

callcc(f) captures the current continuation k.
It calls f(k).
If k(v) is invoked, control jumps back to the point of capture and callcc(f) immediately returns v.

In Python we implement this jump via an internal exception.

from pathlib import Path
import sys

book_root = Path.cwd()
if not (book_root / "advanced").exists():
    book_root = book_root.parent
if str(book_root) not in sys.path:
    sys.path.insert(0, str(book_root))

from advanced import classical_control as cc

def demo_escape():
    # The continuation jump aborts the rest of the function body.
    return cc.callcc(lambda exit_: (exit_("escaped"), "unreachable")[1])

print(demo_escape())

escaped

Key Classical Principles#

Two standard classical principles are:

Peirce’s law

\[ ((A \to B) \to A) \to A \]

and double-negation elimination (DNE)

\[ ((A \to R) \to R) \to A. \]

Both are not derivable in the pure intuitionistic systems we used earlier, but they are realizable once we allow control.

In advanced/classical_control.py we provide:

cc.peirce(f) implementing Peirce’s law
cc.dne(nn_a) implementing DNE

# Peirce: ((A->B)->A)->A
peirce_result = cc.peirce(lambda use_ab: use_ab(42))
print("peirce_result:", peirce_result)

# DNE: ((A->R)->R)->A
# Here we pick A=int and R=str. nn_a must decide an int by calling its argument.

def nn_a(k):
    # Pretend we can only produce an R by running k.
    return k(7)

print("dne_result:", cc.dne(nn_a))

peirce_result: 42
dne_result: 7

Operational Reading (Non-Local Exit)#

A control operator is not only about “logic”; it is a practical tool.

For example, first_satisfying(xs, pred) returns the first element matching pred. Without callcc you can write it with a loop and break, but callcc lets you express “exit immediately with this witness” even when the search is nested or recursive.

xs = [1, 3, 5, 8, 9]
print(cc.first_satisfying(xs, lambda x: x % 2 == 0, default=None))
print(cc.first_satisfying(xs, lambda x: x > 20, default="no hit"))

8
no hit

Backtracking Search (Certificates)#

A more interesting pattern is backtracking.

We can search for a witness (a certificate) of an existential statement:

\[ \exists S \subseteq \{x_0,\dots,x_{n-1}\}.\ \sum S = T. \]

The function subset_sum_first(xs, target) returns such a witness subset if it exists. It uses callcc to escape the recursion as soon as a solution is found.

xs = [3, 5, 6, 7, 9]
print("subset for 14:", cc.subset_sum_first(xs, 14))
print("subset for 2:", cc.subset_sum_first(xs, 2))

subset for 14: [3, 5, 6]
subset for 2: None

CPS Evaluator Reuse#

A CPS evaluator makes the continuation explicit. In cc.cps_eval, the continuation k controls what we do with the final value.

This is the same pattern we used above:

continuations are explicit functions,
evaluation is structured by passing control forward.

expr = ("+", 2, ("*", 3, 4))
print(cc.cps_eval(expr, lambda v: v))
print(cc.cps_eval(expr, lambda v: -v))
print(cc.cps_eval(expr, lambda v: v + 1))

14
-14
15

What Changed Logically?#

Chapter 14’s sequent calculus corresponds to intuitionistic implication, so Peirce’s law fails. When we add control (callcc), we allow programs to:

abort computations,
reuse a continuation multiple times,
treat “the rest of the proof” as a callable object.

That extra power corresponds to classical reasoning principles.

Reality check

These programs have effects (control jumps). They are not definable in pure STLC. In typed settings you track this via answer types, effects, or delimited control operators.

Reuse Note

All core definitions are reusable from advanced/classical_control.py:

callcc(f)
classical combinators: peirce, dne
control patterns: first_satisfying, subset_sum_first
CPS evaluator: cps_eval

Exercise

Use callcc to exit from nested loops as soon as a condition holds (return the witness).
Modify subset_sum_first to also return the sum and confirm it equals the target.
Write a function that searches a list of pairs and returns the first pair whose product is even.
Show (by running search) that Peirce’s law is not derivable in Chapter 14 but is realizable here. See solutions: Exercise 15 (Classical Logic via Control)

Summary#

Continuations make “the rest of the computation” explicit.
callcc captures the current continuation and enables non-local control flow.
Classical principles like Peirce and DNE are executable once control is available.
The same mechanism supports practical patterns: early exit and backtracking with witnesses.

Next: Chapter 16 introduces System F (polymorphism) and a minimal type checker for explicit forall-types.