Classical Realizability, Poles, and Orthogonality

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

An intuitionistic realizer of an implication is a program that turns realizers of the premise into realizers of the conclusion. Try to build one for double-negation elimination. Write $\mathrm{\neg }A$ for $A\Rightarrow \mathrm{\perp }$. A realizer of $\mathrm{\neg }\mathrm{\neg }A\Rightarrow A$ must accept a program $z$ that, given any refutation of $A$, produces an absurdity, and must return a realizer of $A$. The only material available is $z$, and the only way to use $z$ is to supply it with a refutation of $A$; but a refutation of $A$ is not something the realizer has, and manufacturing one is exactly the problem to be solved. The attempt $$\lambda z.z(\lambda w.?)$$ stalls at the hole: whatever is written there must already be a realizer of $A$.

The repair changes what a proposition denotes. Instead of interpreting $A$ by the programs that establish it, interpret $A$ by the stacks that refute it, and recover the programs by an orthogonality condition against a fixed set of forbidden interactions. A program then realizes $A$ when it survives every refutation of $A$; and a program may survive a refutation by using it, which is what a control operator does. With that change the hole above is filled by a captured continuation, and the term $\lambda z.\mathsf{cc}(\lambda k.zk)$ realizes double-negation elimination.

Three parameters are fixed before anything is proved: a machine, a set of processes called the pole, and a language. This chapter fixes the machine and the pole first (section 145.1, section 145.2), then the interpretation (section 145.3), then proves that control operators realize the classical axioms (section 145.4) and that every proof of the frozen system realizes its conclusion (section 145.5). The tripos and forcing connections are named only after all of that, in section 145.6, and no theorem of this chapter depends on them.

The ${\lambda }_c$-calculus and its machine

The two sets are defined by a simultaneous induction: a stack $t\cdot \pi$ contains a term, and a term $k_{\pi }$ contains a stack. $\mathrm{\Pi }$ is nonempty because ${\mathrm{\Pi }}_0$ is, and that is used in corollary 145.23.

Push and Grab implement weak head reduction. Save hands the current stack to the program as the term $k_{\pi }$; Restore discards whatever stack has since accumulated and reinstalls $\pi$. The pattern in which $\mathsf{cc}$ is normally used chains the two: $$\mathsf{cc}(\lambda k.t)\ast \pi \stackrel{Push}{\succ }\mathsf{cc}\ast (\lambda k.t)\cdot \pi \stackrel{Save}{\succ }(\lambda k.t)\ast k_{\pi }\cdot \pi \stackrel{Grab}{\succ }t[k_{\pi }/k]\ast \pi .$$ The body $t$ runs with the name $k$ bound to the stack that was current when $\mathsf{cc}$ was reached. Applying $k$ to an argument abandons the computation in progress and restarts that stack.

Poles and orthogonality

Read $p\in ⟂⟂$ as “the interaction $p$ is admissible”. The closure condition is stated backwards along evaluation because a process is judged by what it becomes.

Proof of Lemma 145.7 — Orthogonality is a Galois connection

Proof. (1) A term orthogonal to every stack in the larger set is orthogonal to every stack in the smaller one.

(2) Let $\pi \in S$ and $t\in S^{⟂}$. By the definition of $S^{⟂}$, $t\ast \pi \in ⟂⟂$. As $t$ was arbitrary in $S^{⟂}$, this says $\pi \in S^{⟂⟂}$.

(3) By (2) applied to $S^{⟂}\subseteq \mathrm{\Lambda }$ we get $S^{⟂}\subseteq S^{⟂⟂⟂}$. By (2) applied to $S$ and then (1), $S\subseteq S^{⟂⟂}$ gives $S^{⟂⟂⟂}\subseteq S^{⟂}$.

(4) $t\in (\bigcup _i{S}_i{)}^{⟂}$ says $t\ast \pi \in ⟂⟂$ for every $\pi$ lying in some $S_i$, which is the conjunction over $i$ of $t\in S_i^{⟂}$. ◻

Falsity values, truth values, and realizability

The definition of $\Vert \cdot \Vert$ is by induction on the formula; the clause for $\Rightarrow$ mentions $|A|$, which is $\Vert A{\Vert }^{⟂}$ and therefore already defined at the smaller formula $A$. Nothing is defined by induction on truth values.

