20th WCP: Dual Identity Combinators

Introduction

Combinatory logic has been invented independently by M. Schönfinkel and H.B. Curry in the 20s of this century (Cf. Schönfinkel 1924, Curry 1930.). The impetus was to reduce the number of primitive notions needed for a logical system, in particular, for first-order logic. Schönfinkel used functions to provide a translation for a closed first-order formula into a functional expression, thereby eliminating bound variables of first-order logic. About the success of this attempt cf. Curry & Feys 1968: beyond this primarily intended connection between first-order logic and (illative) combinatory logic there is another connection between the two, the so called Curry-Howard isomorphism (Curry & Feys 1968, Howard 1980). This relates combinators to implicational formulae. It is just a small step from the Curry-Howard isomorphism to put combinatory bases (which are possibly combinatorially non-complete) into correspondence with logical systems. It is well-known, e.g., that the relevant system R® corresponds in the above sense to the combinatory base {B, C, W, I}. Of course, such combinatory bases are not unique just as axiomatizations are not unique. For instance, the combinatory base {B’, C, S, I} is equally suitable. (Cf. Dunn 1986.)

1. Dual combinators.

Pure combinators operate on left associated sequences of objects. The result of an application of a combinator is a sequence made out of some of the objects on the left (possibly with repetitions) and parentheses scattered across:

( . . . ( ( Qx₁) . . . ) x_n) º ( x_i 1 . . . x_{i m} )

where any x_{i j}(1£ j £ m) is x_k(1£ k £ n) for some k , and the sequence on the right might be associated arbitrarily. The parentheses on the left of the identity are frequently dropped, since left association is taken to be the default. To recall the most familiar combinators as an illustration of the above general statement we have:

Sxyz º xz(yz), Kxy º x, Ix º x, Bxyz º x(yz), Cxyz º xzy, Wxy º xyy.

Using the combinatory axioms above we can define the notions of one-step reduction (4 ₁), of reduction (4 ), and of weak equality (=_w) as usual. (For an introduction to combinatory logic see e.g., Hindley & Seldin 1986.) In case where one is interested in a combinatory base which is not combinatorially complete it might be useful to emphasize that the above notions are restricted to the particular combinatory base. This is almost as simple as subscripting all the definitions as follows. Let B be a possibly non-complete combinatory base. The one-step reduction over the base B (4 _1,B) is defined as follows: if Q Î B, and Qx₁ . . . x_nº ( x_i 1 . . . x_{i m}) is the axiom for Q, then U [Qx₁ . . . x_n] 4 _1,B U [Qx₁ . . . x_n / Qx_i1 . . . x_{i m}], where U [Y ] denotes a particular non-vacuous occurrence of Y in U, and U [ Y/Z ] denotes the replacement of this occurrence of Y by Z. Reduction over the base B (4 _B) is the reflexive transitive closure of 4 _1,B. The weak equality (=_w,B) is defined as usual, X =_w,BY if there are X₀, . . . , X_n ( n ³ 0), such that X ₀º X, X_n º Y and

("i)(X_i 4 _{1, B}X_i+1 Ú X_i+1 4 _{1,
B}X_i), where 0 £ i £ n.

Dual combinators (see Dunn & Meyer 1997) are the mirror images, so to speak, of the usual ones. They operate on right associated sequences, but while the usual combinators apply from the left, dual combinators apply from the right. In other words, dual combinators look like simply as though we were reading from right to left instead of from left to right. All this granted it is easy to define the dual pairs of the above combinators. I will denote each with the same letter as its usual counterpart with a minus attached to its left:

, x º (x -I) , x º (y (x -K)) ,((zy)(zx)) º (z (y (x -S))) ,(y(yx)) º (y(x -W))

,(y(zx)) º (z(yx -C)) ,((zy)x) º (z(yx -B))

I have retained the parentheses in these axioms to emphasize that the sequences are right associated; certainly, if we would be dealing with a combinatory system containing exclusively dual combinators, then we could introduce a convention that if parentheses are omitted the sequences are understood as associated to the right. Since the point of this paper is to consider systems with both types of combinators, I will keep to the usual convention and omit parentheses from left associated sequences of objects. For a dual system the notions of one-step reduction, reduction and weak equality are extended in an obvious way. Before proceeding to a consideration of these systems with both types of combinators it is useful to digress into an analysis of possible systems.

Combinators appear not only in combinatory logic but in l-calculus as well. Combinators are by definition closed l-terms. The pure combinators I considered above form a proper subset of the closed l-terms. Notably, the set of closed l-terms contains terms which correspond to the fixed point combinators—those are not pure according to the definition of pure combinators above. In the ordinary l-calculus functions take their arguments from the right. That is, the most common mathematical notation for function application is carried over into the notation of the l-calculus.

