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

[ok]

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?