Is abstraction needed for application?
Author Message
Is abstraction needed for application?

Recently I've encountered some papers where I needed to pick up some
of the terminology of Lambda calculus to understand. I've begun
reading Lambda Caculus with Types by Barendregt, and something in
there confused me.

Specifically an example he writes:
Application and abstraction work together in the following intuitive
formula[L stands for lambda TO]:
(Lx.x^2+1)3 denotes the function x |--->x^2+1 applied to the
argument 3 giving 3^2+1=10.

What I am confused about is that this example seems to imply that
you need to use abstraction to make application work. Why couldn't
you just do:
(x^2+1,3) |-->10?

Or is this just an example he made up with not much meaning that way?

Tue, 31 Aug 2004 18:20:04 GMT
Is abstraction needed for application?

Quote:
> I've begun reading Lambda Caculus with Types by Barendregt,
> and something in there confused me.
>Specifically an example he writes:
>  Application and abstraction work together in the following intuitive
>formula[L stands for lambda TO]:
>    (Lx.x^2+1)3 denotes the function x |--->x^2+1 applied to the
>argument 3 giving 3^2+1=10.
>What I am confused about is that this example seems to imply that
>you need to use abstraction to make application work. Why couldn't
>you just do:
>     (x^2+1,3) |-->10?

Hi,

If e1 and e2 are (any) expressions in the language of lambda calculus, then

e1 e2

is also an expression in the language.

We say "e1 e2" is an application, and it is simply a syntactic entity.

We can attempt to simplify an expression into something called
a normal form (something akin to the simplest form of an expression).
That's the job of "reduction". To quote Reynolds [1]

... the process of reduction should simplify an expression or
make its meaning more explicit, without changing that meaning.

The rules of reduction are usually named alpha, beta and eta. Note that
some expressions do not have a normal form (ie reduction on them fails
to terminate).

Beta reduction is the rule for applications. In particular, beta reduction
requires that the left expression in an application
_reduces to_ a function.

Functions are expressed in the language as lambda abstractions, ie,
if x is a variable, and e is an expression, then

Lx.e

is also an expression in the language (where L is a lambda symbol).
The whole expression denotes a function.

In terms of reduction, lambda abstraction introduces variables, and
beta reduction eliminates them (by substitution).

So, yes in the sense of reduction, abstraction and application
"work together".

One intuition behind type checking, is that we would like to avoid
attempting to reduce applications where the left expression
does not reduce to a function. In particular, we would like to
be able to determine this without having to begin reduction.

I don't understand your final question.

Hope this helps,
Bernie.

[1] John C. Reynolds, "Theories of Programming Languages". 1998.
Cambridge University Press.

Wed, 01 Sep 2004 14:40:03 GMT
Is abstraction needed for application?
As it says in the previous reply to this message, beta-reduction is
something that you need to look at. By the definition of
beta-reduction, when you apply an application Lx.<something> to another
term <appTerm>, what you get as a result is a new term which is nothing
more than <something> with all the x's inside <something> replaced by
<appTerm> or in the correct syntax, <something>[<appTerm>/x]. Thus, to
answer your last question of why you cannot "just do" (x^2+1,3) is
because this term does not reduce(execute) by the definition of terms.

Mike Tikiliainen

Quote:
>Recently I've encountered some papers where I needed to pick up some
>of the terminology of Lambda calculus to understand. I've begun
>reading Lambda Caculus with Types by Barendregt, and something in
>there confused me.

>Specifically an example he writes:
>  Application and abstraction work together in the following intuitive
>formula[L stands for lambda TO]:
>    (Lx.x^2+1)3 denotes the function x |--->x^2+1 applied to the
>argument 3 giving 3^2+1=10.

>What I am confused about is that this example seems to imply that
>you need to use abstraction to make application work. Why couldn't
>you just do:
>     (x^2+1,3) |-->10?

>Or is this just an example he made up with not much meaning that way?

Wed, 01 Sep 2004 19:31:03 GMT
Is abstraction needed for application?

Quote:

>> I've begun reading Lambda Caculus with Types by Barendregt,
>> and something in there confused me.

>>Specifically an example he writes:
>>  Application and abstraction work together in the following intuitive
>>formula[L stands for lambda TO]:
>>    (Lx.x^2+1)3 denotes the function x |--->x^2+1 applied to the
>>argument 3 giving 3^2+1=10.

>>What I am confused about is that this example seems to imply that
>>you need to use abstraction to make application work. Why couldn't
>>you just do:
>>     (x^2+1,3) |-->10?

>I don't understand your final question.

You can define a-- well call it lamda-algebra ( I haven't seen anyone
name it ), as a 4-tuple: (V,S,( ),(L )); ( S is not the best symbol,
but it is the best symbol that I can type ) such that:
1) V is a subset of S.
2) (): SxS->S
(): (a,b)|->(a b)
( called application)
3)(L ):VxS->S
(L):(x,M)|->(Lx.M)
(called abstraction)

If s is an element of S then s is called a lambda-term.
Presumably the example I initially gave is from within a
lambda-algebra.
This would imply that x^2+1 and 3 are both lambda-terms.
So you can construct:
(x^2+1 3)
since you can make an application out of any two lambda-terms.

Why is it necessary to do ( unfortunately Barendregt abuses his
notation a bit, I'll fix it up below ),
( (Lx.x^2+1) 3)
(x^2+1 3)?
If it's not necessary why do it the first way, since both seem to be
equivalent?

Thu, 02 Sep 2004 17:11:30 GMT
Is abstraction needed for application?

Quote:
> Why is it necessary to do ( unfortunately Barendregt abuses his
> notation a bit, I'll fix it up below ),
> ( (Lx.x^2+1) 3)
> (x^2+1 3)?
> If it's not necessary why do it the first way, since both seem to be
> equivalent?

Perhaps the following, more complicated case would clarify things for
both you and others on this thread:  How would you write

((Lx. (Ly. x-y) 3) 5)

in "the second way", i.e., without L?

--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
http://dlis.gseis.ucla.edu/people/pagre/bar-code.html
http://dlis.gseis.ucla.edu/people/pagre/arguments.html

Thu, 02 Sep 2004 17:28:49 GMT

 Page 1 of 1 [ 5 post ]

Relevant Pages