Barbanera & Berardi 1996 proposed a symmetric lambda calculus. Intuitively symmetry means that a function can be applied to its arguments independently of whether the argument stands on the right or on the left from the function. Thus, e.g., (l x.M )N reduces to the same term as N (l x.M ). At a first glance in this system we have symmetry added to the direction of the functions as well as to the direction of application (taking the ordinary lambda calculus for the starting point). However, it is interesting to take a second look at the symmetric l -calculus and the usual l -calculus to clarify the interaction between the direction of functions and application.

l-calculus. In the usual l I- or l K-calculus a redex of the form (l x.M )( l y.N ) can be reduced in no more than one way, namely, to M [x /l y.N ]. (I chose the visible bound variables so as to avoid the need to talk about clashes of those variables which are on the surface. Of course, I assume the usual definition of the substitution what includes all the necessary precautions.) If we would make explicit the function application together with its direction then we would have (l x.M ) °® (l y.N ) _ M [x /l y.N ]. It is easy to see that appending a ® to the functions would not add anything to the system. On the other hand, making all the l-abstracts to look to the left we would get -(l x.M )°® -(l y.N ). This term does not reduce to anything. Of course, M and N may contain redices, but the point made here and below is about the outermost l-abstracts which are made explicit in the notation. [Due to typographical restrictions, the left looking arrow has been replaced by a minus sign.]

Another way to look at the system would be to assume that functions are all unidirectional (with the same direction, let us say, all looking to the right) while the function application is bidirectional. Then the above term turns into (l x.M )®° (l y.N )® what reduces to M [x /l y.N ] as before. The above considerations show that adding bidirectionality only to one of the function application operation or the l-abstracts does not give new reductions. Taking functions and application as unidirectional but having opposite directions leads to an uninteresting empty theory. Probably, intuitively the l-calculus was thought to have unidirectional functions and unidirectional application, although hardly explicitly—rather this was tacitly taken for granted. It should be obvious by now that if we would reverse the l-calculus, that is, make both the functions and the application directed to the left, then having a term (l x.M ) (l y.N ) in the original calculus is the same as having -(l y.N )-°-( l x.M ) in the reversed one (and vice versa); both terms reduce to the same term: M [x /l y.N ]. Note that the notation for substitution, despite appearances, does not signify a direction; substitution is a different operation than application, and it has no directionality.

Symmetric l-calculus. Here both the l-abstracts and the application are bidirectional. Taking the same term as above we have in fact two redexes in it, (l x.M )( l y.N ). The term reduces both to M [x /l y.N ] and N [y /l x.M ]. This means that the set of the reducts of a term M is a superset of the reducts of the same term in the original l-calculus. In this case, there is nothing more to add as far as directionality is concerned.

Dual l-calculus. Dual l-calculus has not yet been investigated, and I introduce it here on the analogy with the dual combinatory systems. The idea is to make the application operation bidirectional while keeping functions unidirectional. There are a couple of subtleties here. First, as we saw above, if all the l-abstracts have the same direction, then even having bidirectional application does not give more than the usual l-calculus. Second, it would be useless to add bidirectionality (or different unidirectionality) for the l-abstracts while keeping the application operation unidirectional. Thus, in a "really" dual system: (i) the function application operation is bidirectional, (ii) the functions are unidirectional, but (iii) there are at least two functions with different directions. This system is not the same as the usual l -calculus or the symmetric l-calculus. Taking all the functions of the usual l-calculus to be directed to the right, all the reductions which are possible in the original l-calculus are also possible here. On the other hand, while a term (l x.M )( l y.N ) is always reducible in the symmetric l-calculus (since both functions are bidi-rectional), a superficially similar term -(l x.M )( l y.N )® does not contain any redex and does not reduce to anything in the dual l-calculus. Thus, allowing duality in the system (with bidirectional application) supplies additional distinctions with respect to both the usual l-calculus and the symmetric-calculus. The more distinctions a system can reflect, the more value it has, certainly. However, it is also important that the distinctions which are being made are important, interesting or in some way well motivated.

The motivation to introduce dual combinators in Dunn & Meyer 1997 was algebraic. The right arrow corresponds to a residual. In the algebraic approach it is natural to have both residuals. Looking at the provable formulas which are types for combinators it is natural to consider the same formulae with the back arrow. These would then induce combinators which apply from the right. Actually, the paper just mentioned also gives another reason for introducing dual combinators as full-fledged objects of the system: they are viewed as special arguments which do modify the functions applied to them. While this is a nice metaphor, we should not forget that the dual combinators act upon right associated sequences.

