Has a dog Buddha-nature?

This is the most serious question of all.

If you say yes or no,

You lose your own Buddha-nature.

— from Chapter 1 of the Gateless Gate

In the beginning, there was nothing.

Then Alonzo Church came and said, “Let there be:”

- variable [x]
- a symbol or string of symbols that represents a particular value
- λ-abstraction [(λx.E)]
- a function on the λ-term E, with the variable x bound to E
- application [(E F)]
- applying the λ-term E to the argument F

And thus all three and only they attained λ-nature (i.e., are valid λ-terms).

Whence cometh these λ-terms?

Consider the noble function . We note that the name is illusory and thus we can rewrite the same function as . A λ-abstraction then is simple another way of writing this expression:

This is not a trivial transformation, however, as this also **binds** the variable to the λ-term . Their destinies are forever intertwined within their confining parentheses and hence the expression is equivalent to even though the variables have the same names.

To keep the expressions as elegant as possible, we shall adopt the following rules:

- Application is left-associative: is equivalent to
- The outermost parentheses are omitted: write over
- The term in a λ-abstraction extends up until a same-level closing parenthesis is found: is equivalent to , not
- Successive λ-abstractions can be combined under a single λ: is equivalent to .

#### Meditation: Which of the following do not have λ-nature?^{1}

Any λ-term may be further transformed according to the following **reduction rules**:

- α-conversion
- from to , where is the same as but with all instances of replaced by ; only bound variables may be replaced in this manner
- β-reduction
- application to arguments leads to substitution by those arguments, e.g., is equivalent to the λ-term
- η-conversion
- functions are completely determined by their arguments, i.e., is equivalent to iff all instances of in are bound

We are now ready to contemplate the *truth*^{2}. Consider the following definitions:

#### Meditation: Show that OR FALSE TRUE evaluates to TRUE^{3}.

Do not be fooled: the simplicity of our system hides a profound strength. For instance, contemplate the following:

- (etc.)

What do they do with and ? What happens if I apply the two-argument λ-abstraction to (2) and (3)? To (3) and (3)? To (1) and any of the succeeding λ-abstractions in the list?

Indeed, we have defined an operation that behaves like multiplication on a list that behaves like numbers. We have:

(etc.)

And in general these numerals (called **Church numerals**) repeat the functions to which they are arguments. So for instance, if we rename our multiplication λ-abstraction above to , then:

*Note: it may be best if you do this calculation by yourself using only the reduction rules above.*

We may now describe the machinations of *any* sort of calculating apparatus by defining what “computability” is:

- Computability
- a function on the natural numbers is computable if, for all its outputs, there is a corresponding λ-term that β-reduces to the output’s Church numeral

Or in the Platonic realm of mathematics, if I can find a λ-expression that is equivalent to where and are the Church numeral representations of and respectively, and by we mean you can get from by a series of β-reductions and vice versa.

Or in plain English, if anything I can do using in the world of math, I can also do using a corresponding in the world of λ-calculus.

However, our symbolic excursion hides an uncomfortable truth. Can you guess what it is? (Hint: it involves the operator .)

…

…

Consider the following derivation:

Let .

We have just demonstrated a paradox, an inescapable death knell to our naïve λ-calculus.

Wither our quest to bring forth computation? Is computer science a vacuous discipline after all?

Stay tuned for the next in this series.