[Haskell-cafe] Proof in Haskell
Paul Johnson
paul at cogito.org.uk
Fri Sep 25 12:42:53 EDT 2009
One alternative approach is to use QuickCheck to test many trees and
look for counter-examples. You can also use SmallCheck to do an
exhaustive check up to a chosen size of tree.
To do this with QuickCheck you would write a function such as
prop_mirror :: Node a -> Bool
prop_mirror x = (mirror (mirror x)) == x
You would also need to define an instance of "Arbitrary" for Node to
create random values of the Node type. Then you can call:
quickCheck prop_mirror
and it will call the prop_mirror function with 100 random test cases.
Not the formal proof you wanted, but still very effective at finding bugs.
On 25/09/09 12:14, pat browne wrote:
> Hi,
> Below is a function that returns a mirror of a tree, originally from:
>
> http://www.nijoruj.org/~as/2009/04/20/A-little-fun.html
>
> where it was used to demonstrate the use of Haskabelle(1) which converts
> Haskell programs to the Isabelle theorem prover. Isabelle was used to
> show that the Haskell implementation of mirror is a model for the axiom:
>
> mirror (mirror x) = x
>
> My question is this:
> Is there any way to achieve such a proof in Haskell itself?
> GHC appears to reject equations such has
> mirror (mirror x) = x
> mirror (mirror(Node x y z)) = Node x y z
>
>
> Regards,
> Pat
>
>
> =================CODE=====================
> module BTree where
>
> data Tree a = Tip
> | Node (Tree a) a (Tree a)
>
> mirror :: Tree a -> Tree a
> mirror (Node x y z) = Node (mirror z) y (mirror x)
> mirror Tip = Tip
>
> (1)Thanks to John Ramsdell for the link to Haskabelle:
> http://www.cl.cam.ac.uk/research/hvg/Isabelle/haskabelle.html).
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
More information about the Haskell-Cafe
mailing list