[Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?

[Alexander Solla]

On Jun 5, 2010, at 8:10 PM, Thomas Hartman wrote:

> Is there a way to prove they are identical mathematically? What are
> the techniques involved? Or to transform one to the other?

Typically, the easiest way to prove that functions f g are equivalent  
is to (1) show that their domains are the same, and (2) show that for  
every x in the domain, f x = g x.

Usually, this amounts to comparing and understanding the function  
definitions, since each definition if a proof that the function  
relates a value x to f x, its image under f.

So a proof that f = g is a proof that a "characterization" of f is the  
same as the "characterization" for g.  For exposition, I'll do the  
analysis for the Prelude function.  You might note how much like  
evaluating the function Generating the characterization for a  
"caseful" or "stateful" function requires quantifying over cases or  
states.  Exercise left to the reader.

 >  prelbreak p xs = (takeWhile (not . p) xs,dropWhile (not . p) xs)

We seek a characterization of prelbreak in the following terms:
"prelbreak is a function that accepts a proposition p and a list of  
x's, and returns a ..."

To that end, note that prelbreak is a "product function".  It returns  
a pair of images of p and xs, under the functions (\p xs -> takeWhile  
(not . p) xs) and (\p xs -> dropWhile (not . p) xs).

takeWhile is kind of tricky to describe in English, since it depends  
on the intrinsic order of the xs.  But in this case it returns the  
largest prefix of xs for which no x satisfies p.

Dually, (\p xs -> dropWhile (not . p) xs) returns the list complement  
(taken in xs) of the image of (\p xs -> takeWhile (not . p) xs).  (I  
guess this is a very high level characterization, especially since I  
didn't derive it from the function's definition.  The level of detail  
you want in your proof is up to you)

So, finally, prelbreak accepts a proposition p and a list xs, and  
returns a pair whose first element is the largest prefix of xs for  
which no x satisfies p, and whose second element is the complement of  
the first, taken in xs.

To do it for mybreak, you would have to pick apart the semantics of  
evalState and brk, and recharacterize them.  That could be a little  
trickier mathematically, or straight forward.  It depends on how you  
end up quantifying over monadic actions.  Either way, it will be a LOT  
like evaluating the code.  (After all, the function definition is a  
proof that the function relates each x to f x)