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 (and possibly also on other parameters), then

(*)

serves in the language as the notation for the function that transforms the values of the arguments into the object expressed by the term . The expression (*) is also called a Church -abstraction. This Church -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 -conversion" , Princeton Univ. Press (1941)
[2]	H.B. Curry, "Foundations of mathematical logic" , McGraw-Hill (1963)

References

[a1]	H.P. Barendrecht, "The lambda-calculus, its syntax and semantics" , North-Holland (1978)