The Lambda Calculus Approach

The lambda calculus was developed as a computational notation emphasizing variable binding and function application [0] [1]. It is based on three constructs:

1. Variables, such as \(x\), \(y\), \(z\).

2. Function definitions (abstractions), such as \(\lambda x. E\) (where \(E\) is any lambda expression).

3. Function applications, such as \(E_1 E_2\) (where \(E_1\) and \(E_2\) are any lambda expressions).

In practice, you can think of the lambda calculus as a programming language with only one keyword, \(\lambda\) [2].

• \(x\) is a variable.

• \(\lambda x.x\) is the identity function, that is, it returns its argument.

• \((\lambda x.x) y\) applies the identity function to \(y\).

• \(\lambda x. \lambda y. y;x\) is a function that takes two arguments and returns the second one.

The lambda calculus can be used to represent numbers and boolean logic, and ultimately to express any computable function. In practice, the expressions can become cumbersome, particularly for numbers and arithmetic operations. For example, Church numerals represent natural numbers as higher-order functions:

• 0 is represented as \(\lambda f. \lambda x. x\).

• 1 is represented as \(\lambda f. \lambda x. f x\).

• 2 is represented as \(\lambda f. \lambda x. f (f x)\).

• 3 is represented as \(\lambda f. \lambda x. f (f (f x)))\).

• and so forth.

This program calculates the addition of two Church numerals using the lambda calculus:

\[ \text{add} ≡ λm.λn.λs.λz.ms(nsz) \]

Ultimately, any lambda expression can be converted to an SKI combinator expression [1] (and thence also to Nock). (Generally, a combinator in the \(\lambda\text{C}\) is a function with no free variables, such as \(\lambda x.\lambda y. (x y)\).) Thence, per standard transformations and equivalencies among combinators, the expression can be further converted to an expression in any combinator system. The conversion process can be quite verbose; it amounts to replacing the lambda abstractions with combinations of the S, K, and I combinators.

For example, the lambda expression

\[ \lambda x. \lambda y. y;x \]

can be represented (with some manipulation) as the SKI expression

S(K(S;I))K

• [0]: Curry, H. B., Feys, R. (1958) Combinatory Logic. Amsterdam: North-Holland.

• [1]: Kiselyov, O. (2018) “\(\lambda\) to SKI, Semantically”

• [2]: Tunney, J. (2022) “Lambda Calculus in 383 Bytes”

Comparison with Nock

The lambda calculus and Nock are both foundational models of computation, and ultimately equivalent programs can be composed in either system. However, they differ significantly in their approach and structure:

• The lambda calculus is centered around function definition and application, using variables and abstractions. It is a minimalist language that can express any computable function through the use of functions as first-class citizens.

• Nock, on the other hand, is a combinatory system that operates on binary trees (nouns) and uses a small set of combinators to manipulate these trees. It does not have variables or traditional function definitions; instead, it relies on the structure of the data itself to guide computation.

In other words, they bring different emphases of computation to the fore.