Strong and Weak Quantifiers in Focused NL$_{\text {CL}}$

Abstract

We propose an improvement of Barker and Shan’s [4] NL$_{\text {CL}}$ for which derivability is decidable, which has a normal-form for proof search, can analyse scope islands, and distinguish between strong and weak quantifiers.

1 Introduction

In 2014, Kiselyov and Shan [11] published a paper in which they presented an elegant approach to the anaysis of various scope-related phenomena using, what they call, the continuation hierarchy. The phenomena they cover are scope ambiguity, scope islands and strong and weak quantifiers. They cover these phenomena using a mechanism which works on the sentence’s semantics, independent of whatever form of grammar is used.

At around the same time, Barker and Shan [4] published a book containing their findings on NL$_{\lambda }$ and NL$_{\text {CL}}$, a pair of grammar logics, both with the ability to analyse scope ambiguity using a strictly syntactic mechanism. In addition, these logics can analyse “parastic scope” [3, 4] and a quantifier which change the result type of the expressions they take scope over. However, neither of these logics is capable of analysing scope islands or strong and weak quantifiers.

In this paper, we rework NL$_{\text {CL}}$ to a calculus which can analyse both scope islands and strong and weak quantifiers, without losing the ability to analyse parasitic scope or changing result types. For this, we base ourselves on work by Moortgat [13] and Moortgat and Moot [14]. This approach requires a strict focusing regime. Therefore, as an added bonus, adopting it results in the elimination of spurious ambiguity, and greatly enhances the efficiency of proof search when compared to Barker and Shan’s [4] NL$_{\text {CL}}$.

We will start our discussion by giving several examples of each of the aforementioned phenomena. The following sentences are examples of scope ambiguity, scope islands and weak quantifiers, respectively. They are given together with their expected semantics, and are based on examples by Szabolcsi [16, p. 608,622].

The first of these examples is a canonical example of scope ambiguity. Example (2) demonstrates a scope island: there is no reading in which “every book” scopes out of the embedded clause, as this reading would imply that there was potentially a different speaker for each book—“Alex said Kurt wrote Slaughterhouse-Five”, “Jules said Kurt wrote Cat’s Cradle”, “Sam said Kurt wrote...” Example (3) shows that indefinites can scope out of scope islands.

We add two more sentences, which are examples of a quantifier which changes the result type, and of parasitic scope, respectively. These examples based on those given by Barker and Shan’s [4, p. 208] and Kiselyov [10].

These last two examples will play a less important role, as NL$_{\text {CL}}$ is already capable of analysing both. However, in order to demonstrate that we have not lost that capability, we will provide analyses of both near the end of this paper.

2 Background

In this section, we will briefly discuss NL$_{\text {CL}}$ and its sibling, NL$_{\lambda }$. NL$_{\text {CL}}$ is an extension to the non-associative Lambek calculus [12, NL;]. The history behind NL$_{\text {CL}}$ is somewhat intricate, but helpful to understanding, so we will briefly go over it. The initial idea comes from the practice of encoding quantifier movement as a tree transformation which introduces a binder [9]:

To implement this idea in type-logical grammar, Barker and Shan add a structural $\lambda$-construct to NL, and added the following structural postulate:¹

As can be seen, the ($\lambda$) postulate uses a new connective: the $\mathbin {\circ }$ (hollow product). This connective is part of a new residuated family , which starts out as a copy of $\{\mathbin {\backslash }, \bullet , \mathbin {\slash }\}$. However, the addition of the ($\lambda$) postulate allows you to raise any constituent to the top-left² position in the structure, where—if it has the right type—it can be “resolved” against the top-level type as follows:

Barker and Shan call resulting system NL$_{\lambda }$. While NL$_{\lambda }$ fulfils the promise of allowing a syntactic analysis of quantifier raising, scope ambiguity and parasitic scope, it has some problems. Most notably, the system is hard to formalise and to reason about, largely due to the presence of a binding construct in the syntax of structures. While it is not impossible to formalise, the ($\lambda$) postulate greatly complicates meta-logical proofs.

