Publications and other writings


My thesis probably counts as a publication. It is called "Ordinals and Interactive Programs" and can be found here. Please bear in mind that no-one in his right mind would read (or write) a Phd thesis. (As I was told once by a Fellow of the Royal Society.)


Here are some writings about topics that interest me. I greatly appreciate comments from anyone with overlapping interests.

I wrote (2002) with Pierre Hyvernat a draft of something that I hope will converges to a citable paper on interaction structures and related matters (formal topology a la Sambin, refinement calculus, notions of "component"). Here is the draft: PS PDF.

In essence, the subject is a category of interfaces and components. Here are some more recent notes: ps pdf. The whole thing needs to be (yet again) rewritten from scratch.

Hyvernat has shown that this category is a model of linear logic.

What I like about this work is that it is riddled with conceptual questions: "what is a program?", "what does it mean to run a program?", "what does it mean that a program works?", "what is an infinite object?" and so on. It is not only a mathematical topic.

Short note on continuity of stream processing functions
A simpler notion of component is that of a filter: a function over streams. Streams have a natural topology, and one can ask which filters are continuous. The following note concerns the representation of continuous filters. Basic idea. Haskell code.
Short note on number classes
A small thought about how to express uniformly the step from one number class to the next. This cleared up a question that had bothered me for several years. The trick is to lift the operation, from functors to functors.
IO and dependent types
My main interest is in prospects for exploiting dependent types to specify interactive behaviour, particulary command-response interfaces (such as for network services). The idea is that one ought to be able to specify not only syntactical features, but the full "semantics" of a the commands in an interface by exploiting type dependency. This might lead to an application for dependent types in the specification of imperative interfaces. There are many things here to clarify and substantiate.

For some years I have discussed this interest with Anton Setzer. Among other material accessible on his page are some slides he presented at the Workshop on Dependent Types in Programming, Gothenburg 27-28 March 1999) arising from these discussions.

Earlier thoughts about the subject are in the rough notes Data dependent types and input output and in the half written (not even draft) article: Interactive Programs in Type Theory.

State machines
Notes on Mealey and Moore state machines and related notions. The main idea here is that the two kinds of machine are coalgebras for dual functors. There is a natural generalisation of both notions of machine to dependent types. There's some Haskell code that goes with this, also typeset (dvi). The following rather old page on Interactive systems leads to pages on related topics.

In 2000 I completed a machine checked proof of half of something that was long ago known by a few people as Hancock's Conjecture. Most of the proof was made in collaboration with Anton Setzer some years before.

The subject is exotic, at any rate at first sight. It is concerned with proofs of accessibility for expressions in a notation system for countable ordinals, and the extent to which the proofs can be constructed in a particular formal system. Accessibility is a notion that can be defined wherever there is a predecessor structure on a set of `notations', assigning to each notation a countably indexed family of its predecessors. A notation is accessible if it satisfies every progressive predicate, where a progressive predicate is one that contains those notations all of whose predecessors have the property. Intuitively, the notation is "built up from below".

In the case of notations for countable ordinals, the predecessor structure is defined by classifying notations into those that are zero (having no predecessors), those that are successors (having a single predecessor), and those that are limits (having a countable sequence of predecessors). An ordinal notation can be thought of as a kind of `counting-down' process, which

Accessibility means that the counting down eventually stops, however the successive numbers are chosen at limits. A proof of acessibility of an ordinal notation in essence contains the predecessor structure of the ordinal it denotes; it is one measure of the proof-theoretic strength of a formal system that it can be used to write proofs of accessibility for expressions in a certain notation system, but cannot prove the accessibility of further term denoting the limit of those expressions. The concept of accessibility is related to the concept of continuity of interactive programs.

In the case of Hancock's Conjecture the formal system was an early version of Martin-Löf's type theory. The principles it provides are firstly primitive recursion on the natural numbers, and secondly an external sequence of "universe" types (ie. types of types) closed under vanilla logical operations. The transfinite arithmetic involved is that of the predecessors of a certain venerable transfinite ordinal known as Gamma0. The first to identify it, if not to name it, was probably the mathematician Veblen about 100 years ago, but the first to shed light on its importance were the logicians Sol Feferman and Kurt Schutte. They established a connection between this ordinal and a concept arising in the foundations of mathematics called "predicativity", meaning roughly "circularity-free", or accessibility in the sub-formula relation. Roughly speaking Gamma0 measures the strength of systems which are predicative relative to one finitary inductive definition (like that of the natural numbers); nowadays people who are familiar with the subject think that in general predicativity is much more liberal with respect to inductive definitions.

If the proof has any interest, it is only that it provides an example of the essential use of universes in a program; there are not so many of these. Each successive universe is used to add another `layer' of the Veblen-Schutte-Feferman notation system. I tried to write an `algebraic' proof, structuring it around the idea of a certain kind of non-monotone predicate transformer which I call a lens. There is a certain inverse limit construction on sequences of lenses that may have some further interest.

The following tar file contains a variety of machine-checked files including one called ordlens.agda in which the result alluded to above is called Corollary. The files contain a great deal of detritus, are very sketchily commented, and their general organisation is chaotic. There is however no lower bound to human depravity, and there may be people who wish to pick at the entrails of this carrion. Here are the sources, if you want a look.

There is a lightning sketch of agda here. As a simple example, here is a proof of accessibility of notations up to epsilon0 that does not use anything beyond Heyting arithmetic.

The construction makes use of a notion of a "lens for a function". Here are some slides on lenses.

Inspired by from some ideas of Ulrich Berger, I sometimes think about extracting the computational content (ie. some functionals of transfinite type) from these proofs of accessibility, perhaps in the form of a realisability interpretation.

The lambda calculus, and other side-splitting jokes.


Peter Hancock
Last modified: Fri May 18 22:11:31 BST 2003