Papers

This page contains various papers I've written. Some are published, some are unpublished. There are PDFPDF, PostScriptPostScript (gzipped) and .dviTeX.dvi formats.

Use the directory listing if you wish.


Higher order β matching is undecidable. PDF PostScript .dvi

Shows that the solvability of higher order matching equations, up to β equivalence, is not decidable. This problem was posed by Gerard Huet in the 1970's.

2001–2002. Appeared in the Logic Journal of the IGPL, volume 11, issue 1 , pages 51–68 . This article is in the public domain. No permission is needed for copying or other use.


The Undecidability of λ-definability. PDF PostScript .dvi

Shows that that definability by terms of the simply typed lambda calculus, is undecidable. This problem was occasionally (if not entirely accurately) known as the Plotkin-Statman conjecture, in honour of the two people who did the seminal work on models of the calculus.

C. Anthony Anderson and M. Zeleny (eds.), Logic, Meaning and Computation: Essays in memory of Alonzo Church , 331-342, Kluwer 2001. Actually written in 1993 — the volume took ages to appear.


Finitary PCF is not decidable. PDF PostScript .dvi

Achim Jung and Allen Stoughton asked if the observational ordering of finitary PCF is decidable. We show that it isn't.

A pocket calculator computes with certain values — numbers — and we have a pretty good idea what they are.

Higher-order functional languages also compute with certain values, but it's far less obvious what those values actually are. This paper shows that there is no computable presentation of those values for PCF, even after restricting attention to the "finite" ones.

In some sense, this shows that there is a limit to how far we can improve our ability to reason about programing languages by simplifying them, and that the purest functional languages go beyond that limit.

Theoretical Computer Science , Volume 266, Issues 1-2, 6 September 2001, Pages 341-364.


Unary PCF is decidable. PDF PostScript .dvi

We show that unary PCF, a very small fragment of Plotkin's PCF, has a decidable observational pre-order, and that its fully abstract model is effectively presentable. This is in marked contrast to larger fragments, where corresponding results fail. The techniques used are adaptations of those of Padovani, who applied them to the minimal model of the simply typed lambda calculus.

Manfred Schmitt-Schauss later gave a proof that is much simpler and easier to understand.

Theoretical Computer Science , Volume 206, Issues 1-2, 6 October 1998, Pages 317-329.


An Algorithm for the Minimal Model. PDF PostScript .dvi

Vincent Padovani gave an algorithm that calculates the structure of the minimal model of the simply typed lambda calculus. That proof is, ummm, non-trivial. This is a far simpler one. It's based on techniques of Manfred Schmidt-Schauss.

Written in 1995 or so. Never bothered submitting it for publication.


Normalisation by Translation. PDF PostScript .dvi

I outline a new proof of strong normalisation for system F, by direct calculation of the size of a normalisation tree. The system F itself is used as a formulism for representing these calculations, and any reasonably sensible model of the calculus can be used to verify that the correctness of the calculations. The method works for a variety of calculi, and seems reasonably general.

It's more-or-less a generalisation of a paper of Robin Gandy.

Written in 1995 and never published.


Equational Theories for Inductive Types. PDF PostScript .dvi

The paper investigates a recursive-function model of a lambda calculus with inductive types. We show that the equations valid in the model have a natural syntactical characterisation — it's the maximal consistent equational theory.

This is shown by giving a generalisation of the Kreisel-Lacombe-Shoenfield theorem.

Annals of Pure and Applied Logic , Volume 84, Issue 2, 21 March 1997, Pages 175-217


Elementary Proofs of Adequacy. PDF PostScript .dvi

We give a technique for proving computational adequacy, and apply it to models of Plotkin's FPC. "Elementary" is a technical term, by the way, indicating that the proof keeps it's feet firmly on the ground — specifically, it only needs first order reasoning. Don't be fooled into thinking that it's going to be easy to read.

Finally, finally, finally, got referee's reports on this in early 2003. I've got quite extensive changes to make (in particular, I'd like to sort out the proof of determinacy properly). But it should be published sooner or later. Thankfully, the WWW makes the actual publication pretty much irrelevant. Written in 1997.


Linear Logic, Totality and Full Completeness. PDF PostScript .dvi

Presents a model of Linear Logic based on a notion of total computation, and proves a full completeness result. Audrey Tan, and Martin Hyland and Andreas Schalk later did a better job of this...

Appeared in the proceedings of the Ninth Annual Symposium on Logic in Computer Science , IEEE press, 1994.


Notes on Simply Typed Lambda Calculus. PDF PostScript .dvi

These are notes from a course I taught in Edinburgh in early 1998. They were published as a technical report ECS-LFCS-98-381. The version here has some corrections made after the technical report.


Notes on Linear Logic. PDF PostScript .dvi

These are notes from a course I taught at the Computing Laboratory in Oxford in early 1996.


On observing β-equivalence. PDF PostScript .dvi

A quick note on observing β-equivalence in the simply typed λ calculus. The observable is whether or not the normal form is a λ abstraction, and in the standard manner we define an observational equivalence from this. I show that quotient, although finite at each type, is not effectively presentable, using an encoding of β-matching.

The observational equivalence is probably also undecidable, but I don't know how to prove that. Quick and dirty hack, written June 2003.


:-)