  Another application of these models is in the treatment of the semantics of function application. We can think of the points in a model structure as both functions and data, and hold that \(Rxyz\) if and only if \(x\) (considered as a function) applied to \(y\) (considered as data) is \(z\). Traditional accounts of functions do not encourage this dual use, since functions are taken to be of a ‘higher’ than their inputs or outputs (on the traditional set-theoretic model of functions, a function \(is\) the set of its input-output pairs, and so, it can never take itself as an input, since sets cannot contain themselves as members). However, systems of functions modelled by the untyped \(\lambda\)-calculus, for example, allow for self-application. Given this reading of points in a model, a point is of type \(A \rightarrow B\) just if whenever it takes inputs of type \(A\), it takes outputs of type \(B\). The inference rules of this system are then principles governing types of functions: the sequent