15. Classical Logic via Continuations and Control Operators

Working System

This chapter uses reusable control-operator code from book/advanced/classical_control.py. Code is split into principles (Peirce, DNE) and operational examples.

15. Classical Logic via Continuations and Control Operators#

Goal. Show how continuation-style control corresponds to classical reasoning principles, and make that correspondence concrete with runnable encodings.

You will learn

  • What callcc (call-with-current-continuation) means operationally

  • How callcc realizes classical principles like Peirce’s law and double-negation elimination

  • How non-local exits model “proof by contradiction” style control flow

  • How search procedures (like “find the first satisfying element”) can be written using continuations

  • How CPS evaluation makes control explicit

Roadmap#

  1. Implement callcc as an exception-based escape in Python.

  2. Encode Peirce’s law and double-negation elimination using callcc.

  3. Use callcc as a programming tool: early return and search.

  4. Connect this to CPS by evaluating a tiny arithmetic AST.

Continuation View of Proofs#

Constructive implication treats proofs as direct programs. Classical reasoning can be represented by control effects, especially continuation capture.

A standard control type (schematically):

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

This enables terms inhabiting formulas not derivable in pure intuitionistic lambda calculus.

Key Classical Principles#

Peirce’s law:

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

Double-negation elimination (answer-type indexed):

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

Both become executable with continuation capture.

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

Core Operator callcc#

def demo_escape():
    return cc.callcc(lambda k: k("escaped"))

print(demo_escape())

escaped

Peirce and DNE Encodings#

peirce_result = cc.peirce(lambda use_ab: use_ab(42))
print("Peirce witness:", peirce_result)

nnA = lambda notA: notA("classical witness")
print("DNE witness:", cc.dne(nnA))

Peirce witness: 42
DNE witness: classical witness

Operational Reading (Non-Local Exit)#

The same mechanism models early return control flow.

xs = [1, 3, 5, 8, 9]
print("first even in xs:", cc.first_satisfying(xs, lambda x: x % 2 == 0, default=None))

ys = [1, 3, 5]
print("first even in ys:", cc.first_satisfying(ys, lambda x: x % 2 == 0, default=None))

first even in xs: 8
first even in ys: None

CPS Evaluator Reuse#

In continuation-passing style, every computation is already parameterized by continuation k. This is the ambient setting where classical control operators are naturally interpreted.

expr = ("+", 2, ("*", 3, 4))
out = cc.cps_eval(expr, lambda v: v)
print("CPS eval result:", out)

CPS eval result: 14

Reuse Note

The module advanced/classical_control.py separates pure control combinators from examples. You can reuse it to explore CPS transforms, exceptions, and backtracking search.

Exercise

  1. Use cc.callcc to implement an early-exit computation (for example, return the first pair (x,y) from nested loops satisfying a predicate). Test it on a small range.

  2. Use cc.first_satisfying to find the first element divisible by 7 in a list; confirm it returns the default when none exists.

  3. Instantiate Peirce’s law with A = int and B = str and write a function f : (A->B)->A that returns an A. Evaluate cc.peirce(f).

  4. Use cc.cps_eval(expr, k) with a nontrivial continuation k (for example lambda v: -v or lambda v: v+1) and explain the result. See solutions: Exercise 15 (Classical Logic via Control)

Summary#

  • Continuations make “the rest of the computation” explicit, and callcc captures it as a callable value.

  • Control operators can realize classical principles by turning negation into an escape continuation.

  • The same idea explains common programming patterns: early return, exceptions, and search.

  • CPS evaluation is a semantic style where continuations are already explicit.

  • Next: Chapter 16 introduces System F, where polymorphism explains many encodings in a typed setting.

Contents