To address this issue, and to ease their own investigation of the formal properties of NL$_{\lambda }$, Barker and Shan [4, ch. 17] introduce NL$_{\text {CL}}$. This system uses the fact that $\lambda$-terms can be represented as combinators in combinatory logic, which removes the need for a binding construct. Barker and Shan use a variant of Schönfinkel’s mapping to encode the linear $\lambda$-construct as applications of the combinators $\mathbf {I}$, $\mathbf {B}$ and $\mathbf {C}$:³$^{,}$⁴

$$ \mathbf {I}x = x, \qquad \mathbf {B}x y z = x (y z), \qquad \mathbf {C}x y z = x z y $$

The resulting system is presented in Fig. 1.⁵

Fig. 1.

NL$_{\text {CL}}$ as presented by Barker and Shan [4]. (When reading this figure, be wary of the difference between the combinators $\mathbf {B},\mathbf {C}$ and the formulas B, C.)

Using the system in Fig. 1, we can do quantifier raising in much the same way as we did with the ($\lambda$) postulate—although, as we now have to raise the quantifier one step at a time, the proofs are much longer:

The labels john, likes and everyone abbreviate the types np, $({np}\mathbin {\backslash }{s})\mathbin {\slash }{np}$ and , respectively. For a more detailed account of the relation between NL$_{\lambda }$ and NL$_{\text {CL}}$, see Barker and Shan [4]. For a more detailed account of various encodings of combinatorial logic in structural rules, amongst which the encoding of the linear lambda construct used by Barker and Shan, see Finger [8].

3 Scope Islands for NL$_{\text {CL}}$

Our aim for this section is to present an extension to NL$_{\text {CL}}$ which will allow us to analyse scope islands, and therefore example (2).

To analyse scope islands, we need some way to block quantifier movement. If you look at the $\mathbf {IBC}$-rules in Fig. 1, you will notice that they allow constituents attached to (the left of) a hollow product to move past solid products. This leads us to suggest a fairly simple solution: insert anything that is not solid product. For this, we use a residuated pair of unary connectives, and  [13, 15]. The relevant rules are presented in Fig. 2.

Fig. 2.

Scope Islands for NL$_{\text {CL}}$.

Using these connectives, we can assign ‘said’ the type . Instead of taking a sentence-argument from the right, ‘said’ now takes a closed-off sentence—a scope island. Have a look at the derivation for example (2) given below:

As long as the scope island (written ) is in place, ‘$\textsc {every}\bullet \textsc {book}$’ cannot be raised past it, for there is no rule which allows anything to move past a diamond. But in order to remove the scope island, it has to be eliminated against the argument of ‘said’, and doing so isolates the embedded clause in its own branch of the proof.⁶

4 Strong and Weak Quantifiers

In the previous section, we presented an extension to NL$_{\text {CL}}$ which enabled us to analyse scope islands. This extension blocks all quantifier movement out of scope islands. Example (3) demonstrates that this is too coarse an approach. Specifically, we would like to allow weak quantifiers, such as indefinites, to scope out of scope islands.

We could approach this issue as a syntactic problem, and encode it using structural rules, as we did with quantifier movement and scope islands.⁷ However, Szabolcsi [16] writes that “indefinites acquire their existential scope in a manner that does not involve movement and is essentially syntactically unconstrained.” Therefore, we feel that a syntactic approach would be out of place.

How do we approach the problem of weak quantifiers as a semantic problem? The solution is to use continuation-passing style (CPS). But how? Early attempts, such as the work by [2], often works by applying a CPS translation directly to the semantic terms. Such approaches, however, face a fundamental dilemma. Because the CPS translation is applied to a solitary semantic term, a deterministic translation cannot introduce scope ambiguity—or any ambiguity, for that matter. However, making the CPS translation sufficiently nondeterministic without causing spurious ambiguity is an arduous task. When Barker makes the translation ambiguous, in order to capture scope ambiguity, this leads to the number of introduced ambigous interpretations growing exponentially with the sentence length. More recent approaches, such as the work by Kiselyov and Shan [11], are much more sophisticated. Their approach allows for the creation of quantifiers of different strengths (e.g. $\text {everyone}_1$, $\text {everyone}_2$, ...) essentially reducing scope ambiguity to lexical ambiguity. As a linguistic standpoint, this feels wrong. Furthermore, their framework was engineered to be able to analyse phenomena such as scope islands and weak quantifiers. This makes it too expressive (and intricate) for the task at hand.

