Minutes of Meetings of the Algebra of Programming Research Group in 1995

The schedule for Michaelmas Term 1995 was as follows:

Week 1: 13 Oct, Carroll Morgan, University of Oxford

Probabilistic weakest preconditions and the "0-1" law for termination.

Week 2: 20 Oct, Annabelle McIver, University of Oxford

Temporal logic for probabilistic programs.

Week 3: 27 Oct, David Skillicorn, University of Oxford

Accumulations in Trees and Graphs.

Week 4: 3 Nov, Luc Duponcheel, University of Utrecht

Modular programming with catamorphisms, retracts, and monad transformers.

Week 5: 10 Nov, Stephen Jarvis, University of Oxford

Profiling large-scale lazy functional programs.

Week 6: 17 Nov, Jonathan Hill, University of Oxford

Program transformations for vectorising imperative functional programs.

Week 7: 24 Nov, Graham Hutton, University of Nottingham

Monadic parsing combinators.

Week 8: 1 Dec, Peter Freyd, University of Pennsylvania

To be announced.

Week 1: 13 Oct, Carroll Morgan, University of Oxford

Probabilistic weakest preconditions and the "0-1" law for termination.

Probabilistic predicate transformers generalise the usual ones by allowing the predicates, seen as characteristic functions from the state space to {0,1}, to take values in the entire interval [0,1].

I'll explain briefly how that works (without very much justification), and then present the probabilistic version of the usual rule for loop correctness, in which partial correctness and termination can be treated separately.

A surprising result of the loop rule is this "0-1" law (known at least since 1983, but not as easiy proved then): that for fixed set S of states, and fixed p>0, if for all s in S a process starting at s has probability at least p of leaving S -eventually-, then from all s it is in fact certain to leave S eventually (with probability 1).

I'll use that to justify a "probabilistic variant" rule for termination, argue that it's complete over finite state spaces, and then show how it is used to prove the correctness of Herman's Self-stabilising Ring Protocol in a simpler way than he did.

Week 2: 20 Oct, Annabelle McIver, University of Oxford

Temporal logic for probabilistic programs.

Temporal logic, when used to reason about programs, is most often based on a model of execution trees. We formulate the temporal operators ("always", "eventually" and "until") in the probabilistic weakest precondition semantics and use them to reason about a probabilistic algorithm that makes a set of users (processes, diplomats, .......) come to a unanimous decision. Provided they follow the protocol and are prepared to flip coins.

Week 3: 27 Oct, David Skillicorn, University of Oxford

Accumulations in Trees and Graphs.

Accumulations are interesting operations in structures that have a `direction' because they often provide computational shortcuts. I will review what's known about accumulations on trees, illustrating with a search problem, and then talk about graphs, give the only example of an accumulation that I know, and ask you to think of others.

Week 4: 3 Nov, Luc Duponcheel, University of Utrecht

Modular programming with catamorphisms, retracts, and monad transformers.

When writing functional interpreters, there are two things which need to be taken care of when having having modularity in mind: syntax and semantics. In~\cite{bib:LiangHudakJones} the authors present methods for dealing with semantics by making use of subtypes and monad transformers. In this talk we present a method for dealing with syntax by making use of catamorphisms. The usefulness of catamorphisms for functional programming is described in the, so called, banana papers~\cite{bib:Banana1} and~\cite{bib:Banana2}. The Gofer classes for catamorphisms can be combined with the Gofer classes for subtypes and monad transformers, resulting in library code using which one can write interpreters which are composed of reusable components.

Week 5: 10 Nov, Stephen Jarvis, University of Oxford

Profiling large-scale lazy functional programs.

The LOLITA natural language processing system is an example of one of the ever increasing number of large scale systems written entirely in a functional programming language. The system consists of over 40,000 lines of Haskell code (excluding comments) and is able to perform a number of tasks such as semantic and pragmatic analysis of text, context scanning and query analysis. Such a system is only useful if the results are calculated in real-time, therefore the efficiency of such a system is paramount.

While studying the efficiency of the LOLITA system a new profiling tool has been developed. Based on Sansom's Cost Centre profiler, part of the Glasgow Haskell Compiler, the new profiler uses a system of Post-Processing. This allows results which have previously been collected from a program to be analyzed by the programmer after execution, no further compilation is needed, thus greatly reducing the analysis time.

The seminar is based on the development of this new profiler. It considers the theory behind the new system and of course whether it actually works in practice!

Week 6: 17 Nov, Jonathan Hill, University of Oxford

Program transformations for vectorising imperative functional programs.

Traditionally a vectorising compiler matches the iterative constructs of a program against a set of predefined templates. If a loop contains no dependency cycles then a \emph{map} template can be used; other simple dependencies can often be expressed in terms of \emph{fold} or \emph{scan} templates. This talk will address the template matching problem within the context of functional programming. A small collection of program identities are used to specify vectorisable for-loops. By incorporating these program identities within a monad, \emph{all\/} well-typed for-loops in which the body of the loop is expressed using the \emph{vectorisation monad} can be vectorised. This technique enables the elimination of template matching from a vectorising compiler, and the proof of the safety of vectorisation can be performed by a type inference mechanism.

Week 7: 24 Nov, Graham Hutton, University of Nottingham

Monadic parsing combinators.

In functional programming, a popular approach to building recursive descent parsers is to model parsers as functions, and define higher-order functions (or combinators) that implement grammar constructions such as sequencing, alternation, and repetition. Such parsers are well-known to form a monad, an algebraic structure from mathematics that has proved useful in addressing a number of computational problems. The aim of this talk is to give an introduction to the monadic approach to building parsers, and outline some of the benefits that result from using monads. No prior knowledge of parser combinators or monads is assumed. Indeed, this talk can also been seen as a first introduction to the use of monads in programming.

This talk is based upon joint work with Erik Meijer (Utrecht).

Week 8: 1 Dec, Peter Freyd, University of Pennsylvania

To be announced.