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

Michaelmas Term 2002 (all Fridays)

• 29th November
• 22nd November
• 15th November
• 8th November
• 1st November
• 18th October
• 11th October

Trinity Term 2002 (almost all Fridays)

• 28th June
• 14th June
• 31st May
• 24th May
• 17th May
• 3rd May
• 26th April
• Tuesday 19th March

Hilary Term 2002 (all Fridays)

• 22nd February
• 8th February
• 1st February
• 25th January

Friday, 29th November 2002

Claire has been working on her Nim problem using multirelations. She gave a proof of a winning strategy for her simplified version of the game, although there were a few points that needed further clarification.

As another example of the use of multirelations, she discussed the newsboy problem from decision theory.

Friday, 22nd November 2002

Jeremy has done some work on the derivation of hardware for comparing two numbers. He started with the following definitions:

    bin :: [Bool] -> Int
    bin = foldr oplus 0
        where b `oplus` x = (if b then 1 else 0) + 2 * x

    cmp :: [Bool] -> [Bool] -> Ordering
    cmp xs ys = compare (bin xs) (bin ys)

    min xs ys = case (cmp xs ys) xs (xs `box` ys) ys
    max xs ys = case (cmp xs ys) ys (xs `box` ys) xs

He has produced some theorems about fold, tails and scan on non-empty lists, which were used in his derivation.

Friday, 15th November 2002

Geraint has been deriving some more circuits using Haskell. One circuit compares two binary numbers, while the other returns the greatest and least of two binary numbers. Not only must his circuits work quickly, but they must also take up a reasonably small amount of space on a chip.

Friday, 8th November 2002

As nobody had prepared anything to talk about, Richard discussed some of the problems that he is setting for his lecture course in Formal Program Design.

One of the problems that is being set is the rally-driver problem, in which a driver has to get across the desert. There are fuel dumps at distances d_i containing enough fuel to drive p_i miles. The driver has to cross the desert making as few stops as possible. He has an infinite fuel tank, which starts off empty.

The students will also be considering problems involving floors and ceilings, such as the biscuit distribution problem, in which N Leibniz biscuits have do be distributed fairly among M students without breaking any.

Friday, 1st November 2002

Geraint has been thinking about the following problem. Is it true that
value . const = id => value (f x . y) = f x (value y)
for all f, x and y?

Shin has read a paper about extending the guarded command language to include angelic and demonic non-determinism. In this extended language, operations such as assignment and if-then can be expressed in terms of simpler constructs.

Friday, 18th October 2002

Isao has been working on the problem of dead code elimination. He is considering it as a maximum marking problem, implemented with generic Haskell.

Shin posed an interesting puzzle. We have to define begin, push, add and end so that for any integers a and b,
begin push a push b add end = a + b.

Friday, 11th October 2002

Clare has been working on multi-relations and predicate transformers. She gave examples of some programs---involving angelic and demonic non-determinism---and their corresponding multi-relations. There is an equivalence between these multi-relations and predicate transformers, and this was illustrated by an example involving a simplified version of the game of Nim.

Friday, 28th June 2002

Clare talked about multirelations, which are to relations what multifunctions (or set-valued functions) are to functions. It has recently been shown that up-closed multirelations are equivalent to monotonic predicate transformers, and so Clare has been trying to apply some of the known results about predicate transformers to multirelations. In particular, she has been looking at the extension of initial algebras from relations to multirelations. She showed how this can be applied to fold on lists to give a fold on multirelations that has a much more familiar form than its counterpart for predicate transformers, and should therefore be more useful for program derivation. Jeremy observed that she now needs to find some persuasive programming examples to convince people of this.

Thanks to Clare for writing this after I misplaced my notes.

Barney gave a proof that the method used for outputting bits in arithmetic coding is the best possible. People felt that the proof was a bit heavy-going, though.

Friday, 14th June 2002

Richard has been thinking about the Scan Lemma. This says that scanr f e = map (foldr f e) . inits. He has been considering ways to generalise this to arbitrary data types. The Scan Lemma for arbitrary data is scan f = map (fold f) . substructs where, for any data structure, substructs returns a new structure with the same shape as the old structure, but containing all the substructures of the old structure.

Friday, 31st May 2002