Instead, we base our CPS semantics on the approach of Moortgat and Moot [14] and Bastenhof [6], who manage to elegantly integrate CPS semantics into their grammar logic. Moortgat and Moot set up a calculus which enforces one crucial property: every proof in the grammar logic is associated with unique, normal-form semantics. In the context of scope ambiguity, this means that each way to interpret a sentence with ambiguous scope corresponds to exactly one proof in the grammar logic.

Focused NL$_{\mathbf {CL}}$. Moortgat and Moot [14, Sect. 3.1] define a normal-form calculus for the Lambek-Grishin calculus (LG). They refer to this calculus as fLG—for focused LG, after the technique, pioneered by Andreoli [1], which they use in their calculus. Their version of focusing, however, is more general than that of Andreoli, as they allow for the arbitrary assignment of polarities to atoms. Andreoli’s [1] schema can be recovered by assigning all atomic formulas negative polarity.

As NL is a fragment of LG, we can trivially extract a normal-form calculus for NL from their work. We will, in their style, refer to this calculus as fNL.

It is important to note that they develop their calculus within the framework of display calculus [7]. One advantage of this framework is that we can freely add structural rules, without fear that we will lose the cut-elimination property. Barker and Shan’s [4] extension of NL, NL$_{\text {CL}}$, consists solely of a copy of an existing modality () and a number of structural rules. Therefore, by applying these same changes, we can extend fNL to focsed NL$_{\text {CL}}$—or fNL$_{\text {CL}}$. The result is presented in Fig. 3, together with the focused version of the extension for scope islands from Sect. 3.

Fig. 3.

NL$_{\text {CL}}$ reworked as a focused display calculus.

Equivalence between fNL$_{\text {CL}}$ and NL$_{\text {CL}}$ can likely be proven using an intermediate system: display NL$_{\text {CL}}$. One can trivially obtain this system from the focused system in Fig. 3 by dropping the focus marker “” and the focusing and unfocusing rules. Equivalence between the display and focused variants of a system was proven for classical NL by Bastenhof [5]. This proof can likely be adapted for NL$_{\text {CL}}$.

However, it is important to realise that, even in the absence of a formal proof of equivalence between NL$_{\text {CL}}$ and fNL$_{\text {CL}}$, the second remains a logical system which can analyse all phenomena which Barker and Shan [4] show NL$_{\text {CL}}$ can analyse.⁸

Decidable Proof Search. At this point, fNL$_{\text {CL}}$ still has a problem, which it shares with NL$_{\text {CL}}$: we do not have a decidable procedure for proof search. Since it is a grammar logic, this means that we do not have a procedure for parsing. An easy way to obtain such a procedure is to change the system in such a way that backward-chaining search becomes decidable. The reason this is not decidable in NL$_{\text {CL}}$ is because of the $\mathbf {I}$-rule, which does not obey the substructure property.⁹

Admittedly, there are other rules which do not obey the substructure property: the residuation rules and the $\mathbf {B}$ and $\mathbf {C}$ rules do not enjoy it. However, the residuation rules still enjoy a weak form this property: they do not increase the size of the structure. This means that we can use loop checking to filter out problematic branches of the search. More interestingly, the $\mathbf {B}$ and $\mathbf {C}$ rules have the property that “whatever goes up, must come down.” At some point, the quantifier will reach the top of the expression, and at that point, there are only two things to do: (1) resolve the quantifier against the top-level type, thereby eliminating a connective and breaking out of any loop; or (2) go back down along the same path. Yet when searching for a proof with the $\mathbf {I}$-rule, we can always introduce another $\mathbf {I}$.

We will address this issue by restricting access to the $\mathbf {I}$-rule using a license. This license will be a new unary connective, written $\mathbf {Q}{A}$. Semantically, this logical connective corresponds to a hollow product with a right-hand $\mathbf {I}$ (i.e. ${A}\mathbin {\circ }\mathbf {I}$). However, as we want neither hollow products, nor the unit $\mathbf {I}$, on the logical level, we capture these in a single connective. We remove the $\mathbf {I}$-rule, and add the following three rules to the calculus in Fig. 3:

