Bar Recursion, Choice, and Program Extraction

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

A finite product can resolve every continuation before it returns. Countable choice does not come with a last question. A counterexample functional may inspect one more proposed choice than any bound fixed before the functional is run. The required recursion must therefore discover its stopping point from the counterexample while remaining total.

The selected solution has three parts. Finite products of selection functions perform the backward calculation. Their explicitly controlled infinite product satisfies Spector’s equations. Restricted Spector bar recursion implements the same equations in the total continuous functionals, where continuity and bar induction justify totality. No later core chapter depends on this route.

The higher-type arithmetic used here

The finite types are generated by $$\rho ,\tau ::=\mathbb{N}\mid \rho \to \tau .$$ Finite products and finite sequences are conservative codings. Put $$\mathrm{deg}(\mathbb{N})=0,\mathrm{deg}(\rho \to \tau )=max\{\mathrm{deg}(\rho )+1,\mathrm{deg}(\tau )\}.$$ The phrase finite type means a member of this hierarchy; it does not mean a type with finitely many elements. The Boolean set used in examples is finite and discrete, while $\mathbb{N}\to \mathbb{N}$ is a finite type with infinitely many inhabitants.

The shared rule schema in chapter 66 explains the Dialectica clauses, but that chapter proves its direct soundness theorem only for first-order $\mathsf{HA}$. It does not prove the higher-type theorem used here. The weakly extensional base and its functional-interpretation soundness are therefore an explicit imported boundary [Koh98].

Fix a formula $A(n,x)$, and write $A^{\mathsf{N}}$ for its chosen negative translation. Countable choice and its negative form are different formulas: For a quantifier-free matrix, $A^{\mathsf{N}}=A$. The remaining logical principle is double-negation shift $${\mathsf{DNS}}_{\mathbb{N}}:(\mathrm{\forall }n.\mathrm{\neg }\mathrm{\neg }B(n))\to \mathrm{\neg }\mathrm{\neg }\mathrm{\forall }n.B(n).$$ Work in $\mathrm{WE}\text{-}{\mathsf{HA}}^{\omega }+{\mathsf{AC}}_{\mathbb{N}}$. Then ${\mathsf{DNS}}_{\mathbb{N}}$ derives ${\mathsf{cAC}}_{\mathbb{N}}$: apply ${\mathsf{DNS}}_{\mathbb{N}}$ to $B(n)\equiv \mathrm{\exists }x.A^{\mathsf{N}}(n,x)$, then use intuitionistic countable choice inside the final double negation. This is the exact logical reduction realized below [Pow13].

Finite choice as backward calculation

Fix types $X,R$. The selection type is $$J_{R}X:=(X\to R)\to X.$$ A selection function $\epsilon :J_{R}X$ receives a continuation $p:X\to R$ and returns an element of $X$. In a Dialectica argument, $p$ is a proposed counterexample response, not necessarily a numerical score.

The continuation for the first choice contains the entire later product. Replacing it by $x\mapsto q(x,0,\dots ,0)$ changes the choice problem.

Proof of Lemma 67.4 — Finite product equations

Proof. Induct on $m$. At $m=0$ there is no coordinate. At $m+1$, the definition gives $\alpha (0)={\epsilon }_0(p_0)$, and substitution into the same definition gives $p_0(\alpha (0))=q(\alpha )$. Fix . The tail of $\alpha$ is the product of ${\epsilon }_1,\dots ,{\epsilon }_m$ against $q_{\alpha (0)}$. The induction hypothesis at tail coordinate $i$ gives both required equations, and restoring the fixed first coordinate changes $q_{\alpha (0)}$ back to $q$. ◻

Proof of Theorem 67.5 — Finite DNS and finite choice

Proof. Fix $q$, take $\alpha =P_m(\overrightarrow{\epsilon })(q)$, and take the tuple $\overrightarrow{p}$ from lemma 67.4. The premise at coordinate $i$ is $A_i({\epsilon }_i(p_i),p_i({\epsilon }_i(p_i)))$. The two product equations rewrite its arguments to $\alpha (i)$ and $q(\alpha )$, which is the required conclusion. The finite-choice consequence first applies this finite DNS instance to the finitely many existential matrices and then uses intuitionistic finite choice. ◻

This is the equation-level proof of the primary finite-product result [EOP11].

For a complete finite-choice instance, put $A_i(x,y)\equiv x=c_i$, where $(c_0,c_1,c_2)=(1,0,1)$. Take each ${\epsilon }_i$ to be the constant selector $c_i$. For every challenger $q$, the product returns $(1,0,1)$, and each premise and conclusion reduces to $c_i=c_i$. This example is logically complete but computationally degenerate. The score calculation in example 67.3 shows the continuation dependence hidden by constant selectors.