Proof of Lemma 145.11 — Truth values of quantifiers

Proof. The two equalities are lemma 145.7(4) applied to the unions in definition 145.10. For the inclusion, let $t\in |A\Rightarrow B|$, $u\in |A|$ and $\pi \in \Vert B\Vert$. Then $u\cdot \pi \in \Vert A\Rightarrow B\Vert$, so $t\ast u\cdot \pi \in ⟂⟂$. Since $tu\ast \pi \stackrel{Push}{\succ }t\ast u\cdot \pi$ and the pole is closed under anti-evaluation, $tu\ast \pi \in ⟂⟂$. As $\pi$ was arbitrary, $tu\in |B|$. ◻

Control operators realize the classical axioms

Fix a pole throughout this section. The two theorems below are the reason the interpretation was arranged around stacks: they read a computational rule of definition 145.2 directly as a logical property, with no induction on formulas.

Proof of Proposition 145.13 — Typing a continuation constant

Proof. Let ${\pi }^{\prime }\in \Vert A\Rightarrow B\Vert$. By definition 145.10, ${\pi }^{\prime }=u\cdot {\pi }^{″}$ with $u\in |A|$ and ${\pi }^{″}\in \Vert B\Vert$. Then $$k_{\pi }\ast {\pi }^{\prime }=k_{\pi }\ast u\cdot {\pi }^{″}\stackrel{Restore}{\succ }u\ast \pi ,$$ and $u\ast \pi \in ⟂⟂$ because $u\in |A|$ and $\pi \in \Vert A\Vert$. Closure under anti-evaluation gives $k_{\pi }\ast {\pi }^{\prime }\in ⟂⟂$. As ${\pi }^{\prime }$ was arbitrary, $k_{\pi }\in \Vert A\Rightarrow B{\Vert }^{⟂}$. ◻

The stack ${\pi }^{″}$ is discarded by Restore and never examined; that is why $B$ may be any formula. A continuation constant is a realizer of an implication whose conclusion it never has to produce.

Proof of Theorem 145.14 — cc realizes Peirce's law

Proof. Let $\pi \in \Vert ((A\Rightarrow B)\Rightarrow A)\Rightarrow A\Vert$. By definition 145.10, $\pi =t\cdot {\pi }^{\prime }$ with $t\in |(A\Rightarrow B)\Rightarrow A|$ and ${\pi }^{\prime }\in \Vert A\Vert$. By Save, $$\mathsf{cc}\ast t\cdot {\pi }^{\prime }\succ t\ast k_{{\pi }^{\prime }}\cdot {\pi }^{\prime }.$$ Now ${\pi }^{\prime }\in \Vert A\Vert$, so proposition 145.13 gives $k_{{\pi }^{\prime }}\in |A\Rightarrow B|$, whence $$k_{{\pi }^{\prime }}\cdot {\pi }^{\prime }\in |A\Rightarrow B|\cdot \Vert A\Vert =\Vert (A\Rightarrow B)\Rightarrow A\Vert .$$ Since $t$ realizes that formula, $t\ast k_{{\pi }^{\prime }}\cdot {\pi }^{\prime }\in ⟂⟂$, and closure under anti-evaluation gives $\mathsf{cc}\ast \pi \in ⟂⟂$. ◻

Neither proof used any property of the pole beyond definition 145.5, and neither inspected $A$ or $B$. The next proposition shows that the correspondence between machine behavior and realized formulas runs in both directions.

Proof of Proposition 145.16 — Behavior determines the formula

Proof. From behavior to realizability. Let $t$ be identity-like, fix a pole, and let $\pi \in \Vert \mathrm{\forall }X(X\Rightarrow X)\Vert$. By definition 145.10 that set is $\bigcup _{S\subseteq \mathrm{\Pi }}\Vert \dot{S}\Rightarrow \dot{S}\Vert$, so $\pi \in \Vert \dot{S}\Rightarrow \dot{S}\Vert =S^{⟂}\cdot S$ for some $S$, that is, $\pi =u\cdot {\pi }^{\prime }$ with $u\in S^{⟂}$ and ${\pi }^{\prime }\in S$. Then $u\ast {\pi }^{\prime }\in ⟂⟂$ by the definition of $S^{⟂}$, and $t\ast \pi =t\ast u\cdot {\pi }^{\prime }\succ u\ast {\pi }^{\prime }$, so $t\ast \pi \in ⟂⟂$ by anti-evaluation.