The first two of these rules are the display calculus rules for right-hand products. The third is the remaining direction of the original $\mathbf {I}$-rule. With this change, quantifier raising is restricted to expressions of the form , and proof search becomes decidable.

One problem which remains is that the $\mathbf {B}$ and $\mathbf {C}$ rules cause a huge amount of spurious ambiguity. To see why, note that when raising multiple quantifiers, it is possible to intersperse the various applications of the $\mathbf {B}$ and $\mathbf {C}$ rules in many different ways. To solve this, we will take some inspiration from Barker and Shan [4, ch. 17.6], who solve this issue, albeit in a convoluted way. They show that NL$_{\lambda }$ can be embedded in NL$_{\text {CL}}$, using a variant of Schönfinkel’s mapping from $\lambda$-terms to combinatory logic. Later, they show that a pair of derived rules, and , can serve as a normal-form for the structural rules of NL$_{\text {CL}}$. However, these derived rules employ the structural $\lambda$ which, in the context of NL$_{\text {CL}}$, is presumably immediately translated using Schönfinkel’s mapping. Instead of employing this two-step process, we exploit the similarities between single-hole contexts and linear $\lambda$-terms to derive a variant of the $\lambda$-rule which directly uses Schönfinkel’s mapping (written $\overline{\cdot }$) [cf. [4], ch. 17.5]:

We can use this mapping in the definition of a derived rule: the $\uparrow \downarrow$-rule, written as $\uparrow$ or $\downarrow$, depending on the direction in which it is applied.¹⁰ We can derive the this rule using three lemmas:

Using these lemmas, we can derive the two directions of $\uparrow \downarrow$ as follows:

The lemmas themselves can be derived by induction on the structure of the context $\varSigma$. The derivation of $\mathbf {Q}/\mathbf {I}$ and $\mathbf {I}^{-\prime }$ is done as follows:

These rules simply introduce or eliminate the unit $\mathbf {I}$ under some context $\varSigma$. The actual movement takes place in the definition of $\uparrow \downarrow '$. In this proof, the base case is simply the identity, as no movement is required to move out of the empty context:

Note that the $\uparrow$-rule eliminates a logical connective—the $\mathbf {Q}$—and therefore has the subformula property. In addition, the $\downarrow$-rule, on the other hand, eliminates the trail of $\mathbf {B}$s and $\mathbf {C}$s, and thus has the substructure property. Because of this, proof search with these rules is decidable.

Furthermore, proof search with the $\uparrow \downarrow$-rule is complete. Briefly, this is true because the $\mathbf {I}$ $\mathbf {B}$ $\mathbf {C}$-rules can do nothing but move a constituent up, or down along an existing path—the $\uparrow \downarrow$-rule mere captures this more succintly. A formal proof of this can be given by implementing a normalisation function using the commutative conversions for the $\mathbf {B}$ and $\mathbf {C}$ rules: one can move the applications of the $\mathbf {B}$ and $\mathbf {C}$ rules around until they form a continuous sequence (interspersed with residuation rules) starting (or ending) with an application of the $\mathbf {I}$-rule. This sequence of applications can then be replaced by a single application of the $\uparrow \downarrow$-rule. Therefore, proof search using the $\uparrow \downarrow$-rule is complete with repsect to the $\mathbf {I}$ $\mathbf {B}$ $\mathbf {C}$-rules.

We follow Barker and Shan [4], and derive rules corresponding to the - and -rules. These rules combine an application of $\uparrow \downarrow$-rule with an application of or . We name them qL and qR, to signify that they no longer employ a structural $\lambda$, and because they can be composed to implement Moortgat’s [13] q-connective:

As these rules eliminate at least one logical connective each, they still enjoy the subformula property, so proof search with these rules is decidable. In fact, it is slightly more efficient than with the $\uparrow \downarrow$-rule. The reason for this is that after raising a quantifier, the only course of action is applying the -rule anyway—and likewise for qR.¹¹

