Editing Combinatory logic (section)

== Summary of lambda calculus ==
{{main|Lambda calculus}}

Lambda calculus is concerned with objects called ''lambda-terms'', which can be represented by the following three forms of strings:

*       {{tmath|v}}
*       {{tmath|\lambda v.E_1}}
*       {{tmath|(E_1 E_2)}}

where {{tmath|v}} is a variable name drawn from a predefined infinite set of variable names, and {{tmath|E_1}} and {{tmath|E_2}} are lambda-terms.

Terms of the form {{tmath|\lambda v.E_1}} are called ''abstractions''. The variable ''v'' is called the [[formal parameter]] of the abstraction, and {{tmath|E_1}} is the ''body'' of the abstraction. The term {{tmath|\lambda v.E_1}} represents the function which, applied to an argument, binds the formal parameter ''v'' to the argument and then computes the resulting value of {{tmath|E_1}}&mdash; that is, it returns {{tmath|E_1}}, with every occurrence of ''v'' replaced by the argument.

Terms of the form {{tmath|(E_1 E_2)}} are called ''applications''. Applications model function invocation or execution: the function represented by {{tmath|E_1}} is to be invoked, with {{tmath|E_2}} as its argument, and the result is computed. If {{tmath|E_1}} (sometimes called the ''applicand'') is an abstraction, the term may be ''reduced'': {{tmath|E_2}}, the argument, may be substituted into the body of {{tmath|E_1}} in place of the formal parameter of {{tmath|E_1}}, and the result is a new lambda term which is ''equivalent'' to the old one. If a lambda term contains no subterms of the form {{tmath|((\lambda v.E_1) E_2)}} then it cannot be reduced, and is said to be in [[Beta normal form|normal form]].

The expression {{tmath|E[v :{{=}} a]}} represents the result of taking the term {{mvar|E}} and replacing all free occurrences of {{mvar|v}} in it with {{mvar|a}}. Thus we write

:{{tmath|((\lambda v.E) a) \Rightarrow E[v :{{=}} a]}}

By convention, we take {{tmath|(a b c)}} as shorthand for {{tmath|((a b) c)}} (i.e., application is [[Associative#Non-associativity|left associative]]).

The motivation for this definition of reduction is that it captures the essential behavior of all mathematical functions. For example, consider the function that computes the square of a number. We might write

:The square of ''x'' is {{tmath|x*x}}

(Using "{{tmath|*}}" to indicate multiplication.)  ''x'' here is the [[formal parameter]] of the function. To evaluate the square for a particular argument, say 3, we insert it into the definition in place of the formal parameter:

:The square of 3 is {{tmath|3*3}}

To evaluate the resulting expression {{tmath|3*3}}, we would have to resort to our knowledge of multiplication and the number 3. Since any computation is simply a composition of the evaluation of suitable functions on suitable primitive arguments, this simple substitution principle suffices to capture the essential mechanism of computation.
Moreover, in lambda calculus, notions such as '3' and '{{tmath|*}}' can be represented without any need for externally defined primitive operators or constants. It is possible to identify terms in lambda calculus, which, when suitably interpreted, behave like the number 3 and like the multiplication operator, q.v. [[Church encoding]].

Lambda calculus is known to be computationally equivalent in power to many other plausible models for computation (including [[Turing machine]]s); that is, any calculation that can be accomplished in any of these other models can be expressed in lambda calculus, and vice versa. According to the [[Church–Turing thesis]], both models can express any possible computation.

It is perhaps surprising that lambda-calculus can represent any conceivable computation using only the simple notions of function abstraction and application based on simple textual substitution of terms for variables. But even more remarkable is that abstraction is not even required. ''Combinatory logic'' is a model of computation equivalent to lambda calculus, but without abstraction. The advantage of this is that evaluating expressions in lambda calculus is quite complicated because the semantics of substitution must be specified with great care to avoid variable capture problems.  In contrast, evaluating expressions in combinatory logic is much simpler, because there is no notion of substitution.