[Haskell-cafe] [Off topic] Proving an impossibility

[Dan Piponi]

On 9/3/07, Vimal <j.vimal at gmail.com> wrote:
> Hi
> In my Paradigms of Programming course, my professor presents this piece of code:
>
> while E do
>   S
>   if F then
>      break
>   end
>   T
> end

This is seriously offtopic but kinda fun anyway...

There's a nice formalism for investigating this kind of problem called
"Kleene Algebra with Tests" (KAT). Google to find out more - I
hesistate to give a link as every link I can find points to a file in
a proprietary format or requires a password, but there are lots of
documents out there.

The idea is that it gives a way to describe the path of execution of
imperative programs using notation remarkably like regular
expressions. The above loop could be written as X where X =
E'+ES(F+F'TX). E and F are 'tests' while S and T are more like
'actions'. For a test X, X' means "not X" and these symbols behave
just like regular expressions except that X+X'=1. A normal while loop
with no breaks, while (A) { B }, is given by Y where Y = ABY+A', so Y
= (AB)*A'. Anyway, the task is now an algebraic one: show that you
can't construct a solution to X = E'+ES(F+F'TX) using composition of
E, F, S, T and the Y = ABY+A' while-construction. Note that the
process of converting the imperative code to algebraic notation is
remarkably similar to that of porting imperative code to recursive
Hakell code, and that tests look a lot like guards in a
non-determinstic monad. (That was my obligatory mention of Haskell to
make things seem vaguely on topic.)

Also check out the folk theorem here:
http://citeseer.ist.psu.edu/harel80folk.html which can  be solved much
more easily using KAT.
--
Dan