Henceforth, if we refer to proof search for fNL$_{\text {CL}}$, we are referring to search using the logical and residuation rules for $\mathbin {\backslash }, \bullet , \mathbin {\slash }$, and , and the qL and qR rules.¹²

Continuation Semantics for NL$_{\mathbf {CL}}$. A normal-form calculus for proof search is a great improvement, but we were really after Moortgat and Moot’s [14, Sect. 3.1] CPS semantics. As with the calculus itself, we can trivially restrict their translation function to fNL, and then extend it to cover fNL$_{\text {CL}}$. In Fig. 4, we present the translation on types and sequents.

Fig. 4.

CPS semantics for focused NL$_{\text {CL}}$.

We extend the translation on types to a translation on structures as follows: we translate all structural constants ($\mathbf {I}$,$\mathbf {B}$,$\mathbf {C}$) as units, forget all unary structural connectives (), and translate all binary structural connectives as products. Atomic structures $\cdot A \cdot$ are translated as $\llbracket {A}\rrbracket ^-$ or $\llbracket {A}\rrbracket ^+$, depending on the polarity of the structure $\cdot A \cdot$.

In this particular CPS translation, all function applications and abstractions are contained within the focusing and unfocusing rules, which are translated as follows:

The other rules are translated either as axioms ($Ax^L$, $Ax^R$), identities ($\mathbin {\backslash }R$, $\mathbin {\slash }R$, , and all rules for , ) or permutations (the rest). For instance,

An exception to this are the $\mathbf {I}$-rules. Because we would like to be able to simply forget the $\mathbf {Q}$-connective upon translation, so that we do not have to store unnecessary units in our lexicon, we have to insert or remove the units upon using these rules.

Using these semantics, we can assign the indefinite article the type $np \mathbin {\slash }n$.¹³ This will result in two interpretations for (2), and three interpretations for (3), as required. Let us consider the important steps in the derivation of (3):

• 1. the quantifier movement and scope taking of “everyone”;

• 2. the collapsing of the scope island, isolating the clause “[$_S$ Kurt .. Mary]” in its own branch of the derivation;

• 3. the collapsing of “a book”, with the indefinite taking scope at the top-level.

If these steps are taken [1,2,3], we obtain interpretation (3a); if they are taken [1,3,2], we obtain (3b); and if they are taken [3,1,2], we obtain (3c).¹⁴

5 Examples

In this section, we will present a number of analyses of the examples presented in Sect. 1. In the interest of brevity, we will summarise numerous applications of the residuation rules, beginning or ending with focusing or unfocusing rules with ‘dp’, for display postulate. In addition, we will leave out uninteresting subproofs.

First off, we present an analysis of (1), resulting in interpretation (1b). The quantifier every is assigned the type , and someone is assigned the type of a “strong” quantifier—that is to say, .

Secondly, we present an analysis of (2), resulting in interpretation (2a)—the only interpretation.

As a third example, we show that we can analyse ‘a’ as a weak quantifier, using the type ${np}\mathbin {\slash }{n}$. We give an analysis of (3), resulting in the interpretation where the indefinite takes wide scope—(3b). The quantifier ‘a’ takes scope when it is combined with book.

Fig. 5.

Analysis of examples (4) and (5).

Lastly, we present analyses of examples (4) and (5). We demonstrate changing result types using the word ‘which’, which we assign the type

In the second, for parasitic scope, we deviate slightly from Barker’s [3] treatment of parasitic scope. We assign ‘same’ (and ‘different’) the type

What this type does is quantify over an expression twice—once normally, to plant its top-level quantifier, and once parasitically. Using this type, we can obtain the semantics advocated by Kiselyov [10]. The proofs for these two examples can be found in Fig. 5.

6 Conclusion

We presented an improvement over Barker and Shan’s [4] NL$_{\text {CL}}$ for which derivability is decidable, and which has a normal-form for proof search. In addition, it can analyse scope islands, and distinguish between strong and weak quantifiers, shown by the ability to analyse examples (1–5). Of these examples, (1–3) are representative examples of scope islands and strong and weak quantifiers, for which Kiselyov and Shan [11] provides a purely semantic analysis. The remaining examples, (4) and (5), are examples from the work by Barker and Shan [4] which motivated us to start from their syntactic approach.