ch:bar-recursion: finite controlled selection

Problem, calculus, and invariant. Implement the applied product of Boolean selection functions and a bounded instance of the dependent explicitly controlled product. At every recursive call, the prefix argument is exactly the choices already fixed, the zero completion has the remaining fuel length, and equality between control and depth takes the recursive branch. The concrete accepted results are $(1,0)$, $[1,0,1]$ with score five, strict trace $[1,0,1,0]$, and non-strict trace $[0,0,0,0]$.

Representation choice. Use one datatype with policies Maximize and Minimize. Use a second datatype with stopping rules Strict and NonStrict. This exposes the mutation and keeps continuations as ordinary Kappa functions. An alternative syntax tree for arbitrary selection functionals would support more policies, but its evaluator and value encoding would obscure the two equations tested here. Fuel makes the controlled recursion structurally total; the cost is that this program cannot express the semantic infinite product.

First end-to-end version. Define choose, then lift it to select : Policy -> (Nat -> Nat) -> Nat. Build binaryProduct by computing the right choice for each proposed left choice, offering the resulting outcome as the left continuation, and finally recomputing the right choice at the selected left point. On $2x+y$, maximizing left and minimizing right returns $(1,0)$. This case already exercises the defining dependency of $\epsilon \otimes \delta$.

Finite product stage. Define the tail as the binary product of the minimizing second selector and maximizing third selector. Offer its score to the maximizing first selector. The result is $[1,0,1]$, and scoreStream computes five. For the exercise extension use $$q_4(x_0,x_1,x_2,x_3)=8x_0+4x_1+2x_2+x_3$$ with policies maximize, minimize, maximize, minimize. Backward calculation predicts $[1,0,1,0]$ and score ten; add exactly that oracle before running.

Controlled stage. Implement list append, length, zero completion, and lookup-with-zero. In epsBounded, compute the control on the zero completion. Stop only when control < depth; otherwise recursively calculate both candidate tails, offer their complete scores to the selector at this depth, and retain the selected head and tail. Fuel four on the empty prefix returns $[1,0,1,0]$. The explicit fuel proves termination of this Kappa function, not of SBR.

Incorrect version. Change only the strict branch to control < depth || control == depth. At the equality boundary the mutant returns zeros instead of consulting the selector. The unchanged strict oracle fails; the separately named non-strict branch records the changed trace $[0,0,0,0]$.

Acceptance test. Run the four commands in appendix E. Require a silent check, one passing inline test, the exact five-line transcript, and audit result []. After adding the fourth selector, require $[1,0,1,0]$ and score ten. Restore the accepted source after replaying the mutation and rerun all four commands.

Agda inspection. Open the pinned module Examples.agda. Locate the equation containing pigeon-program, applied to a6 and 2. Any normalized pair must have a list of exactly three strictly increasing indices, and every a6 entry at those indices must equal the returned Boolean. The dependent theorem carries that specification. The module PigeonProgram.agda erases it. Do not report a fresh Agda run unless a compatible toolchain actually checks and normalizes the archived project.

Mathematical boundary. The program illustrates the binary product equations and the strict control boundary. It does not prove finite DNS, Spector’s equations, BI, or the semantic totality theorem. Those claims are the mathematical results of the chapter, not consequences of four finite oracles.