Many programming tasks can be specified as optimisation problems in which a relation is used to generate all possible solutions, from which we wish to choose an optimal one. A relational operator “shrink”, developed by José N. Oliveira, is particularly suitable for constructing greedy algorithms from such specifications. Meanwhile, it has become standard in many sub-fields in programming language that proofs must be machine-verified. This tutorial leads the readers through the development of algebraic derivations of three greedy algorithms, one fold-based and two unfold-based, using AoPA, a library designed for machine-verified relational program calculation.
The problem of finding a densest segment of a list is similar to the well-known maximum segment sum problem, but its solution is surprisingly challenging. We give a general specification of such problems, and formally develop a linear-time online solution, using a sliding window style algorithm. The development highlights some elegant properties of densities, involving partitions that are decreasing and all right-skew.
The accompanying Haskell programs and Agda proofs are available on GitHub:
The Haskell program consists of the following files:
FDSList.hs: a main program that, for expository purpose, represents sequences by lists.
FDSSeq.hs: a linear-time implementation of the algorithm, using refined data structures as described in the paper.
ProbMDS.hs: problem specification for the MDS problem. To be imported by
ProbMMS.hs: problem specification for the MMS problem. To be imported by
MDSTest.hs: QuickCheck tests for the MDS problem.
MMSTest.hs: QuickCheck tests for the MMS problem.
Problem statements often resort to superlatives such as in eg. “… the smallest such number”, “… the best approximation”, “… the longest such list” which lead to specifications made of two parts: one defining a broad class of solutions (the easy part) and the other requesting the optimal such solution (the hard part).
This article introduces a binary relational combinator which mirrors this linguistic structure and exploits its potential for calculating programs by optimization. This applies in particular to specifications written in the form of Galois connections, in which one of the adjoints delivers the optimal solution.
The framework encompasses re-factoring of results previously developed by Bird and de Moor for greedy and dynamic programming, in a way which makes them less technically involved and therefore easier to understand and play with.
This is an extended version of our conference paper published in RAMiCS 2011.
The following is superseded by our later work Functional pearl: finding a densest segment.
- Page 3: “This input sequence does not have a solution…” what we meant was “This input does not have a prefix that is within bounds.” We used another example where the input does not have a feasible segment at all before changing to example, but I forgot to change the text accordingly.
- Page 4, Proof of Theorem 3.2: the first
mdsM x ⇑d win (a:x)should be
mdsM x ⇑d wp (trim (a:x));
a : x <b Land
a : x ≥b Lshould respectively be
trim (a : x) <b Land
trim (a : x) ≥b L.
Thanks to Josh Ko for pointing out both errors.
The problem of finding a maximally dense segment (MDS) of a list is a generalisation of the well-known maximum segment sum (MSS) problem, but its solution is more challenging. We extend and illuminate some recent work on this problem with a formal development of a linear-time online algorithm, in the form of a sliding window zygomorphism. The development highlights some elegant properties of densities, involving partitions which are decreasing and all right-skew.
Code and supplementary proofs are available online.
keywords: program derivation, segment problem, maximum density, sliding window, zygomorphism, right-skew.
Relational program derivation is the technique of stepwise refining a relational specification to a program by algebraic rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties to be verified by the type checker.
We have developed a library, AoPA, to encode relational derivations in the dependently typed programming language Agda. A program is coupled with an algebraic derivation whose correctness is guaranteed by the type system.
Two non-trivial examples are presented: an optimisation problem, and a derivation of quicksort where well-founded recursion is used to model terminating hylomorphisms in a language with inductive types.
This article extends the paper we published in Mathematics of Program Construction 2008. Code accompanying the paper has been developed into an Agda library AoPA.
This paper presents an application of bidirectional transformations to design and implementation of a novel editor supporting interactive refinement in the development of structured documents. The user performs a sequence of editing operations on the document view, and the editor automatically derives an efficient and reliable document source and a transformation that produces the document view. The editor is unique in its programmability, in the sense that transformation can be obtained through editing operations. The main tricks behind are the utilization of the view-updating technique developed in the database community, and a new bidirectional transformation language that can describe not only relationship between the document source and its view, but also data dependency in the view.
A transformation from the source data to a target view is said to be bidirectional if, when the target is altered, the transformation somehow induces a way to reflect the changes back to the source, with
the updated source satisfying certain healthiness conditions. Several bidirectional transformation languages have been proposed. In this paper, on the other hand, we aim at making existing transformations bidirectional.
As a case study we chose the Haskell combinator library, HaXML, and embed it into Inv, a language the authors
previously developed to deal with bidirectional updating. With the embedding, existing HaXML transformations gain bidirectionality.
Countdown is the name of a game in which one is given a list of source numbers and a target number, with the aim of building an arithmetic expression out of the source numbers to get as close to the target
as possible. Starting with a relational specification we derive a number of functional programs for solving Countdown. These programs are obtained by exploiting the properties of the folds and unfolds of various data types, a style of programming Gibbons has aptly called origami programming. Countdown is attractive as a case study in origami programming both as an illustration of how different algorithms can emerge from a single specification, as well as the space and time trade-offs that have to be taken into account in comparing functional programs.
The Burrows-Wheeler Transform is a string-to-string transform which, when used as a preprocessing phase in compression, significantly enhances the compression rate. However, it often puzzles people how the inverse transform can be carried out. In this pearl we to exploit simple equational reasoning to derive the inverse of the Burrows-Wheeler transform from its specification. We also outline how to derive the inverse of two more general versions of the transform, one proposed by Schindler and the other by Chapin and Tate.
This paper is devoted to the proof, applications, and generalisation of a theorem, due to Bird and de Moor, that
gave conditions under which a total function can be expressed as a relational fold. The theorem is illustrated with three problems, all dealing with constructing trees with various properties. It is then generalised to give conditions under which the inverse of a partial function can be expressed as a relational hylomorphism. Its proof makes use of Doornbos and Backhouse’s theory on well-foundedness and reductivity. Possible applications of the generalised theorem is discussed.