Ordinals and Interactive Programs

Abstract

The work reported in this thesis arises from the old idea, going back to the origins of constructive logic, that a proof is fundamentally a kind of program.

If proofs can be considered as programs, then one might expect that proof theory should have much to contribute to the theory of programming. This has indeed turned out to be the case. Various technologies developed in proof theory are now widely used in computer science for formulating and investigating programming languages and logics connected with them.

Yet there is a vigorous and venerable part of proof theory which has so far had little impact in computer science, namely ordinal-theoretic proof theory. This focuses on proofs of wellfoundedness, usually expressed in the form of a schema of transfinite induction with respect to a representation of an initial segment of the countable ordinals. Proof theory of this kind is connected with what it is that limits the capacity of a proof system to 'see into the transfinite.

If proofs can be considered as programs, what kind of program is a proof of wellfoundedness? My hypothesis is that the limitations of a formal system for writing proofs of wellfoundedness reflect its limitations as a system in which to program strategies for defeating ones opponent in a certain kind of game. In recent computer science, games have proved invaluable as models for describing patterns of interaction between a system and its environment.

I cannot claim to have substantiated this hypothesis, but only to have taken a few steps in that direction. The work reported in the thesis lies in three areas.

First, I present a framework for dependently typed programming in the style advocated by Martin-Löf. The novelties here are connected with bringing the type-theoretic approach to programming that comes from the Curry-Howard correspondence closer to the calculational approach in the categorical tradition that comes from Lambek and Lawvere. A particular challenge is to find a smooth and practical way of encoding inductive and coinductive definitions.

Second, I have investigated a number of ways of modeling interactive systems and transition systems in a constructive context. The focus here is on models with a direct computational interpretation, that can actually be used in programming. The approach is inspired by a construction due to Petersson and Synek. It is shown how one may represent game-theoretic strategies of various kinds using these models.

Finally, I give a construction of provable ordinals within a Martin-Löf style type theory that has a type of natural numbers, and an external sequence of universes closed under generalised Cartesian products. The locus of the ideas for this construction lie more in conventional proof theory, and were the basis for a conjecture made by me almost thirty years ago in work that I then abandoned. What is new here is the concept of a 'lens'. This is a predicate transformer that has been implicit in the construction of proofs of wellfoundedness since Gentzen. I hope this concept may be of some use in an algebraic, systematic approach to setting lower bounds on the proof-theoretic strength of more extensive type theories.