^^Lambda calculus. Combinators.

"lambda calculus" & "theory of combinators" closely related.


λ-calculus (=def) wp

  1. a formal system in mathematical logic for expressing computation by way of variable binding and substitution
  2. a way to formalize mathematics through the notion of functions, in contrast to the field of set theory. So formulated by Alonzo Church.

Although not very successful in that respect, the lambda calculus found early successes in the area of computability theory, such as a negative answer to Hilbert's Entscheidungsproblem.


Lambda explorer.


  1. Category theory.
  2. Turing machine.
  3. FP Functional programming.


Lambda calculus is

  1. an elegant notation for working with applications of functions to arguments.
  2. a well-formed theory of functions as rules of computation.
  3. arose from the study of functions as rules.
    It was introduced in the 1930s by Alonzo Church as a way of formalizing the concept of effective computability.
  4. the smallest universal programming language of the world
  5. consists of
    1. a single transformation rule: variable substitution
    2. a single function definition scheme.
  6. equivalent to Turing machines.
    the difference is that lambda calculus emphasizes the use of transformation rules, and it does not care about the actual machine implementing them. It is an approach more related to software than to hardware.


variable: x 
lambda abstraction (function): f = λx.[x˛ + 3x + 4]
function application: f y

The lambda abstraction

is a function

The lambda operator allows us to abstract over x.

f = λx.x  is the identity


(λx.M)N -> M[x := N]

to replace all occurrences of x with N.

To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction

Links inet

  1. A Graphical Notation for the Lambda Calculus with Animated Reduction
  2. csvoss/circuit-notation-lambda-calculus

Lambda-Calculus and Combinators.pdf

The λ-calculus and combinatory logic are two systems of logic which can also serve as abstract programming languages. They both aim to describe some very general properties of programs that can modify other programs, in an abstract setting not cluttered by details. In some ways they are rivals, in others they support each other. The λ-calculus was invented around 1930 by an American logician Alonzo Church, as part of a comprehensive logical system which included higher-order operators (operators which act on other operators). In fact the language of λ-calculus, or some other essentially equivalent notation, is a key part of most higher-order languages, whether for logic or for computer programming. Indeed, the first uncomputable problems to be discovered were originally described, not in terms of idealized computers such as Turing machines, but in λ-calculus. Combinatory logic has the same aims as λ-calculus, and can express the same computational concepts, but its grammar is much simpler. Its basic idea is due to two people: Moses Sch¨onfinkel, who first thought of it in 1920, and Haskell Curry, who independently re-discovered it seven years later and turned it into a workable technique.

To motivate combinators

consider the commutative law of addition in arithmetic, which says
(∀ x, y)   x + y = y + x.
The above expression contains bound variables ‘x’ and ‘y’. But these can be removed, as follows. We first define an addition operator A by
A(x, y) = x + y    (for all x, y),
and then introduce an operator C defined by
(C(f))(x, y) = f(y, x)    (for all f, x, y).
Then the commutative law becomes simply
A = C(A)

Other examples of such operators are the following:

(B(f, g))(x) = f(g(x)) B, composes two functions
(B′(f, g))(x) = g(f(x)) B′, a reversed composition operator
I(f) = f I, the identity operator
(K(a))(x) = a K, forms constant functions
(S(f, g))(x) = f(x, g(x)) S, a stronger composition operator
(W(f))(x) = f(x, x) W, for doubling or ‘diagonalizing’

Instead of trying to define ‘combinator’ rigorously in this informal context, we shall build up a formal system of terms in which the above ‘combinators’ can be represented.


  1. fun with combinators
  2. johndcook/schonfinkel-combinators
  3. stackexchange/what-are-combinators-and-how-are-they-applied
  4. arxiv Combinators: A Centennial View. Stephen Wolfram





> knock knock

< who's there?

> (λx.x)

< (λx.x) who?

> who?