Combinatorial logic
Combinatorial logic is ultimate logic and as such can be a simplified model of computation, used in computability theory (the study of what can be computed) and proof theory (the study of what can be proven mathematically).
Introduction
The theory, because of its simplicity, captures the essential features of the nature of computation. Combinatorial logic (LC) is the foundation of lambda calculus, by removing the last type of variable from it: the lambda variable. In LC lambda expressions (used to allow functional abstraction) are replaced by a limited system of combinators, primitive functions that do not contain any free (or bound) variables. It is easy to transform lambda expressions into combinatorial expressions, and since combinator reduction is simpler than lambda reduction, LC has been used as the basis for the implementation of some functional programming languages. no-strict in software and hardware.
Summary of lambda calculus
Lambda calculus refers to objects called lambda-terms, which are strings of symbols in one of the following ways:
- v
- λv.E1
- (E1 E2)
where v is a variable name taken from a predefined infinite set of variable names, and E1 and E2 are lambda-terms. Terms of the form λv.E1 are called abstractions. The variable ν is called the formal parameter of the abstraction, and E1 is the body of the abstraction.
The term λv.E1 represents the function that, if applied to an argument, binds the formal parameter v to the argument and then computes the resulting value of E1- -- that is, return E1, with each occurrence of ν replaced by the argument.
Terms of the form (E1 E2) are called applications. Applications model the invocation or execution of a function: The function represented by E1 is called, with E2 as its argument, and the result is computed. If E1 (sometimes called the applicand) is an abstraction, the term can be reduced: E2, the argument, can be substituted into the body of E1 instead of the formal parameter of E1, and the result is a new lambda term that is equivalent to the old one. If a lambda term does not contain any subterms of the form (λv.E1 E2) then it cannot be reduced, and is said to be in normal form.
The expression E[a/v] represents the result of taking the term E and substituting all free occurrences of v for the term E a. we write like this
(λv.E a) ⇒ E[a/v]
by convention, we take (b c d... z) as shorthand for (... (((a b) c) d)... z). (Left association rule).
The motivation for this definition of reduction is that it captures the essential behavior of all mathematical functions. For example, consider the function that computes the square of a number. You can write the square of x as x*x (using "*" to indicate multiplication.) x here is the formal parameter of the function. To evaluate the square for a particular argument, say 3, we insert it into the definition in place of the formal parameter:
The square of 3 is 3*3
To evaluate the expression that results in 3*3, we would have to call upon our knowledge of multiplication and the number 3. Since any computation is simply a composition of the evaluation of suitable functions with suitable primitive arguments, this simple principle of substitution is enough to capture the essential mechanism of computation. On the other hand, in lambda calculus, notions such as '3' and '*' it can be represented without any need for externally defined primitive operators or constants. It is possible to identify the terms that in the lambda calculus, when properly interpreted, behave like the number 3 and the multiplication operator.
The lambda calculus is computationally equivalent in power to many other plausible models for computation (Turing machines included); that is, any calculation that can be achieved in any of these other models can be expressed in the lambda calculus, and vice versa. According to the Church-Turing thesis, both models can express any possible computation. It may seem surprising that the lambda calculus can represent any conceivable computation using only the simple notions of functional abstraction and application based on simple textual substitution of terms for variables. But even more remarkable is that even abstraction is not required. Combinatorial Logic is a computational model equivalent to lambda calculus, but without the abstraction.
Combinatorial Calculations
Since abstraction is the only way to fabricate functions in lambda calculus, something must replace it in combinatorial calculus. Instead of abstraction, combinatorial calculus provides a limited set of primitive functions and from which other functions can be built.
Combinatorial Terms
A combinatorial term has one of the following forms:
- V
- P
- (E1 E2)
where V is a variable, P is one of the primitive functions, E1 and E2 are combinatorial terms. The primitive functions themselves are combinators, or functions that do not contain any free variables.
Combinator Examples
The simplest example of a combinator is I, the combinator identity, defined by
(I x) = x
for all x terms. another simple combinator is K, which produces constant functions: (K x) is the function that, for any argument, returns x , so we say
(K x) and) = x
for all terms x and y. Or, following the same convention for multiple use as in the lambda calculus,
(K x and) = x
A third combinator is S, which is a generalized version of the application:
(S x and z) = (x z (and z)
S applies x to y after first substituting z into each of them.
Given S and K, even I itself is unnecessary, since it can be constructed by the other two:
(S K K) x) =S K K x) =K x (K x) = x
for any term x. Note that although ((S K K) x) = (I x) for any x, (S K K) itself is not equal to I. We say that the terms are extensionally equal.
Extensional equality
Extensional equality captures the mathematical notion of equality of functions: that two functions are 'equal' if they always produce the same results for the same arguments. In contrast, the terms themselves capture the notion of intensional equality of functions: that two functions are 'equal'; only if they have identical implementations. There are many ways to implement an identity function; (S K K) and I are among these ways. (S K S) is another. We will use the word equivalent to indicate extensional equality, reserving equal for identical combinatorial terms.
A more interesting combinator is the Y combinator, which can be used to implement recursion.
Completion of the S-K base
It is, perhaps, an amazing fact that S and K can be composed to produce combinators that are extensionally equal to any lambda term, and therefore, by Church's thesis, to any computable function. The proof is to present a transformation, T[ ], that converts an arbitrary lambda term into an equivalent combinator. T[ ] can be defined as follows:
T[V] ⇒ V
T[(E1 E2)] ⇒ (T[E1 ] T[E2])
T[λx.E] ⇒ (K E) (if x is not free in E)
T[λx.x] ⇒ I
T[λx.λy.E] ⇒ T [λx.T[λy.E]] (if x is free in E)
T[λx.(E1 E2)] ⇒ (S T[λx.E1] T[λx.E2])
Conversion of a lambda term to an equivalent combinatorial term
For example, we will convert the lambda term λx.λy.(y x)) to a combiner:
T[chuckles]λx.λy. (and x)] = T[chuckles]λx.T[chuckles]λy. (and x)] ] (by 5) = T[chuckles]λx. (S T[chuckles]λy.and] T[chuckles]λy.x])] (by 6) = T[chuckles]λx. (S I T[chuckles]λy.x]] (by 4) = T[chuckles]λx. (S I (K x)] (by 3) =S T[chuckles]λx. (S I)] T[chuckles]λx. (K x)) (per 6) =S (K (S I) T[chuckles]λx. (K x)) (by 3) =S (K (S I) (S T[chuckles]λx.K] T[chuckles]λx.x])) (by 6) =S (K (S I) (S (K K) T[chuckles]λx.x]) (by 3) =S (K (S I) (S (K K) I) (by 4)
if we apply this combinator to any two terms x and y, reduce as follows:
(S (K (S I) (S (K K) I) x and =K (S I) x (S (K K) I (x) (y) =S I (S (K K) I (x) (y) =I and (S (K K) I (x (y)) = (and)S (K K) I (x (y)) = (and)K K x (I (x) (y)) = (and)K (I (x) (y)) = (and)I (x)) = (y x)
The combinatorial representation, (S (K (S I)) (S (K K) I)) is much longer than the representation as a lambdaλx term. λy.(y x). This is typical. In general, the construction of T[ ] can extend a lambda term of length n to a combinatorial term of length Θ(3n).
Explanation of the transformation T[ ]
The T[ ] transformation is motivated by a desire to remove abstraction. Two special cases, rules 3 and 4, are trivial: λx.x is clearly equivalent to I, and λx. E is clearly equivalent to (K E) if x does not appear free in E.
The first two rules are also simple: Variables are converted to themselves, and applications allowed in combinatorial terms are converted to combinators by simply converting the applicand and argument to combinators.
It's rules 5 and 6 that are of interest. Rule 5 says simply this: to convert a complex abstraction to a combinator, we must first convert its body to a combinator, and then remove the abstraction. Rule 6 really removes the abstraction.
λx.(E1E2) is a function that takes an argument, say a, and substitutes it into the lambda term (E1 E2) instead of x, giving (E1 E2)[a/x]. But substituting a into (E1 E2) instead of x is precisely the same as substituting it into E1 and E2, so
(E1 E2)[a/x] = (E1[chuckles]a/x] E2[chuckles]a/x])
(λx. (E1 E2) a) = ((λx.E1 a) (λx.E2 a) =S λx.E1 λx.E2 a) =S λx.E1 λx.E2) a)
By extensional equality,
λx. (E1 E2) = (S λx.E1 λx.E2)
Therefore, to find a combinator equivalent to λx.(E1 E2), it is enough to find a combinator equivalent to (S λx.E1 λx.E2), and
(S T[chuckles]λx.E1] T[chuckles]λx.E2])
Obviously it serves the purpose. E1 and E2 each contain strictly fewer maps than (E1 E2), so the repetition must end in a lambda term with no map- neither a variable nor a term of the form λx.E.
Transformation simplifications
Η-reduction
The combinators generated by the transformation T[ ] can be made smaller by considering the η-reduction rule:
T[chuckles]λx. (E x) T[chuckles]E] (yes x He's not free. E)
λx.(E x) is the function that takes an argument, x, and applies the function E to it; this is extensionally equal to the function E itself. It is therefore sufficient to convert E to the combinatorial form. Taking this simplification into account, the example above becomes:
T[chuckles]λx.λy. (and x)] =... =S (K (S I) T[chuckles]λx. (K x)])
=S (K (S I) K) (by Bolivarian-reduction)
This combinator is equivalent to the previous one, longer:
(S (K (S I) K x and) =K (S I) x (K x) and) =S I (K x) and) =I and (K x and) =and (K x and) =and x)
similarly, the original version of the transformation T[ ] transformed the identity function λf.λx.(f x) in (S (S (K S) (S (K K) I)) (K I)). With the η-reduction rule, λf.λx.(f x) became I.
Curry's B, C Combinators
The combinators S, K are already found in Schönfinkel (although the symbol C was used for the actual K) Curry introduced the use of B, C, W (and K), already before his 1930 doctoral thesis. In Combinatorial Logic T. I, S, K have been reverted to, but it is shown, (via Markov algorithms) that the use of B and C can simplify many reductions. This seems to have been used much later by David Turner, whose name has become linked to its computational use. Two new combinators are introduced:
(C a b c) = (a c b) (B a b c) = (a (b c)
Using these combinators, we can extend the rules for transformation as follows:
- T[chuckles]V] ⇒ V
- T[E1 E2) ⇒ (T[chuckles]E1] T[chuckles]E2])
- T[chuckles]λx.E⇒K E(if) xHe's not free. E)
- T[chuckles]λx.x] ⇒ I
- T[chuckles]λx.λy.E] ⇒ T[chuckles]λx.T[chuckles]λy.E]] x is free in E)
- T[chuckles]λx. (E1 E2) ⇒ (S T[chuckles]λx.E1] T[chuckles]λx.E2]) (yes) x He's free so much. E1 as in E2)
- T[chuckles]λx. (E1 E2) ⇒ (C T[chuckles]λx.E1] E2(if) x is free in E1 but not in E2)
- T[chuckles]λx. (E1 E2) ⇒ (B E1 T[chuckles]λx.E2]) (yes) x is free in E2 but not in E1)
Using the B and C combinators, the transformation of λx.λy.(y x) looks like this:
T[chuckles]λx.λy. (and x)] = T[chuckles]λx.T[chuckles]λy. (and x)] = T[chuckles]λx. (C T[chuckles]λy.and] x)] (by rule 7) = T[chuckles]λx. (C I x)] =C I(reduction) = C♪(traditional canonical performance: X♪ = XI) = I'(traditional canonical score: X' = CX)
And indeed (C I x y) reduces to (y x):
(C I x and) =I and x) =and x)
The motivation here is that B and C are limited versions of S.
While S takes a value and substitutes it in both the applicand and the argument before performing the application, C performs the substitution only in the applicand, and B in the argument only.
Reverse conversion
The conversion L[ ] of combinatorial terms to lambda terms is trivial:
L[chuckles]I] = λx.x L[chuckles]K] = λx.λy.x L[chuckles]C] = λx.λy.λz. (x z and) L[chuckles]B] = λx.λy.λz. (x (and z) L[chuckles]S] = λx.λy.λz. (x z (and z) L[E1 E2) = (L[chuckles]E1] L[chuckles]E2])
Note, however, that this transformation is not the inverse transformation of any of the versions of T[ ] that have been seen.
Undecidability of Combinatorial Calculus
It is undecidable when a general combinatorial term has normal form; when two combinatorial terms are equivalent, etc. This is equivalent to the undecidability of the corresponding problems for lambda terms. However, a direct proof is as follows:
First, note that the term
A =S I I (S I I)
has no normal form, because it reduces itself in three steps, as follows:
(S I I (S I I) =I (S I I) (I (S I I()))) =S I I (I (S I I()))) =S I I (S I I)
and clearly no other reduction order can make the expression shorter.
Now, suppose N were a combinator to detect normal forms, such that
(N x⇒ TYeah. x It's normal. FOtherwise.
(Where T and F are the transformations of the conventional definitions in true-false lambda calculus, λx.λy .x y λx.λy.y. The combinatorial versions have T = K and F = (K I) = 0 = K'.)
Now be
Z =C (C (B N (S I I) A) I)
and consider the term (S I I Z). Does (S I I Z) have a normal form? It does if and only if:
(S I I Z) =I Z (I Z) =Z (I Z) =Z Z) =C (C (B N (S I I) A) I Z(definition of Z) =C (B N (S I I) A Z I) =B N (S I I) Z A I) =N (S I I Z) A I)
Now we must apply N to (S I I Z). Either (S I I Z) has normal form, or it doesn't. If it had normal form, then it is reduced as follows:
(N (S I I Z) A I) =K A I(definition of N) = A
but A does not have a normal form, so we have a contradiction. But if (S I I Z) does not have normal form, then reduce as follows:
(N (S I I Z) A I) =K I A I(definition of N) =I I) I
which means that the normal form of (S I I Z) is simply I, another contradiction. Therefore, the hypothetical normal form combinator N cannot exist.