Proof of Proposition 67.6 — Exact finite-type level

Proof. The first construction recurses over a continuation state of type $X^{\ast }\to X^{\mathbb{N}}$. The second makes a product write the successive states of an $X$-valued recursor into an $X^{\mathbb{N}}$ register. The third uses selection functions over $X\to X$, which raises the result-type degree once. ◻

These are precisely Theorems 18, 19, and 21 and Corollary 22 of the finite-product source [EOP11].

Why no uniform truncation suffices

Proof of Proposition 67.7 — No uniform coordinate horizon

Proof. Define $q_m(\alpha )=1$ when $\alpha (m)=1_X$, and zero otherwise. The functional inspects one coordinate, so it is continuous. Streams that agree below $m$ and differ at $m$ receive different values. ◻

The proposition refutes a uniform truncation of all continuous challengers. It does not by itself prove that System T cannot realize DNS; such a nondefinability theorem needs a semantic separation argument not developed here. What the proposition forces locally is a control functional whose value is consulted during the recursion.

The explicitly controlled product

Let $X$ be a discrete type with a distinguished point $0_X$. Write $X^{\ast }$ for finite lists. For a stream $\alpha :X^{\mathbb{N}}$, its prefix of length $n$ is $[\alpha ](n)$. Write $s\ast x$ for list append, $s\ast \alpha$ for prefixing a stream, and $\mathbf{0}$ for the constant $0_X$-stream. For $q:X^{\mathbb{N}}\to R$, put $q_s(\beta ):=q(s\ast \beta )$.

The strict inequality is part of the interface. Equality takes the recursive branch. This is the simple product of the primary source, not its later history-sensitive dependent variant [EO14].

Proof of Lemma 67.9 — Prefix factorization

Proof. Induct on $i$. At zero the equation is the definition of $\alpha$. Assume the factorization at $i$. If , the recursive call is $\mathbf{0}$, so $\alpha =[\alpha ](i)\ast \mathbf{0}$. The same value of $q$ occurs after one more zero, and the strict inequality implies ; the call at $i+1$ is also zero. If the inequality fails, one unfolding writes a head $c=\alpha (i)$ and the tail call at $i+1$. In both cases the factorization at $i+1$ follows. ◻

This is the full two-case induction of Lemma 3.2 [EO14].

Proof of Theorem 67.10 — Controlled-product equations

Proof. First prove that the call at stage $i$ takes the recursive branch. If it stopped, then . Prefix factorization would give $\alpha =[\alpha ](i)\ast \mathbf{0}$, hence a contradiction. One unfolding therefore gives $\alpha (i)={\epsilon }_i(p_i)$. Prefix factorization at $i+1$ gives  ◻

The hypothesis and contradiction are exactly those of Theorem 3.8 [EO14].

Dependent control and restricted Spector recursion

Restricted Spector recursion lets the selector depend on the finite history. For $s\in X^{\ast }$ and $\beta :X^{\mathbb{N}}$, define the prefix-preserving update Unlike list prefixing, $\mathsf{put}$ does not shift the tail indices.

This is Definition 3.11 of the arXiv source. Its course-of-values adapter proves that the simple product defines the dependent product by a System T term [EO14].

The result preserves $s$ definitionally: $$[{\mathsf{SBR}}_s^{\omega }(\delta )](|s|)=s.$$ In the recursive branch, the child already preserves $s\ast c$, so applying $\mathsf{put}(s,-)$ changes no coordinate. The source writes this operation with its update symbol; the explicit definition above prevents it from being mistaken for shifting concatenation. This is the special recursor in Definition 3.17 [EO14].

Proof of Theorem 67.13 — The controlled product defines SBR

Proof. Take $R^{\prime }=X^{\mathbb{N}}\times \mathbb{N}$, $l={\pi }_2$, and $$q_s^{\omega }(\beta ):=(s\ast \beta ,\omega (s\ast \beta )),{\tilde{\delta }}_s(P):={\delta }_s(\lambda x.{\pi }_1(Px)).$$ Define $${\mathsf{SBR}}_s^{\omega }(\delta ):=s\ast {\mathsf{EPS}}_s^{{\pi }_2}(\tilde{\delta })(q_s^{\omega }).$$ The base tests agree because ${\pi }_2(q_s^{\omega }(\mathbf{0}))=\omega (s\ast \mathbf{0})=\omega (\mathsf{put}(s,\mathbf{0}))$. In the recursive branch, ${\pi }_1$ removes the numerical control before the continuation reaches ${\delta }_s$. The identities $$s\ast (x\ast \beta )=(s\ast x)\ast \beta ,(q_s^{\omega }{)}_x=q_{s\ast x}^{\omega }$$ make the selected heads equal and turn the recursive EPS call into the child SBR call. The outer shifting prefix then agrees with the prefix-preserving update in the SBR equation because the child stream already preserves $s\ast x$. ◻

