Difference between revisions of "Church lambda-abstraction"
From Encyclopedia of Mathematics
(Importing text file) |
m (label) |
||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
| − | 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 | + | {{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 | + | 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==== | ====References==== | ||
| − | <table><TR><TD valign="top">[1]</TD> <TD valign="top"> A. Church, "The calculi of | + | <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> |
Latest revision as of 17:18, 14 February 2020
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 $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 [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) |
How to Cite This Entry:
Church lambda-abstraction. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Church_lambda-abstraction&oldid=17774
Church lambda-abstraction. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Church_lambda-abstraction&oldid=17774
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article