CODEWITHSUNDEEP
lambdalambda-calculus
yuxingdubai
yuxingdubai

Reputation: 53

In lambda calculus, what if apply expression to an non-function expression?

I'm new to Lambda Calculus. I've read about definition of lambda expression on Wikipedia.

The set of lambda expressions, Λ, can be defined inductively:

  1. If x is a variable, then x ∈ Λ
  2. If x is a variable and M ∈ Λ, then (λx.M) ∈ Λ
  3. If M, N ∈ Λ, then (M N) ∈ Λ

Instances of rule 2 are known as abstractions and instances of rule 3 are known as applications.

I know the meaning of rule 2 when the M is a function abstraction, that is in the form of (λx.E) .

But What is the meaning when M is not a function? Such as, just a variable x or an non-function expression x + y

Upvotes: 2

Views: 377

Answers (2)

user6428287
user6428287

Reputation:

Lambda calculus consists in a context-free grammar

E ::= v        Variable
   |  λ v. E   Abstraction
   |  E E      Application

where v ranges over variables, together with the beta- and eta-reduction rules

(λ x. B) E  ->  B   where every occurrence of x in B in substituted by E
  λ x. E x  ->  E   if x doesn't occur free in E

a is free in λ b. b a, but not in λ a. λ b. b a. An expression to which neither of the two reduction rules apply is in normal form.

So, if M N is not a beta-redex (λ x. B) E, and both M and N are in normal form, then M N whole is in irreducible normal form.

Upvotes: 1

Andrea Asperti
Andrea Asperti

Reputation: 1003

So, the meaning of (M N) is clear to you when M is a function. Let us consider the case of the identity, for simplicity, i.e. M = I = \x.x.

                          (*)    (\x.x) N

that reduces to N. Suppose now you want to make your program a bit more generic. You do not want to just apply the identity to N, but apply a generic function f that you take as input. So, you replace \x.x with f and abstract the whole term w.r.t. f:

                                 \f.f N

that must be understood as \f.(f N). Pretty simple.

You can now feed the identity as argument to the previous term, to obtain a term equivalent to (*):

                       (\f.f N) \x.x = \x.x N

To make things even more complex, you may imagine to process your input function f before applying it to N. For instance, if you expect a binary (currified) function as input, you may wish to apply f to the "pair" of arguments (N,N), that, since f is currified, amounts to pass N as argument twice:

                        (**)    \f. f N N

to be understood as \f. ((f N) N). So, you clearly see the point of having applications in functional position of other applications.

To see the previous example at work, take the term K = \x.\y.x, instead of the identity. K eats two arguments ad returns the first. If you feed K as input to the previous term you still get a term equivalent to (*)

                       (\f.f N N) K = K N N = N

In general, programming languages are a way of providing abstractions. To abstract with respect to a notion you need first of all a way to give a name to instances of the notion. For instance, in an imperative language, a variable is essentially an abstraction of a memory cell. To abstract with respect to functions you need the possibility to use names for functions. The second step, it to allow notions to be "expressible", that is to provide a language of expressions that allows to dynamically synthetise new instances of the given notion (in our case, new functions). The lambda calculus is just a core calculus where functions are (directly) expressible.

Upvotes: 1

Related Questions