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)

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

Here's two implementations of break, a snappy one from the prelude, and a slow stupid stateful one.

They are quickchecked to be identical.

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

If you want a proof assistant, you could try using Haskabelle: http://www.cl.cam.ac.uk/research/hvg/isabelle/haskabelle.html Jason