 The syntax of \(\lambda\)-calculus is quite flexible. One can form all sorts of terms, even self-applications such as \(xx\). Such terms appear at first blush to be suspicious; one might suspect that using such terms could lead to inconsistency, and in any case one might find oneself reaching for a tool with which to forbid such terms. If one were to view functions and sets of ordered pairs of a certain kind, then the \(x\) in \(xx\) would be a function (set of ordered pairs) that contains as an element a pair \((x,y)\) whose first element would be \(x\) itself. But no set can contain itself in this way, lest the axiom of foundation (or regularity) be violated. Thus, from a set theoretical perspective such terms are clearly dubious. Below one can find a brief sketch of one such tool, type theory. But in fact such terms do not lead to inconsistency and serve a useful purpose in the context of \(\lambda\)-calculus. Moreover, forbidding such terms, as in type theory, does not come for free (e.g., some of the expressiveness of untyped \(\lambda\)-calculus is lost).