In previous work on higher-order games, we accounted for finite games of unbounded length by working with continuous outcome functions, which carry implicit game trees. In this work we make such trees explicit. We use concepts from dependent type theory to capture history-dependent games, where the set of available moves at a given position in the game depends on the moves played up to that point. In particular, games are modelled by a W-type, which is essentially the same type used by Aczel to model constructive Zermelo-Frankel set theory (CZF). We have also implemented all our definitions, constructions, results and proofs in the dependently-typed programming language Agda, which, in particular, allows us to run concrete examples of computations of optimal strategies, that is, strategies in subgame perfect equillibrium.

Abstract We present an effective proof (with explicit bounds) of the Podelski and Rybalchenko Termination Theorem. The sub-recursive bounds we obtain make use of bar recursion, in the form of the product of selection functions, as this is used to interpret the Weak Ramsey Theorem for pairs. The construction can be seen as calculating a modulus of well-foundedness for a given program given moduli of well-foundedness for the disjunctively well-founded finite set of covering relations. When the input moduli are in system T , this modulus is also definable in system T by a result of Schwichtenberg on bar recursion.

Abstract In [12], Schwichtenberg showed that the System T definable functionals are closed under a rule-like version Spector’s bar recursion of lowest type levels 0 and 1. More precisely, if the functional Y which controls the stopping condition of Spector’s bar recursor is T-definable, then the corresponding bar recursion of type levels 0 and 1 is already T-definable. Schwichtenberg’s original proof, however, relies on a detour through Tait’s infinitary terms and the correspondence between ordinal recursion for $\alpha < {\varepsilon _0}$ and primitive recursion over finite types. This detour makes it hard to calculate on given concrete system T input, what the corresponding system T output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into T-definitions under the conditions of Schwichtenberg’s theorem. Finally, with the explicit construction we can also easily state a sharper result: if Y is in the fragment Ti then terms built from $BR^{\mathbb{N},\sigma } $ for this particular Y are definable in the fragment ${T_{i + {\rm{max}}\left\{ {1,{\rm{level}}\left( \sigma \right)} \right\} + 2}}$ .

Abstract This paper considers a generalisation of selection functions over an arbitrary strong monad T, as functionals of type $J_R^T X = (X \to R) \to TX$ . It is assumed throughout that R is a T-algebra. We show that $J_R^T$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$ . We use this to derive that the explicitly controlled product of T-selection functions is definable from the explicitly controlled product of quantifiers, and hence from Spector’s bar recursion. We then prove several properties of this product in the special case when T is the finite powerset monad ${\cal P}_{\rm{f}} \left( \cdot \right)$ . These are used to show that when $TX = {\cal P}_{\rm{f}} \left( X \right)$ the explicitly controlled product of T-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift.

Abstract We show how two iterated products of selection functions can both be used in conjunction with systemTto interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over systemTto Spector’s bar recursion, whereas the other isT-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of ‘skewed’ selection functions. Iterations of the dependent binary products are also considered but in all cases are shown to beT-equivalent to the iteration of the simple products.

We use Gödel's dialectica interpretation to produce a computational version of the well-known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics.

Abstract We consider reasoning about linear systems expressed as block diagrams that give a graphical representation of a system of differential equations or recurrence equations. We use the notion of additive relation borrowed from homological algebra to give a convenient framework in which all diagrams have a semantic value. We give a sound system of Hoare-style rules for the block diagram constructors that singles out a tractable subset of the block diagram language in which all diagrams represent total functions. We show these rules in action on some simple examples from a variety of applications domains.

This article shows how different functional interpretations can be combined into whatweterm hybrid functional interpretations. These hybrid interpretations work on the setting of a multi-modal linear logic. Functional interpretations of intuitionistic logic can be combined via Girard’s embedding of intuitionistic logic into linear logic. We first show how to combine the usual Kreisel’s modified realizability, Gödel’s Dialectica interpretation and the Diller–Nahm interpretation into a basic hybrid interpretation.We then prove a monotone soundness theorem for the basic hybrid interpretation, in the style of Kohlenbach’s monotone interpretations. Finally, we present a hybrid bounded functional interpretation that, except for the additives, corresponds to a combination of the recently developed bounded functional interpretation and bounded modified realizability.

Bar recursion arises in constructive mathematics, logic, proof theory and higher-type computability theory. We explain bar recursion in terms of sequential games, and show how it can be naturally understood as a generalisation of the principle of backward induction that arises in game theory. In summary, bar recursion calculates optimal plays and optimal strategies, which, for particular games of interest, amount to equilibria. We consider finite games and continuous countably infinite games, and relate the two. The above development is followed by a conceptual explanation of how the finite version of the main form of bar recursion considered here arises from a strong monad of selections functions that can be defined in any cartesian closed category. Finite bar recursion turns out to be a well-known morphism available in any strong monad, specialised to the selection monad.

This article presents an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. Our abstraction is based on a traced monoidal functor from an arbitrary traced monoidal category into the category of preorders and monotone relations. We give several examples of how our theory generalizes usual Hoare logics (partial correctness of while programs, partial correctness of pointer programs), and provide some case studies on how it can be used to develop new Hoare logics (runtime analysis of while programs and stream circuits).

This paper presents a modified realizability interpretation of classical linear logic. The interpretation is based on work of de Paiva (1989), Blass (1995), and Shirahata (2006) on categorical models of classical linear logic using Gödel's Dialectica interpretation. Whereas the Dialectica categories provide models of linear logic, our interpretation is presented as an endo-interpretation of proofs, which does not leave the realm of classical linear logic. The advantage is that we obtain stronger versions of the disjunction and existence properties, and new conservation results for certain choice principles. Of particular interest is the simple branching quantifier used in order to obtain a completeness result for the modified realizability interpretation.

This paper studies modified bar recursion, a higher type recursion scheme, which has been used in Berardi et al. (1998) and Berger and Oliva (2005) for a realisability interpretation of classical analysis. A complete clarification of its relation to Spector's and Kohlenbach's bar recursion, the fan functional, Gandy's functional and Kleene's notion of S1–S9 computability is given.

We present a constructive procedure for extracting polynomial-time realizers from ineffective proofs of /spl Pi//sub 2//sup 0/-theorems in feasible analysis. By ineffective proof we mean a proof which involves the noncomputational principle weak Konig's lemma WKL, and by feasible analysis we mean Cook and Urquhart's system CPV/sup /spl omega// plus quantifier-free choice QF-AC. We shall also discuss the relation between the system CPV/sup /spl omega// + QF-AC and Ferreira's base theory for feasible analysis BTFA, for which /spl Pi//sub 2//sup 0/-conservation of WKL has been non-constructively proven. This paper treats the case of weak Konig's lemma, we indicate how to formalize the proof of the Heine/Borel covering lemma in this system. The main techniques used in the paper are Godel's functional interpretation and a novel form of binary bar recursion.