Application in mathematics is when you choose some values from a function domain and compute the function result for the given arguments, which will be in the range of course. So simply for function f(x)=2x from N to N, f(2)=4 or f(10)=20 are applications. Or for f(x,y)=xy from NxN to N we have applications like f(1,2)=2 or f(5,10)=50 and ...
In λ calculus, the notation for the above examples are like the followings:
- f(x)=2x , x=2 => (λx.* 2 x) 2 // sometimes like (λx.* 2 x 2) but it is a bit ambiguous especially if we don't now * operates on how many operands so i prefer the first version
- f(x,y)=xy , x=5, y=10 => (λxy.* x y) 5 10 or (λx.(λy.* x y) 10) 5
Note in the first example we don't write λx.* 2 x 2 which means the multiplication operator operates on any number of operands and multiply them which means (4x in this case), so we have to use parentheses to show this is an application otherwise it is totally something else. So always use open and close parentheses to show an application.
The second example may be a bit complex, let us talk about it. We are going to show what λxy.* x y can be interpreted to something a bit easier to understand. We can write λxy.* x y like λx.(λy.* x y) which is nothing but an anonymous function with bound variable x. The term which this function (λx) returns is another function which is λy.* x y with bound variable y and the free variable x.
Now if we want the result of application (λxy.* x y) 5 10 we can convert it to some more understandable form to calculate the result. It is clear that (λy.* x y) 10 returns expression like * x 10 so the result of application (λy.* x y) 10 is * x 10, now we have the application (λx.* x 10) 5 which comes to 50.
There is no limit to have application like (λx.* 2 x) x which comes to expression * 2 x. Note this result is not an anonymous function, but an expression or term. Here are some other examples of applications:
- (λx.+ x x) x = + x x = * 2 x
- (λx.+ x y) y = + y y = * 2 y
- (λxy.+ x y) x x = + x x = * 2 x
- (λxy.+ x y) 0 = (λx.λy.+ x y) 0 = (λx.(λy.+ x y)) 0 = λy.y
- (λx.x) λx.x = λx.x // the λx.x function is called identity function
- (λx.x x x) x = x x // note that the term x x is not reducible more