Isao spoke about his current research, which is about the translation from logical formulae to recursive functions. He used the following logical formula as an example:
One v_1 v_2 = there exists v_3 s.t. Adj v_1 _v3 and Adj v_2 v_3 We weren't quite sure whether the v_i were intended to be members of a list or a graph, nor whether they were intended to represent values of locations within the data structure.

Friday, 24th May 2002

Sharon has been thinking about the problem of arranging conference calls in a telephone system.

You have a set of callers, each of which wants to hear only some of the other callers. For example, no caller wants to hear his own voice. The machinery in the telephone exchange can only "remember" a single signal at once, and can add or subtract a single caller's voice to that signal. You can also reset to the zero signal at any time (otherwise the problem is a simpler path problem). There is no way to save intermediate results. The problem is to minimise the number of steps needed to produce the sound that each caller wants to hear.

As an example, suppose that there are three callers, a, b and c, and the outputs that they want are {a}, {a, b} and {a, c}. We can get all three signals by going through this process:

No signal--> +a --> {a} --> +b --> {a, b} --> -b --> {a} --> +c --> {a, c}.

Sharon has been thinking about this as a graph problem, with the desired outputs as nodes of the graph, whereas Richard proposed a relational programming solution.

Friday, 17 May 2002

Richard has been thinking about the countdown problem again, and gave the latest version of his relational program to solve it. He's been trying to eliminate intermediate data structures, but the resulting program ran quite slowly because it was repeating part of the computation.

Graham also gave his latest work on the problem.

Friday, 3rd May 2002

The last meeting was spent discussing the countdown problem. Mike has constructed a program using a top-down approach, while Richard has bee thinking about oriented binary trees, and has come up with a recurrence relation to calculate the numbers of such trees.

Friday, 26th April 2002

It seems like everyone is thinking about the countdown problem at the moment. Both Richard and Shin have produced programs to find solutions. Richard is looking at oriented trees to help solve the problem in general.

Tuesday, 19th March 2002

Barney has been working on the "division problem" in arithmetic coding. He has come up with an improved solution, but this is still not as good as he would like.

Shin has been continuing on the countdown problem. He's trying to cache intermediate results, and to throw out results that aren't useful before spending too much time on them, but he's having trouble with the memory consumption of his program.

Jeremy presented his work on the question of when a function is a fold.

Friday, 22nd February 2002

Shin spoke about the data mining problem, in which we want to find out which sets of items were bought by customers in a shop on each visit. For each customer, we have a bag of sets of items bought on each visit, and we build a tree to find out which items occur together.

Richard has been looking at how to build a logic program that will decide how to play Poker. We could produce a very slow program which produces an exact result, or a faster program that produces an approximate result. The problem is to find how fast we can make the program while still winning enough games.

He has also been looking at the unfoldr f . foldl g e problem. His latest solution is as follows:

unfoldr f . foldl g e = produce f g e
  where produce f g x ys = case f x of
                             Just (a, b) -> a:produce f g b ys
                             Nothing     -> consume f g x ys
        consume f g x [] = []
        consume f g x (y:ys) = produce f g (g x y) ys

Barney has been looking at ways of making arithmetic coding faster by changing the way in which bits are output from the encoder.

Friday, 8th February 2002

Jeremy discussed a connection between category theory and a "visual" style of programming.

Shin has been studying a data mining algorithm which uses a suffix-tree-like data structure, and he gave an example to illustrate the algorithm.

Friday, 1st February 2002

Arithmetic coding an be expressed as an unfoldr after a foldl, and this was Richard's motivation for looking at such things. He gave some conditions under which we can fuse the two together, which will be useful for the formal derivation of the algorithm for arithmetic coding which is used in practice.

Jeremy has been thinking about the minimum edit distance problem between sets of more than two strings. He showed how we can produce a tree showing how closely related a pair of strings in the set is. This has applications in biology, where the strings are genomes.

Friday, 25th January 2002

From Shin:

Shin modelled the Countdown problem in terms of the converse of a function flattening an expression tree. The generalised converse-of-a-function theorem was used to write the converse as an iteration. The hope was to apply the thinning theorem to remove redundant solutions. Richard and Sharon suggested possible ways the thinning theorem could be applied.

Finally, Richard discussed arithmetic coding and explained why it has been so difficult to produce a formal derivation of the algorithm and its inverse.