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

Michaelmas Term 2001 (all Fridays)

• 30th November
• 23rd November
• 16th November
• 9th November
• 2nd November
• 26th October
• 19th October

Summer Break 2001 (all Fridays)

• 13th July
• 6th July
• 29th June
• 22nd June

Trinity Term 2001 (all Tuesdays)

• 12th June
• 5th June
• 29th May
• 22nd May
• 15th May
• 8th May
• 1st May

Trinity Term 2001 (all Fridays)

• 27th April
• 20th April

Hilary Term 2001 (all Fridays)

• 30th March
• 23rd March
• 16th March
• 9th March
• 2nd March
• 9th February
• 2nd February

Friday, 30th November 2001

Richard spoke about how we can define axioms for arithmetic coding and translated them into a relational programming style. The axioms for an arithmetic coder are:

1) encode [] = [0, 1)
2) encode (xs ++ ys) is a subset of encode xs
3) encode (xs ++ [p]) intersect encode (xs ++ [q]) /= empty => p = q

He also mentioned a new method for inverting programs, based on the way we invert arithmetic coding. If there is some h such that
x = foldl f y (z:zs) => x /= y and h x y = z, then
unfoldr (g (foldl f y zs)) y = zs where
g x y = if x == y then Nothing else Just (h x y, f y (h x y)).

Jeremy told us about minimum edit distances and minimum cost spanning trees.

Friday, 23rd November 2001

Last meeting was used to discuss people's thoughts on the Countdown Problem again. Ross has managed to significantly improve the performance of his algorithm by using a series of rewrite rules:

(a + b) + c => a + (b + c)
(a - b) + c => (a + c) - b
(a - b) - c => a - (b + c)
a + (b - c) => (a + b) - c

He also managed to achieve a performance increase by memoising the results.

Shin has been thinking about the problem in terms of closures of relations and here are his comments on what he said.

To establish the background, I was trying to derive an algorithm
(for the count-down problem) and in one of the phases I need to
build all legal expression trees bottom-up.
I therefore need an algorithm to compute the closure of a relation
of type A*A -> A. There is an algorithm which is basically a direct
extension of the one in 'the book' and looks intuitively
correct, but I was not able to prove it in the meeting today. I
believe I've constructed a proof just now.

In chapter 6 of AoP there is a derivation of a recursive
equation for computing R* (the closure of a relation R :: A -> A).
We start with the specification (I'll denote union by U and fixed-point
operator by fix. For ease of reading, I'll write relations in small
letters):

  close(p,q) = p U fix(x: q U r.x - p)

When p = 0, the above definition reduces to

  close(0,q) =fix(x: q U r.x) = r* . q

So we can use close to compute r* given q as the initial value.
It was then derived that:

  close(p,0) = p
  close(p,q) = close(pUq, r.q - (pUq))

To generalise close to a relation taking two arguments, a natural
specification to start with is:

  close(p,q) = p U fix(x: q U (r.(x*x) - p))

But it does not work. After some trial and error, I came up
with the following specification:

  close(p,q) = p U fix(x: q U (r.((x*x) U (x*p) U (p*x)) - p))

The derived algorithm is:

  close(p,0) = p
  close(p,q) = close(pUq, r.((p*q) U (q*p) U (q*q)) - (pUq))

