Logic&Semantics

## Adding subtypes to a computational category to make it mathematical

By Paul Taylor (Queen Mary, University of London)

The existence or otherwise of extensional subtypes seems to be a point of demarcation between pure mathematics and programming: the axiom of comprehension is a prominent feature of mathematical constructions, but neither programming languages nor the type theories that are most popular in computer science admit subtypes. (I do NOT mean the notion of this name in object-oriented programming, which is like an extension of the signature of an algebraic theory.) The nearest analogous notion is Floyd--Hoare logic, with pre- and post-conditions, but it is an up-hill struggle to get programmers to use this!

The basic idea of Abstract Stone Duality was to replace the infinitary lattice theory behind general topology with a category of "frames" that's monadic over "spaces" instead of sets, "frames" also being dual to "spaces". The import of the monadic property turns out to be that it provides subtypes - with the subspace topology.

The underlying categorical construction (without subtypes) is the same as that used by Thielecke to model continuations, and makes the spaces "sober"; it is also equivalent to Russell's theory of descriptions, and to general recursion. Formal subspaces can be added to this construction to achieve the monadic property.

There is an equivalent lambda calculus, which is similar to a type-theoretic presentation of Zermelo's original set theory. This calculus has a normalisation theorem, in which the subtype data is erased. Hence the construction is computationally anodyne: lambda-terms typed using the subspaces may simply be regarded as belonging to the ambient types, and validly reduced as such.

I will conclude with some speculations about a comprehension calculus in which open subsets are classified by Sigma and general subspaces by a new object Pi. Reasoning in the Sigma logic would prove partial correctness, whilst the Pi logic is about termination.