These are the full adapters of Theorem 3.18 [EO14].

The reverse comparison uses the source’s relativized bar induction, not the decidable two-predicate principle used for semantic totality below. For predicates $S,P$ on $X^{\ast }$, write $\alpha \in S$ for $\mathrm{\forall }n.S([\alpha ](n))$. The scheme ${\mathrm{BI}}_{\mathrm{rel}}$ concludes $P([])$ from $$\begin{array}{c}S([]),\mathrm{\forall }\alpha \in S.\mathrm{\exists }n.P([\alpha ](n)),\\ \mathrm{\forall }s\in S.((\mathrm{\forall }x.(S(s\ast x)\to P(s\ast x)))\to P(s)).\end{array}$$

Proof of Theorem 67.14 — Conditional reverse definability

Proof. The sourced reverse route has four steps. First, restricted SBR defines the general bar recursor That adapter is Powell’s external edge in the comparison. The direct primitive-recursive equivalence between dependent EPS and SBR alone does not give the return from the dependent product to the simple product used here. Second, bar induction and Spector’s condition define the explicitly controlled product of quantifiers $\mathsf{EPQ}$ from $\mathsf{BR}$. Third, the simple quantifier product is the history-independent instance of EPQ. Fourth, bar induction defines the simple selection product from that quantifier product. Finally Theorem 3.13 defines dependent EPS from the simple product.

The two uses of ${\mathrm{BI}}_{\mathrm{rel}}$ are hypotheses, not System T programs. The source records them in Theorems 3.7 and 3.16 and leaves their removal open; its Theorems 3.13 and 3.18 prove only the forward direction used in theorem 67.13. ◻

Powell proves the direct dependent-EPS/SBR equivalence in Example 9.5 and Theorem 9.6(a)[Pow13]. The conditional return to the simple product follows the comparison route in Escardó and Oliva[EO14].

Totality from continuity and bar induction

The semantic model is the hierarchy of total continuous functionals: every object is total, and each observation of a higher-type output depends on a finite observation of its input. Put ${\hat{\alpha }}_n:=\mathsf{put}([\alpha ](n),\mathbf{0})$.

Proof of Lemma 67.15 — Spector's condition

Proof. Continuity at $\alpha$ gives a number $k$ such that streams agreeing with $\alpha$ below $k$ receive the same value. Choose . Then The witness depends on $\alpha$ and $\omega$; it is not a uniform recursion depth. ◻

This principle is SPEC in the primary comparison [EO14].

The totality proof assumes the following decidable form of bar induction. For predicates $D,Q$ on $X^{\ast }$, $$\begin{array}{}\text{(}{\mathrm{BI}}_{\mathrm{dec}}\text{)}& \frac{\begin{array}{c}\mathrm{\forall }\alpha \mathrm{\exists }n.D([\alpha ](n))\mathrm{\forall }s.(D(s)\vee \mathrm{\neg }D(s)),\\ \mathrm{\forall }s.(D(s)\to Q(s))\mathrm{\forall }s.((\mathrm{\forall }x.Q(s\ast x))\to Q(s))\end{array}}{Q([])}.\end{array}$$ The bar $D$ and inductive predicate $Q$ are distinct. Combining them would delete the premise that a stopping prefix has a total value. This decidable bar-induction boundary is explicit in the primary theorem map [Pow13].

Proof of Theorem 67.16 — Totality of restricted Spector recursion

Proof. Define Spector’s condition makes $D$ a bar, and comparison of natural numbers makes $D(s)$ decidable. If $D(s)$, the base equation returns $\mathsf{put}(s,\mathbf{0})$, so $Q(s)$.

For the inductive premise, fix $s$ and assume $Q(s\ast x)$ for every total $x:X$. The map $x\mapsto {\mathsf{SBR}}_{s\ast x}^{\omega }(\delta )$ is then a total continuation. Totality of ${\delta }_s$ gives a total selected value $c$, and the assumption at $s\ast c$ gives a total recursive result. Thus $Q(s)$ in the recursive branch; the base branch was handled above. The rule ${\mathrm{BI}}_{\mathrm{dec}}$ gives $Q([])$. Transport along the sourced reverse adapter gives the EPS claim. This proves semantic totality, not strong normalization of the bare equations. ◻