The derivation goes:

     close(p,q)
  =    { definition }
     p U fix(x: q U (r.((x*x) U (x*p) U (p*x)) - p))
  =    { x U y = x U (y-x) }
     p U fix(x: q U (r.((x*x) U (x*p) U (p*x)) - (p U q)))
  =    { rolling } 
     p U q U fix(x: q U
                    (r.(((qUx)*(qUx)) U ((qUx)*p) U (p*(qUx)))
                     - (p U q)))
  =    { claim that the two long chains of unions are
         equal; see below }
     p U q U fix(x: q U
                    (r. ((p*q) U (q*p) U (q*q) U
                         (x*x) U (x*(pUq)) U ((pUq)*x)) - (pUq)))
  =    { (r.) and (-(pUq)) distributes into union }
     p U q U fux(x: q U (r . ((p*q) U (q*p) U (q*q)) - (pUq))
                      U (r . (x*x) U (x*(pUq)) U ((pUq)*x) - (pUq))
  =    { folding the definition of close }
     close(p U q, r . ((p*q) U (q*p) U (q*q)) - (pUq))


The claim to prove in the big step above is that the two horrible
looking chain of unions indeed equal. We use the following fact:

   (a U b) * (c U d) = (a*c) U (a*d) U (b*c) U (b*d)

The claim can be proved as:

     ((qUx)*(qUx)) U ((qUx)*p) U (p*(qUx))
  =     { expanding all the terms }
     (q*q) U (q*x) U (x*q) U (x*x) U
     (q*p) U (x*p) U (p*q) U (p*x)
  =     { simply rearranging }
     (p*q) U (q*p) U (q*q) U
     (x*x) U (q*x) U (p*x) U (x*q) U (x*p)
  =     { folding the last four terms }
     (p*q) U (q*p) U (q*q) U
     (x*x) U ((pUq) * x) U (x * (pUq))

Friday, 16th November 2001

Richard gave us the latest version of his derivation of arithmetic coding, which goes like this:

encode :: [Char] -> [Bit]
encode = incode (0, 1)

incode (l, r) cs
  | 2 * r <= 1 -> 0:incode (2 * l, 2 * r) cs
  | 1 <= 2 * l -> 1:incode (2 * l - 1, 2 * r - 1) cs
  | null cs    -> [1]
  | otherwise  -> incode ((l, r) (+) (a, b)) (tail cs)
                      where (a, b) = subint (head cs)
                            (l, r) (+) (a, b) = (l + (r - l) * a, l + (r -  l) * b)

There is still a problem in that changing to the integer version of the algorithm is not a data refinement.

Shin spoke about the Countdown Problem (named aftyer the TV programme) in which you have to apply + - * and / to six numbers, using each number only once, to obtain a randomly chosen target number.

Friday, 9th November 2001

Ross began proceedings with a talk on finite state automata in Haskell, after which we had Shin's revised proof of his converse function theorem. The new proof uses well-foundedness instead of F-inductivity and F-reductivity.

Shin has also been doing some reading on functional quantum computing, and how quantum computers can reduce the time required for some kinds of algorithms.

Richard has been thinking about the conditions under which unfoldr f . g = unfoldr f' for certain f, g and f'. This is useful for the derivation of arithmetic coding from its specification.

Friday, 2nd November 2001

The subject of the discussion at the last meeting was arithmetic coding. Richard is interested in deriving a program which implements the algorithm from first principles. He began by defining the encoding function as follows:

encode :: [Char] -> [Bit]
encode = toBits . contract . map bounds

where toBits is the function taking a range (represented as a pair of Reals (left, right)) to the shortest sequence of bits representing a number in the range, bounds takes each characted to an interval representing its probability of occurrence, and

contract = foldl narrow (0, 1)
where narrow (l, r) (a, b) = (l + (r - l) * a, l + (r - l) * b)

Geraint suggested that it might be more helpful to represent ranges as the pair (left, length) instead of (left, right), while Jeremy proposed that it would be clearer to use the notation a[l, r] instead of l + (r - l) * a.

It turns out that narrow is associative, so contract = foldr narrow (0, 1).

Barney then attempted to explain how the integer-valued version of the coding algorithm works, and the (small) tradeoff that occurs because the compression becomes slightly less with this method.

Friday, 26th October 2001

To begin with, Richard spoke about the problem of computing minlength {bs | l <= frac bs < r} where frac = foldr op 0, and op b r = (b + r) / 2.
Jeremy has been working on a method of assigning distinction / pass / fail marks to MSc students. The problem is to work out where the borderlines fall under different mappings, p, from grades achieved in the exams to degree results. We can define a preorder on the lists of exam results by taking the pointwise order after sorting the lists of results. Under this ordering, p must be monotonic - ie better grades in the exams lead to better degree results. Several methods for determining where the borderlines lay under vaious mappings p were discussed, including zigzagging across the borderline and dividing the set of all possible sets of grades up into bite-sized chunks and considering each chunk separately.
Finally, Shin gave a proof of his converse function theorem. He is going to try to simplify the proof by avoiding using the notions of F-inductivity and F-reductivity.

Friday, 19th October 2001

Jeremy explained the class of bracketting problems, focussing in particular on constructing trees of minimum height. He showed that this problem could be solved by a greedy algorithm but he wanted to solve it by a thinning algorithm instead. This meant, by definition, keeping more than one solution at each stage. Eventually Shin suggested a suitable ordering on which to thin, whereby trees are only compared pointwise if their spines have equal length. As a separate topic, Shin introduced the group to Erwig's recent JFP paper on graph algorithms. Graphs are represented using an inductive datatype and can be built up by repeatedly adding nodes. Each node contains lists of incoming nodes and outgoing nodes.

Friday, 13th July 2001

Richard wished to derive the program he had written to compute the pattern-matching statistics of a string. He specified it as the result of mapping a certain function on the text over the initial segments of the pattern. Then he wrote the function on the text as a fold-left, applied the scan lemma and considered thinning the result. He finished by discussing the intended data structure of suffix dags and the unrelated topic of space-efficient representations of binary search trees.

Friday, 6th July 2001

Pedro had written a polytypic predicate that tested whether a value was in the domain of a function. He had hoped to define the predicate perfect as the domain of the unembedding function on nests written as an unfold. Unfortunately, for lazy functional languages, he had defined instead a predicate that tested whether the shape of the input was completely defined. He then tried to define perfect by composing this predicate with the unembedding function but the resulting predicate could never return false.

Friday, 29th June 2001

As a prelude to his main question, Shin continued last week's discussion on inductive relations, focussing on a theorem which related the entireness of a hylomorphism to the entireness of its parameters. Shin then proved the converse function theorem, which expresses the converse of a function f as a fold with a relation R. He asked how the proof could be saved if f need not be entire. He derived a further condition which said that R and the fold with R must have the same range but Roland said this was unlikely to be satisfied.

Roland explained how to make any amount over 13 cents from 3 cent and 8 cent pieces alone. He wanted a constructive (no need to know the method beforehand) proof by induction that one could always do this for values over a certain amount, generalising the problem to relatively prime X and Y cent pieces. Roland conjectured in terms of X and Y, an expression for the number Z such that every number greater than or equal to Z is the sum of positive multiples of X and Y.

Friday, 22nd June 2001

Ian, Richard, and Shin rearranged the definition of the efficient fold for nests in the hope that Ian might be able to prove the uniqueness theorem. Barney explained range encoding, which compresses strings far more than Huffman encoding does. Each string corresponds to a range, which narrows as the string lengthens. The encoding of the string is the lowest least precise number in that range. Much of his talk concerned the implementation details of how to avoid underflow. Richard has written an efficient O(mn) program to compute the matching statistics for a pattern of length m inside of text of length n. He compared suffix trees with suffix dags.

Tuesday, 12th June 2001

Jeremy wrote up the generalised fold and the efficient fold for nests. Richard disputed Hinze's claim that the latter was more efficient but Jeremy convinced the group that it was, since it had no nest-to-nest transformations. Clare said she might be able to show that efficient folds had unique solutions by generalising a proof at the end of Bird and Paterson's paper. To do this, she needed to understand inductive relations. The group will now meet on Fridays instead of Tuesdays, starting on June 22.

Tuesday, 5th June 2001

Ian wanted to know if efficient folds satisfied a universal property. He explained the advantages of efficient folds, why they were needed in proofs (to write maps), their typings, and their definition for nests in Haskell, contrasting them with simple folds and generalised folds. Universal properties have two halves: a definition (here trivial) and a uniqueness theorem. Jeremy observed that for standard folds, the universal property was equivalent to the fusion law.

Tuesday, 29th May 2001

Barney gave a three-axiom definition of a suffix tree, a data structure that can be used to look up a substring in a long text file. Each edge is labelled with a string, but for convenience, Barney labels each node too with the path to it, so each node has a substring but not vice versa. He explained Wiener's algorithm to build a suffix tree for a string in linear time and space. Richard opined that the algorithm could be better described in a functional style as a fold on the tails of a list to build a tree. Reasoning about the algorithm's efficiency involved too many details of Wiener's exact implementation for the group to be satisifed that it used as little time and space as the author claimed.

Tuesday, 22nd May 2001

Richard described the latest variant of the Burrows-Wheeler transform to have caught his interest. Manzini sorts the rotations using only the first k characters of each. Remarkably, the transform is still invertible (and Richard can prove this) even though the matrix (the sorted list of rotations) cannot be recovered in full. The output is the last column of the matrix and only the first k columns can be reconstructed, but the original input can be worked out from this information alone.

Tuesday, 15th May 2001

Pedro uses zips to write embeding functions on nested datatypes, because his target datatypes are different from those suggested by Okasaki. His functor category is built from CPO, which is easier to handle as a base category than Rel is. He constrains the form of his nested datatypes to keep both the embedding and the unembedding operations functional (and therefore implementable). He can derive as a simple fold a predicate that tests whether a value is in the domain of the unembedding function.

Tuesday, 8th May 2001

Richard talked about another variation of the Burrows-Wheeler transform in which an alternating lexicographic ordering is used in place of lexicographic ordering. He claimed that the transformation is still invertible. He then mentioned another variation proposed by Barney to deal with compressing Haskell scripts, which involves riffling.

Shin summarised the recent work of the Tokyo University group on longest segment problems. The group then discussed possible future work of each member. Jeremy will look into Mendler's datatype.

Tuesday, 1st May 2001

Barney talked about a variant of the Burrows-Wheeler transform: compute the sorted list of rotations, and output not the last column, but the penultimate column instead. He had discovered a pair of inputs which demonstrate that the transform is not injective, and therefore not invertible either. Extra information could restore its injectivity but so much was needed as to make it useless for data compression. However, Barney discovered that simply permuting the rotations was another way to make the transform invertible again.

Ian asked how to write generalised folds for alternating lists. Finally, Richard talked about Dijkstra's problem of designing a non-deterministic algorithm to tile a chessboard with dominoes. A coreflexive relation could be used to enforce an invariant on the state of the board. He debated with Geraint whether backtracking could be avoided.

Friday, 27th April 2001

Jeremy had written a paper about necessary conditions on a relation that can be expressed as a fold. Bart Jacobs had then told him of an alternative simpler (not using kernels) congruence (or "lifting relations") condition, which he explained by structural induction on the polynomial base functor. However, Richard used the universal property to show that Jacobs' condition was just that the relation was simple. Jeremy also gave a dual condition (using invariants) for unfolds, equivalent to entireness, and considered extending the conditions to partial functions.

Friday, 20th April 2001

Richard suggested a variation to the Burrows-Wheeler transform where, instead of the last column, the penultimate column of the sorted rotations was taken. To reconstruct the rotations from the penultimate column, it was necessary to compute the square roots of a permutation. However, there are more than one square roots of a permutation and it was unclear which one to use. The group tried some examples but did not come to a conclusion how it could be done.

Friday, 30th March 2001

Ian described how to show that nested relators commute with converse. Shin announced a further problem that he and Richard had encountered with their work on the Burrows-Wheeler transform. Clare was stuck with the "Id" case of her proof that her efficient folds were equal to her generalised folds composed with maps.

Finally, Jeremy explained a meaning-preserving transformation on programs that Ralf Lammel had recently mentioned called refactoring. It can be used to rename variables and tidy up class hierarchies. More interesting applications in the functional programming setting may include the automated introduction of monads.

Friday, 23rd March 2001

Richard had greatly simplified Shin's derivation of the converse of the Burrows-Wheeler transform. However, Jeremy pointed out that the point-free style of his proof was not rigorous enough since some functions depended on the input string, which therefore couldn't be omitted. A notation for modulo equality might allow Richard to preserve his proof.

Friday, 16th March 2001

Ian explained to Richard the difference between his definition of generalised folds and Clare's. Then Richard talked about the contravariant property of a function apply that he had just invented; it permutes a string according to a given function on indices. The meeting lasted less than an hour.

Friday, 9th March 2001

Richard started the short meeting by explaining how a simple coding trick could be used to reduce the number of comparisons needed to sort the tails of a list. Barney belived the problem could be solved in linear time and tried to construct an algorithm to do this. Ian's notational difficulties with generalised folds were also briefly discussed once more.

Friday, 2nd March 2001

Richard tried to show that his function sperm could be computed functionally in O (n log n) time, where n is the length of the input list. It required a logarithmic number of passes, but some of them appeared to take longer than linear time. Shin showed that the informal algorithm given by Richard four weeks ago was indeed, as then claimed, the converse of the Burrows-Wheeler transform. Ian and Jeremy briefly explained the higher-order naturality property of zips, which Shin had needed to use. Finally, Richard discussed the problems Ian was having with writing generalised folds generically. Clare suggested he should use a bottom-up approach.

Friday, 9th February 2001

Richard proposed that the number of comparisons needed to sort the list of tails of a list is O (n log n) but he had no proof of this. Shin has verified the candidate inverse of the Burrow-Wheeler transform. Oege had conjectured that interpretting a lambda-term in Set and then turning it into a relation gave the same result as interpretting the lambda-term in Rel directly. Jeremy presented Nick Benton's proof of this, which took up most of the meeting. Then he returned to the last week's relational extension of his characterisation of folds. He produced counterexamples (one due to Clare) given two different definitions of kernel. Finally, Richard and Jeremy discussed how to write run-length encoding as a fold on lists.

Friday, 2nd February 2001

Richard introduced the Burrows-Wheeler transform on strings, which groups together multiple occurrences of the same letter in order to aid compression. He explained a simple algorithm to invert the transform (not an application of the converse function theorem) but why it worked was a mystery.

Jeremy gave an iff condition for when a function can be expressed as a fold. It used the concept of the kernel of a function: the set of pairs of elements on which the function has the same output. Although he couldn't see how to adapt his working from functions to relations, he attempted a diagram-chasing categorical proof of the "iff", observing that kernels are equivalent to pullbacks for those categories that have them.