key: cord-0046628-a7izel0u authors: Kanovich, Max; Kuznetsov, Stepan; Nigam, Vivek; Scedrov, Andre title: Soft Subexponentials and Multiplexing date: 2020-05-30 journal: Automated Reasoning DOI: 10.1007/978-3-030-51074-9_29 sha: a0ff95c91c10f3c6a05f01f836ab3c818c6d7cae doc_id: 46628 cord_uid: a7izel0u Linear logic and its refinements have been used as a specification language for a number of deductive systems. This has been accomplished by carefully studying the structural restrictions of linear logic modalities. Examples of such refinements are subexponentials, light linear logic, and soft linear logic. We bring together these refinements of linear logic in a non-commutative setting. We introduce a non-commutative substructural system with subexponential modalities controlled by a minimalistic set of rules. Namely, we disallow the contraction and weakening rules for the exponential modality and introduce two primitive subexponentials. One of the subexponentials allows the multiplexing rule in the style of soft linear logic and light linear logic. The second subexponential provides the exchange rule. For this system, we construct a sequent calculus, establish cut elimination, and also provide a complete focused proof system. We illustrate the expressive power of this system by simulating Turing computations and categorial grammar parsing for compound sentences. Using the former, we prove undecidability results. The new system employs Lambek’s non-emptiness restriction, which is incompatible with the standard (sub)exponential setting. Lambek’s restriction is crucial for applications in linguistics: without this restriction, categorial grammars incorrectly mark some ungrammatical phrases as being correct. For the specification of deductive systems, linear logic [4, 5] , and a number of refinements of linear logic have been proposed, such as commutative [23, 25] and non-commutative [11, 12] subexponentials, light linear logic [7] , soft linear logic [16] , and easy linear logic [10] . The key difference between these refinements is their treatment of the linear logic exponentials, !, ?. These refinements allow, e.g., a finer control on the structural rules, i.e., weakening, contraction and exchange rules, and how exponentials affect the sequent antecedent. For example [12] , we proposed a logical framework with commutative and noncommutative subexponentials, applying it for applications in type-logical grammar. In particular, we demonstrated that this logical framework can be used to "type" correctly sentences that were not able before with previous logical frameworks, such as Lambek calculus. However, as we have shown recently, our logical framework in [12] is incompatible with the important Lambek's non-emptiness property [15] . This property, which requires all antecedents to be non-empty, is motivated by linguistic applications of Lambek-like calculi. Namely, it prevents the system from recognizing ("typing") incorrectly formed sentences as grammatically correct. We discuss these linguistic issues in detail in Sect. 3 . The lack of Lambek's restriction means that the logical framework proposed in our previous work is too expressive, typing incorrectly sentences. To address this problem, we propose a new non-commutative proof system, called SLLM, that admits Lambek's non-emptiness condition and at the same time is expressive enough to type correctly sentences in our previous work. This system is also still capable of modelling computational processes, as we show in Sect. 5.1 on the example of Turing computations. In particular, SLLM takes inspiration from the following refinements of linear logic: subexponentials, by allowing two types of subexponentials, ! and ∇; soft linear logic, which contributes a version of the multiplexing rule, ! L , shown below to the left; and light linear logic, which contributes the two right subexponentials rules, ! R , ∇ R , shown below to the right. In our version of the system, the premise of the rule ! L does not allow zero instances of F . Hence, ! is a relevant subexponential as discussed in [12] . This rule is used to type sentences correctly, while the rules ! R and ∇ R are used to maintain Lambek's condition. SLLM contains, therefore, soft subexponentials and multiplexing. Our main contributions are summarized below: -Admissibility of Cut Rule: We introduce the proof system SLLM in Sect. 2. We also prove that it has basic properties, namely admissibility of Cut Rule and the substitution property. The challenge is to ensure a reasonable balance between the expressive power of systems and complexity of their implementation, and in particular, to circumvent the difficulties caused by linear logic contraction and weakening rules. -Lambek's Non-Emptiness Condition: We demonstrate in Sect. 3 that SLLM (and thus also SLLMF) admits Lambek's non-emptiness condition. This means that SLLM cannot be used to "type" incorrect sentences. We demonstrate this by means of some examples. -Focused Proof System: We introduce in Sect. 4 a focused proof system (SLLMF) proving that it is sound and complete with respect to SLLM. The focused proof system differs from the focused proof system in our previous work [12] by allowing a subexponential that can contract, but not weaken nor be exchanged. Such subexponentials were not allowed in the proof system introduced in [12] . A key insight is to keep track on when a formula necessarily has to be introduced in a branch and when not. -Complexity: We investigate in Sect. 5 the complexity of SLLM. We first demonstrate that the provability problem for SLLM is undecidable in general and identify a fragment for which it is decidable. Finally, in Sect. 6, we conclude by pointing to related and future work. The Non-commutative System SLLM with Multiplexing As the non-commutative source, we take the Lambek calculus [17] , Table 1 , the well-known fundamental system in linguistic foundations. The proof system introduced here, SLLM, extends the Lambek calculus by adding two new connectives (subexponentials) ! and ∇ and their rules in Table 2 . Drawing inspiration from commutative logics such as linear logic [6] , light linear logic [7] , soft linear logic [16] , and easy linear logic [10] , here we introduce our primitive non-commutative modalities !A and ∇A controlled by a minimalistic set of rules. Multiplexing Rule (local): Informally, !A stands for: "any positive number of copies of A at the same position". Remark 1. In contrast to soft linear logic and light linear logic, where Weakening is one of the necessary ingredients, here we exclude the Weakening case: (k = 0). Unlike Contraction rule that can be recursively reused, and !A keeps the subexponential (it is introduced by Dereliction), our Multiplexing can only be used once with all copies provided immediately at the same time in one go, and the subexponentials get removed. Thus, if one wishes to reuse Multiplexing further in the proof, nested subexponentials would be needed (like !!A for two levels of Multiplexing). The second subexponential, ∇A, provides the exchange rule. Exchange Rule (non-local): and Dereliction Rule (local): "∇A can be thought of as storing a missing candidate A in a fixed local storage, with the ability to deliver A to the right place at the appropriate time." Remark 2. Notwithstanding that the traditional Promotion rule Γ → C !Γ → !C is accepted in linear logic as well as in soft linear logic, we confine ourselves to the restricted light linear logic promotion A → C !A → !C , in order to guarantee cut admissibility for the non-commutative SLLM (cf. [11] ). E.g., with is derivable by cut but, to finalize a cut-free proof for (4), we need commutativity: The following theorem states that SLLM enjoys cut admissibility and the substitution property. (a) The calculus SLLM enjoys admissibility of the Cut Rule: Proof. (a) By reductions. E.g., In this Section we illustrate how (and why) our modalities provide parsing complex and compound sentences in a natural language. We start with standard examples, which go back to Lambek [17] ; for in-depth discussion of linguistic matters we refer to standard textbooks [3, 19, 21] . The sentence "Bob sent the letter yesterday" is grammatical, and the following "type" specification is provable in Lambek calculus, Table 1 . Here the 'syntactical type' N stands for nouns "the letter" and "Bob", and ((N \S)/N ), i.e., (V /N), for the transitive verb "sent", and (V \V ) for the verb modifier "yesterday", where V = (N \S). The whole sentence is of type S. Lambek's non-emptiness restriction is important for correctness of Lambek's approach to modelling natural language syntax. Without this restriction Lambek grammars overgenerate, that is, recognize ungrammatical phrases as if they were correct. The standard example [19, § 2.5] is as follows: "very interesting book" is a correct noun phrase, established by the following derivation: The sequent above is derivable in the Lambek calculus. Without Lambek's restriction, however, one can also derive (N / N) /(N / N), N → N (since → N / N is derivable with an empty antecedent). This effect is unwanted, since the corresponding phrase "very book" is ungrammatical. Thus, Lambek's non-emptiness restriction is a highly desired property for linguistic applications. Fortunately, SLLM enjoys Lambek's non-emptiness property. That is: The calculus SLLM provides Lambek's non-emptiness restriction: If a sequent Γ → C is derivable in the calculus then the list of formulas Γ is not empty. Proof. The crucial point is that, in the absence of Weakening, !A never happens to produce the empty list. Theorems 1 and 2 show how our new system SLLM resolves the issues discussed in [15] for the case of the Lambek calculus extended with a full-power exponential in linear logic style. Namely, as we show in that article, no reasonable extension of the Lambek calculus with the exponential modality can have the three properties simultaneously: -cut elimination; -substitution; -Lambek's restriction. Moreover, as also shown in [15] , for the one-variable fragment the same happens to the relevant subexponential, which allows contraction and permutation, but not weakening. Our new system overcomes these issues by refining the rules for subexponentials. Now let us show how one can use subexponentials of SLLM to model more complicated sentences. Our analysis shares much with that of Morrill and Valentín [22] . Unlike ours, the systems in [22] do not enjoy Lambek's restriction. (1) The noun phrase: "the letter that Bob sent yesterday," is grammatical, so that its "type" specification (6) should be provable in Lambek calculus or alike: Here ((N \ N ) / S stands for a subordinating connective "that". As a type for the whole dependent clause, "Bob sent yesterday, we take some S , not a full S, because the direct object, "the letter", is missing. Our solution refines the approach of [2, 20] . We mark the missing item, the direct object "the letter" of type N , by a specific formula ∇N stored at a fixed local position and by means of Exchange Rule (2) and Dereliction Rule (3) deliver the missing N to the right place with providing which is the type specification for the sentence "Bob sent the letter yesterday " completed with the direct object, "the letter". By taking S = (∇N \S), we can prove (6): "Bob sent the letter yesterday" If we allowed Weakening, we would prove the ungrammatical "the letter that Bob sent the letter yesterday," (2) The noun phrase: "the letter that Bob sent without reading" is grammatical despite two missing items: the direct object to "sent" and the direct object to "reading", resp. Hence, the corresponding "type" specification (7) should be provable in Lambek calculus or alike: Here N stands for "the letter", and ((N \ N ) / S ) for "that", and some Δ 1 for "Bob sent", and Δ 2 for "without reading". As a type for the whole dependent clause, "Bob sent without reading we have to take some S , not a full S, to respect the fact that this time two items are missing: the direct objects to "sent" and "reading", resp. To justify "the letter that Bob sent without reading " with its (7), in addition to the ∇-rules, we invoke Multiplexing Rule (1) . The correlation between the full S and S with its multiple holes is given by: As compared with the previous case of S representing one missing item ∇N , the S here is dealing with !∇N which provides two copies of ∇N to represent two missing items. Then the proof for (7) is as: This section introduces a sound and complete focused proof system SLLMF for SLLM. Focusing [1] is a discipline on proofs that reduces proof search space. We take an intermediate step, by first introducing the proof system SLLM# that handles the non-determinism caused by the multiplexing rule. For bottom-up proof-search, the multiplexing rule has a great deal of don't know non-determinism as one has to decide how many copies of F appears in its premise. This decision affects provability as each formula has to be necessarily be used in the proof, i.e., they cannot be weakened. To address this problem, we take a lazy approach by using two new connectives * and + . The formula * F denotes zero or more local copies of F , and + F one of more copies of F . We construct the proof system SLLM# from SLLM as follows. It contains all rules of SLLM, except the rule ! L , which is replaced by the following rules Notice that there is no need for explicit contraction and only * allows for weakening. We accommodate contraction into the introduction rules, namely, by modifying the rules where there is context splitting, such as in the rules \ L . In particular, one should decide in which branch a formula C is necessarily be used. This is accomplished by using adequately + F and * F . For example, some rules for \ L are shown below: In the first rule, the C is necessarily used in the right premise, while in the left premise one can chose to use C or not. SLLM# contains similar symmetric rules where C is necessarily moved to the left premise. Also it contains the corresponding rules for / L . SLLM# also include the following more refined right-introduction rules for ! and ∇. where Γ * 1 , Γ * 2 are lists containing only formulas of the form * H. 1 , ∇F, Γ * 2 → ∇G Notice how the decision that all formulas in Γ 1 , Γ 2 represent zero copies is made in the rules above. Completeness follows from straightforward proof by induction on the size of proofs. One needs to slightly generalize the inductive hypothesis. Soundness follows from the fact that contractions are local and can be permuted below every other rule. First proposed by Andreoli [1] for Linear Logic, focused proof systems reduce proof search space by distinguishing rules which have don't know nondeterminism, classified as positive, from rules which have don't care nondeterminism, classified as negative. We classify the rules · R , \ L , / L as positive and the rules · L , \ R , / R as negative. Non-atomic formulas of the form F · G are classified as positive, ∇F, * F, + F and !F are classified as modal formulas, and formulas of the form F \ G and F / G as negative. The focused proof system manipulates the following types of sequents, where Γ 1 and Γ 2 are possibly empty lists of non-positive formulas, Θ is multiset of formulas, and N N is a non-negative formula. Intitively, Θ will contain all formulas of the form ∇F . As they allow exchange rule, their collection can be treated as a multiset. Γ 1 , Γ 2 contain formulas that cannot be introduced by negative rules. Intuitively, the formulas in Δ and F are eagerly introduced whenever they negative rules are applicable, as one does not lose completeness in doing so. The focused proof system SLLMF is composed by the rules in Figs. 1 and 2. Intuitively, reaction rules R L1 , R L2 , R R and negative phase rules are applied until no more rules are applicable. Then a decision rule is applied which focuses on one formula. One needs, however, to be careful on whether the focused formula's main connective is + or * . If it is the former, then we have committed to one copy of the formula and therefore, it can be modified to be * , while the latter does not change. The number of rules in Fig. 2 simply reflects the different cases emerging due to the presence or not of formulas whose main connective is + or * . For example, \ L2 considers the case when the splitting of the context occurs exactly on a formula + C. In this case, the decision is to commit to use a copy of C in the right-premise, thus containing + C, while * C on the left-premise. The other rules follow the same reasoning. Finally, notice that in the rules I, ! R and ∇ R the context may contain formulas with main connective * in their conclusion, but not in their premise. This illustrates the lazy decision of how many copies of a formula are needed. The proof of this theorem follows the same ideas as detailed in [26] and [12] . Remark 4. The focused proof system introduced above enables the use of more sophisticated search mechanisms. For example, lazy methods can reduce the non-determinism caused by the great number of introduction rules caused by managing * , + , e.g., Fig. 2 NNA represent a non-atomic, non-negative formula. NP represents a non-positive formula whose main connective is not ∇. N ∇ P represents a non-positive formula. We use R for both ⇑ G or [NN ] . We use +/ * F for both + F and * F . We use Γ * for a possibly empty list of formulas of the form * F . In this section, we investigate the complexity of SLLM. In particular, we show that it is undecidable in general, by encoding Turing computations. This encoding also illustrate how the focused proof system SLLMF reduces non-determinism. We then identify decidable fragments for SLLM. Any Turing instruction I is encoded by !∇A I with an appropriate A I . E.g., an instruction I : qξ → q ηR if in state q looking at symbol ξ, replace it by η, move the tape head one cell to the right, and go into state q , is encoded by !∇A i where Let M lead from an initial configuration, represented as B 1 · q 1 · ξ · B 2 , to the final configuration q 0 (the tape is empty). We demonstrate how focusing improves search with the encoding of Turing computations. For example, an instruction that write to the tape and moves to the right has the form: while the Turing Machine (TM) configuration is encoded as in the sequent context: [B 1 , q 1 , ξ, B 2 ] specifies A TM at state q 1 looking at the symbol ξ in the tape B 1 , ξ, B 2 . Assuming that A 1 , . . . , A n is used at least once, !∇A 1 , . . . , !∇A n specifies the behavior of the TM. This becomes transparent with focusing. The following focused derivation illustrate how a copy of an instruction encoding, below A 1 , can be made available to be used. Recall that the one has to look at the derivation from bottom-up. Notice that A 1 is placed in the Θ context. This means that it can be moved at any place. Also notice that since one copy of A 1 is used, + ∇A 1 is replaced by * ∇A 1 . The following derivation continues from the premise of the derivation above by focusing on A 1 , A = * ∇A 1 , . . . , !∇A n : Notice that the resulting premise (at the right of the tree) specifies exactly the TM tape resulting from executing the instruction specified by A 1 . Moreover, notice that for the rule D 4 , there are many options on where exactly to use A 1 . However, it will only work if done as above. This is because otherwise it would not be possible to apply the initial rules as to the left of the derivation above. This reduces considerably the non-determinism involved for proof search. Finally, once the final configuration q 0 (our Turing machine is responsible for garbage collection, so the configuration is just q 0 , with no symbols on the tape) is reached, one finishes the proof: The focusing discipline guarantees that the structure of the proof described above is the only one available. Therefore our encoding soundly and faithfully encodes Turing computations, resulting in the following theorem. However, notice additionally, that due to the non-determinism due to the ! left introduction, the encoding of Turing computations is not on the level of derivations, but on the level of proofs, following the terminology in [24] . The absence of Weakening seems to reduce the expressive power of our system SLLM in the case where not all instructions might have been applied within a particular computation, see Remark 5. However, we are still able to get a strong positive statement. Namely, given a subset {I 1 , I 2 , . . . , I m } of Turing instructions, the following two statements are equivalent: (a) The deterministic Turing machine M leads from an initial configuration, represented as B 1 · q 1 · ξ · B 2 , to the final configuration q 0 so that I 1 , I 2 , . . . , I m are only those instructions that have been actually applied in the given Turing computation. !∇A I1 , !∇A I2 , . . . , !∇A Im , B 1 · q 1 · ξ · B 2 q 0 (9) Corollary 2. The derivability problem for SLLM is undecidable. Proof. Assume the contrary: a decision algorithm α decides whether any sequent in SLLM is derivable or not. In particular, for any Turing machine M and any initial configuration of M , α decides whether any sequent of the form (9) is derivable or not, where B 1 · q 1 · ξ · B 2 represents the initial configuration. Then for each of the subsets {I 1 , I 2 , . . . , I m } of the instructions of M , we apply α to the corresponding sequent of the form (9) . If all results are negative then we can conclude that M does not terminate on the initial configuration, represented as Otherwise, M does terminate. Since the halting problem for Turing machines is undecidable, we conclude that α is impossible. The traditional approach to machine-based undecidability is to establish a one-to-one correspondence between machine computations and derivations in the system under consideration. Namely, given a Turing/Minsky machine M , we encode M as a formula code M , the 'product' of all C I representing instructions I. The 'product' ranges over all M 's instructions. Then we have to establish that, whatever initial configuration W we take, a sequent of the form code M , W q 0 is decidable in the logical system at hand iff M terminates on the initial configuration represented as W . Here one and the same code M is used for each of the initials W . Now, suppose that M terminates on each of the initial configurations W 1 and W 2 so that some instruction represented by C is used within the computation starting with W 1 , but it is not used within the computation starting with W 2 . Then, because of W 1 , C takes an active part within code M . On the other hand, C becomes redundant and must be 'ignored' within the derivation for the sequent code M , W 2 q 0 . To cope with the problem, it would be enough, e.g., to assume Weakening in the system under consideration, which is not a case here. The novelty of our approach to the machine-based undecidability is to circumvent the problem caused by the absence of Weakening, by changing the order of quantifiers. Instead of code M , one and the same for all W , we introduce a finite number of candidates of the form (9) with ranging over subsets {I 1 , I 2 , . . . , I m } of the instructions of M . According to Theorem 5, for any initial configuration W , there exists a sequent, say code M,W , W q 0 , chosen from the finite set of candidates of the form (9) such that the terminated computation starting from W corresponds to an SLLM derivation for the chosen code M,W , W q 0 . See also Corollary 2. An advantage of our approach is that, unlike the contraction rule, we can syntactically control the multiplexing to provide decidable fragments still sufficient for applications. Theorem 6. If we bound k in the multiplexing rule in the calculus SLLM with a fixed constant k 0 , such a fragment becomes decidable. Proof Sketch. Each application of Multiplexing of the form: multiplies the number of formulas with the factor k 0 , which provides an upper bound on the size S of the sequents involved: here S 0 is the size of the input, and n is a bound on the nesting depth of the !-formulas. It suffices to apply a non-deterministic decision procedure but generally on the sequents of exponential size. In the case where we bound k in the multiplexing rule in the calculus SLLM with a fixed constant k 0 , and, in addition, we bound the depth of nesting of !A, we get NP-completeness. Remark 6. In fact Theorem 7 gives NP-procedures for parsing complex and compound sentences in many practically important cases. Remark 7. The strong lower bound is given by the following. The !-free fragment that invokes only one implication, (A\B), and ∇A is still NP-complete. In this paper we have introduced SLLM, a non-commutative intuitionistic linear logic system with two subexponentials. One subexponential implements permutation and the other one obeys the multiplexing rule, which is a weaker, miniature version of contraction. Our system was inspired by subexponentials [23] , linear logic [6] , light linear logic [7] , soft linear logic [16] , and easy linear logic [10] . We have also provided a complete focused proof system for our calculus SLLM. We have illustrated the expressive power of the focused system by modelling computational processes. The general aim is to develop more refined and efficient procedures for the miniature versions of non-commutative systems, e.g., Lambek calculus and its extensions, based on the multiplexing rule. We aim to ensure a reasonable balance between the expressive power of the formal systems in question and the complexity of their algorithmic implementation. The calculus SLLM, with multiplexing instead of contraction, provides simultaneously three properties: cut elimination, substitution, and Lambek's restriction. One particular advantage of our system SLLM to systems in our previous work [12, 15] is the fact that it naturally incorporates Lambek's non-emptiness restriction, which is incompatible with stronger systems involving contraction [15] . Lambek's non-emptiness restriction plays a crucial role in applications of substructural (Lambek-style) calculi in formal linguistics (type-logical grammars). Indeed, overcoming this impossibility result is one of our main motivations in looking for a system that would satisfy cut-elimination, substitution, and the Lambek's restriction. The new system proposed in this paper is our proposed solution to this subtle and challenging problem. Moreover, there is no direct way of reducing the undecidability result in this paper, say, to the undecidability results from our previous papers [11, 14, 15 ] by a logical translation or representation of the logical systems. Since a number of those systems are also undecidable, there are of course Turing reductions both ways to the system in this paper. However, the Turing reductions factor through the new representation of Turing machines introduced in this paper. That is, the undecidability result in this paper is a new result. Also the focused proof system proposed here has innovations to the paper [12] . For example, our proof system contains relevant subexponentials that do not allow contraction, something that was not addressed in [12] . Indeed such subexponentials have also been left out of other focused proof systems, e.g., in the papers [23, 25] . Another advantage of this approach is that, unlike the contraction rule, we can syntactically control the multiplexing to provide feasible fragments still sufficient for linguistic applications. As future work, we plan to investigate how to extend the systems proposed in this paper with additives. In particular, the proposed focused proof system using the introduced connectives * , + may have to be extended in order to support additives. This is because it seems problematic, with these connectives, to provide that the same number of copies of a contractable formula are used in both premises when introducing an additive connective. Logic programming with focusing proofs in linear logic Proof figures and structural operators for categorial grammar Type-Logical Semantics A linear logic framework A linear logical framework Light linear logic Horn programming in linear logic is NP-complete Phase semantics for light linear logic Light linear logics with controlled weakening: expressibility, confluent strong normalization Subexponentials in noncommutative linear logic A logical framework with commutative and non-commutative subexponentials L-models and R-models for Lambek calculus enriched with additives and the multiplicative unit Undecidability of the Lambek calculus with a relevant modality Reconciling Lambek's restriction, cutelimination, and substitution in the presence of exponential modalities Soft linear logic and polynomial time The mathematics of sentence structure Decision problems for propositional linear logic The Logic of Categorial Grammars. A Deductive Account of Natural Language Syntax and Semantics Constants of grammatical reasoning Categorial Grammar: Logical Syntax, Semantics, and Processing Computational coverage of TLG: nonlinearity Algorithmic specifications in linear logic with subexponentials A framework for proof systems An extended framework for specifying and reasoning about proof systems Uneétude logique du contrôle Quantales and (noncommutative) linear logic