At 14:30 +0000 98/10/26, Peter Thiemann wrote:
>> Haskell translates f f = f into f := f |-> f; on the right hand side
>>"f" is a bound variable, on the left hand side "f" is a name. Suppose I
><inidicate variables with a slash, then the formula would read
>> f := \f |-> \f
>>> or f(\f) := \f.
>
>I don't really understand your remark. f f = f as a toplevel
>definition is equivalent to (in this special case)
>
>letrec ...
> f = \f -> f
> ...
I just avoid using Haskell notation in order to not get the notation
confused as Haskell does.
>It's not different logical entities, all occurrences of f are variables.
Different occurrences of f have different semantic meaning (that is, the
"f" in one place is not the same as the "f" in another place).
>It's not Haskell that's causing the confusion if any, it's the lambda
>calculus, more precisely: alpha-conversion.
The original question was this: What is the meaning of "f(f) = f"? I
remarked that in this case Haskell has a very good strategy, namely
interpreting it as the expression f := f |-> f, or "f is assigned the
expression lambda f f" if you so want; the lack of such a good strategy
seemed to cause the other problems discussed in this thread.
Otherwise, the naming of functions is not part of the lambda calculus;
one must add an interpretation of this lambda calculus in order to arrive
at a meaning of an assignment in the computer sense. (For example, if I
define \f to denote a free variable, I could assign f := \f + 1, and later
bind this \f by the assignment f := \f |-> f, which would work out to the
increment function. In this example, free variables and symbol table names
have a distinctly different behavior.)
Hans Aberg
* Email: Hans Aberg <mailto:[EMAIL PROTECTED]>
* Home Page: <http://www.matematik.su.se/~haberg/>
* AMS member listing: <http://www.ams.org/cml/>
