Re: [Haskell-cafe] Sending bottom to his room

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

On Sat, 29 Dec 2007 13:30:03 +0200, Luke Palmer wrote:

...

On Dec 29, 2007 11:14 AM, Cristian Baboi 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