[Haskell-cafe] Proof in Haskell
pat browne
Patrick.Browne at comp.dit.ie
Fri Sep 25 07:14:17 EDT 2009
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).
More information about the Haskell-Cafe
mailing list