Foundations of Programming Meetings 2000
School of Computer Science and ITUniversity of Nottingham
Program schemes are computational devices which accept classes of
finite structures (as opposed to sets of strings). Whilst resembling
high-level programs, they remain amenable to logical analysis. In this
talk, I shall introduce classes of program schemes and show how the classes
of problems accepted by these program schemes are none other than the
classes of problems defined by the sentences of certain (generalized
quantifier) logics. I shall explain how we can use these program schemes to
prove strict logical hierarchy results without employing
Ehrenfeucht-Fraisse games. Whilst the problems accepted by program schemes
augmented with a stack can be defined within bounded-variable infinitary
logic, there are problems accepted by program schemes with arrays which can
not be so defined. However, the class of problems accepted by program
schemes with arrays still has a zero-one law. Finally, I shall relate open
problems involving program schemes with open problems from complexity theory.
We give a fresh look at the typed region calculus
of Tofte and Talpin using an encoding in a
typed pi-calculus equipped with groups.
In a functional programming language with regions,
memory allocations are made on statically determined
storage regions. Regions are allocated
and de-allocated according to a stack discipline,
thus improving memory management.
The idea of groups arose in the typed ambient calculus
of Cardelli, Ghelli, and Gordon. There,
and in our pi-calculus, each name has a statically
determined group to which it belongs. Groups allow
for type-checking of certain mobility
properties, as well as effect analyses.
Our encoding makes precise the intuitive correspondence
between regions and groups. We propose a new
formulation of the type preservation property of the
region calculus, and we prove the correctness of
region de-allocation using a new
garbage collection equation for our pi-calculus.
In the world of functional programming, many accumulating parameter
optimisations can be derived using a theorem known as fusion. In my
talk I will show how this theorem can be applied mechanically, thus
helping functional programmers write efficient programs.
It has been remarked that Z is a specification language without an associated
program development methodolgy. Although some attempts have been made to this
end, their semantic basis locks into a model which is rather inappropriate for
the most important and powerful aspect of Z: the schema calculus.
I will describe some experiments in formalising notions of operation refinement
in Z which are more sympathetic, and look at two rather trivial though
illustrative examples of program development. Along the way I hope to
demonstrate that having a Z logic (recent work with Steve Reeves, University of
Waikato, New Zealand) is a major benefit.
Nested datatypes are recursively defined parameterised datatypes in which the
parameter of the datatype changes in the recursive call.
The standard semantic definition of recursively defined datatypes is as
initial algebras in the category Set of sets and total
functions. It has been shown that this theory is inadequate
to describe nested datatypes. Instead, one proposed solution is to
define them as initial algebras in the functor category
Nat(Set), with objects all endofunctors on
Set and arrows all natural transformations between them.
We will show that the initial algebras of nested datatypes
are not guaranteed to exist in the functor category itself, but that they
do exist in one of its subcategories: the category of all
cocontinuous endofunctors and natural transformations. This category is
then a suitable semantic domain for both first order and higher order
nested datatypes.
Regular datatypes are inductive types generated by polynomial type
functors closed under least fixed point. As such, the data they
contain are tree-like. Given any such type, a useful auxiliary
structure) is the associated notion of `linear context' or `tree
with one subtree deleted' or `tree with a hole' or whatever you want
to call it. Unlike Theseus's piece of string, these record not
only the path we take from root to hole (or vice versa), but also
all the subtrees we pass by on the way, so that we have the entire
context surrounding the hole.
One sunny afternoon, I was waiting for a connection at Shrewsbury and
wondering how to construct an appropriate type of linear contexts for
an arbitrary regular datatype. I was suddenly overwhelmed by
deja-vu. I shall describe this construction informally, and then I
shall show how to implement it in a dependently typed language, where
the `names' of regular types are just data and the inhabitants of
regular types are values in a type family indexed by names.
I will represent a translation of first-order function spaces in
isomorphic coinductive types. The motivation of this construction is
to explain function types algebraically. However, there are also
practical applications as the recent work of Ralf Hinze on memo
functions (generalized tries) shows. Another interesting aspect of
this construction is that the use of nested datatypes is essential to
translate function spaces over non-linear types.
I shall sketch how to verify the correctness of the construction using
limits and local colimits.
Recent work by Bird, Hinze, Meertens, Okasaki and Paterson
(among others) has stimulated interest in the theory and application of
nested datatypes. An unresolved issue is what the theoretical
limitations of nested datatypes are. Can nested datatypes be used to
define, for example the set of all lists of prime length? This talk
will demonstrate how nested datatypes can be systematically constructed
by programming in the lambda calculus at type level (rather than at
value level). I will argue that nested datatypes are in principle
unlimited provided that one has the full power of Church's lambda
calculus at the type level. Unfortunately this appears not to be the
case; the problems encountered with the approach will be discussed.
(In collaboration with Kevin Backhouse and members of the Oxford AoP group.)