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

the permutation relation is an equivalence relation,
 if l2 is permutation
of l1 then l1 and l2 are of the same length,
 if rev(l) denotes l reversed,
then rev(l) is a permutation of l,
 if l1 is a permutation of l2 and l3 a
permutation of l4, then
append(l1,l3) is a permutation of append(l2,l4).
Typechecking.
We consider the simply typed lambda calculus with variables represented
by de Bruijn indices. Define
 the set of terms,
 the set of types (e.g. one ground type and function types),
 the typing relation.
Then define a typechecker 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 typechecker.
Bengt Nordstrm
Tue Apr 30 13:39:35 MET DST 1996