This formal core has been formalised well before computer sciences appeared in the '40s. It has been formalised by Alonzo Church in what he called the l-calculus or calculus of l-conversion. It is a very terse formal system and it is completely described here. The syntax is given by terms. Terms can be variables, or they may be abstractions (we write an abstraction by using this Greek letter l), or they may be applications, where one term is applied to another term. In the construct lx.M, the variable x is a bound variable. It is just a placeholder while l is a binder, like many other binders in mathematical languages, for instance, the integral sign in calculus. Computation in this formal system is explained by textual substitution, that is, by rewriting. When an abstraction is applied to another term, then in our intuition this is a function applied to an argument. Hence, in order to compute the value of the function, we take the actual parameter - N in this case - and we substitute it for the free occurrences of the formal parameter x inside the body of the function M. And this is the meaning of the notation M[N/x]: the substitution of M for the free occurrences of the variable x in M. Now, the actual, precise definition of this notion of substitution is quite tricky. Conceptually, however, it is simple and I think everybody will understand what is going on under this notion. I want you to pay attention to the fact that in this system there is nothing but symbols. This formal system and its computational process is just symbol pushing. There are no numbers, there is no arithmetic. There is nothing more than just symbol pushing.

---