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)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
