Curry defines the -combinator as:

which, when applied to a lambda term , -reduces in two steps to:

An equivalent -combinator definition is the following:

which consists of part of the combinator named and the term .

If we -reduce the equivalent form once:

we would obtain Curry's form of the -combinator.

Whilst the Curry form should work perfectly fine in Scheme and untyped lambda calculus, a statically typed language will not accept a function application such as since the type system will forbid it. In order to do that, we start by applying an additional -abstraction to obtain the form:

which can be re-written as:

We notice that the combinator () appears twice in the resulting -combinator which lets us express the -combinator using the combinator:

where and are -equivalent.

Expressing the combinator in terms of allows us to implement the combinator in statically typed programming languages.

You may have seen the definition of exponentiation as the combinator (or ) given by the lambda abstraction:

where and are both Church numerals. will perform the mathematical equivalent of using Church numerals.

Therefore the application of a Church numeral to another Church numeral will yield the Church numeral equivalent to . For instance, applying the Church numeral to Church numeral should yield . While all the numerals work out, the application of the Church numeral zero to any other Church numeral -reduces to the identity function . For instance, applying the Church numeral to we have:

Since the identity function is not a Church numeral, it would seem that the application is not defined. However, by the rules of exponentiation, any number to the power zero should yield one; in other words: .

The trick here is that the identity function is equivalent with the Church numeral under the -expansion.

The -expansion is given by:

so we can re-work the application of the Church numeral zero to the Church numeral two:

which yields the expected result.

-reduction is given by:

-expansion is given by:

fuss/lambda_calculus.txt · Last modified: 2017/02/22 18:30 (external edit)

For the copyright, license, warranty and privacy terms for the usage of this website please see the license, privacy and plagiarism pages.