Church lambda-abstraction
A notation for introducing functions in the languages of mathematical logic, in particular in combinatory logic. More precisely, if in an exact language a term has been defined, expressing an object of the theory and depending on parameters x_1,\dots,x_n (and possibly also on other parameters), then
\lambda x_1,\dots,x_nA\label{*}\tag{*}
serves in the language as the notation for the function that transforms the values of the arguments x_1,\dots,x_n into the object expressed by the term A. The expression \eqref{*} is also called a Church \lambda-abstraction. This Church \lambda-abstraction, also called an explicit definition of a function, is used mostly when in the language of a theory there is danger of confusing functions as objects of study with the values of functions for certain values of the arguments. Introduced by A. Church [1].
References
[1] | A. Church, "The calculi of \lambda-conversion" , Princeton Univ. Press (1941) |
[2] | H.B. Curry, "Foundations of mathematical logic" , McGraw-Hill (1963) |
Comments
References
[a1] | H.P. Barendrecht, "The lambda-calculus, its syntax and semantics" , North-Holland (1978) |
Church lambda-abstraction. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Church_lambda-abstraction&oldid=44751