Namespaces
Variants
Actions

Difference between revisions of "Church lambda-abstraction"

From Encyclopedia of Mathematics
Jump to: navigation, search
(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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c022/c022230/c0222302.png" /> has been defined, expressing an object of the theory and depending on parameters <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c022/c022230/c0222303.png" /> (and possibly also on other parameters), then
+
{{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
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c022/c022230/c0222304.png" /></td> <td valign="top" style="width:5%;text-align:right;">(*)</td></tr></table>
+
$$\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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c022/c022230/c0222305.png" /> into the object expressed by the term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c022/c022230/c0222306.png" />. The expression (*) is also called a Church <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c022/c022230/c0222307.png" />-abstraction. This Church <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c022/c022230/c0222308.png" />-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]]].
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c022/c022230/c0222309.png" />-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>
+
<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
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article