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.