After this brief digression I return to considering systems with dual combinators, that is, systems containing both some of the usual combinators and some of the dual ones. Let me repeat once again that with a single kind of combinator we do not gain anything more than a usual combinatory system (perhaps, read from right to left). It does not matter whether the combinators apply from left or from right. To start the investigation of the properties of dual systems let us first look at the diamond (CR) property. It is rather easy to see that the Church-Rosser property fails in general for dual systems. An example which shows that the reduction relation lacks this property goes as follows. Consider a (rather minimal) combinatory base, B₀= {T,I, -T}. T is the elementary permutator which is defined either as CI or by the axiom Txy º yx. This is Curry's C_*—denoted by T by Smullyan. The term ((T(I -T))Q) (where Q is any combinatory term over B₀) is a well-formed term and it reduces in one step to (Q(I -T)) as well as to ((IT)Q) depending which redex is contracted. These two terms do not reduce immediately to a common term, moreover, the only possible further reductions are (Q -T), (IQ) and (TQ). There is a substitution for Q, namely, (T -T) which makes two of these terms to further reduce to a common term. Under this substitution the first and the third term both reduce to (-TT). However, (IQ) reduces to (T -T) or (TI). This particular substitution shows that the set of terms over B₀ is not confluent. A more complicated argument is needed to show that in fact the three terms do not reduce to a common term under any possible substitution, and here one has to use the fact that B₀does not contain any cancellative combinator, thus, whatever is substituted for Q, stays in the term unless it is a head of a redex and contracted.

If reduction has the Church-Rosser property, then the consistency of the system is almost immediate. Since we showed by a counterexample that dual systems in general do not have this property it is natural to consider whether these systems are consistent, or to what extent they are consistent and to what extent they are inconsistent, "collapse."

2. Varieties of triviality.

Inconsistency of a (dual) system means that for any term X and Y we have X =_wY. In general, combinatory logics include some primitive terms (variables) which are assumed to be distinct from the combinators (and the compound terms). Thus, to show that a system is inconsistent we have to show that any two terms, including any two variables, are weakly equal. We observed above—using l-terms—that certain terms formed from functional terms do not reduce to any other term. As an illustration let us consider a combinatory base B₁containing a combinator Q and its dual -Q, where Q and -Q are not the one-place identity combinator and its dual. The reason for this requirement will become clear later on. The term -QQ is a well-formed term over this base, and it has two properties: (i) it is essentially irreducible and (ii) it is essentially inapplicable. (i) is meant to capture the fact that there is no other term to which -QQ reduces. (ii) is a perhaps surprising feature of this term, namely, that despite the fact that this term resembles, for a superficial glance, a functional term which can be supplied by arguments and so turned into a redex, in fact it cannot be turned into a redex no matter how many objects and in what grouping are added on either side. Take—for the sake of an example—Q to be a 1-place combinator. Then neither (x(-QQ)) nor ((-QQ)x) contain a redex, because the x-s are wrongly grouped to form a redex with -Q and Q, respectively, in the two terms. Of course, the same argument holds for any n-place (n > 1) combinator. Since terms having the properties (i) and (ii) are really like stones—they do not disappear easily—I will simply call them stone-terms. It is immediate that all the variables are stone-terms. Since the rest of the stone-terms (the non-variables) look like a useless kind of combinatory terms, I define the set of the good terms by a simultaneous recursive definition where the superscript indicates the arity of the combinator:

