Lambek-Calculus-Recognizing-Power-and-Complexity.pdf
《Lambek-Calculus-Recognizing-Power-and-Complexity.pdf》由会员分享,可在线阅读,更多相关《Lambek-Calculus-Recognizing-Power-and-Complexity.pdf(14页珍藏版)》请在三一文库上搜索。
1、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 ca
2、lculus3 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 notio
3、n 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
4、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
5、 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 comple
6、xity 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 exi
7、st 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
8、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
9、 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 form
10、at. 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
11、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
12、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
13、 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. 2
14、Lambek 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 formul
15、a. 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-
16、 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 fragm
17、ent. 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. recognizi
18、ng 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 undecidabl
19、e 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 co
20、mplete 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 un
21、decidable, 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
22、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 applicatio
23、n 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
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- Lambek Calculus Recognizing Power and Complexity
链接地址:https://www.31doc.com/p-3789370.html