Dual Identity Combinators(1) Katalin Bimbó

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 firstorder logic. Schönfinkel used functions to provide a translation for a closed firstorder formula into a functional expression, thereby eliminating bound variables of firstorder logic. About the success of this attempt cf. Curry & Feys 1968: beyond this primarily intended connection between firstorder logic and (illative) combinatory logic there is another connection between the two, the so called CurryHoward isomorphism (Curry & Feys 1968, Howard 1980). This relates combinators to implicational formulae. It is just a small step from the CurryHoward isomorphism to put combinatory bases (which are possibly combinatorially noncomplete) into correspondence with logical systems. It is wellknown, 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: ( . . . ( ( Q_{ }x_{1 }) . . . ) 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 onestep reduction (4 _{1}), 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 noncomplete combinatory base. The onestep reduction over the base B (4 _{1,B}) is defined as follows: if Q Î B, and Qx_{1} . . . x_{n }º ( x_{i} 1 . . . x_{i m }) is the axiom for Q, then U [Qx_{1} . . . x_{n}] 4 _{1,B} U [Qx_{1} . . . x_{n} / Qx_{i }1 . . . x_{i m }], where U [Y ] denotes a particular nonvacuous 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,B }Y if there are X_{ 0 }, . . . , X_{ n} ( n ³ 0), such that X _{0 }º 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 onestep 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 lcalculus as well. Combinators are by definition closed lterms. The pure combinators I considered above form a proper subset of the closed lterms. Notably, the set of closed lterms contains terms which correspond to the fixed point combinators—those are not pure according to the definition of pure combinators above. In the ordinary lcalculus 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 lcalculus. 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. lcalculus. In the usual l I or l Kcalculus 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 labstracts 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 labstracts 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 labstracts does not give new reductions. Taking functions and application as unidirectional but having opposite directions leads to an uninteresting empty theory. Probably, intuitively the lcalculus 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 lcalculus, 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 lcalculus. Here both the labstracts 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 lcalculus. In this case, there is nothing more to add as far as directionality is concerned. Dual lcalculus. Dual lcalculus 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 labstracts have the same direction, then even having bidirectional application does not give more than the usual lcalculus. Second, it would be useless to add bidirectionality (or different unidirectionality) for the labstracts 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 lcalculus. Taking all the functions of the usual lcalculus to be directed to the right, all the reductions which are possible in the original lcalculus are also possible here. On the other hand, while a term (l x.M )( l y.N ) is always reducible in the symmetric lcalculus (since both functions are bidirectional), a superficially similar term (l x.M )( l y.N )® does not contain any redex and does not reduce to anything in the dual lcalculus. Thus, allowing duality in the system (with bidirectional application) supplies additional distinctions with respect to both the usual lcalculus and the symmetriccalculus. 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 fullfledged 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 ChurchRosser 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_{0 }= {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_{0 }) is a wellformed 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_{0} 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_{0 }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 ChurchRosser 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 =_{w }Y. 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 lterms—that certain terms formed from functional terms do not reduce to any other term. As an illustration let us consider a combinatory base B_{1 }containing a combinator Q and its dual Q, where Q and Q are not the oneplace identity combinator and its dual. The reason for this requirement will become clear later on. The term QQ is a wellformed 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 1place combinator. Then neither (x(QQ)) nor ((QQ)x) contain a redex, because the xs are wrongly grouped to form a redex with Q and Q, respectively, in the two terms. Of course, the same argument holds for any nplace (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 stoneterms. It is immediate that all the variables are stoneterms. Since the rest of the stoneterms (the nonvariables) 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; 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 stoneterms (which is trivial in any dual system) is not sufficient to prove consistency. While stoneterms really do not reduce to anything and so they do not disappear via reduction, good terms might reduce to stoneterms and so a stoneterm might be weakly equal to a good term. As an example consider the combinatory base B_{2 }= {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_{1 }. . . x_{n }º (x_{j}1 . . . 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_{3} containing some combinators (but not the oneplace identity combinator I) and some dual combinators among them the dual identity combinator I. Consider Q_{i }Î B_{3 }, an nplace combinator, and the term X formed from it as follows: X = ( . . .(( Q_{i
}^{ }I) . . . )_{ }^{ }I) 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 nplace 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 Is, since Q_{i} is a pure combinator. Now, use an easily provable fact, namely, that any finite sequence of Is, independently of grouping, reduces to a single I; in other words, any term consisting exclusively of oneplace 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 1place 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 oneplace 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 =_{w }Q_{i }. If there are other combinators than Q_{i }in the base B_{3 }, let us say, Q_{j }Î B_{3 }, then we have—using the very same reasoning — that I =_{w }Q_{j }. Applying transitivity and symmetry of =_{w }, we get Q_{i }=_{w }Q_{j }for 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 leftright symmetry for so long I will not repeat the argument for a symmetric situation when the combinatory base contains some dual combinators, and the oneplace 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 1place 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 oneplace 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 lcalculus) are worthwhile objects of further investigations. 
Notes (1) I wish to thank Michael Dunn and Robert Meyer for introducing dual combinators to me, as well as, for discussing them with me. I also wish to thank the Cognitive Science Program of Indiana University for a fellowship what I held at the time when I worked on this paper. (2) A more detailed and formal investigation of the problems of inconsistency and of the ChurchRosser property can be found in Bimbó 199+. References Barbanera, F. & S. Berardi 1996. `A symmetric lambda calculus for classical program extraction', Information and Computation 125 (1996), pp. 103–117. Barendregt, H.P. 1984. The Lambda Calculus: Its Syntax and Semantics, (rev.ed.), NorthHolland, Amsterdam &c. Bimbó, K. 199+. `Investigation into combinatory systems with dual combinators’, to appear in Studia Logica. Church, A. 1941. Calculi of Lambdaconversion, (Annals of Mathematical Studies 6), Princeton University Press, Princeton. Curry, H.B. 1930. `Grundlagen der kombinatorischen Logik', [`Foundations of combinatory logic’] American Journal of Mathematics 52 (1930), pp. 509–536, 789–834. Curry, H.B. & R. Feys 1968. Combinatory Logic, v.I, NorthHolland, Amsterdam. Dunn, M. 1986. `Relevance logic and entailment', in: Gabbay, D. & F. Guenthner (eds.), Handbook of Philosophical Logic, v.III, pp. 117–224. Dunn, M. & R. Meyer 1997. `Combinators and structurally free logic', Logic Journal of IGPL 5 (1997), pp. 505–537. Hindley, J.R. & J.P. Seldin 1986. Introduction to Combinators and l calculus, (London Mathematical Society student texts 1), Cambridge University Press, Cambridge. Howard, W.A. 1980. `The formulaeastypes notion of construction', in: Seldin, J.P. & J.R. Hindley (eds.), To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, London &c., pp. 479–490. Meyer, R.K. 1976. `A general Gentzen system for implicational calculi', Relevance Logic Newsletter 1 (1976), pp. 189–201. Meyer, R.K., K. Bimbó & J.M. Dunn 1997. `Dual combinators bite the dust', (abstract), forthcoming in The Journal of Symbolic Logic. (Presented by title at the Annual Conference of the Australasian Association for Logic, July 4–6, 1997, University of Auckland, New Zealand.) Schönfinkel, M. 1924. `Über die Bausteine der mathematischen Logik', Mathematische Annalen 92 (1924), S. 305–316. [`On the building blocks of mathematical logic', in: van Heijenoort, J. (ed.), From Frege to Gödel: A Source Book in Mathematical Logic, Harvard University Press, Cambridge (MA), 1967, pp. 355–366.] Smullyan, R.M. 1968. Firstorder Logic, Dover, New York, 1995. ^{} 