From realizability to behavior. Let $t$ realize $\mathrm{\forall }X(X\Rightarrow X)$ for every pole, and fix $u\in \mathrm{\Lambda }$ and $\pi \in \mathrm{\Pi }$. Choose the pole $⟂⟂:=\{p\mid p\succ u\ast \pi \}$ of example 145.8 and the falsity value $S:=\{\pi \}$. Then $u\ast \pi \in ⟂⟂$ by reflexivity of $\succ$, so $u\in S^{⟂}$, and therefore $$u\cdot \pi \in S^{⟂}\cdot S=\Vert \dot{S}\Rightarrow \dot{S}\Vert \subseteq \Vert \mathrm{\forall }X(X\Rightarrow X)\Vert .$$ Since $t$ realizes the formula at this pole, $t\ast u\cdot \pi \in ⟂⟂$, which by the definition of this particular pole says $t\ast u\cdot \pi \succ u\ast \pi$. ◻

The second half is the pattern used throughout classical realizability to prove converses: a single process is turned into a pole, and a single stack into a falsity value, so that “realizes” collapses to the one behavioral statement wanted.

Adequacy

Only $\Rightarrow$ and the two universal quantifiers are primitive; the other connectives are the usual second-order abbreviations, and no rule mentions them. Proof terms are proof-like: no continuation constant occurs in definition 145.18.

Proof of Lemma 145.20 — Substitution in falsity values

Proof. Induction on $A$. At an atom $X(e_1,\dots ,e_k)$ with $X$ the substituted variable, the left-hand side is $\Vert C[\rho ][{\overrightarrow{e}}^{\mathbb{N}}/\overrightarrow{x}]\Vert$ by definition 145.10 and the right-hand side is $F_{P,\rho }({\overrightarrow{e}}^{\mathbb{N}})$, the same set by the definition of $F_{P,\rho }$. At an atom whose head is a different variable or a parameter, both sides are unchanged. The clause for $\Rightarrow$ applies the induction hypotheses to the two immediate subformulas, and the two quantifier clauses apply them under each substitution instance, the bound variable being chosen outside $\mathrm{dom}(\rho )$, outside the free variables of $e$ and outside those of $C$. ◻

Proof of Theorem 145.21 — Adequacy

Proof. Induction on the derivation; each case checks definition 145.19 for the conclusion. Fix a valuation $\rho$, fix realizers $u_i$ of $A_i[\rho ]$, and abbreviate the simultaneous substitution by $\theta :=[u_1/z_1,\dots ,u_n/z_n]$.

Ax. $t=z_j$ and $A=A_j$, so $t[\theta ]=u_j$, which lies in $|A_j[\rho ]|$ by hypothesis.

Peirce. $t=\mathsf{cc}$, which is closed, so $t[\theta ]=\mathsf{cc}$; theorem 145.14 at the formulas $A[\rho ]$ and $B[\rho ]$ gives the membership.

$\Rightarrow$-I. Let $\pi \in \Vert A[\rho ]\Rightarrow B[\rho ]\Vert$, so $\pi =u\cdot {\pi }^{\prime }$ with $u\in |A[\rho ]|$ and ${\pi }^{\prime }\in \Vert B[\rho ]\Vert$. Then $$(\lambda z.t)[\theta ]\ast u\cdot {\pi }^{\prime }=(\lambda z.t[\theta ])\ast u\cdot {\pi }^{\prime }\stackrel{Grab}{\succ }t[\theta ][u/z]\ast {\pi }^{\prime },$$ the bound name $z$ being chosen distinct from every $z_i$ and fresh for every $u_i$. The induction hypothesis for the premise, applied to the extended list of realizers $u_1,\dots ,u_n,u$, gives $t[\theta ][u/z]\in |B[\rho ]|$, hence $t[\theta ][u/z]\ast {\pi }^{\prime }\in ⟂⟂$; anti-evaluation finishes the case.

