This very simple system that we have called the type-free l-calculus is indeed a very powerful system. Church showed early that all computable functions are expressible in this calculus. All Turing computable functions may be encoded in this very simple framework. Here is a way in which we may encode natural numbers. We say that a term like this underlined "n" is a numeral; it is the encoding of the number n. By using this encoding, we can prove the following property. For any computable function f, there exists a term F, such that, for any n and any m, if the function f is defined on n and its value is m, then the term F applied to the numeral n will reduce to the normal form corresponding to the numeral m. On the other hand if f (n) is undefined, then F applied to n does not have a normal form. So, by this we may think of this very simple formal system as a fully-fledged programming language.

---