Send Beginners mailing list submissions to
[email protected]
To subscribe or unsubscribe via the World Wide Web, visit
http://www.haskell.org/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Formal proof with haskell (Sebastien Lannez)
2. Re: Formal proof with haskell (Daniel Fischer)
----------------------------------------------------------------------
Message: 1
Date: Tue, 20 Sep 2011 14:53:02 +0200
From: Sebastien Lannez <[email protected]>
Subject: [Haskell-beginners] Formal proof with haskell
To: [email protected]
Message-ID:
<CAEb8wO=Ad2comSPFyawoD0QgwBwSEaU-7bDB=niyzbwc4y+...@mail.gmail.com>
Content-Type: text/plain; charset=ISO-8859-1
Dear all,
I am currenlty learning Haskell.
I want to use it to solve combinatorial problems.
I want Haskell to prove a simple logical assertion (a tautology) ...
Unfortunately, I failed to express it in Haskell.
The logical proposition:
proof1 x z = ( (not (x<z)) || ( (x<y) && (y<z) )
where y = (x+z)/2
It is easy to see that simple substitution lead to
proof1 x z = (not (x<z)) || (x<z) = True
Is Haskell smart enough to automatically solve such tautology ?
------------------------------------------
S?bastien Lannez
Expert Optimisation
------------------------------------------
www: http://www.lannez.fr
tel. (home): +33 9 81 16 50 74
tel. (office): +33 1 64 47 85 73
mob.: +33 6 31 82 32 19
------------------------------------------
------------------------------
Message: 2
Date: Tue, 20 Sep 2011 16:02:45 +0200
From: Daniel Fischer <[email protected]>
Subject: Re: [Haskell-beginners] Formal proof with haskell
To: [email protected]
Cc: Sebastien Lannez <[email protected]>
Message-ID: <[email protected]>
Content-Type: Text/Plain; charset="iso-8859-1"
On Tuesday 20 September 2011, 14:53:02, Sebastien Lannez wrote:
> Dear all,
>
> I am currenlty learning Haskell.
>
> I want to use it to solve combinatorial problems.
>
> I want Haskell to prove a simple logical assertion (a tautology) ...
> Unfortunately, I failed to express it in Haskell.
>
> The logical proposition:
> proof1 x z = ( (not (x<z)) || ( (x<y) && (y<z) )
> where y = (x+z)/2
>
> It is easy to see that simple substitution lead to
> proof1 x z = (not (x<z)) || (x<z) = True
>
> Is Haskell smart enough to automatically solve such tautology ?
No. It's not a tautology without some extra assumptions, such as that (<)
be a total order compatible with the arithmetic of the domain (and (x+z)/2
exists for all x and z and is different from either x or z).
The compiler cannot make such assumptions.
Another problem is that
isItTrue :: Bool
isItTrue = b || not b
where
b = {- some expression of type Bool -}
is not equivalent to True, since b might not terminate.
So the most you could get from the latter is (b `seq` True).
In the first version of proof1, there are more potential points of
nontermination, so the compiler cannot rewrite it to the second version.
And, in particular, the two versions of proof1 can give different results
without nontermination even with fairly run-of-the-mill datatypes, like
Double:
Prelude> let x :: Double; x = 0.0
Prelude> let z :: Double; z = 0.5^1074
Prelude> not (x < z) || (x < z)
True
Prelude> let y = (x+z)/2 in not (x < z) || ((x < y) && (y < z))
False
Prelude>
So, to rewrite
proof1 = not (x < z) || ((x < y) && (y < z))
where
y = (x+z)/2
to
proof1 = True
and be sure you have not changed the meaning of proof1, you need a lot of
information not available to the compiler (it may be possible to make that
information available to the compiler in languages like Agda or Coq, but I
wouldn't bet on it).
------------------------------
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
End of Beginners Digest, Vol 39, Issue 24
*****************************************
