Publications and other writings

Publications

Anton Setzer, Peter Hancock: Interactive Programs in Dependent Type Theory. In: P. Clote, H. Schwichtenberg: Computer Science Logic. 14th international workshop, CSL 2000. Springer Lecture Notes in Computer Science, Vol. 1862, pp. 317 - 331, 2000.
(On the question whether data dependency in a type system has avantages for specifying and designing interactive programs.)
Preprint version: (postscript) Interactive programs in dependent type theory. U.U.D.M. Report 2000:5, ISSN 1101-3591, Dept. of Mathematics, Uppsala University, February 2000.
Chapters 8 (Polymorphic type checking) and 9 (A type checker) in The Implementation of Functional Programming Languages, Simon L. Peyton Jones, Prentice-Hall, 1987.

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.)

Unpublications

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

Interfaces

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.

Wellfoundedness

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

stops when the notation is zero
emits a `beep' when the notation is a successor and replaces it by its predecessors
when the notation is a limit, reads a natural number n from its environment and replaces the notation by the limit's nth predecessor.

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.

How to bind a variable . The question was once posed by Plotkin of finding a category and an endofunctor on it having an initial algebra in which one can recognise the expressions of the type-free lambda calculus. Among other things, it should be possible to define (all interesting forms of) substitution using only the initiality of the algebra. Here is my (positive) answer. At roughly this time (199-something), several people independently re-discovered essentially the same thing.
AMEN, the last word in combinators. Functional completeness of the arithmetical machine code: Add, Mul, Exp and Nop. This is sheer entertainment. There is also some code here (slightly type-set here) for looking at AMEN reduction sequences. Here are some slides. How to add . Yet another attempt to be amusing about AMEN. Apparently the analogy between logarithms and linear abstraction was known to Boehm.

Misc

Conway games. I wish I had time to seriously learn something about this. I've recently added a link to a Haskell implementation.
A very simple (but still open) problem of Skolem's
what does it mean to write down an ordinal? . Some Haskell code defining a data type of ordinal notations up to Gamma0.
Ordinals as families, Ordinals and programs Notes about an idea of Peter Dybjer's, that there are close parallels between ordinals defined by closure properties, and universes in dependent type theory.
Applied mathematics and models.
Models of discrete behaviour.
discreteness of time. A note on an axiom of "discreteness" in temporal logic. I am fascinated that this seems to be connected with inductive definition.
What are types (for)?
Transaction processing is about atomicity of actions. These are some remarks on what I find interesting about the subject: link.
Operator notation. An idea about nestable operator grammars.

Peter Hancock