$\Rightarrow$-E. By the induction hypotheses $t[\theta ]\in |A[\rho ]\Rightarrow B[\rho ]|$ and $u[\theta ]\in |A[\rho ]|$. Lemma 145.11 gives $t[\theta ]u[\theta ]\in |B[\rho ]|$, and $(tu)[\theta ]=t[\theta ]u[\theta ]$.

${\mathrm{\forall }}_1$-I. By definition 145.10, $\Vert (\mathrm{\forall }xA)[\rho ]\Vert =\bigcup _n\Vert A[\rho [x\mapsto n]]\Vert$, so by lemma 145.7(4) $|(\mathrm{\forall }xA)[\rho ]|=\bigcap _n|A[\rho [x\mapsto n]]|$. Fix $n$. Since $x$ is not free in $\mathrm{\Gamma }$, the hypotheses $u_i\in |A_i[\rho ]|$ read equally as $u_i\in |A_i[\rho [x\mapsto n]]|$, so the induction hypothesis at the valuation $\rho [x\mapsto n]$ gives $t[\theta ]\in |A[\rho [x\mapsto n]]|$. As $n$ was arbitrary, $t[\theta ]$ lies in the intersection.

${\mathrm{\forall }}_1$-E. By the induction hypothesis $t[\theta ]\in |(\mathrm{\forall }xA)[\rho ]|=\bigcap _n|A[\rho [x\mapsto n]]|$. Take $n:=e^{\mathbb{N}}[\rho ]$; then $t[\theta ]\in |A[\rho [x\mapsto n]]|$, which equals $|(A[e/x])[\rho ]|$ by lemma 145.20.

${\mathrm{\forall }}_2$-I and ${\mathrm{\forall }}_2$-E. The same two arguments with falsity functions in place of natural numbers: the union in definition 145.10 is over all $F:{\mathbb{N}}^k\to \mathcal{P}(\mathrm{\Pi })$, the side condition $X\notin \mathrm{FV}(\mathrm{\Gamma })$ makes the hypotheses on the $u_i$ independent of $F$, and the elimination case instantiates $F$ at $F_{P,\rho }$, which is the falsity function named by lemma 145.20.

Every rule being adequate, an induction on the derivation gives adequacy of every derivable judgment. ◻

Proof of Corollary 145.22 — Proofs give universal realizers

Proof. $t$ is proof-like because definition 145.18 produces no continuation constant. Apply theorem 145.21 with $n=0$ at an arbitrary pole and an arbitrary valuation; $A$ is closed, so $A[\rho ]=A$. ◻

Proof of Corollary 145.23 — Consistency

Proof. By definition 145.10, $\Vert \mathrm{\forall }XX\Vert$ is the union of $\Vert \dot{F}\Vert =F$ over all $F:\mathcal{P}(\mathrm{\Pi })$ of arity $0$, that is, over all subsets of $\mathrm{\Pi }$; so $\Vert \mathrm{\forall }XX\Vert =\mathrm{\Pi }$. Take the empty pole (example 145.8). Then $$|\mathrm{\forall }XX|={\mathrm{\Pi }}^{⟂}=\{t\in \mathrm{\Lambda }\mid t\ast \pi \in \varnothing \text{ for every }\pi \in \mathrm{\Pi }\}=\varnothing ,$$ the last equality because $\mathrm{\Pi }\ne \varnothing$: the set ${\mathrm{\Pi }}_0$ of stack constants is nonempty by definition 145.1. If $⊢t:\mathrm{\forall }XX$ held, corollary 145.22 would put $t$ in the empty set. ◻

Corollary 145.23 is the payoff of the arrangement. It uses the whole chapter: the syntax to know that $\mathrm{\Pi }$ is nonempty, the pole axiom to know that $\varnothing$ is admissible, the definition of falsity values to compute $\Vert \mathrm{\forall }XX\Vert$, and adequacy to connect the computation to derivability.

What the model does not do

The machine of definition 145.2 is not required to normalize, and nothing above uses confluence. Definition 145.2 fixes $\succ$ as a parameter containing four rules; adding instructions and rules to $\mathcal{K}$ and to $\succ$ preserves every proof in this chapter, because each proof used only closure of the pole under anti-evaluation and the four displayed rules in the forward direction. That extensibility is the point of axiomatizing evaluation rather than defining it.

Suggested first pass.

Begin with exercise 145.7 and exercise 145.9, then complete exercise 145.11.

