[Haskell-cafe] Sending bottom to his room
cristian.baboi at gmail.com
Sat Dec 29 07:39:06 EST 2007
On Sat, 29 Dec 2007 13:30:03 +0200, Luke Palmer <lrpalmer at gmail.com> wrote:
> On Dec 29, 2007 11:14 AM, Cristian Baboi <cristian.baboi at gmail.com>
>> 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
>> 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
> a definition of a function in a language, but rather the denotational
> 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
> 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'
More information about the Haskell-Cafe