"lambda calculus" & "theory of combinators" closely related.
λ-calculus (=def) wp
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.
variable: x lambda abstraction (function): f = λx.[x˛ + 3x + 4] function application: f y
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.
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.
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)
(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.
https://twitter.com/atom_geller/status/1274874494025216000
> knock knock
< who's there?
> (λx.x)
< (λx.x) who?
> who?