Combinatorial logic.Computability theory (the study of what can be computed) and proof theory (the study of what can be mathematically proven.) The theory, because of its simplicity, captures the essential characteristics 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 set of combiners, the primitive functions that do not contain any free (or bound) variables. It is easy to transform lambda expressions into combinatorial expressions, and since reducing a combiner is simpler than reducing lambda,
Summary
[ hide ]
- 1 Summary of the lambda calculation
- 2 Combinatorial Calculations
- 1 Combinatorial terms
- 2 Examples of combiners
- 3 extensional equality
- 4 Completeness of the SK base
- 5 Conversion of a lambda term to an equivalent combinatorial term
- 6 Explanation of transformation T []
- 7 Simplifications of transformation
- 8 η-reduction
- 9 Curry combiners B, C
- 10 Reverse conversion
- 3 Undecidability of Combinatorial Calculation
- 4 Source
Lambda calculation summary
The lambda calculus refers to objects called lambda-terms, which are symbol strings 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, returns E1, with each occurrence of ν replaced by the argument . The terms of the form (E1 E2) are called applications. Applications model the invocation or execution of a function: The function represented by E1 is invoked, with E2 as its argument, and the result is computed. If E1 (sometimes called the applying) is an abstraction, the term can be reduced: E2, the argument can be substituted in 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 sub-terms of the form (λv.E1 E2) then it cannot be shortened, and is said to be in normal form. The expression E [a / v] represents the result of taking the term E and replacing all free occurrences of v with a. We write like this The expression E [a / v] represents the result of taking the term E and replacing all free occurrences of v with a. We write like this The expression E [a / v] represents the result of taking the term E and replacing all free occurrences of v with a. We write like this
(λv.E a) => E [a / v]
By convention, we take (bc d … z) as an abbreviation for (… (((ab) c) d) … z). (Association rule by left). 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 is 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 instead of the formal parameter: The square of 3 is 3 * 3 to evaluate the expression that results in 3 * 3, we would have to draw on our knowledge of multiplication and number 3. Since any computation is simply a composition of the evaluation of adequate functions with adequate primitive arguments, this simple substitution principle is sufficient to capture the essential mechanism of computation. On the other hand, in lambda calculus, notions such as ‘3’ and ‘*’ can be represented without any need for externally defined primitive operators or constants. It is possible to identify the terms that in the lambda calculation, 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 (including Turing machines); that is to say, any computation that can be accomplished in any of these other models can be expressed in the lambda computation, 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 the simple textual substitution of variable terms. But even more remarkable is that even abstraction is not required. Combinatorial Logic is a computational model equivalent to lambda calculus, but without abstraction. 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 the simple textual substitution of variable terms. But even more remarkable is that even abstraction is not required. Combinatorial Logic is a computational model equivalent to lambda calculus, but without abstraction. 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 the simple textual substitution of variable terms. But even more remarkable is that even abstraction is not required. Combinatorial Logic is a computational model equivalent to lambda calculus, but without abstraction.
Combinatorial Calculations
Since abstraction is the only way to manufacture functions in lambda calculus, something must replace it in combinatorial calculus. Rather than abstraction, combinatorial calculus provides a limited set of primitive functions and from which the other functions can be constructed.
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.
Combiner Examples
The simplest example of a combiner is I, the identity combinator, 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) y) = x
for all x and y terms. Or, following the same convention for multiple use as in lambda calculus,
(K xy) = x
A third combiner is S, which is a generalized version of the application:
(S xyz) = (xz (yz))
S applies x and a after first substituting az on each of them. Given S and K, even I itself is unnecessary, since it can be constructed by the other two:
((SKK) x) = (SKK x) = (K x (K x)) = x
for any x term. Note that although ((SKK) x) = (I x) for any x, (SKK) 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; (SKK) and I are between these ways. (SKS) is another. We will use the equivalent word to indicate extensional equality, reserving equal for identical combinatorial terms. A more interesting combiner is the fixed point combiner or Y combinator, which can be used to implement recursion.
SK base completeness
It is, perhaps, an amazing fact that S and K can be composed to produce combiners that are extensionally equal to any lambda term, and therefore, by Church’s thesis, to any computable function. The test is to present a transformation, T [], that converts an arbitrary term lambda to an equivalent combiner. T [] can be defined as follows: T [V] => VT [(E1 E2)] => (T [E1] T [E2]) T [λx.E] => (KE) (if x is not free in E) T [λx.x] => IT [λx.λy.E] => T [λx.T [λy.E]] (if x is free in E) T [λx. (E1 E2)] => (ST [λx.E1] T [λx.E2])
Conversion of a lambda term to an equivalent combinatorial term
For example, we will convert the term lambda λx.λy. (yx)) to a combinator:
T [λx.λy. (yx)] = T [λx.T [λy. (Yx)]] (by 5) = T [λx. (ST [λy.y] T [λy.x])] (by 6) = T [λx. (SIT [λy.x])] (by 4) = T [λx. (SI (K x))] (by 3) = (ST [λx. (SI)] T [λx. (K x)]) (by 6) = (S (K (SI)) T [λx. (K x)]) (by 3) = (S (K (SI)) (ST [λx.K] T [λx.x])) (by 6) = (S (K (SI)) (S (KK) T [λx.x])) (by 3) = (S (K (SI)) (S (KK) I)) (by 4)
if we apply this combinator to any two x and y terms, it reduces as follows:
(S (K (SI)) (S (KK) I) xy) = (K (SI) x (S (KK) I x) y) = (SI (S (KK) I x) y) = (I y (S (KK) I xy)) = (y (S (KK) I xy)) = (y (KK x (I x) y)) = (y (K (I x) y)) = (y (I x)) = (yx)
The combinatorial representation, (S (K (SI)) (S (KK) I)) is much longer than the representation as a term lambdaλx.λy. (Yx). 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 transformation T [] is motivated by a desire to eliminate abstraction. Two special cases, rules 3 and 4, are trivial: λx.x is clearly equivalent to I, and λx.E is clearly equivalent to (KE) if x does not appear free in E. The first two rules are also simple: The variables they become themselves, and the applications allowed in combinatorial terms, the combiners are converted simply by converting the applicant and the argument to combiners. Rules 5 and 6 are of interest. Rule 5 simply says 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 eliminates abstraction. λx. (E1E2) is a function that takes an argument, say to, and substitutes it in the term lambda (E1 E2) instead of x, giving (E1 E2) [a / x]. But substituting in (E1 E2) instead of x is just like substituting it in E1 and E2, so
(E1 E2) [a / x] = (E1 [a / x] E2 [a / x]) (λx. (E1 E2) a) = ((λx.E1 a) (λx.E2 a)) = (S λx.E1 λx.E2 a) = ((S λx.E1 λx.E2) a)
For extensional equality,
λx. (E1 E2) = (S λx.E1 λx.E2)
Therefore, to find a combiner equivalent to λx. (E1 E2), it is enough to find a combiner equivalent to (S λx.E1 λx.E2), and
(ST [λx.E1] T [λx.E2])
evidently fulfills the objective. E1 and E2 each contain strictly fewer applications than (E1 E2), so repetition must end in a lambda term with no application – not a variable, not a term of the form λx.E.
Transformation simplifications
η-reduction
The combiners generated by the transformation T [] can be made smaller if we consider the η-reduction rule:
T [λx. (E x)] = T [E] (if x is not free in 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 [λx.λy. (yx)] = … = (S (K (SI)) T [λx. (K x)]) = (S (K (SI)) K) (by η-reduction)
This combiner is equivalent to the previous one, longer:
(S (K (SI)) K xy) = (K (SI) x (K x) y) = (SI (K x) y) = (I y (K xy)) = (y (K xy)) = (yx)
similarly, the original version of the transformation T [] transformed the identity function λf.λx. (fx) into (S (S (KS) (S (KK) I)) (KI)). With the η-reduction rule, λf.λx. (fx) became I.
Curry combiners B, C
Combiners S, K are already in Schönfinkel (although the symbol C was used by the current K) Curry introduced the use of B, C, W (and K), already before his doctoral thesis in 1930. In Combinatorial Logic T I, We have returned to S, K but it shows, (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 been linked to its computational use. Two new combiners are introduced:
(C abc) = (acb) (B abc) = (a (bc))
Using these combiners, we can extend the rules for the transformation as follows:
1.T [V] => V 2.T [(E1 E2)] => (T [E1] T [E2]) 3.T [λx.E] => (KE) (if x is not free in E) 4.T [λx.x] => I 5.T [λx.λy.E] => T [λx.T [λy.E]] (if x is free in E) 6.T [λx. (E1 E2)] => (ST [λx.E1] T [λx.E2]) (if x is free in both E1 and E2) 7.T [λx. (E1 E2)] => (CT [λx.E1] E2) (if x is free in E1 but not in E2) 8.T [λx. (E1 E2)] => (B E1 T [λx.E2]) (if x is free in E2 but not in E1)
Using combiners B and C, the transformation of λx.λy. (yx) looks like this:
T [λx.λy. (yx)] = T [λx.T [λy. (Yx)]] = T [λx. (CT [λy.y] x)] (by rule 7) = T [λx. (CI x)] = (CI) (η-reduction) = C * (traditional canonical notation: X * = XI) = I ‘(traditional canonical notation: X’ = CX)
And certainly (CI xy) reduces to (yx):
(CI xy) = (I and x) = (yx)
The motivation here is that B and C are limited versions of S. As long as S takes a value and substitutes it both in the applying and in the argument before making the application, C makes the substitution only in the applying, and B only in the argument.
Reverse conversion
The conversion L [] from combinatorial terms to lambda terms is trivial:
L [I] = λx.x L [K] = λx.λy.x L [C] = λx.λy.λz. (xzy) L [B] = λx.λy.λz. (x (yz)) L [S] = λx.λy.λz. (xz (yz)) L [(E1 E2)] = (L [E1] L [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 Calculation
It is undecidable when a general combinatorial term has a 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 = (SII (SII))
it has no normal form, because it reduces itself in three steps, as follows:
(YES YES)) = (I (SII) (I (SII))) = (SII (I (SII))) = (IBS (IBS))
and clearly no other order of reduction can make the expression shorter. Now suppose that N were a combiner to detect normal shapes, such that
(N x) => T, if x has a normal shape F, otherwise.
(Where T and F are the transformations of the conventional definitions in true and false lambda calculus, λx.λy.x and λx.λy.y. The combinatorial versions have T = K and F = (KI) = 0 = K ‘. ) Now be
Z = (C (C (BN (SII)) A) I)
and consider the term (SIIZ). Does (SIIZ) have a normal shape? It does if and only if:
(SIIZ) = (IZ (IZ)) = (Z (IZ)) = (ZZ) = (C (C (BN (SII)) A) IZ) (definition of Z) = (C (BN (SII)) AZI) = (BN (SII) ZAI) = (N (SIIZ) AI)
Now we must apply N to (SIIZ). Either (SIIZ) has a normal shape, or it does not. If it had normal form, then it is reduced as follows:
(N (SIIZ) AI) = (KAI) (definition of N) = A
but A does not have a normal form, therefore we have a contradiction. But if (SIIZ) does not have a normal form, it is reduced as follows:
(N (SIIZ) AI) = (KIAI) (definition of N) = (II) I
which means that the normal form of (SIIZ) is simply I, another contradiction. Therefore, the hypothetical normal-form combiner N cannot exist.
