On Sat, 29 Dec 2007 13:30:03 +0200, Luke Palmer <[EMAIL PROTECTED]> wrote:
On Dec 29, 2007 11:14 AM, Cristian Baboi <[EMAIL PROTECTED]>
wrote:
In The Implementation of Functional Programming Languages by S.P. Jones,
section 2.5.3, page 32 it is written:
Eval [[*]] a b = a x b
Eval [[*]] _|_ b = _|_
Eval [[*]] a _|_ = _|_
but in section 2.5.2 it is said that _|_ is an element of the value
domain.
What business does it have on the left side of the '=' ?
I don't know the book you're talking about, but I suspect that this is
not
a definition of a function in a language, but rather the denotational
semantics
for a function.
Yes. Eval is the thing that do that.
Just as mathematics is allowed to categorize all
turing machines
into two categories (those that halt and those that do not), even
though to actually
do this is impossible, so too can mathematics talk about what a function
returns
when given _|_, even though it is impossible in general to know when
you actually
do have _|_ or you're just waiting for a value.
What confused me is the Eval seems to be defined by recursion, but maybe
it is not.
It would have been clear if it was written
Eval [[*]] env = x where x is extended to handle _|_
The "recursivity" I was talking about is:
Eval([[\x.E]], env) a = Eval([[E]], env[x=a])
Eval([[E1 E2]],env) = Eval([[E1]],env) (Eval([[E2]],env))
It appears as if lambda calculus is defined by lambda calculus.
These are equations that Eval must satisfy, but the text call '=' 'define'
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe