Re: [Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?
On Sun, Jun 6, 2010 at 5:10 AM, Thomas Hartman tphya...@gmail.com wrote: Here's two implementations of break, a snappy one from the prelude, ... prelbreak p xs = (takeWhile (not . p) xs,dropWhile (not . p) xs) -- fast, more or less as implemented in prelude iiuc I had a look at the prelude, and I was surprised to see there's 2 versions, depending on a flag : #ifdef USE_REPORT_PRELUDE break p = span (not . p) #else -- HBC version (stolen) break _ x...@[] = (xs, xs) break p xs@(x:xs') | p x= ([],xs) | otherwise = let (ys,zs) = break p xs' in (x:ys,zs) #endif I'm curious why is it so, and which version is compiled in the platform or the ghc binaries. ( my guess is USE_REPORT_PRELUDE compiles functions as defined in the haskell report, but the other version is faster and used by default. ) David. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?
This isn`t a manifestation of the Curry-Howard isomorphism? 2010/6/8 Alexander Solla a...@2piix.com On Jun 7, 2010, at 4:10 PM, Alexander Solla wrote: You might note how much like evaluating the function generating the analysis is. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?
Hello David, Tuesday, June 8, 2010, 10:33:51 AM, you wrote: ( my guess is USE_REPORT_PRELUDE compiles functions as defined in the haskell report, but the other version is faster and used by default. ) you are right -- Best regards, Bulatmailto:bulat.zigans...@gmail.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?
On Tuesday 08 June 2010 08:33:51, David Virebayre wrote: On Sun, Jun 6, 2010 at 5:10 AM, Thomas Hartman tphya...@gmail.com wrote: Here's two implementations of break, a snappy one from the prelude, ... prelbreak p xs = (takeWhile (not . p) xs,dropWhile (not . p) xs) -- fast, more or less as implemented in prelude iiuc I had a look at the prelude, and I was surprised to see there's 2 versions, depending on a flag : #ifdef USE_REPORT_PRELUDE break p = span (not . p) #else -- HBC version (stolen) break _ x...@[] = (xs, xs) break p xs@(x:xs') | p x= ([],xs) | otherwise = let (ys,zs) = break p xs' in (x:ys,zs) #endif I'm curious why is it so, and which version is compiled in the platform or the ghc binaries. ( my guess is USE_REPORT_PRELUDE compiles functions as defined in the haskell report, but the other version is faster and used by default. ) Aye. I'm not sure whether there's a difference with -O2, but it's substantial without optimisations. David. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?
On Jun 8, 2010, at 2:38 AM, Alberto G. Corona wrote: This is`t a manifestation of the Curry-Howard isomorphism? Yes, basically. If we rephrase the isomorphism as a proof is a program, the formula it proves is a type for the program (as Wikipedia states it), we can see the connection. The characterization of prelBreak I gave is a type for prelBreak. The type is richer than we can express in the Haskell type system (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.), but we can still reason about the richer type mathematically, and the Curry-Howard isomorphism applies to it.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?
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? import Control.Monad.State import Test.QuickCheck tThis = take 5 . show . mybreak (400) $ [1..10^7] tPrel = take 5 . show . prelbreak (400) $ [1..10^7] prelbreak p xs = (takeWhile (not . p) xs,dropWhile (not . p) xs) -- fast, more or less as implemented in prelude iiuc mybreak p xs = evalState (brk p) ([],xs) -- stateful, slow brk p = do (notsat,remaining) - get case remaining of [] - return (notsat,remaining) (r:rs) - if p r then return (notsat,remaining) else do put (notsat++[r],rs) -- ++ is probaby a major reason brk p ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?
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
Re: [Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?
On Jun 7, 2010, at 4:10 PM, Alexander Solla wrote: For exposition, I'll do the analysis for the Prelude function. You might note how much like evaluating the function Correction: You might note how much like evaluating the function generating the analysis is. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?
On Sat, Jun 5, 2010 at 8:10 PM, Thomas Hartman tphya...@gmail.com 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
