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).
It is not possible at the value level, because Haskell does not
support dependent types and thus cannot express the type of the
proposition "forall a . forall x:Tree a, mirror (mirror x) = x", and
therefore a proof term also cannot be constructed.
However, if you manage to express those trees at type level, probably
with typeclasses and type families, you might have some success.
2009/9/25 pat browne
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Eugene Kirpichov Web IR developer, market.yandex.ru
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
Eugene Kirpichov -
pat browne -
Paul Johnson