Exercise 145.7¶

★★☆ Write the complete machine trace of $\mathsf{cc}(\lambda k.\lambda x.kx)\ast u\cdot \pi$, naming the rule at each step, and identify the stack that is discarded. Then say which line of the proof of theorem 145.14 corresponds to each step.

Referenced from 3 locations

• Classical Realizability, Poles, and Orthogonality

Exercise 145.8¶

★★☆ Show that the poles of definition 145.5 are closed under arbitrary intersection and arbitrary union, so that they form a complete lattice ordered by inclusion. Identify its top and bottom elements, and show that $A$ is realized with respect to the top pole for every closed $A$.

Referenced from 2 locations

• Classical Realizability, Poles, and Orthogonality

Exercise 145.9¶

★★★ (Storage.) Call a closed term $M$ a storage operator when $$M\ast t\cdot u\cdot \pi \succ t\ast \bar{n}\cdot u\cdot \pi$$ for every $t$ realizing $\bar{n}\in \mathrm{N}$, where $\mathrm{N}$ is the relativization predicate of remark 145.24. Prove that $$M:=\lambda n.\lambda f.n(\lambda g.g\bar{0})(\lambda h.\lambda g.h(\lambda y.g(\mathsf{s}y)))(\lambda z.z)f$$ satisfies this specification for the numerals of definition 145.4, or repair it and prove the repaired term correct. State exactly which clause of definition 145.10 makes the specification a statement about all poles.

Referenced from 3 locations

• Classical Realizability, Poles, and Orthogonality

Exercise 145.10¶

★★★ Prove that $|A\Rightarrow B|$ is in general a proper subset of $|A|\to |B|$ (remark 145.12), by exhibiting a pole, formulas $A$ and $B$, and a term belonging to the second set and not the first. Hint: choose a pole in which a term can detect whether its stack has the shape $u\cdot \pi$ before any Push occurs.

Referenced from 2 locations

• Classical Realizability, Poles, and Orthogonality

Exercise 145.11¶

★★★ Practical project.krivine-machine-and-realizer-checker Implement the Krivine machine of definition 145.2 together with a checker for the two decidable specifications used in this chapter. The machine takes a closed term and a stack, both given as syntax trees over the grammar of definition 145.1, and a step budget; it returns either the process reached after that many steps or the first process on which no rule applies. Continuation constants are represented by the stack they carry, so that Restore is a genuine stack replacement and not a return.

Invariant. After every step the machine’s state is a well-formed process: the term is closed, and every $k_{\pi }$ occurring in it carries a stack built only from closed terms and stack constants. The implementation checks this invariant after each step and aborts, naming the offending subterm, rather than continuing on a malformed state.

Concrete result. For the identity-like test the program takes a closed term $t$, a finite list of test pairs $(u,\pi )$, and reports for each pair either identity-like together with the trace witnessing $t\ast u\cdot \pi \succ u\ast \pi$, or not identity-like together with the process at which the trace stopped. For the storage test it takes a term $M$ and a bound $N$ and reports, for each $n\le N$, whether $M\ast \bar{n}\cdot u\cdot \pi$ reaches $u\ast \bar{n}\cdot \pi$.

Acceptance test. With ${\mathrm{\Pi }}_0=\{\alpha \}$ and $u:=\lambda x.x$: the three terms of example 145.17 must all report identity-like on the pair $(u,\alpha )$; the trace of the third must contain a Save step followed by a Restore step, and the trace of the second must contain a Save step and no Restore step. On the pair $(\omega ,\alpha )$ with $\omega :=\lambda z.zz$, the term $\lambda x.xx$ must report not identity-like with budget exhausted, and the printed last process must have a stack strictly longer than $\alpha$. Finally, run the term of example 145.3 applied to two copies of $u$, against the stack $\alpha$, for nine steps: the trace must contain two Grab steps and must end with a Restore step whose stack is the saved $u\cdot \alpha$ and not the caller’s $\alpha$. A run in which Restore returns to the caller instead of installing $\pi$ passes the three identity-like checks unchanged and fails only here, which is why the acceptance test includes it: the two stacks coincide on the identity-like probes and differ exactly on this one.

Referenced from 3 locations

• Classical Realizability, Poles, and Orthogonality