A framework for Hyland–Ong innocent strategies. Types are arenas, terms are strategies. Games model program behaviour, and they are also an interface: you design a term by playing Proponent, constrained by the P-view.
B → B
Copycat on B → B. Opponent asks on the result (right) copy; Proponent mirrors the question into the argument (left) copy, waits for an answer, and copies it back. The constant-true strategy never inspects its argument.
copycatconst-truebot
B → B → B
Four sequential disjunctions on B → B → B. Left-or (lor) queries the first argument first and can return true without looking at the second; right-or is the symmetric sequential strategy. Parallel-or is not among them: no innocent strategy can return true when either argument is true and the other diverges.
lorrorlrorrlorbot
B → B → B → B
Sequential conditional of type B → B → B → B. The canonical strategy queries the condition and then exactly one of the two branches. The unused branch is never interrogated — that is definable, unlike por.
iteconst-thenbot
((B → B) → B) → B
Proponent is a term of type ((B → B) → B) → B: it receives an oracle f and queries it by supplying an argument strategy (identity, negation, or constant true). Each interrogation of that argument is a separate P-view; innocence forbids a hidden call counter.
ask-idask-notask-const-truebot
(N → B) → B
Search a predicate N → B for a witness. exists-true queries 0,1,2,… until the predicate returns tt. When Opponent backtracks to an earlier query, innocence forces Proponent to replay the same Nat; there is no mutable search index.
exists-trueexists-from-2never-lookbot
(B → B) → B → B
The evaluation map of type (B → B) → B → B. eval queries the function with a copy of the value argument and copies the function's answer to the result. ignore-fun skips the function and copies the value.
evalignore-funbot
The game of tic-tac-toe as an arena: Opponent starts, Proponent plays X. Occupancy and terminal positions are arena legality, so every strategy is automatically a legal playing policy. Perfect play is minimax; it never loses.
perfectcenter-firstnaivebot
Single-heap Nim from 5 stones, last take wins. The winning strategy leaves a multiple of four; greedy always takes three (or the rest); take-one is the slowest legal policy.
winninggreedytake-onebot