Lambek-Calculus-Recognizing-Power-and-Complexity.pdf

Lambek Calculus: Recognizing Power and Complexity Makoto Kanazawa Abstract I survey known results and results that easily follow from known results about the recognizing power and complexity of various fragments of the Lambek calculus. Contents 1Complexity and recognizing power of logics2 2Lambek calculus3 3Multiplicative-exponential Lambek calculus5 4Multiplicative-additive Lambek calculus8 5Multiplicative Lambek calculus12 1Complexity and recognizing power of logics We fi rst have to explain what we mean by the complexity and the recognizing power of a logic. To most people, the former notion should be familiar, but the latter may sound novel. We assume that a logic K is presented in the form of a sequent calculus, which is the favorite format for substructural logics. A sequent is an expression of the form A1,.,Am B1,.,Bn where m,n 0 and A1,.,Am,B1,.,Bnare formulas.1We denote the set of well-formed formulas of K by FormKand the set of sequents of K by SeqK. Any logic K determines the set ProvKof provable sequents. Members of ProvK are expressions made up from a fi nite stock of symbols, so ProvKis a language in the sense of formal language theory. The complexity of K is defi ned to be the complexity-theoretic characteristic of this language ProvK. We can be said to have determined the complexity of K if we have succeeded in locating ProvKprecisely in the space of complexity classes as we know it today. Thus, if we know that ProvKis, say, PSPACE-complete, we know the complexity of K, in which case we also say that K is PSPACE-complete. The complexity of a logic K is the property of a single language associated with K.In contrast, the recognizing power of K has to do with a class of languages. Given a fi xed alphabet , K is said to recognize a language L + if there exist some fi nite subset A of FormK, some B FormK, and some relation R × A such that L = w +| (w e R B ProvK), where e R × Form K is the extension of R to a relation between strings of symbols and strings of formulas: w e R w = = ? cvAFormKForm K (w = cv = A c R A v e R ). Then RecK is defi ned to be the class of all languages (over ) recognized by K. Note that in this defi nition, the empty string is disregarded, so that languages recognized consist of non-empty strings.This is for the sake of simplifying some results. Henceforth, when we talk about recognizing power, we simply say language to mean language without the empty string.We know the recognizing power of K when we can characterize RecKin terms of familiar notions from formal language theory, e.g., when we know that RecKis the class 1Sometimes one-sided sequents of the form A1,.,An are used, but we use the more general two-sided format. 2 of all context-free languages (i.e., context-free languages that do not include the empty string). The notion of recognizing power has its origin in the Lambek calculus, where a pair hR,Bi with R ×A for some fi nite A is viewed as a grammar. Yet the notion applies to any logic presented in the form of a sequent calculus. When G = hR,Bi, where R and B are as above, we say that G is a K-grammar, and write L(G) for the language w +| (w e R B ProvK). There are some properties of RecK that do not depend on any specifi c choice of K. For instance, RecKis always closed under strictly alphabetic morphisms, homomorphisms that are length-preserving. Also, if K2is a conservative ex- tension of K1, one has RecK1 RecK2. Some connections between ProvKand RecKare apparent. For instance, if ProvKis recursive, then all languages in RecKare recursive, and likewise, if ProvKis in NP, RecKis a subclass of NP. An additional interest of investigating RecKlies in the fact that it sometimes admits of a natural language-theoretic characterization which cannot be captured by a rough complexity-theoretic measure, and which sometimes provides valuable additional information about the logic in question. 2Lambek calculus We are interested in a family of logics related to the system fi rst presented in Lambek 1958, 1961. In modern terms, they are systems of noncommutative intuitionistic propositional linear logic. In these systems, sequents are of the form A1,.,Am B having exactly one succedent formula. Lambek also required that m 1, but we choose not to do so here. So the antecedent of a sequent can be empty. This choice is signifi cant in just one place. There are six propositional connectives: , , , the multiplicative- additive Lambek calculus (MALC), which has the mulitplicatives and the ad- ditives but not the exponential; and the multiplicative-exponential Lambek cal- culus (MELC), which has the mulitplicatives and the exponential. The full Lambek calculus with all the connectives mentioned so far has the same recog- nizing power and complexity as the multiplicative-exponential fragment. What is known about the recognizing power and complexity of the three calculi is 4 summarized in Table 1. The complexity of MLC and the recognizing power of MALC have not been precisely characterized. In the following sections, we will review these results in turn, starting with MELC. recognizing powercomplexity MLC= CFL NP MALC fi nite intersections of CFLsPSPACE-complete MELC= r.e.undecidable (r.e.-complete) Table 1: Recognizing power and complexity of various fragments of the Lambek calculus. 3Multiplicative-exponential Lambek calculus Lincoln et al. (1992) show that MELC is undecidable by a reduction from semi-Thue systems.Their proof is given in the one-sided cyclic format for noncommutative linear logic, but the idea is even more transparent with the two-sided intuitionistic format adopted here. The proof provides an exact char- acterization of the complexity of MELC: it is complete for the r.e. sets (under computable many-one reductions). It also shows that MELC recognizes all r.e. languages. The main idea is coding of MLC theories in MELC formulas. Since MLC provability in a theory, even for the fragment MLC() with as the only connective, is quite easily shown to be undecidable, the coding can be used to show the undecidability of MELC (or MELC(,!) is necessary for the coding purpose).2 A K theory is just a fi nite subset of SeqK. If T is a K theory, a sequent of K is provable in K + T if there is a derivation of it which is just like a proof in K (possibly with applications of Cut) except that sequents in T may appear at some leaves. The following lemma about MLC may be proved using standard cut elim- ination techniques. Lemma 1. Let T be an MLC theory. If an MLC sequent t is provable in MLC + T, then there is a proof of t in MLC + T where every application of Cut involves an axiom in T as one of its premises. For any theory T = t1,.,tl , its translation T is defi ned to be the sequence !t1,.,!tl, where for any sequent A1,.,An B, A1,.,An B is the formula (A1 ··· An)B. 2We sometimes denote a calculus with a restricted set of connectives by displaying the connectives, as we do here. 5 Lemma 2. Let T be an MLC theory, and let D be an MLC sequent. Then the following are equivalent: (i) D is provable in MLC + T. (ii) T, D is provable in MELC. Proof.(i) (ii).By induction on the depth of proof, noting that if A1,.,An B T, T,A1,.,An B is provable in MELC. (ii) (i). Remove all occurrences of formulas of the form !t from a proof of T, D. All applications of rules for the mulitplicatives remain applications of the same rule. Applications of !W, !C1, and !C2become repetitions of the same sequent, so just delete one of the two occurrences. Applications of (! ) change as follows: . . . ,A1,.,An B, C ,!A1,.,An B, C ; . . . 0,A1,.,An B,0 C 0,0 C Then we can change all such parts simultaneously as follows: A1,.,An B . . . . A1,.,An B . . . 0,A1,.,An B,0 C 0,0 C Cut making the resulting fi gure a proof of D in MLC + T.a Note that in the above proof it is crucial to allow a sequent to have an empty antecedent. We now describe a reduction from type 0 grammars of Chomsky to MELC(,!). A type 0 grammar G is a quadruple h,N,S,Pi, where is a fi nite alphabet, N is a fi nite set of nonterminals disjoint from , S is a designated member of N, and P is a fi nite set of rewriting rules of the form , where ( N)+and ( N). The rewrites relation G associated with G is defi ned by the following axioms and rule: for ( N)+ for P G is defi ned to hold if is derivable using the above axioms and rule. This defi nition of G is diff rent from, but equivalent to, the standard defi nition. The language generated by G, denoted L(G), is defi ned to be w | S G w. 6 Given a type 0 grammar G = h,N,S,Pi, we defi ne an MLC theory TG as follows.Suppose = c1,.,cm and let N = D1,.,Dn.We put N = c1,.,cm D1,.,Dn into a one-one correspondence with a set p1,.,pm+n of atomic formulas. For any expression of the form X1.XiY1.Yj, where X1,.,Xi,Y1,.,Yj N and i 1, we associate the following sequent as its translation (X1.XiY1.Yj): q1,.,qj r1 ··· ri, where q1,.,qjand r1,.,riare atomic formulas that correspond to Y1,.,Yj and X1,.,Xi , respectively, by (note the fl ip-fl op of the two sides). Let TG= ( ) | P . We have the following: Lemma 3. For any ( N)+and ( N), G holds if and only if ( ) is provable in MLC + TG. The proof is straightforward, given our defi nition of G. By Lemmas 2 and 3, we get Lemma 4. Let G = h,N,S,Pi be a type 0 grammar.For any w , w L(G) if and only if TG, q is provable in MELC, where q = (S w). Since the question w L(G)? is undecidable, we get Theorem 5 (Lincoln et al.). Provability in MELC is undecidable. In fact, since type 0 grammars generate all r.e. sets, it follows that the set ProvMELCis complete for the r.e. sets. Also, note that TG, D is provable if and only if O TGD is, where N(A 1,.,An) is A1 ··· An. Then Lemma 4 implies Theorem 6. MELC recognizes all r.e. languages. 7 The present reduction uses only the connectives , , and !, so the above results hold of MELC(,!). Kanovich (1993) shows that MELC(,!) is undecidable by a reduction from a two-counter machine. In fact, Buszkowski (1982) has shown that provability in MLC() theories is undecidable by a reduction from type 0 grammars.Since we can use An(.(A1B).) in place of (A1 ··· An)B in Lemma 2 and Theorem 6, it follows that MELC(,!) already has the same complexity and recognizing power as the full (multiplicative-additive-exponential) Lambek calculus. As noted above, it is crucial to allow sequents with empty antecedent to capture provability in MLC theories by provability in MELC. To the best of my knowledge, there is no published proof that the MELC with Lambeks nonempty antecedent requirement has the same complexity and recognizing power as the MELC without the requirement.3 4Multiplicative-additive Lambek calculus Lincoln et al. (1992) show that multiplicative-additive linear logic is PSPACE- complete by reducing quantifi ed Boolean formula satisfi ability (QBF). Adapting their proof, we can show the same for multiplicative-additive Lambek calculus (MALC).(I arrived at this proof in ignorance of Kanovich 1994, where a similar proof is provided.) The key observation here is that satisfi ability of closed quantifi ed Boolean formulae whose quantifi er-free matrix is in disjunctive normal form (DNF) is already PSPACE-complete. This enables us to do away with the Exchange rule which was necessary in Lincoln et al.s encoding. Linear negation also turns out to be unnecessary. Let x1,x2,x3,. be the set of propositional variables. Without loss of generality, we can assume that a closed quantifi ed Boolean formula is of the form Q1x1.Qnxn(D1 ··· Dm),(1) where for each i, Qiis either or and Diis a conjunction of literals from x1,.,xn,¬x1,.,¬xn such that for every j, at most one of xjand ¬xj occurs in Di . Satisfi ability of such formulas is PSPACE-complete. This follows from the well-known fact that satisfi ability of quantifi ed Boolean formulae with conjunctive normal form (CNF) matrix is PSPACE-complete and the fact that PSPACE = co-PSPACE. We fi rst show how the quantifer-free matrix M = D1···Dmof (1) can be encoded in MALC. Corresponding to the literals in M, the MALC encoding uses atomic formulas x1, ¯ x1,.,xn, ¯ xn. Each disjunct is translated as follows: Di = y1 ··· yn, 3In personal communication (1996), Max Kanovich informed me that MELC with Lam- beks requirement is undecidable. 8 where yj= xjif xjoccurs in Di, ¯ xjif ¬xjoccurs in Di, (xj ¯ xj)otherwise. Note that in the translation of Di, the propositional variables appear in the sorted order. Then the translation of the DNF matrix is given by D1 ··· Dm = D1 ··· Dm. If I is an assignment of truth values to propositional variables x1,.,xn, then we let I = y1,.,yn where yj= ( xjif I(xj) = true, ¯ xjif I(xj) = false. The following lemma is straightforward. Lemma 7. Let M be a DNF formula in propositional variables x1,.,xn, and let I be an assignment of truth values to x1,.,xn. Then I |= M if and only if I M is provable in MALC. To translate quantifi ed formulas,we introduce new atomic formulas q0,q1,.,qn . We translate each quantifi er as follows: xi = qi1(xi qi) (¯ xi qi), xi = qi1(xi qi) the latter ques- tion is undecidable by the proof of Theorem 5. In fact, the linear logic counter- parts of the two questions are equivalent (see Ono 1998). This is not so in the Lambek calculus. The following simple example shows that the two questions are not equivalent. p1,p2,p3 p1 p2 p3 p1,!p2,p3 p1 p2 p3 . . . . p1,p3,!p2 p1 p2 p3 p1 p3,!p2 p1 p2 p3 !(p1 p3),!p2 p1 p2 p3 As the above proof shows, the sequent !(p1p3),!p2 p1p2p3is provable, but there is no sequence p1p3,p2such that p1p2p3is provable. 4A sequent of the form: p0(p1(.pm).) q0(q1(.qn).) is provable if and only if m = n and pi= qifor i = 0,.,m. 5The term strong reducibility is from Ono 1998. This was called -derivability by van Benthem (1991). 13 Note also that the above result about the recognizing power of MALC (The- orem 11) implies that MALC has an undecidable strong deducibility problem, in contrast to MLC. This follows from the fact that the question of whether given two context-free languages have a non-empty intersection is undecidable. Here we see that a language-theoretic characterization of the recognizing power of a logic can help to settle more standard questions about the logic. References van Benthem, J.1991.Language in Action.Amsterdam: North-Holland. (Second edition 1995, MIT Press.) Buszkowski, W. 1982. Some decision problems in the theory of syntactic cat-