You are holding a necklace in your hands, composed of no fewer than thirteen exquisite pearls. The pearls are from all over the world, selected for the finest quality, smoothness and lustre. For your viewing pleasure, the necklace emphasizes variety, stringing pearls of wildly different color, shape and size. Satisfaction is guaranteed.

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 is 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.

Teacher: Good morning class. Today I would like you to construct a program for finding out how many ways a chessboard can be tiled with dominoes. For those who don't play games, a chessboard is a 8×8 board divided into 64 squares, and a domino is a 2×1 tile which can cover two squares of the board either vertically or horizontally. For example, a 2×2 board can be covered with two dominoes in exactly two ways, with both dominoes horizontal or both vertical.

We give transparent proofs of the PTIME-completeness of two decision problems for terms in the λ-calculus. The first is a reproof of the theorem that type inference for the simply-typed λ-calculus is PTIME-complete. Our proof is interesting because it uses no more than the standard combinators Church knew of some 70 years ago, in which the terms are linear affine – each bound variable occurs at most once. We then derive a modification of Church's coding of Booleans that is linear, where each bound variable occurs exactly once. A consequence of this construction is that any interpreter for linear λ-calculus requires polynomial time. The logical interpretation of this consequence is that the problem of normalizing proofnets for multiplicative linear logic (MLL) is also PTIME-complete.

A permutation phrase is a sequence of elements (possibly of different types) in which each element occurs exactly once and the order is irrelevant. Some of the permutable elements may be optional. We show how to extend a parser combinator library with support for parsing such free-order constructs. A user of the library can easily write parsers for permutation phrases and does not need to care about checking and reordering the recognized elements. Applications include the generation of parsers for attributes of XML tags and Haskell's record syntax.

This work presents simple decision procedures for the propositional calculus and for a simple predicate calculus. These decision procedures are based upon enumeration of the possible values of the variables in an expression. Yet, by taking advantage of the sequential semantics of boolean connectors, not all values are enumerated. In some cases, dramatic savings of machine time can be achieved. In particular, an equivalence checker for a small programming language appears to be usable in practice.

An injective finite mapping is an abstraction common to many programs. We describe the design of an injective finite mapping and its implementation in Curry, a functional logic language. Curry supports the concurrent asynchronous execution of distinct portions of a program. This condition prevents passing from one portion to another a structure containing a partially constructed mapping to ensure that a new choice does not violate the injectivity condition. We present some motivating problems and we show fragments of programs that solve these problems using our design and implementation.

This paper implements a simple and elegant version of bottom-up Kilbury chart parsing (Kilbury, 1985; Wirén, 1992). This is one of the many chart parsing variants, which are all based on the data structure of charts. The chart parsing process uses inference rules to add new edges to the chart, and parsing is complete when no further edges can be added. One novel aspect of this implementation is that it doesn't have to rely on a global state for the implementation of the chart. This makes the code clean, elegant and declarative, while still having the same space and time complexity as the standard imperative implementations.

Comparing two types for equality is an essential ingredient for an implementation of dynamic types. Once equality has been established, it is safe to cast a value from one type to another. In a language with run-time type analysis, implementing such a procedure is fairly straightforward. Unfortunately, this naive implementation destructs and rebuilds the argument while iterating over its type structure. However, by using higher-order polymorphism, a casting function can treat its argument parametrically. We demonstrate this solution in two frameworks for ad-hoc polymorphism: intensional type analysis and Haskell type classes.

Using Haskell as a digital circuit description language, we transform a ripple carry adder that requires $O(n)$ time to add two $n$-bit words into a parallel carry lookahead adder that requires $O(\log n)$ time. The ripple carry adder uses a scan function to calculate carry bits, but this scan cannot be parallelized directly since it is applied to a non-associative function. Several techniques are applied in order to introduce parallelism, including partial evaluation and symbolic function representation. The derivation given here constitutes a semi-formal correctness proof, and it also brings out explicitly each of the ideas underlying the algorithm.

This paper describes a simple but flexible family of Haskell programs for drawing pictures of fractals such as Mandelbrot and Julia sets. Its main goal is to showcase the elegance of a compositional approach to program construction, and the benefits of a clean separation between different aspects of program behavior. Aimed at readers with relatively little experience of functional programming, the paper can be used as a tutorial on functional programming, as an overview of the Mandelbrot set, or as a motivating example for studies in computability.

The tedium of writing pickling and unpickling functions by hand is relieved using a combinator library similar in spirit to the well-known parser combinators. Picklers for primitive types are combined to support tupling, alternation, recursion, and structure sharing. Code is presented in Haskell; an alternative implementation in ML is discussed.

We derive a combinator library for non-deterministic parsers with a monadic interface, by means of successive refinements starting from a specification. The choice operator of the parser implements a breadth-first search rather than the more common depth-first search, and can be seen as a parallel composition between two parsing processes. The resulting library is simple and efficient for “almost deterministic” grammars, which are typical for programming languages and other computing science applications.

The Sieve of Eratosthenes is an efficient algorithm for computing the successive primes. Rendered informally, it is as follows:

1. Write down the successive “plurals”: 2, 3, 4, …

2. Repeat:

(a) Take the first number that is not circled or crossed out.

(b) Circle it.

(c) Cross out its proper multiples.

3. What is left (i.e. the circled numbers) are the successive prime numbers.