n. the operation, in lambda calculus, that forms an expression denoting a function (or, equivalently, a class or predicate) from any expression whatever, by prefixing to it the abstraction operator, λ, and a bound variable; the notation λx[...] can be most generally read as `is an x such that...'. For example, lambda abstraction applied to a binary relation such as x is to the left of y (here written Lxy), yields