 Type theory enriches the untyped \(\lambda\)-calculus by requiring that terms be given types. In the untyped \(\lambda\)-calculus, the application \(MN\) is a legal term regardless of what \(M\) and \(N\) are. Such freedom permits one to form such suspicious terms as \(xx\), and thence terms such as the paradoxical combinator \(\mathbf{Y}\). One might wish to exclude terms like \(xx\) on the grounds that \(x\) is serving both as a function (on the left-hand side of the application) and as an argument (on the right-hand side of the application). Type theory gives us the resources for making this intuitive argument more precise.