Spector’s equations and countable choice

Proof of Theorem 67.17 — Spector equations

Proof. Use $R^{\prime }=R\times \mathbb{N}$, $$q^{\prime }(\beta ):=(q(\beta ),\omega (\beta )),l:={\pi }_2,{\epsilon }_n^{\prime }(P):={\epsilon }_n(\lambda x.{\pi }_1(Px)).$$ Apply theorem 67.10 to $q^{\prime },l,{\epsilon }^{\prime }$, and write its continuation as $p_n^{\prime }:X\to R^{\prime }$. Define $p_n:={\pi }_1\circ p_n^{\prime }$. Since $l(q^{\prime }(\alpha ))=\omega (\alpha )$, the theorem applies at every $n\le \omega (\alpha )$. Projection of its two equations gives the required equations. The adjustment ${\epsilon }_n^{\prime }$ is necessary: the original selector expects an $R$-valued continuation, not an $R\times \mathbb{N}$-valued one. ◻

This is Corollary 3.9 [EO14].

Proof of Theorem 67.18 — Selected choice interpretation

Proof. Negative translation sends the classical derivation into the weakly extensional intuitionistic base. The functional-interpretation induction handles its logical rules, arithmetic equations, induction, and quantifier-free choice. The new DNS case requires a sequence $f$, counterexample continuations $p_n$, and the index $n=\omega (f)$. Theorem 67.17 gives $$f(n)={\epsilon }_n(p_n),p_n(f(n))=q(f),$$ which are exactly the two substitutions in the Dialectica matrix of DNS. The logical reduction at the end of section 67.1 then handles ${\mathsf{cAC}}_{\mathbb{N}}$. Theorem 67.16 gives totality of the new functional; all other extracted constants belong to System T. ◻

The exact imported metatheorem is Powell’s Theorem 4.4; its accompanying remark records that verification in the weakly extensional base requires the formalization cited there, rather than Spector’s extensional argument alone [Pow13]. Spector’s original Section 10 gives the restricted one-unknown construction. Sections 12.2 and 12.3 of the printed paper were completed by its editor, Georg Kreisel [Spe62].

Finite evidence from the pigeonhole extraction

The pinned Agda development proves, under a Friedman $A$-translation, that every Boolean stream has a constant infinite subsequence. Its finite specialization erases the proof component to the executable type $$\mathsf{Two}\times \mathsf{List}\mathbb{N}.$$ The archive has seven named streams $a1,\dots ,a7$ and six named executable examples. The Agda type of the first is the displayed product above. Its defining equation in the archived module is

example1 = pigeon-program a6 2

The request $2$ means that the returned list has length three. Its acceptance check requires three strictly increasing indices and verifies that all three entries of $a6$ at those indices equal the returned Boolean. The dependent theorem in FinitePigeon.agda proves this specification before PigeonProgram.agda erases the proof component. The archived sources are Agda from 2011; this edition records no fresh typecheck under an unavailable historical toolchain.

The selection-function, BBC, and modified-bar-recursion modules are alternative realizers of the shift principle. They do not prove equality with the restricted SBR interface fixed here. The project page also records that the three realizer modules disable Agda’s termination checker [Esc11].

The book-owned Kappa corpus in artifacts/ch67-bar-choice-replay/ implements the applied binary product, the three-stage calculation, and a fuel-bounded specialization of dependent EPS. The bound makes it a finite executable shadow, not an implementation of infinite bar recursion. Its strict and non-strict stopping variants return different four-entry traces, so the mutation checks the equation that the chapter uses.

Nearby recursors are not interchangeable

The implicitly controlled product has no explicit length test. Continuity of the outcome functional instead bounds the demanded recursive calls. In the primary comparison it realizes a J-shift by modified realizability, while the explicit product realizes DNS by Dialectica.

Modified bar recursion returns a different object and satisfies different equations. Its equivalence with an implicitly controlled product does not change theorem 67.18. Escardó and Oliva’s comparison separates the arrows that require ${\mathrm{BI}}_{\mathrm{rel}}$, SPEC, or continuity; one cannot erase those annotations when moving between recursors [EO14].

Finally, a finite run concerns one extracted term at one input. Semantic totality quantifies over all total inputs in the chosen continuous model. Neither observation proves the other.

Chapter seminar