From there, the proofs are by induction over the expression. Another proof obligation is the substitution lemma itself, i.e. the substitution of the typing, which finally establishes the all-quantification. The later cannot formally be proven, since no such syntax is at hand. Extensions Recursive definitions To make programming practical recursive functions are needed. A central property of the lambda calculus is that recursive definitions are not directly available, but can instead be expressed with a fixed point combinator. But unfortunately, the fixpoint combinator cannot be formulated in a typed version of the lambda calculus without having a disastrous effect on the system as outlined below. Typing rule The original paper shows recursion can be realized by a combinator . A possible recursive definition could thus be formulated as . Alternatively an extension of the expression syntax and an extra typing rule is possible: where basically merging and while including the recursively defined variables in monotype positions where they occur to the left of the but as polytypes to the right of it. Consequences While the above is straightforward it does come at a price. Type theory connects lambda calculus with computation and logic. The easy modification above has effects on both: The strong normalisation property is invalidated, because non-terminating terms can be formulated. The logic collapses because the type becomes inhabited. Overloading Overloading means that different functions can be defined and used with the same name. Most programming languages at least provide overloading with the built-in arithmetic operations (+,<,etc.), to allow the programmer to write arithmetic expressions in the same form, even for different numerical types like int or real. Because a mixture of these different types within the same expression also demands for implicit conversion, overloading especially for these operations is often built into the programming language itself. In some languages, this feature is generalized and made available to the user, e.g. in C++. While ad hoc overloading has been avoided in functional programming for the computation costs both in type checking and inference, a means to systematise overloading has been introduced that resembles both in form and naming to object oriented programming, but works one level upwards. "Instances" in this systematic are not objects (i.e. on value level), but rather types. The quicksort example mentioned in the introduction uses the overloading in the orders, having the following type annotation in Haskell: quickSort :: Ord a => [a] ->