On May 23, 2010, at 2:53 AM, Lennart Augustsson wrote:
BTW, the id function works fine on bottom, both from a semantic and
implementation point of view.
Yes, but only because it doesn't work at all. Consider that calling
id undefined
requires evaluating undefined before you can call id.
Alexander Solla a...@2piix.com writes:
On May 23, 2010, at 1:35 AM, Jon Fairbairn wrote:
It seems to me relevant here, because one of the uses to which
one might put the symmetry rule is to replace an expression “e1
== e2” with “e2 == e1”, which can turn a programme that
terminates into a
That's totally false. You don't evaluate 'undefined' before calling 'id'.
(Or if you, it's because you've made a transformation that is valid
because 'id' is strict.)
On Mon, May 24, 2010 at 9:05 AM, Alexander Solla a...@2piix.com wrote:
Yes, but only because it doesn't work at all. Consider
Consider that calling
id undefined
requires evaluating undefined before you can call id. The program will
crash before you ever call id. Of course, the identity function should
have produced a value that crashed in exactly the same way. But we never got
there.
In which sense does id need
On Monday 24 May 2010 15:48:14, Jonas Almström Duregård wrote:
Consider that calling
id undefined
requires evaluating undefined before you can call id. The program will
crash before you ever call id. Of course, the identity function
should have produced a value that crashed in
Alexander Solla a...@2piix.com writes:
On May 22, 2010, at 1:32 AM, Jon Fairbairn wrote:
Since Bool is a type, and all Haskell types include ⊥, you need
to add conditions in your proofs to exclude it.
Not really. Bottom isn't a value, so much as an expression
for computations that don't
On May 23, 2010, at 1:35 AM, Jon Fairbairn wrote:
It seems to me relevant here, because one of the uses to which
one might put the symmetry rule is to replace an expression “e1
== e2” with “e2 == e1”, which can turn a programme that
terminates into a programme that does not.
I don't see how
For Bool, I'm not sure, but for, e.g., () it's certainly true.
Take this definition of ==
() == _ = True
Using case analysis of just the constructors, ignoring the value
bottom, you can easily prove symmetry.
But '() == undefined' terminates, whereas 'undefined == ()' does not.
Ignore bottom
On Sat, 2010-05-22 at 00:15 +, R J wrote:
I'm trying to prove that (==) is reflexive, symmetric, and transitive
over the Bools, given this definition:
(==) :: Bool - Bool - Bool
x == y = (x y) || (not x not y)
My question is: are the
R J rj248...@hotmail.com writes:
I'm trying to prove that (==) is reflexive, symmetric, and
transitive over the Bools, given this definition:
(==):: Bool - Bool - Bool
x == y = (x y) || (not x not y)
Since Bool is a type, and all Haskell types include ⊥, you need
to add conditions in
On May 22, 2010, at 1:32 AM, Jon Fairbairn wrote:
Since Bool is a type, and all Haskell types include ⊥, you need
to add conditions in your proofs to exclude it.
Not really. Bottom isn't a value, so much as an expression for
computations that don't refer to real values. It's close enough
Note that all (True ==) is logically equivalent to all id and to
the and function from the prelude.
A more general approach based on type classes, the function taut takes
a boolean function and determines (by exhaustive search) if it is a
tautology:
class BooleanFunction a where
taut :: a -
12 matches
Mail list logo
