[Haskell-cafe] The Riddle of the Buddhist Monk

[Richard O'Keefe]

On 21/12/2011, at 4:34 AM, Patrick Browne wrote:

> I have simplified the code using constructors and export.
> I can evalute the qualified expressions but I do not get the expected results.
> 
> module  MONKONMOVE (module MONKONMOVE)where

When I see "MONKONMOVE" I think "what's a MONKON?"

Even the Java designers say "if you paste together several words all in
capitals, put underscores between them".  So is it MONKON_MOVE,
MONK_ONMOVE, MONK_ON_MOVE (what does that mean?) or something else?

The classic puzzle has nothing to do with monks, Buddhist or otherwise.
It goes something like this:
	"One morning you start climbing a mountain at 8am and reach the
	 top by 6pm.  You stay there overnight.  Next morning, you start
	 down on the same path at 8am and reach the bottom by 6pm.
	 Prove that there is some time of day 8am <= t <= 6pm such that
	 you are at the same place at time t on both days."

The solution as given by Lewis Carroll is
	"Pretend there are two people doing the trip, one up and one
	 down, on the same day.  Clearly they must meet.  QED."

So what exactly is the program supposed to do?  The problem lacks
the information from which a specific value of t can be computed;
all that can be determined is that *some* value of t must exist.
However, that proof depends on the *continuity* of the time->place
mappings:
	if f, g: [0,1] -> [0,1] are continuous functions
	and f(0) = 0, f(1) = 1, g(0) = 1, g(1) = 0
	then there exists t in [0,1] such that f(t) = g(t)
and I don't see anything in the code that talks about continuity.
It should be clear that daredevils going up and down the mountain
on sufficiently springy pogo sticks (or electrons jumping in their
insouciant quantum way) need *not* meet.