From: Charles Lin
Subject: Need genius for lambda calculus
Date: 
Message-ID: <1pgk0kINNdbb@mojo.eng.umd.edu>
    Actually, I am somewhat frightened about posting my question underneath
this title since I saw what happened to the first person.   However, this
is really not a homework question but something that has been bothering
me about lambda calculus.

    In lambda calculus, an application is usually written as something
like

        (A B)

   where A is typically an abstraction, and B the argument to that
abstraction.  So, for example,

       (Lx.(x + x)  4)

   will produce the result of 8.   Now, what happens if the A portion
of the application is NOT a function abstraction.   Then, what happens
if anything.   For example, is the following a legal lambda expression?
If so, what does it evaluate to?

      (x y)

   where x and y are variables.

   Thanks.

p.s. I doubt this requires a genius.

--
Charles Lin
····@eng.umd.edu

From: Jim Barnett
Subject: Re: Need genius for lambda calculus
Date: 
Message-ID: <BARNETT.93Apr2134901@paintbrush.mcc.com>
 I'm not an expert on the lambda calculus, but checking in Church's
"The Calculus of Lambda-Conversion", I find that (x y) - where x and y
are both variables - is a well-formed formula of the lambda calculus -
but it is in normal form and cannot be reduced further. So it just
sorta sits there -

- Jim 
From: Marty Hall
Subject: Re: Need genius for lambda calculus
Date: 
Message-ID: <C4x83C.5nM@aplcenmp.apl.jhu.edu>
In article <············@mojo.eng.umd.edu> ····@eng.umd.edu (Charles Lin) 
writes:
>    In lambda calculus, an application is usually written as something
>like  (A B)
>   where A is typically an abstraction, and B the argument to that
>abstraction.  So, for example,
>       (Lx.(x + x)  4)
>   will produce the result of 8.   Now, what happens if the A portion
>of the application is NOT a function abstraction.   Then, what happens
>if anything.   For example, is the following a legal lambda expression?
>If so, what does it evaluate to?
>      (x y)
>   where x and y are variables.

Well, in the pure (no predefined constants), untyped lambda calculus,
(x y) is a perfectly legal expression, even if x and y are free variables.
After all, at the bottom level what else is there besides functions, so how 
else can you interpret x?  Since beta reduction (evaluate the function with 
the supplied argument, where the function is an *explicit* abstraction 
[lambda form]) is your only way to do reductions, this cannot be reduced 
further. 

Now, in your example you used "+", so you seem to be implicitly using
an applied calculus. Even so, however, you still can interpret everything
as a function, so that (4 3) [call the function "4" on the value "3"] is
perfectly legal. Church numerals are one way to represent integers as
functions and still define addition, multiplication, etc.

However, if by your use of "+" and "4" in the above example you are implying
a typed lambda calculus, then (x y) is not legal unless the type of x
is x:a-->b and y is y:a. You still couldn't reduce it.

					- Marty

(proclaim '(inline skates))