Our main weapon is going to be beta-reduction (i.e. simple function application). The sub-expression which gets reduced is known as a redex. When you keep beta-reducing an expression you may reach the stage where there are no further reductions to be done.
A lambda expression is in normal form if no subexpression of it has the form (λx.P Q). [An expression is considered to be a subexpression of itself.]
Any abstraction
λ<variable1>.<expr>
can be converted to
λ<variable2>.<expr>/.<variable1> -><variable2> provided the substitution <expr> /. <variable1> -> <variable2> is sound.
In an abstraction λ<variable>.<expr> the <expr> is known as the scope of the abstraction.
Egs. λx.λy.(m x) has scope λy.(m x), and λy.(m x) has scope (m x)
An occurrence of a variable v in a lambda expression is bound if it is within the scope of an λv.<expr> abstraction.
Eg. in λx.λy.(m x) the occurrence of x is bound, but the occurrence of m is not bound.
There are widely differing conventions for notation. Let me explain what the problems are and some of the suggestions. We have to capture three types of thing... variables, abstractions, and applications and the problem is that many even quite simple expressions will contain lots of these. So if brackets are used, say with applications and abstractions, there will be lots of them or a bracket omitting convention will be needed coupled with left or right associativity.
The basic grammar for Lambda expressions is:
<expression> := <variable> | <function> | <application>
<function> := λ<variable>.<scope>
<application> := (<function expression> <argument expression>)
<scope>:= <expression>
<function expression>:= <expression>
<argument expression>:= <expression>
<variable>:= any string of characters (excepting ( λ . )) starting with a lower case letter