[Haskell-cafe] Sending bottom to his room

[Cristian Baboi]

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>  
> 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'