Re: [Haskell-cafe] Proof in Haskell
On Thursday 23 December 2010 12:52:07 pm Daniel Peebles wrote:
> Fair enough :) that'll teach me to hypothesize something without thinking
> about it! I guess I could amend my coinductive proof:
>
> http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517
>
> does that cover bottom-ness adequately? I can't say I've thought through it
> terribly carefully.
That isn't the usual way to model partially defined values. For instance, you
can write functions with that datatype that would not be monotone:
pdefined :: {A : Set} -> Tree A -> Bool
pdefined ⊥ = false
pdefined _ = true
It's somewhat more accurate to take the partiality monad:
data D (A : Set) : Set where
now : A -> D A
later : ∞ (D A) -> D A
⊥ : {A : Set} -> D A
⊥ = later (♯ ⊥)
Then we're interested in an equivalence relation on D As where two values are
equal if they either both diverge, or both converge to equal inhabitants of A
(not worrying about how many steps each takes to do so).
Then, the partially defined trees are given by:
mutual {A}
Tree = D Tree'
data Tree' : Set where
node : Tree -> A -> Tree -> Tree'
tip : Tree'
And equivalence of these trees makes use of the above equivalence for D-
wrapped things. (It's actually a little weird that this works, I think, if you
expect Tree' to be a least fixed point; but Agda does not work that way).
If you're just interested in proving mirror (mirror x) = x, though, this is
probably overkill. Your original type should be isomorphic to the Haskell type
in a set theoretic way of thinking, and the definition of mirror does what the
Haskell function would do at all the values. So the fact that you can write
functions on that Agda type that would have no corresponding implementation in
Haskell is kind of irrelevant.
-- Dan
___
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
Fair enough :) that'll teach me to hypothesize something without thinking about it! I guess I could amend my coinductive proof: http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517 does that cover bottom-ness adequately? I can't say I've thought through it terribly carefully. On Thu, Dec 23, 2010 at 12:30 PM, Ryan Ingram wrote: > On Thu, Dec 23, 2010 at 8:19 AM, Daniel Peebles > wrote: > > Simulating bottoms wouldn't be too hard, but I don't think the statement > is > > even true in the presence of bottoms, is it? > > Isn't it? > > data Tree a = Tip | Node (Tree a) a (Tree a) > > mirror :: Tree a -> Tree a > mirror Tip = Tip > mirror (Node x y z) = Node (mirror z) y (mirror x) > > -- > > -- base cases > mirror (mirror _|_) > = mirror _|_ > = _|_ > > mirror (mirror Tip) > = mirror Tip > = Tip > > -- inductive case > mirror (mirror (Node x y z)) > = mirror (Node (mirror z) y (mirror x)) > = Node (mirror (mirror x)) y (mirror (mirror z)) > -- induction > = Node x y z > > -- ryan > ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
On Tue, Dec 21, 2010 at 9:57 AM, austin seipp wrote:
> For amusement, I went ahead and actually implemented 'Mirror' as a
> type family, and used a little bit of hackery thanks to GHC to prove
> that indeed, 'mirror x (mirror x) = x' since with a type family we can
> express 'mirror' as a type level function via type families. It uses
> Ryan Ingram's approach to lightweight dependent type programming in
> Haskell.
>
> https://gist.github.com/750279
Thanks for the shout out :)
I think the type of your proof term is incorrect, though; it requires
the proof to be passed in, which is sort of a circular logic.
The type you want is
proof1 :: forall r x. BinTree x => ((x ~ Mirror (Mirror x)) => x -> r) -> r
proof1 t k = ...
Alternatively,
data TypeEq a b where Refl :: TypeEq a a
proof1 :: forall x. BinTree x => x -> TypeEq (Mirror (Mirror x)) x
proof1 t = ...
Here's an implementation for the latter
newtype P x = P { unP :: TypeEq (Mirror (Mirror x)) x }
baseCase :: P Tip
baseCase = P Refl
inductiveStep :: forall a b c. P a -> P c -> P (Node a b c)
inductiveStep (P Refl) (P Refl) = P Refl
proof1 t = unP $ treeInduction t baseCase inductiveStep
(I haven't tested this, but I believe it should work)
-- ryan
___
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
On Thu, Dec 23, 2010 at 8:19 AM, Daniel Peebles wrote: > Simulating bottoms wouldn't be too hard, but I don't think the statement is > even true in the presence of bottoms, is it? Isn't it? data Tree a = Tip | Node (Tree a) a (Tree a) mirror :: Tree a -> Tree a mirror Tip = Tip mirror (Node x y z) = Node (mirror z) y (mirror x) -- -- base cases mirror (mirror _|_) = mirror _|_ = _|_ mirror (mirror Tip) = mirror Tip = Tip -- inductive case mirror (mirror (Node x y z)) = mirror (Node (mirror z) y (mirror x)) = Node (mirror (mirror x)) y (mirror (mirror z)) -- induction = Node x y z -- ryan ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
I think it's pretty legit. You aren't actually making a claim about the values in the tree but I think parametricity handles that for you, especially since you have existential types for the payload at every tree level (so you can't go shuffling those around). The only thing missing (and that you can't change in Haskell) is that your statement is about Mirror (Mirror x) == x, rather than mirror (mirror x) == x. mirror gives you Mirror but there's currently no proof to show that it's the only way to do it, so there's a missing step there, I think. Anyway, for those talking about the coinductive proof, I made one in Agda: http://hpaste.org/42516/mirrormirror Simulating bottoms wouldn't be too hard, but I don't think the statement is even true in the presence of bottoms, is it? Dan On Thu, Dec 23, 2010 at 9:27 AM, Sjoerd Visscher wrote: > > On Dec 21, 2010, at 6:57 PM, austin seipp wrote: > > > https://gist.github.com/750279 > > I took Austins code and modified it to run on a Tree GADT which is > parameterized by its shape: > > https://gist.github.com/752982 > > Would this count as a function mirror with proof that mirror (mirror x) == > x? > > -- > Sjoerd Visscher > > > > ___ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
On Dec 21, 2010, at 6:57 PM, austin seipp wrote: > https://gist.github.com/750279 I took Austins code and modified it to run on a Tree GADT which is parameterized by its shape: https://gist.github.com/752982 Would this count as a function mirror with proof that mirror (mirror x) == x? -- Sjoerd Visscher ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
On 22/12/2010 14:48, Artyom Shalkhakov wrote: > ..Do you want to prove a property of > a function formally, using some kind of formal logic? I am aware that functional languages do not do proofs at term level, but the motivation for my question is to get a precise reason why this is so. The replies from the café have clearly articulated the reasons. Thanks to all, Pat This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
On Tue, Dec 21, 2010 at 5:02 PM, Daniel Fischer wrote: > On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote: >> >> Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x. >> induction x; simpl; auto. >> rewrite IHx1; rewrite IHx2; trivial. >> Qed. > > Since mirror (mirror x) = x doesn't hold in Haskell, I take it that Coq > doesn't allow infinite structures? Even if the theorem does hold with infinite structures, I don't really know the answer to your question. I'm just starting to study Coq in my free time =). My guess would be "no", because functions need to be total. But that's just a wild guess, and you shouldn't take my word for it =). Cheers! -- Felipe. ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
- Original Message > From: Colin Paul Adams > To: Daniel Fischer > Cc: [email protected] > Sent: Tue, December 21, 2010 1:11:37 PM > Subject: Re: [Haskell-cafe] Proof in Haskell > > >>>>> "Daniel" == Daniel Fischer writes: > > Daniel> On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote: > >> > > Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x. > >> induction x; simpl; auto. rewrite IHx1; rewrite IHx2; trivial. > >> Qed. > > Daniel> Since mirror (mirror x) = x doesn't hold in Haskell, I take > Daniel> it that Coq doesn't allow infinite structures? > > Why doesn't it hold? You are both onto something. It is true, but the Coq proof only covered finite trees. Infinite tree could be defined with coinduction, but even that doesn't allow the possibility of bottoms in the tree. CoInductive Tree (A:Set) := Branch (l r : Tree A) | Leaf. CoFixpoint mirror {A:Set} (x : Tree A) : Tree A := match x with | Leaf => Leaf A | Branch l r => Branch A (mirror r) (mirror l) end. Also, you'd have to define some notion of Bisimilarity rather than working with the direct equality. CoInductive bisimilar {A : Set} : Tree A -> Tree A -> Prop := | bisim_Leaf : bisimilar (Leaf A) (Leaf A) | bisim_Branch (l1 r1 l2 r2 : Tree A) : bisimilar l1 l2 -> bisimilar r1 r2 -> bisimilar (Branch A l1 r1) (Branch A l2 r2). I was hoping to write a proof, but it's much more annoying to work with coinductive definitions. Brandon ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
On Tuesday 21 December 2010 20:11:37, Colin Paul Adams wrote: > > "Daniel" == Daniel Fischer > > writes: > > Daniel> On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote: > > Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x. > > > >> induction x; simpl; auto. rewrite IHx1; rewrite IHx2; trivial. > >> Qed. > > Daniel> Since mirror (mirror x) = x doesn't hold in Haskell, I take > Daniel> it that Coq doesn't allow infinite structures? > > Why doesn't it hold? Hit send before I finished thinking, it should hold. ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
> "Daniel" == Daniel Fischer writes: Daniel> On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote: >> > Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x. >> induction x; simpl; auto. rewrite IHx1; rewrite IHx2; trivial. >> Qed. Daniel> Since mirror (mirror x) = x doesn't hold in Haskell, I take Daniel> it that Coq doesn't allow infinite structures? Why doesn't it hold? -- Colin Adams Preston Lancashire () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
I wrote: > On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote: >> >> Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x. >> induction x; simpl; auto. >> rewrite IHx1; rewrite IHx2; trivial. >> Qed. > Since mirror (mirror x) = x doesn't hold in Haskell, I take it that Coq > doesn't allow infinite structures? Oops, mirroring infinite binary trees should work. Ignore above. ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote: > > Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x. > induction x; simpl; auto. > rewrite IHx1; rewrite IHx2; trivial. > Qed. Since mirror (mirror x) = x doesn't hold in Haskell, I take it that Coq doesn't allow infinite structures? ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
On Tue, Dec 21, 2010 at 3:57 PM, austin seipp wrote:
> However, at one point I wrote about proving exactly such a thing (your
> exact code, coincidentally) in Haskell, only using an 'extraction
> tool' that extracts Isabelle theories from Haskell source code,
> allowing you to prove such properties with an automated theorem
> prover.
You may also write your program, for example, using Coq and then extract
correct Haskell code from it. I'm far from a Coq expert so there must be a
better way, but the following works =):
Inductive Tree (A : Type) :=
| Tip : Tree A
| Node : Tree A -> A -> Tree A -> Tree A.
Fixpoint mirror {A : Type} (x : Tree A) : Tree A :=
match x with
| Tip => Tip A
| Node l v r => Node A (mirror r) v (mirror l)
end.
Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
induction x; simpl; auto.
rewrite IHx1; rewrite IHx2; trivial.
Qed.
Extraction Language Haskell.
Recursive Extraction mirror.
Then Coq generates the following correct-proven code:
data Tree a = Tip
| Node (Tree a) a (Tree a)
mirror :: (Tree a1) -> Tree a1
mirror x =
case x of
Tip -> Tip
Node l v r -> Node (mirror r) v (mirror l)
Cheers! =)
--
Felipe.
___
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
Patrick, Dependent types are program types that depend on runtime values. That is, they are essentially a type of the form: f :: (a :: X) -> T where 'a' is a *value* of type 'X', which is mentioned in the *type* 'T'. You do not see such things in Haskell, because Haskell separates values from types - the language of runtime values, and the language of compile-time values are separate by design. In dependently typed languages, values and types are in fact, the same terms and part of the same language, not separated by compiler phases. The distinction between runtime and compile time becomes blurry at this stage. By the Curry-Howard isomorphism, we would like to make a proof of some property, particularly that "mirror (mirror x) = x" - but by CH, types are the propositions we must prove, and values are the terms we must prove them with (such as in first-order or propositional logics.) This is what Eugene means when he says it is not possible to prove this at the value level. Haskell cannot directly express the following type: forall a. forall x:Tree a, mirror (mirror x) = x We can think of the 'forall' parts of the type as bringing the variables 'a' and 'x' into scope with fresh names, and they are universally quantified so that this property is established for any given value of type 'a'. As you can see, this is a dependent type - we establish we will be using something of type a, and then we establish that we also have a *value* x of type 'Tree a', which is mentioned finally by saying that 'mirror (mirror x) = x'. Because we cannot directly express the above type (as we cannot mix runtime values and type level values) we cannot also directly express a proof of such a proposition directly in Haskell. However, if we can express such a type - that is, a type which can encode the 'Mirror' function - it is possible to construct a value-level term which is a proof of such a proposition. By CH, this is also possible, only not nearly as palatable because we encode the definition of 'mirror' at the value level as well as the type level - again, types and values in haskell exist in different realms. With dependent types we only need to write 'mirror' *once* because we can use it at both the type and value level. Also, because dependently typed languages have more expressive type systems in general, it quickly becomes a burden to do dependent-type 'tricks' in Haskell, although some are manageable. For amusement, I went ahead and actually implemented 'Mirror' as a type family, and used a little bit of hackery thanks to GHC to prove that indeed, 'mirror x (mirror x) = x' since with a type family we can express 'mirror' as a type level function via type families. It uses Ryan Ingram's approach to lightweight dependent type programming in Haskell. https://gist.github.com/750279 As you can see, it is quite unsatisfactory since we must encode Mirror at the type level, as well as 'close off' a typeclass to constrain the values over which we can make our proof (in GHC, typeclasses are completely open and can have many nonsensical instances. We could make an instance for, say 'Mirror Int = Tip', for example, which breaks our proof. Ryan's trick is to encode 'closed' type classes by using a type class that implements a form of 'type case', and any instances must prove that the type being instantiated is either of type 'Tip' or type 'Node' by parametricity.) And well, the tree induction step is just a little bit painful, isn't it? So that's an answer, it's just probably not what you wanted. However, at one point I wrote about proving exactly such a thing (your exact code, coincidentally) in Haskell, only using an 'extraction tool' that extracts Isabelle theories from Haskell source code, allowing you to prove such properties with an automated theorem prover. http://hacks.yi.org/~as/posts/2009-04-20-A-little-fun.html Of course, this depends on the extractor tool itself being correct - if it is not, it could incorrectly translate your Haskell to similar but perhaps subtly wrong Isabelle code, and then you'll be proving the wrong thing! Haskabelle also does support much more than Haskell98 if I remember correctly, although that may have changed. I also remember reading that Galois has a project of having 'provable haskell' using Isabelle, but I can't verify that I suppose. On Tue, Dec 21, 2010 at 5:53 AM, Patrick Browne wrote: > Hi, > In a previous posting[1] I asked was there a way to achieve a proof of > mirror (mirror x) = x > > in Haskell itself. The code for the tree/mirror is below: > > 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 > > The reply from Eugene Kirpichov was: >>> 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", >>>
Re: [Haskell-cafe] Proof in Haskell
Hi Patrick, Indeed, you cannot really write proofs in Haskell because it is just an ordinary (more or less) programming language and not a theorem prover. (As an aside: you could write "tests", i.e. properties which may or may not be theorems about your program, and test them on random data (see QuickCheck), or exhaustively---if you managed to test a property for all possible inputs, then you have essentially proved it.). Now about dependent types. Some programming languages have very expressive type systems (even more so then Haskell!) and they allow for types which are parameterized by values. Such types are called "dependent types". Here is an example: decrement :: (x :: Int) -> (if x > 0 then Int else String) decrement x = if x > 0 then x - 1 else "Cannot decrement" This function maps values of type "Int" to either "Int"s or "String"s. Note that the _type_ of the result of the function depends on the _value_ of the input, which is why this function has a dependent type. It turns out---and this is not at all obvious at first---that languages with dependent types (and some other features) are suitable not only for writing programs but, also, for proving theorems. Theorems are expressed as types (often, dependent types), while proofs are programs inhabiting the type of the theorem. So, "true" theorems correspond to types which have some inhabitants (proofs), while "false" theorems correspond to empty types. The correspondence between "proofs-theorems" and "programs-types" is known as the Curry-Howard isomorphism. Examples of some languages which use depend types are Coq, Agda, and Cayenne. I hope that this helps, -Iavor PS: The "forall"s in your example are just depend function types: in this setting, to prove "forall (x :: A). P x" amounts writing a function of type: "(x :: A) -> P x". In other words, this is a function, that maps values of type "A" to proofs of the property. Because the function can be applied to any value of type "A", we have prove the result "forall (x::A). P x)". The dependent type arises because the property depends on the value in question. On Tue, Dec 21, 2010 at 8:15 AM, aditya siram wrote: > I don't know the formal definition, but dependent types seem analogous > to checking an invariant at runtime. > -deech > > On Tue, Dec 21, 2010 at 5:53 AM, Patrick Browne wrote: >> Hi, >> In a previous posting[1] I asked was there a way to achieve a proof of >> mirror (mirror x) = x >> >> in Haskell itself. The code for the tree/mirror is below: >> >> 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 >> >> The reply from Eugene Kirpichov was: 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. >> >> Could anyone explain what *dependent types* mean in this context? >> What is the exact meaning of forall a and forall x? >> >> Thanks, >> Pat >> [1] http://www.mail-archive.com/[email protected]/msg64842.html >> >> >> >> >> >> >> >> >> This message has been scanned for content and viruses by the DIT Information >> Services E-Mail Scanning Service, and is believed to be clean. >> http://www.dit.ie >> >> ___ >> Haskell-Cafe mailing list >> [email protected] >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > > ___ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
I don't know the formal definition, but dependent types seem analogous to checking an invariant at runtime. -deech On Tue, Dec 21, 2010 at 5:53 AM, Patrick Browne wrote: > Hi, > In a previous posting[1] I asked was there a way to achieve a proof of > mirror (mirror x) = x > > in Haskell itself. The code for the tree/mirror is below: > > 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 > > The reply from Eugene Kirpichov was: >>> 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. > > Could anyone explain what *dependent types* mean in this context? > What is the exact meaning of forall a and forall x? > > Thanks, > Pat > [1] http://www.mail-archive.com/[email protected]/msg64842.html > > > > > > > > > This message has been scanned for content and viruses by the DIT Information > Services E-Mail Scanning Service, and is believed to be clean. > http://www.dit.ie > > ___ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
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 [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
