View source for Church lambda-abstraction

{{TEX|done}}
A notation for introducing functions in the languages of mathematical logic, in particular in [[Combinatory logic|combinatory logic]]. More precisely, if in an exact language a term $A$ 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 [[#References|[1]]].

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Church,   "The calculi of $\lambda$-conversion" , Princeton Univ. Press  (1941)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  H.B. Curry,   "Foundations of mathematical logic" , McGraw-Hill  (1963)</TD></TR></table>



====Comments====


====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  H.P. Barendrecht,   "The lambda-calculus, its syntax and semantics" , North-Holland  (1978)</TD></TR></table>