*λ*calculus which we call it term, then the following syntax shows almost the fundamental of this system:

*T := x | c |*

*λx.*

*T | T T*

The above means that every term in

*λ*calculus can be a variable like

*x*or a constant value like

*c*, an abstraction like

*λx.*

*T*or an application like

*T T*.

The only thing which is a bit new in this notation is that we never show an abstraction like

*λx.*

*T*which is exactly like something

*λx.* 2 x,*if we just assume

*T*equals

** 2 x.*We also are not familiar with

*T T*which is a general form of application, we saw examples like

*(λxy.* x y) 5 10*or

*(λx.* 2 x) x*or

*(λx.x) λx.x ,*... and if you look at them carefully, you'll see these are nothing but

*T T.*We just used parentheses to explicitly show which part of the expression is the abstraction and which part is the term we want to pass to the abstraction, in fact we used

*(T) T*instead of

*T T*.

*λ*terms are in prefix notation so we evaluate them from left to right, this means the applications also evaluated this way like the one we talked about in short in last paragraph:

*T T1 T2 ... Tn*≡

*( ... ((T T1) T2) ... Tn)*

*You can assume that*

*λ*is a binding operator which binds the attached variable to its following expression. So for

*λx.*

*T ,*variable

*x*is bounded to term

*T*. If

*T*contains

*x*we call

*x*as a bound variable and if

*T*doesn't contain

*x*we call it free or sometimes unbound variable. A term in λ calculus is called closed if there are no unbound variables in it.

So for a term like

*λy.- ((λx.+ y x) x) x*, variable

*x*is bounded to

*λx*but

*y*is free related to

*λx.*And for

*λy*variable x is free. A good practice is to see how we can find a simpler or reduced version of this term. The application

*(λx.+ y x) x*result is

*+ y x*if we use it in the main term we will have

*λy.-*

*+ y x x*or

*λ*

*y.*

*y*!

**Some abstractions**

Constant:

*λx.0 // returns 0 regardless of what x is*

Identity:

*λx.x*

*// returns the passed argument*

Selection:

*λxyz.y*

*// returns the selected argument regardless of the others*

**A new assumption from now on**

Since writing expressions in prefix notation is not what we mostly are familiar with it, we will start using normal infix notation for

*λ*calculus terms. So from the next post instead of writing

*λx.+ y x*we will have

*λx.y+x,*which is easier for us to read and understand. The reason is we are going to talk about using functional programming in Java and most of the other programming languages even many of the pure functional ones uses infix notation. Even in Lisp, expressions are not fully in prefix notation, so since we are not going to study mathematics let us accept this assumption to make life easier.

## No comments:

## Post a Comment