As we have discussed in the introductory lecture, we shall deal first with the Lambda calculus, then with its type version, the typed l-calculus, and finally with the p-calculus.
The l-calculus is the formalism for describing functions. It is one of the most important and the first universal model of computation, of sequential computation; while the p-calculus is trying to become 'the' universal or 'a' universal model of concurrent and mobile computation.
So, I will first give a brief introduction to l-calculus.
First, a few dates. It was invented in the late '30s by Church. Then Landin in the early '60s together with Bohm realised that it was a very good meta-language for programming languages, and then finally Barendregt developed its theory to a greater depth.
The l-calculus has an extremely simple syntax: you have variables, abstraction, application. It has a very simple reduction semantics, that essentially amounts to term re-writing where there is a very simple rule of re-writing: it is just a replacing a term for all occurrences of the bound variable.
There is another notion which is important, and it has to do with the fact that this l is a binding operation; and therefore the name of the variable is not meaningful, if we replace all occurrences of the variable 'x' with the variable 'y', which does not occur free in N. That is, if we operate an alpha conversion, the intended meaning of the term is preserved .
So this very syntax is extremely powerful because it captures this basic concept of re-writing and replacing. A very important theorem amid the Church-Rosser theorem which essentially states that this calculus is consistent.