[Off topic] Proving an impossibility
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 He then asked us to *prove* that the above programming fragment cannot be implemented just using if and while statement, even if S and T can be duplicated a finite number of times He also asked us to state our assumptions if any. 1. We have assignment statements (to create a flag and check) 2. The execution of E or F does not affect execution of S or T... Well, learning Haskell, I quickly realized that even if S and T have to be expressions and came up with this, assuming that 1. There are boolean operations 2. Boolean expressions are evaluated from Left to Right 3. Boolean expressions can be short-circuited while E and (S or 1) and F and (T or 1) do (* Nothing *) end But I would also like to consider an option of proving that its impossible, under the given constraints... Any thoughts? Vimal
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
He then asked us to *prove* that the above programming fragment cannot be implemented just using if and while statement, even if S and T can be duplicated a finite number of times
But it IS possible. Just add a boolean flag: done = False while E and not(done) do... I'll let you work out the rest. Unless I am missing something here... are you not allowed to introduce extra variables? It's a strange thing for your professor to ask, since under reasonable assumptions, anything that is computable can be done only using if and while. goto (which is essentially what break is) is never necessary. -Brent
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
On 4 Sep 2007, at 6:47 am, Vimal wrote:
In my Paradigms of Programming course, my professor presents this piece of code:
while E do S if F then break end T end
He then asked us to *prove* that the above programming fragment cannot be implemented just using if and while statement, even if S and T can be duplicated a finite number of times
You might want to look up the Bohm-Jacopini theorem. If you think about it, you'll realise that it's actually quite straightforward to convert *any* flow-chart into a single while loop containing a single case statement, with just one extra integer variable. (Hint: the integer variable plays to rôle of PC.) But to keep it simple, all we really need is procedures and if; no whiles and no extra variables. proc Example if E then S if not F then T Example end if end if end proc I remember my amusement, years ago, when I finally understood tail recursion: ANYTHING you can program using labels and gotos can be programmed using procedure calls, provided your compiler supports TRO (as both the C compilers I use do, in fact). Now let's do the example without procedures: Stopped: Boolean := False; while not Stopped and (E) loop S; if F then Stopped := True; else T; end if; end loop; Off-hand, the only assumption I'm aware of making is that E, S, F, and T do not themselves contain non-local control transfers. Or let's do it in another language. (do () ((or (not E) (progn S F))) T) That's Common Lisp. To get the Scheme version, replace 'progn by 'begin. One can do very similar things in Algol 68, Pop-2, Pop-11, any member of the Bliss family, BCPL, lots of languages.
1. There are boolean operations 2. Boolean expressions are evaluated from Left to Right 3. Boolean expressions can be short-circuited
You don't need 2 or 3. Take the loop version and tweak it: Stopped: Boolean := False; while not Stopped loop if E then S; if F then Stopped := True; else T; end if; else Stopped := True; end if; end loop; In order to prove the transformation impossible, you now know that you will need to assume that A. You are not allowed to introduce any new variables. B. You are not allowed to define any new procedures. C. You are not allowed to use a programming language with a loop-and-a-half construct. Ad C, consider Ada's loop exit when not E; S; exit when F; T; end loop; It's a long time since I saw any reference to it, but there's "Zahn's situation-case", see http://en.wikipedia.org/wiki/ Zahn's_construct This must also be ruled out under C. In fact, you have to make so many apparently arbitary restrictions on what you are allowed to do that the question becomes "why?". What *is* the point of this exercise?
participants (4)
-
Brent Yorgey -
Dan Piponi -
ok -
Vimal