* Wouter Swierstra w...@cs.nott.ac.uk [2009-02-19 11:58:38+0100]
There are several problems with this approach.
For example, I can show:
const 0 (head []) = 0
But if I pretend that I don't know that Haskell is lazy:
const 0 (head []) = const 0 (error ) = error ...
Where does the last
On Thu, 2009-02-19 at 23:06 +0200, Roman Cheplyaka wrote:
* Wouter Swierstra w...@cs.nott.ac.uk [2009-02-19 11:58:38+0100]
There are several problems with this approach.
For example, I can show:
const 0 (head []) = 0
But if I pretend that I don't know that Haskell is lazy:
const
Roman Cheplyaka schrieb:
Evaluation order matters for operational semantics, not for axiomatic.
And even in operational semantics Church–Rosser theorem should prevent
getting different results (e.g. 0 and error) for different evaluation
orders.
Let's consider
omega = omega
const omega 42
* Tillmann Rendel ren...@cs.au.dk [2009-02-19 22:43:24+0100]
Roman Cheplyaka schrieb:
Evaluation order matters for operational semantics, not for axiomatic.
And even in operational semantics Church–Rosser theorem should prevent
getting different results (e.g. 0 and error) for different
I am surprised that no one has mentioned David Sands' work yet in this
thread. He has studied this issue extensively in the nineties (setting
out from an analogous problem as the one given in Neil's original post).
There are a number of papers that came out of this. The one probably
most
Janis Voigtlaender wrote:
()
http://portal.acm.org/citation.cfm?doid=227699.227716
This paper cites works by L. Kott, but not his PhD thesis Des
substitutions dans les systemes d'equations algebriques sur le magma
(Univ. Paris VII, 1979) which is (as far as I can remember) among the
Hi
Haskell is known for its power at equational reasoning - being able to
treat a program like a set of theorems. For example:
break g = span (not . g)
Which means we can replace:
f = span (not . g)
with:
f = break g
by doing the opposite of inlining, and we still have a valid program.
Neil Mitchell wrote:
Hi
Haskell is known for its power at equational reasoning - being able to
treat a program like a set of theorems. For example:
break g = span (not . g)
Which means we can replace:
f = span (not . g)
with:
f = break g
by doing the opposite of inlining, and we still
Hi Neil
You'll be pleased to know that lots of people have been banging their
heads
off this one.
On 22 Jul 2007, at 15:53, Neil Mitchell wrote:
[..]
break g = span (not . g)
[..]
However, if we use the rule that anywhere we encounter span (not . g)
we can replace it with break g then
On 7/22/07, Neil Mitchell [EMAIL PROTECTED] wrote:
However, if we use the rule that anywhere we encounter span (not . g)
we can replace it with break g then we can redefine break as:
break g = break g
For some reason this reminds me of the paradoxes of being able to go back in
time. What I
Note that you can take any closed term e and do the following
equational reasoning:
e
== let x = e in x
== let x = x in x
== _|_
Technically, though, this is not wrong, in that it is still
consistent, where consistency is defined using the usual information
ordering on domains. Conventional
Haskell is known for its power at equational reasoning - being able
to treat a program like a set of theorems.
when you're trying to do equational reasoning, you better make
sure that you're reasoning with equations. as others have pointed
out some of the more interesting relations between
It seems to me that the best answer, rather than constraining equational
reasoning, is to recognize what we're doing.
We start out with a specification for the program we're writing (this could be
a Haskell script for a previous version of the program, or just a set of
equations (or other
13 matches
Mail list logo