0. if x_i is a variable, then x_i Î good;
1. if Q is a (right-looking) combinator, then Q Î good+;
2. if -Q is a dual (left-looking) combinator, then -Q Î good-;
3. if X_iⁿÎ good+ and X_jÎ good± then
        (X_i X_j )^n-1Î good+ if n ³ 2;
        { (X_i X_j ) ^n-1Î good otherwise.
4. if X_iⁿÎ good- and X_jÎ good± then
        (X_j X_i )^n-1Î good- if n ³ 2;
        { (X_j X_i ) ^n-1Î good otherwise.
5. if X_iÎ good and X_jÎ good È good+ then (X_i X_j )Î good;
6. if X_iÎ good È good- and X_jÎ good then (X_i X_j )Î good;
7. good± = good È good+ È good-.

A somewhat unfortunate fact about the good terms, the terms in good± above, is that this set is not closed under reduction. This means that the existence of stone-terms (which is trivial in any dual system) is not sufficient to prove consistency. While stone-terms really do not reduce to anything and so they do not disappear via reduction, good terms might reduce to stone-terms and so a stone-term might be weakly equal to a good term. As an example consider the combinatory base B₂= {T, -T}, and the term (T(T -T))-T. It is easy to check that -TT _ (T(T -T)) -T _ T-T, therefore, -TT =_w T-T. The term on the left of equality is a stone term, the term we started with and the one on the right of the equality are good terms. All these definitions and examples stress again that we can show inconsistency if we can show that two variables are equal. I recall briefly the result of a reasoning reflected in Meyer, Bimbó & Dunn 1997: to show two variables to be equal the system must contain a cancellative combinator in the sense of Curry. A combinator Q is called a cancellator if Qx₁. . . x_nº (x_j1 . . . x_jm) and ($ x_k)(1 £ k £ n Ù ("l)(1 £ l £ m ® x_k ¹ x_jl)). Probably the nicest example, suggested by R.K. Meyer, involves the elementary cancellator K and its dual -K: ( K x)(y -K) (where x and y are arbitrary terms, possibly variables). This term reduces to x on one hand, and to y on other, thus, giving x = _w y . The key in the argument is to notice that a term containing two different variables can reduce to either of them only if one of the two is dropped off from the term. As a side remark I note that it is known in the l folklore that (l xy. x) trivializes the symmetric l -calculus.

In the remaining part of this paper I investigate what happens when a dual system contains the usual identity combinators. Let us assume that we have a combinatory base B₃ containing some combinators (but not the one-place identity combinator I) and some dual combinators among them the dual identity combinator -I. Consider Q_iÎ B₃, an n-place combinator, and the term X formed from it as follows:

X = ( . . .(( Q_i^-I) . . . )^-I)
n n

We have X 8 -I and X 8 Q_i. It is easier to see that the term X really reduces to the first term, so I start with arguing this case: Q_i is an n-place combinator and it is followed by a sequence of dual identity combinators. The whole sequence is left associated. We simply apply the appropriate axiom for Q_i which gives a sequence of -I-s, since Q_i is a pure combinator. Now, use an easily provable fact, namely, that any finite sequence of -I-s, independently of grouping, reduces to a single -I; in other words, any term consisting exclusively of one-place dual identity combinators reduces to -I in finitely many steps. This justifies the first reduction.

To see that the second reduction holds as well, it is enough to consider the original term from right to left. Since -I is a 1-place combinator, for each -I there is a properly associated argument for it on the left—since any term is properly associated to be an argument of a one-place combinator. The identity combinators do not do anything, so to speak, they just "drop off themselves" from the expression, so in n steps X reduces to the leftmost combinator of the expression, i.e., to Q_i.

From these two facts by the definition of weak equality we obtain -I =_wQ_i. If there are other combinators than Q_iin the base B₃, let us say, Q_jÎ B₃, then we have—using the very same reasoning — that -I =_wQ_j. Applying transitivity and symmetry of =_w, we get Q_i=_wQ_jfor arbitrary combinators Q_i and Q_j. This means that the dual identity combinator collapses all the combinators. Note that it does not necessarily follow that all the combinators and dual combinators collapse, since the argument above hinged on Q_i and Q_j being combinators directed to the right. However, it is possible that conflating all the combinators and the dual identity combinator all the combinatory expressions lacking variables become weakly equal to each other.

Depending on the left-right symmetry for so long I will not repeat the argument for a symmetric situation when the combinatory base contains some dual combinators, and the one-place identity combinator, I, is also a member of the combinatory base. All the dual combinators become weakly equal to the identity combinator. Taking any combinatory base which includes both the 1-place identity combinator and its dual the whole purely combinatory part of the system collapses, since I3 (I -I)4 -I. This result does not mean by itself that the whole system is inconsistent, since if there are no cancellative combinators, then the distinct variables cannot be shown to be weakly equal.(2)

3. Conclusions

Lastly, it is interesting to quickly answer the question what happens if we add the identity combinator (l x. x) to the symmetric l -calculus. Really, it is obvious from the previous paragraph that this collapses a great part of the system. We could mimic the symmetric case in the dual one having shown I = _w-I : in each term in each reduction we substitute I or -I depending on the reduction we wish to perform on a symmetric term. The converse, however, is false. Since in the symmetric l -calculus functions are bidirectional there is nothing to block the application of the symmetric identity. That is, adding one-place identity to the symmetric l -calculus is more devastating than adding one of the two halves of it, so to speak, to a dual system. Although it was not the main purpose of this paper, still it should be pointed out as a conclusion that this result also supports the earlier claim I made in Section 1 that dual combinatory systems (and a dual l-calculus) are worthwhile objects of further investigations.