Dutch national flag problem

This exercise consists of solving the Dutch national flag problem, which can be described as follows :

Given a list whose elements are coloured red, white and blue in any order, construct a new list in which the elements are reordered in such a way that it constitutes a representation of the Dutch flag.

There are many ways to formalize this problem. In this exercise you should compare the internal and external approaches:

In the internal approach you start with stating a theorem to be proven: For a given l : List(C) there exist l1, l2, l3:List(C) such that Red(l1), White(l2), Blue(l3) and Perm(l, l1 ++ l2 ++ l3), where C = {red, white, blue}, ++ is list concatenation, and Perm is a predicate expressing that the two arguments are permutations of each other.

In the external approach you start to write a function dutch : (List(C))List(C) X List(C) X List(C) and then prove that the function has the desired properties.

For this exercise it is not necsessary to prove all properties of Perm. See also the exercise below.

Bounded linear search

Consider a Boolean function f on the natural numbers. The problem we consider is that of finding the smallest n:N for which f(n) = true. The obvious algorithm is to evaluate first f(0), then f(1) etc until the proper n is found. There are two obstacles: first, no such n need exist and, second, even if it does we have no bound on how far we need to search. We therefore consider only bounded linear search, where we give the search function two arguments, f and a bound max:N and want as output either the smallest n<max for which f(n)=true or, if no such n exists, max itself.

Permutations.

Define the permutation relation between lists. You may want to do it for some particular type of elements (e.g. lists of natural numbers) or more generally. There are many possible definitions. Then develop some theory for permutations, such as

Type-checking.

We consider the simply typed lambda calculus with variables represented by de Bruijn indices. Define

Then define a type-checker as a function taking a term as argument and returning either a type error or a correct type for the argument. Prove the soundness and completeness of the type-checker.

Bengt Nordstr|m
Tue Apr 30 13:39:35 MET DST 1996