On 9/3/07, Vimal
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