[Haskell-cafe] Sending bottom to his room

[Jonathan Cast]

On 29 Dec 2007, at 6:39 AM, Cristian Baboi wrote:

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

Right.  There's a convention in CS that any object may be defined by  
giving a list of conditions, to which is implicitly added the  
understanding that the object in question is in some sense the  
`least' object satisfying those conditions.  So Eval is `defined' by  
those equations in the sense that its graph is the least relation  
closed under the equations given.

jcc