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.
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