Discontinuity and Pied-Piping in Categorial Grammar

Glyn Morrill^{∗}

Secció d’Intel·ligència Artificial

Departament de Llenguatges i Sistemes Informàtics Universitat Politècnica de Catalunya Pau Gargallo, 5 08028 Barcelona

              morrill@lsi.upc.es

Abstract

Discontinuity refers to the phenomena in many natural language constructions whereby signs differ markedly in their prosodic and semantic forms. As such it presents interesting demands on monostratal computational formalisms which aspire to descriptive adequacy. Pied-piping, in particular, is argued by Pollard (1988) to motivate phrase structure-style feature percolation. In the context of categorial grammar, Bach (1984), Moortgat (1988, 1990, 1991a) and others have sought to provide categorial operators suited to discontinuity. These attempts encounter certain difficulties with respect to model theory and/or proof theory, difficulties which the current proposals are intended to resolve. These proposals are accompanied by introduction of a new categorial proof format: labelled Fitch-style natural deduction.

The associative Lambek calculus is complete with respect to interpretation by residuation with respect to the adjunction operation of semigroup algebras (Buszkowski 1986). In Moortgat and Morrill (1991) is is shown how to give calculi for families of categorial operators, each defined by residuation with respect to an operation of prosodic adjunction (associative, non-associative, or with interactive axioms). The present paper treats discontinuity in this way, by residuation with respect to three adjunctions: + (associative), (., .) (split-point marking), and W (wrapping) related by the equation (s_{1}, s_{2})W s_{3} = s_{1} + s_{3} + s_{2}. The system is illustrated by reference to particle verbs, discontinuous idioms, quantifier scope and quantifier scope ambiguity, pied-piping, gapping, and object-antecedent reflexivisation.

∗This paper in its current form has benefited by the review of an earlier paper for Linguistics and Philosophy; I thank an anonomous reviewer for a commentary half the length of the submission itself.

1 Introduction

In order to specify a model of the relation between forms and meanings in natural language, it is necessary to list those associations in which a meaning is not attributable to meanings of parts. In general we expect a lexical enumeration of properties of “words”, but insofar as morphological semantics may be systematic, and phrasal idioms may be truly idiomatic, lexical items may be smaller or larger than an intuitive or lexicographic construal of “word”. When an element with such an unanalysable meaning is not continuous in surface form the phenomenon of discontinuity is exhibited. Examples are provided by phrasal verbs such as those in (1) and discontinuous idioms such as those in (2).

a. Mary rang John/the man up. b. Mary put John/the man down.

(1)

a. Mary gave John/the man the cold shoulder.

b. Mary gets John’s/the man’s goat. c. Mary put John/the man down.

(2)

Such constructions present difficulties for any approach to grammar in which expressions are to be generated just by concatenation in an algbra of strings (but see e.g. Wasow, Sag and Nunberg 1983). Such phenomena are in fact just the simplest examples of discontinuity that arise in a monostratal setting. Thus, if by discontinuity we understand mismatch between surface form and logical form,^{1} the question arises as to how a quantifier is to obtain sentential semantic scope in logical form, while the corresponding quantifier phrase is embedded:

a. John likes everything.
b. ∀x((like x) j)

(3)

Furthermore, at least on the standard view, there must be admitted the quantifier scope ambiguity of (4a), and also that of (4b).

a. Everyone loves something.
b. John believes someone walks.

(4)

1Such terms are used initially in view of their familiarity. We shortly refer systematically to prosodic form and semantic form. Other terms for the former might be phonetic form, phonological form, or syntax; the understanding is that it pertains to such properties as to rhyme, rhythm, syllabification and word order that are under study. Likwise, semantics refers to such properties as to presupposition, truth conditions, implicature and so on that are relevant.

For the current purposes prosodics is just word order, and semantics, truth conditions.

For (4b) there is a de dicto or non-specific reading with “someone” within the scope of “believes”, and a de re or specific reading with “someone” outside the scope of “believes”; the latter necessitates quantifier “raising” to the level of a superordinate sentence.

The particular difficulty that quantifier-raising represents is to some extent evaded by appeal to non-monostratal architecture and/or relaxations of compositionality. But what is essentially the same puzzle is presented with an inescapable surface form realisation in pied-piping, that is relativisation in which additional material accompanies the “fronted” relative pronoun:

a. (the man) for whom John works

b. (the contract) the loss of which after so much wrangling John

would finally have to pay for (with his job) c. (the thesis) the height of the lettering on the cover of which

is prescribed by university regulations (5)

In such a construction the relative pronoun needs to take semantic scope at the level of the entire fronted constituent in order to bind the gap in the body of the relative clause, i.e. some kind of raising is required, as for quantifiers. In addition, the category of the gap (e.g. prepositional phrase or noun phrase) needs to match that of the fronted constituent, creating, aside from semantics, a complex surface form discontinuous dependency.

We consider two more kinds of discontinuity in the present paper. Firstly, there is gapping, in which medial (as opposed to peripheral) material from a first conjunt is understood in a second:

(6) John studies logic and Charles, phonetics.

Again, the semantic dependency is accompanied by a need to correlate the category of the “deleted” material on the right with the category of material appearing on the left.

The final case we consider is object-antecedent reflexivisation:

a. John showed Mary the book.
b. John showed Mary herself.
c. *John showed herself Mary.

(7)

Although perhaps a little strange (we could think of John showing Mary pictures or photos of various people including herself) (7b) is acceptable, whereas (7c) is not. In order for reflexivisation to occur in the semantics, it is necessary for a reflexive to combine with, and reflexivise, a predicate, before the predicate applies to the antecedent: the other way round, the antecedent semantics is not accessible for duplication. The facts in (7) are thus precisely the opposite of those expected if surface form is generated by concatenation of the verb first with the adjacent complement, and then with the remote one. This motivates a “head-wrapping” analysis of such verbs (see e.g. Dowty 1979) in which they combine with the surface-form remote complement first, and then “head-wrap” around the other complement.

Discontinuity represents much that is problematic in natural language syntax, and it is not the pretence of the present paper to provide a comprehensive account of the instances cited above. However, it does aim to show how each is rendered ammenable in its basic form in the context of categorial grammar in the logical tradition, that is the tradition of Lambek calculus and extended Lambek calculus (see e.g. Moortgat 1988, van Benthem 1991, Morrill 1992a). Moortgat (1988) attempted to place on a more logical footing the earlier proposals for discontinuous categorial operators of e.g. Bach (1981, 1984). But the logic was incomplete; indeed the sequent proof format used seemed in principle incapable of supporting a full logic for discontinuity. We shall see ultimately that for the proposals made here this turns out not to be the case after all. We shall present an alternative algebraic interpretation, together with a labelled Gentzen-style sequent proof theory, and a “user-friendly” labelled Fitch-style natural deduction proof theory. Before turning to the content of these proposals, we shall review relevant features of Montague’s semiotic programme, within which they are construed.

2 Methodology

Linguistic objectives, and hence methodologies, tend to differ depending upon which of two conceptions of language are taken as central: what we may call language-in-intension, and language-in-extension. Language-in-intension, the Chomskyan view, takes language to be a psychological state; roughly speaking, universal grammar is the initial, genetically determined, state of the psychological language faculty which develops, under linguistic experience, to a stable or mature state of parochial knowledge. Language-in-extension, the semiotic or Montagovian view, takes language to be a set (or family of sets, for varying parts of speech) of signs, where a sign is an association of prosodic and semantic properties. In this case universal grammar is the architecture or formalism within which fragments are developed.

We will assume that the two conceptions may coexist comfortably under the construal of language-in-intension as knowledge of language-in-extension. Our concern is with language-in-extension, a concern ultimately motivated by interest in language processing, in which a model of language-in-extension represents a specification for computation. The study of language-in-intension, as practiced within the Chomskyan tradition, has been attacked for lack of formalisation (e.g. Pullum 1989), and defended (e.g. Ludlow 1992). In this case formalisation does indeed seem largely irrelevant in that hypotheses can be formulated, falsified, and refined in a manner to which increased “rigour” would be only a diversion. In looking for properties of language-in-intension, it is possible that deep insights should be found without these constituting models of fragments; that is, such characterisations may be partial with respect to computational concerns. In relation to language-in-extension on the other hand, and its computational motivation, it is in the nature of the objectives that models of fragments must be developed which are formal and complete, in the sense that a relation between prosodic and semantic properties is specified which is mechanically interpretable.

2.1 Architecture

Montague’s Universal Grammar (UG; Montague 1974) requires surface forms to be freely generated in order that semantic denotation can be defined by recursion on their structure, in the same way as for formal languages of logic. Of its nature, such an approach cannot characterise ambiguity, so that a disambiguating relation is needed to associate surface forms with actual expressions. In The Proper Treatment of Quantification (PTQ; Montague 1973) ambiguity is accommoded another way, though in a manner permitting systematic conversion to the “official UG” format, defining by mutual recursion on syntactic types (or: categories) a relation between expressions and terms of intensional logic.

We can orient ourselves for the present proposals by reference to a fragment (which is only extensional) in the PTQ style, which we shall now present.

Prosodic terms P (α, β, γ, …) are generated from prosodic constants K (written in italics) and prosodic variables U (a, b, c, …) thus:

{P ::= ϵ | U | K | P + P | (P, P) | (PW P). \atop (8)}

Intuitively + represents concatenation and ϵ the empty string, (., .) represents split string formation, and (.W.) represents wrapping, so that there are the following equations for prosodic terms:

{α + ϵ = ϵ + α = α \atop ((α, β)W γ) = α + γ + β} ; (9)

Prosodic terms without variables are called prosodic forms.

Semantic terms are interpreted in type theory. A set T of semantic types is freely generated from a set D of basic semantic types thus:

{T ::= D | T → T \atop (10)}

A semantic function hierarchy consists of a family {D_{τ}}_{τ∈T} of sets (semantic domains) such that D_{τ_{1}→τ_{2}} is the set of all functions from D_{τ_{1}} to D_{τ_{2}}. Typed semantic terms are defined and interpreted as usual. Starting from a set C_{τ} of constants (written in boldface) and a denumerably infinite set V_{τ} of variables for each type τ, the set S_{τ} of typed semantic terms for each type τ is freely generated thus:

\begin{matrix}S_{τ} ::= C_{τ} | V_{τ} | (S_{τ′→τ} S_{τ′}) \\ S_{τ′→τ} ::= λV_{τ′}S_{τ} \end{matrix} ; (11)

There are the standard equations of e.g. β- and η- conversion:

(λxϕ ψ) = ϕ[ψ/x] λx(ϕ x) = ϕ if x is not free in ϕ

(12) Semantic terms which are closed, i.e. which have no free variables, are called semantic forms.

Given a set of syntactic types, for parts of speech, a type map T is a function from syntactic types to semantic types. We consider the following.

Part of Speech  Syntactic Type Semantic Type
Referring nominal N e
Intransitive verb (phrase) VP  e→t
Sentence S t
Ditransitive verb (phrase) TTV  e→(e→(e→t))
Transitive verb (phrase)  TV  e→(e→t)
Definite article  DEF  (e→t)→e
Common noun (phrase)  CN  e→t
Object antecedent reflexive OBJRFLX  (e→(e→(e→t)))→ (e→(e→t))
Prepositional verb  PV  e→(e→t)
Prepositional phrase  PP  e
Quantifier  Q  (e→t)→((e→t) →t)
Quantifier phrase  QP  (e→t) →t
Preposition  P  e→e

(13)

Note that noun phrases are partioned into quantifier phrases QP (e.g. ‘every man’, ‘a tall cook’) and referring nominals N (e.g. ‘John’, ‘the tall cook’), and that, unlike Montague, we do not raise the semantic type of the latter to share that of the former.

A statement of formation is a statement of the form:

{a_{1} – x_{1}: A_{1}, …, a_{n} – x_{n}: A_{n} ⇒ α – ϕ: A \atop (14)}

Here, A_{1}, …, A_{n}, A are syntactic types, a_{1}, …, a_{n} are prosodic variables, and x_{1}, …, x_{n} are semantic variables of types T (A_{1}), …, T (A_{n}) respectively, such that no variable is associated with two distinct syntactic types; α is a prosodic term the variables of which are contained in {a_{1}, …, a_{n}}, and ϕ is a semantic term of type T (A) the free variables of which are contained in {x_{1}, …, x_{n}}.

We may now give a list of rules of formation which are statements of formation under which a lexicon is to be closed to generate a formal language model:

R1. a − x: N, b − y: VP ⇒ a + b − (y x): S
R2. a − x: TTV, b − y: N ⇒ (a, b) − (x y): TV
R3. a − x: TV, b − y: N ⇒ aW b − (x y): VP
R4. a − x: DEF, b − y: CN ⇒ a + b − (x y): N
R5. a − x: TTV, b − y: OBJRFLX ⇒ (a, b) − (y x): TV
R6. a − x: PV, b − y: PP ⇒ a + b − (x y): VP
R7. a − x: Q, b − y: CN ⇒ a + b − (x y): QP
R8. a − x: P, b − y: N ⇒ a + b − (x y): PP

(15)

A lexicon is a list of assignments α – ϕ: A where A is a syntactic type, α is a prosodic form, and ϕ is a semantic form of type T (A). The formal language model defined is the reflexive and transitive closure of the lexicon under the rules of formation. Recursively supplying the output of one rule as input to another corresponds to Cut:

(16) a. a – x: A ⇒ a – x: A  id
b. Γ ⇒ α – ϕ: A a – x: A, Δ ⇒ β(a) – ψ(x): BCut Γ, Δ ⇒ β(α) – ψ(ϕ): B

The parenthetic notation indicates a distinguished occurrence of a subterm, thus the Cut rule shows that we may substitute the output of one rule for the input of another. The id rule represents reflexivity; it is redundant though harmless at the moment, but in Gentzen sequent presentations later it provides the base case for recursive rules.

Let us illustrate by showing how this fragment deals with the object antecedent reflexive paradigm already mentioned:

a. John showed Mary the book.
b. John showed Mary herself.
c. *John showed herself Mary.

(17)

Derivations will be represented Dowty, Wall and Peters (1979)-style. For (17a) there is the following:

1. John − j: N
2. showed − show: TTV
3. the − λxιy(x y): DEF
4. book − book: CN
5. Mary − m: N
6. the + book − (λxιy(x y) book): N  3, 4 R4
7. the + book − ιy(book y): N  = 6
8. (showed, the + book) − (show ιy(book y)): TV  2, 7 R2
9. ((showed, the + book)W Mary) − ((show ιy(book y)) m): VP 5, 8 R3
10. showed + Mary + the + book − ((show ιy(book y)) m): VP = 9
11. John + showed + Mary + the + book−
(((show ιy(book y)) m) j): S  1, 10 R1

(18)

Lines 1 to 5 are lexical assignments. Lexical semantic forms may be atomic or complex; in that for the determiner at line 3 an iota operator is used to represent definite description. At each subsequent line a derived assignment is given together with an indication of the rule and previous assignments from which it is obtained. Thus line 6 is obtained by applying rule R4 to 3 and 4. When assignments are obtained by means of equations on terms this is indicated by = together with the relevant earlier line number (sometimes such manipulations will be carried out without being represented explicitly). Thus 7 is obtained from 6 by β-conversion. At 8 a split string is formed in the prosodics, and at 9 the prosodic term is constructed by means of wrap.^{2} 10 is obtained from 9 by evaluating the wrap of a split string.

In the generation of (17b) as follows, the reflexive combines at line 5 as semantic functor with the ditransitive, forming a split string prosodically, and reflexivising the non-subject arguments of the predicate semantically. Combination by wrap with the object argument yields the acceptable word order.

1. John − j: N
2. showed − show: TTV
3. herself − λxλy((x y) y): OBJRFLX
4. Mary − m: N
5. (showed, herself ) − (λxλy((x y) y) show): TV  2, 3 R5
6. (showed, herself ) − λy((show y) y): TV  = 5
7. ((showed, herself )W Mary) − (λy((show y) y) m): VP  4, 6 R3
8. showed + Mary + herself − ((show m) m): VP  = 7
9. John + showed + Mary + herself − (((show m) m) j): S 1, 8 R1

(19)

The unacceptable word order (17c) is not obtained because although (showed, Mary) is generated as a TV, the rule R3 combining a TV with its object requires an N, not the object-antecedent reflexive pronoun syntactic type OBJRFLX.

By way of providing a familiarising stepping stone between the grammar presentations and derivations to appear later, and the standard ones seen so far, we now exemplify the use of recursive rules in the PTQ-like fragment.

Montague treats quantification and relativisation by means of syntactic, or what we shall call prosodic, variables and semantic variables. In his treatment of quantification, a sentence built out of a prosodic variable and associated semantic variable may be combined with a quantifier phrase by substituting the latter’s prosodics for the prosodic variable; this step is accompanied by application of the quantifier phrase semantics to the input sentence semantics abstracted over the semantic variable associated with the prosodic variable. Semantically this achieves sentencial scope for the quantifier, while binding the position occupied by the quantifier phrase prosodically. Montague used the case where there is more than one occurrence of the prosodic variable to define binding of pronouns, by substituting for the first prosodic variable, and changing the others to pronouns. If there was no occurrence, we would obtain a non-sensical vacuous quantification. On the other hand, treating assignments to variables like regular lexical declarations leads to the anonomolous generation of sentences containing variables.

2Of course, a regular transitive verb need not combine with its object by wrap, but we are not considering these in the fragment.

We make two observations: first, the analysis has a conditional form: if something formed out of a referring nominal would be a sentence, then that something with a quantifier phrase in place of the referring nominal would be a sentence, with semantics given by applying the quantifier phrase to the sentence abstracted over the referring nominal semantics. Second, the derivational anomolies arise because there is no management of the hypothetical referring nominal engaged.

The situation is similar with respect to relativisation. For Montague a sentence built out of a prosodic variable may be prefixed by the relativiser ‘such that’, and the variable occurrences changed to pronouns. The semantic application of the relativiser to the sentencial abstraction binds an extraction site. In the case that there are multiple occurrences a “parasitic resumptive” construction would be obtained (e.g. ‘the man such that he thinks Mary likes him’), and in the case that there are none, a non-sensical vacuous form (e.g. ‘the man such that Mary walks’).

The same design can be used for relativisers that have gaps rather than pronouns at their extraction sites, by deleting the prosodic variables. Overall the analysis again has a conditional structure: if something formed out of a referring nominal would be a sentence, then that something with a reflexiviser prefixed … (and so on). And again, as things stand the hypothetical is slipped in in a way that does not control anomolies.

The essential content of these analyses is formulable in a robust way by means of recursive rules. By recursive rules, or metarules (cf. Gazdar, Klein, Pullum and Sag 1985), we mean rules generating an output statement of formation schema from one or more input statement of formation schemata. Recursive rules may be called proper rules of formation, and non-recursive rules (like those seen until now) axiomatic rules of formation. Montague tried to get by with axiomatic rules of formation; proper rules of formation for non-resumptive relativisation and quantification, both binding exactly one position, are as follows (cf. Morrill 1990b).

(20)  Δ, a − x: N ⇒ α + a + γ − χ: S  R9 Δ, b − y: RELPRO ⇒ b + α + γ − (y λxχ): R

(21)  Δ, a − x: N ⇒ β(a) − ϕ: S R10 Δ, b − y: QP ⇒ β(b) − (y λxϕ): S

The relativisation rule R9 states that where some assumptions plus a referring nominal with prosodic variable a and semantic variable x yield a sentence with prosodics α+a+γ (α or γ might be ϵ), those assumptions plus a relative pronoun yield a relative clause with prosodics α + γ prefixed by the relative pronoun, and semantics the application of the relative pronoun to the abstraction over x of the input sentence semantics. And the quantification rule R10 states that where some assumptions plus a referring nominal with prosodic variable a and semantic variable x yield a sentence, then those assumptions plus a quantifier phrase yield a sentence with prosodics the result of substituting the quantifier phrase prosodics for a, and semantics the application of the quantifier phrase to the abstraction over x of the input sentence semantics.

Derivations including such metarules can be given in a quite accessible manner by extending the PTQ-style derivation format to one akin to Fitch-style natural deduction. That is, we have “smart” block-structure to manage hypotheses and their scope and discharge. Derivations are obtained by five kinds of steps:

a. n.  α – ϕ: A  for any lexical entry
b. n.  | a_{1} – x_{1}: A_{1}  H
| ⋮  ⋮
n + m. | \underline{a_{m} – x_{m}: A_{n}}  H
c. n.  α – ϕ: A
α′ – ϕ′: A  =n, if α = α′ & ϕ = ϕ′
d. n.  α – ϕ: N
m.  β – ψ: VP
α + β – (ψ ϕ): S  R1 n, m
e. n.  β – ψ: RELPRO  H
m.  |\underline{a – x: N}
p. |α + a + γ – χ: S unique a as indicated
β + α + γ – (ψ λxχ): R R9 n, m, p

(22)

The rule (22a) states that we may introduce a lexical assignment at any point. The hypothesis rule (22b) states that at any point a subderivation with some number of hypotheses may be begun. Since we shall later want to have subderivations with two hypotheses, we allow at once the general case with any number. The variables in each hypotheses should be new, i.e. not occurring in any other hypothesis in scope. The relabelling rule (22c) states that terms may be rewritten to equivalents. We have rules like (22d) for axiomatic rules of formation, and rules like (22e), exiting from subderivations and discharging hypotheses, for proper rules of formation. Note that the condition limits the number of uses of the hypothesis, i.e. the number of positions bound, to exactly one.

An example of relativisation ‘which John talks about’ is obtained as follows.

1. which − λxλyλz[(y z) ∧ (x z)]: RELPRO
2. John − j: N
3. talked − talk: PV
4. about − about: P
5. |\underline{a − x: N}  H
6. |about + a − (about x): PP  4, 5 R8
7. |talked + about + a − (talk (about x)): VP  3, 6 R6
8. |John + talked + about + a − ((talk (about x)) j): S  2, 7 R1
9. |John + talked + about + a + ϵ − ((talk (about x)) j): S = 8
10. which + John + talked + about + ϵ−
(λxλyλz[(x z) ∧ (y z)] λx((talk (about x))) j)): R  1, 5, 9 R9
11. which + John + talked + about−
λyλz[(y z) ∧ ((talk (about z))) j)]: R  = 10

(23)

The manipulation between line 8 and 9 is needed in order to match the form of the relativisation rule. In the case of medial extraction (i.e. with a non-peripheral extraction site) the required form would already be present. We shall not spell out such cases, and the embedding of subderivations for quantifier scoping, and its recursion for quantifier scope ambiguity, since many essentially equivalent examples appear later in the context of categorial grammar. Rather, we assume that the architectural and technical space is established, and begin to consider the way in which it is instanciated by categorial grammar.

3 Model Theory

The theory of presentation given until now is a “dumb” syntactic system, such as is ubiquitous in formal grammar and the tradition of the Chomsky hierarchy. The central tenet of categorial grammar in the logical tradition, as it is to be assumed here, is that the theory of formation can be defined model theoretically. This stance occupies an extreme minimalist lexicalist position in which there is no syntactic component playing a definitional rôle in the specification of a language model. There is just a lexicon and a universal theory of formation under which the lexicon is to be closed to specify the language model, declaratively defined by the interpretation of categorial types. Rules of syntax serve to calculate, but not to define. Ultimately a computational and developmental gain is anticipated. When a lexicon defines a language model in interaction with a variable syntactic component, universal parsers and generators must accomodate the varying syntactic parameter, and grammar development must constantly readdress the possible tradeoff between lexical and syntactic variation. Such advantages cannot be proved a priori however, so we must be content now with the interest with regards structure of a model theoretic perspective on grammar.

3.1 Multiplicative Operators and Groupoid Prosodic Interpretation

Assume a set F of categorial syntactic types or (“category”) formulas freely generated from a set A of atomic formulas thus:

{F ::= A | F•F | F\F | F/F \atop (24)}

We consider interpretation with respect to model structures starting with a groupoid algebra (L, +), which is simply a set L closed under a binary operation +. An interpretation is a mapping D of formulas into subsets of L such that (cf. e.g. Lambek 1988):^{3}

\begin{aligned}D(A•B) & = \{s_{1} + s_{2}|s_{1} ∈ D(A) ∧ s_{2} ∈ D(B)\} \\ D(A\B) & = \{s|∀s′ ∈ D(A), s′ + s ∈ D(B)\} \\ D(B/A) & = \{s|∀s′ ∈ D(A), s + s′ ∈ D(B)\} \end{aligned} ; (25)

Such an interpretation for (in linear logic terminology; Girard 1987) multiplicative operators • (product), \ and / (divisions) is referred to as interpretation by residuation with respect to the groupoid operation +. Consider a semantic consequence relation ⊧ between formulas:

(26) ⊧ A ⇒ B iff in all interpretations D(A) ⊆ D(B)

Then interpretation by residuation delivers the following (see Lambek 1958, 1961, 1988; Dunn 1991; Moortgat 1991b; Moortgat and Morrill 1991):^{4}

{A ⇒ C/B =|⊧ A•B ⇒ C =|⊧ B ⇒ A\C \atop (27)}

Keeping the interpretation clauses and adjusting the algebra gives us alternative logics, in particular the non-associative Lambek calculus, and the associative Lambek calculus. For groupoids we have the non-associative Lambek calculus NL (Lambek 1961). If we impose the condition of associativity on the algebra of interpretation, we are dealing with semigroup algebras (L, +):

{s_{1} + (s_{2} + s_{3}) = (s_{1} + s_{2}) + s_{3} \atop (28)}

This gives us associative Lambek calculus L (Lambek 1958), a version of noncommutative linear logic.

The interpretation in groupoids and semigroups corresponds to the prosodic dimension of signs (e.g. an algebra of binary trees is a groupoid, and an algebra of strings is a semigroup). For description of language we are interested also in a semantic dimension.

3Note that we keep to the categorial notation as originally used by Lambek.

4In fact the residuation laws are valid for an even more general interpretation scheme than that which we need here: they apply for ternary “accessibility” relations in general, not just to binary functions, i.e. deterministic, “total” ternary relations.

3.2 Type-logical Semantic Interpretation

Categorial product and division operators are to be semantically (as opposed to prosodically) interpreted as spaces in type-theory. A set T of semantic types is freely generated from a set D of basic semantic types thus:

{T ::= D | T → T | T × T \atop (29)}

A semantic algebra consists of a family {D_{τ}}_{τ∈T} of sets (semantic domains) such that D_{τ_{1}→τ_{2}} is the set of all functions from D_{τ_{1}} to D_{τ_{2}} (function space) and D_{τ_{1}×τ_{2}} is the set of all ordered pairs of objects from D_{τ_{1}} and D_{τ_{2}} respectively (cross product, or: Cartesian product). A type map is a function T from category formulas to semantic types such that

{T (A\B) = T (B/A) = T (A) → T (B) \atop T (A•B) = T (A) × T (B)} ; (30)

Working in two dimensions, each formula A has an interpretation D(A) which is a set of ordered pairs of prosodic objects from L and semantic objects from T (A) (cf. e.g. Morrill 1992a):

\begin{aligned}D(A•B) & = \{⟨s_{1} + s_{2}, ⟨m_{1}, m_{2}⟩⟩|⟨s_{1}, m_{1}⟩ ∈ D(A) ∧ ⟨s_{2}, m_{2}⟩ ∈ D(B)\} \\ D(A\B) & = \{⟨s, m⟩|∀⟨s′, m′⟩ ∈ D(A), ⟨s′ + s, m(m′)⟩ ∈ D(B)\} \\ D(B/A) & = \{⟨s, m⟩|∀⟨s′, m′⟩ ∈ D(A), ⟨s + s′, m(m′)⟩ ∈ D(B)\} \end{aligned} ; (31)

4 Proof Theory

Lambek (1961) gives a Gentzen-style sequent proof theory for the non-associative calculus. A sequent is of the form Γ ⇒ A where the succedent A is a type formula and the antecedent Γ is what we shall call a configuration, which in this case is a binary bracketed sequence of one or more type formulas. A sequent is read as stating that for any objects in the antecedent types the result of applying the operation implicit in the configuration is an object in the succedent type. The calculus is as follows. The parenthetical notation Γ(Δ) represents a configuration containing a distinguished subconfiguration Δ.

(32) a. A ⇒ A  id  Γ ⇒ A Δ(A) ⇒ BCut Δ(Γ) ⇒ B

b. Γ ⇒ A Δ(B) ⇒ C\L Δ([Γ, A\B]) ⇒ C  [A, Γ] ⇒ B\R Γ ⇒ A\B

c. Γ ⇒ A Δ(B) ⇒ C/L Δ([B/A, Γ]) ⇒ C  [Γ, A] ⇒ B/R Γ ⇒ B/A

d. Γ([A, B]) ⇒ C•L Γ(A•B) ⇒ C  Γ ⇒ A Δ ⇒ B•R Γ, Δ ⇒ A•B

A Gentzen sequent presentation has a left rule and a right rule for each connective. The former introduces an occurrence of the connective on the left hand side of the sequent, the latter on the right hand side. Or reading from conclusion to premisses, the former removes a connective occurrence on the left, and the latter removes a connective occurrence on the right. Apart from that, no new formula occurrences are introduced in going from conclusion to premisses, accept by the rule Cut. If a Cut-elimination result can be given, that is a demonstration that all theorems have a proof without Cut, a Gentzen sequent presentation may thus provide a decision procedure. Lambek (1961) proved Cut-elimination (a technical error is corrected by Kandulski 1988).

Lambek (1958) gives a Gentzen-style sequent proof theory for the associative calculus. For this a configuration is an unbracketed sequence of one or more type formulas:

(33) a. A ⇒ A  id  Γ ⇒ A Δ(A) ⇒ BCut Δ(Γ) ⇒ B

b. Γ ⇒ A Δ(B) ⇒ C\L Δ(Γ, A\B) ⇒ C  A, Γ ⇒ B\R Γ ⇒ A\B

c. Γ ⇒ A Δ(B) ⇒ C/L Δ(B/A, Γ) ⇒ C  Γ, A ⇒ B/R Γ ⇒ B/A

d. Γ(A, B) ⇒ C•L Γ(A•B) ⇒ C  Γ ⇒ A Δ ⇒ B•R Γ, Δ ⇒ A•B

Lambek proves Cut-elimination for this case also.

Rather than use these more standard formulations, we shall for the most part use labelled deductive systems (LDSs) to present proof theory (Gabbay 1991; see Moortgat 1991b for categorial application). The philosophy of labelled deduction is “to bring semantics back into syntax”. What that will mean for grammar is that prosodic terms and semantic terms, elements of term algebras of the algebras of interpretation, are explicitly managed, providing a formulation maximally comparable to the PTQ perspective. In addition to a language of formulas interpreted as sets of objects, there are defined languages of terms (labels) interpreted as particular objects.

We propose to formulate the labelling discipline as follows. Ignoring the distinction between prosodic and semantic variables, statements of formation are sequents of the form:

{l_{1}: A_{1}, …, l_{n}: A_{n} ⇒ μ(l_{1}, …, l_{n}): A \atop (34)}

Where l_{1}, … l_{n} are variables and A_{1}, …, A_{n} are formulas such that the antecedent is a mapping from variables to formulas, and μ(l_{1}, …, l_{n}) is a term with free variables l_{1}, …, l_{n}. It is read as stating that the image of A_{1}, …, A_{n} under the operation μ is contained in A, i.e. that under every interpretation D of formulas as sets of objects, and every interpretation d of terms, if for each i d(l_{i}) ∈ D(A_{i}) then d(μ(l_{1}, …, l_{n})) ∈ D(A).

In our labelling for grammar, we maintain this convention that antecedent formulas are labelled with prosodic and semantic variables (not arbitrary terms):

{a_{1} – x_{1}: A_{1}, …, a_{n} – x_{n}: A_{n} ⇒ α – ϕ: A \atop (35)}

As a result each theorem can be read as a Montagovian rule of formation with input categories A_{1}, …, A_{n} and output category A and prosodic and semantic operations α and ϕ. Other versions of labelling allow labelling antecedent formulas with prosodic and semantic terms in general. However such labelling constrains the value of the elements to which the theorems apply by reference to the terms that represent them. In relation to grammar, this would mean conditioning rules on the semantic and/or prosodic form of the input. For instance, with respect to semantics, this would constitute essential reference to semantic form in the way which Montague grammar deliberately avoids. We advocate exactly the same transparency in relation to the prosodic dimension.

A theory is a set of such statements closed under Cut and id. A theory is sound iff all its statements are true. It is complete iff it contains every statement formulable which is true. There is a dependence on languages of terms chosen here, but by taking these to be term algebras it is intended that there is completeness with respect to full classes of operations in the algebras of interpretation.

4.1 Prosodic and Semantic terms

For groupoid models, a set P of prosodic terms is freely generated from a set K of prosodic constants and a denumerably infinite set U of prosodic variables thus:

{P ::= U | K | P + P \atop (36)}

Each prosodic term α has an interpretation d(α) as an object in a groupoid algebraic model structure, given in the obvious way.

To include the semantic side, typed semantic terms are defined and interpreted as usual, but including pairing and projection for the Cartesian product semantic type. Starting from a set C_{τ} of constants and a denumerably infinite set V_{τ} of variables for each type τ, the set S_{τ} of typed semantic terms for each type τ is freely generated thus:

\begin{matrix}S_{τ} ::= C_{τ} | V_{τ} | (S_{τ′→τ} S_{τ′}) | π_{1}S_{τ×τ′} | π_{2}S_{τ′×τ} \\ S_{τ′→τ} ::= λV_{τ′}S_{τ} \\ S_{τ×τ′} ::= (S_{τ}, S_{τ′}) \end{matrix} ; (37)

4.2 Labelled Proof Theory

We are now in a position to give labelled deductive systems for the Lambek calculi. We do so in Gentzen sequent-style, and Fitch natural-deduction style.

4.2.1 Gentzen-style sequent rules

As a labelled deductive system the non-associative Lambek calculus with just prosodics is as follows in a labelled Gentzen-style sequent presentation. As before, the parenthetical notation indicates distinguished subterms. The prosodic terms are constructed by a non-associative binary adjunction operation. Note that the definition of statements of formation as being functional in their left-hand side assignment of types to variables rules out as ill-formed binary metarule instances where the same variable would receive different type assignments in the conclusion from the different premisses.

(38) a. a: A ⇒ a: A  id
b. Γ ⇒ α: A a: A, Δ ⇒ β(a): BCut Γ, Δ ⇒ β(α): B

c. Γ ⇒ α: A b: B, Δ ⇒ γ(b): C\L Γ, d: A\B, Δ ⇒ γ((α + d)): C

d. Γ, a: A ⇒ (a + γ): B\R Γ ⇒ γ: A\B

e. Γ ⇒ α: A b: B, Δ ⇒ γ(b): C/L Γ, d: B/A, Δ ⇒ γ((d + α)): C

f. Γ, a: A ⇒ (γ + a): B/R Γ ⇒ γ: B/A

g. a: A, b: B, Δ ⇒ γ((a + b)): C•L c: A•B, Δ ⇒ γ(c): C

h. Γ ⇒ α: A Δ ⇒ β: B•R Γ, Δ ⇒ (α + β): A•B

In (38g) the succedent of the premise must contain the complex subterm (a + b), which is replaced by c in the conclusion sequent. As is normal in sequent calculus, each operator has a L(eft) rule of use and a R(ight) rule of proof. Cut-free backward chaining proof search is terminating since in every proof step going from conclusion to premisses, the total number of operator occurrences is reduced by one. And such proof search constructs in the succedent label of a sequent proved a term representing the operation mapping the antecedent type inhabitants into the succedent type.

An example of a Gentzen proof deriving “subject lifting” of a referring nominal is thus:

(39) a: N ⇒ a: N c: S ⇒ c: S\L a: N, b: N\S ⇒ (a + b): S/R a: N ⇒ a: S/(N\S)

Including also the semantic dimension, the labelled Gentzen sequent presentation is (40). In (40g) the parenthetical notation with commas indicates two distinguished subterm occurrences in the semantics.

(40) a. a – x: A ⇒ a – x: A  id
b. Γ ⇒ α – ϕ: A a – x: A, Δ ⇒ β(a) – ψ(x): BCut Γ, Δ ⇒ β(α) – ψ(ϕ): B

c. Γ ⇒ α – ϕ: A b – y: B, Δ ⇒ γ(b) – χ(y): C\L Γ, d – w: A\B, Δ ⇒ γ((α + d)) – χ((w ϕ)): C

d. Γ, a – x: A ⇒ (a + γ) – ψ: B\R Γ ⇒ γ – λxψ: A\B

e. Γ ⇒ α – ϕ: A b – y: B, Δ ⇒ γ(b) – ψ(y): C/L Γ, d – w: B/A, Δ ⇒ γ((d + α)) – ψ((w ϕ)): C

f. Γ, a – x: A ⇒ (γ + a) – ψ: B/R Γ ⇒ γ – λxψ: B/A

g. a – x: A, b – y: B, Δ ⇒ γ((a + b)) – χ(x, y): C•L c – z: A•B, Δ ⇒ γ(c) – χ(π_{1}z, π_{2}z): C

h. Γ ⇒ α – ϕ: A Δ ⇒ β – ψ: B•R Γ, Δ ⇒ (α + β) – (ϕ, ψ): A•B

With semantics the previous derivation becomes the following.

(41) a – x: N ⇒ a – x: N c – z: S ⇒ c – z: S\L a – x: N, b – y: N\S ⇒ (a + b) – (y x): S/R a – x: N ⇒ a – λy(y x): S/(N\S)

4.2.2 Fitch-style Natural Deduction

For labelled Fitch-style categorial derivation, the lexical assignment, subderivation hypothesis, and term label equation rules are as given earlier:

n.  α – ϕ: A  for any lexical entry
n.  | a_{1} – x_{1}: A_{1} H
| ⋮  ⋮
n + m. | \underline{a_{m} – x_{m}: A_{n}} H
n.  α – ϕ: A
α′ – ϕ′: A  =n, if α = α′ & ϕ = ϕ′

(42)

As for a Gentzen formulation, there are two rules for each operator: a rule of elimination (corresponding to the Gentzen left rule) showing how to use a formula with that operator as principal connective, and a rule of introduction (corresponding to the Gentzen right rule) showing how to prove a formula with that operator as principal connective.

n. α – ϕ: A
m. γ – χ: A\B
(α + γ) – (χ ϕ): B E\ n, m
n. |\underline{a – x: A}  H
m. |(a + γ) – ϕ: B  unique a as indicated
γ – λxϕ: A\B  I\ n, m

(43)

n. α – ϕ: A
m. γ – χ: B/A
(γ + α) – (χ ϕ): B E/ n, m
n. |\underline{a – x: A}  H
m. |(γ + a) – ϕ: B  unique a as indicated
γ – λxϕ: B/A  I/ n, m

(44)

n.  γ – χ: A•B
m. |a – x: A H
m + 1. |\underline{b – y: B}  H
p.  |δ[(a + b)] – ω[x, y]: D unique a, b as indicated
δ[γ] – ω[π_{1}χ, π_{2}χ]: D E• n, m, m + 1, p
n.  α – ϕ: A
m.  β – ψ: B
(α + β) – (ϕ, ψ): A•B I• n, m

(45)

The previous theorem is now derived:

1. a – x: N
2. |\underline{b – y: N\S}  H
3. |(a + b) – (y x): S  E\ 1, 2
4. a – λy(y x): S/(N\S) I/ 2, 3

(46)

4.3 LDS for Associative Lambek Calculus

A Gentzen-style labelled calculus for the associative Lambek calculus L can be obtained from that for the non-associative calculus by adding a structural rule of associativity:

(47) Γ ⇒ α(((α_{1} + α_{2}) + α_{3})): AA Γ ⇒ α((α_{1} + (α_{2} + α_{3}))): A

For the Fitch-style we may add a prosodic equation:

{((α_{1} + α_{2}) + α_{3}) = (α_{1} + (α_{2} + α_{3})) \atop (48)}

Alternatively, the associative Lambek calculus can be given by dropping parentheses in prosodic labels. Illustrating in Fitch-style, this gives the following:

n. α – ϕ: A
m. γ – χ: A\B
α + γ – (χ ϕ): B E\ n, m
n. |\underline{a – x: A}  H
m. |a + γ – ϕ: B  unique a as indicated
γ – λxϕ: A\B  I\ n, m

(49)

n. α – ϕ: A
m. γ – χ: B/A
γ + α – (χ ϕ): B E/ n, m
n. |\underline{a – x: A}  H
m. |γ + a – ϕ: B  unique a as indicated
γ – λxϕ: B/A  I/ n, m

(50)

n.  γ – χ: A•B
m. |a – x: A H
m + 1. |\underline{b – y: B}  H
p.  |δ(a + b) – ω(x, y): D unique a, b as indicated
δ(γ) – ω(π_{1}χ, π_{2}χ): D E• n, m, m + 1, p
n.  α – ϕ: A
m.  β – ψ: B
α + β – (ϕ, ψ): A•B I• n, m

(51)

This allows derivation of e.g. composition theorems not valid in the non-associative case.

1. d – w: VP/PP
2. e – u: PP/N
3. |\underline{c – z: N}  H
4. |e + c – (e z): PP  E/ 2, 3
5. |d + e + c – (w (e z)): VP E/ 1, 4
6. d + e – λz(w (e z)): VP/PP I/ 3, 4

(52)

We now have all we need in order to give linguistic illustration.

5 Linguistic Application

5.1 Left extraction: relativisation and topicalisation

We have already seen the relativisation example (53a) (exhibiting the same kind of dependencies as other left extraction constructions such as topicalisation (53b) and interrogativisation (53c)) in the context of the PTQ-style grammar.

a. which John talked about
b. Mozart John talked about
c. What did John talk about?

(53)

The relativisation can be derived as follows in Fitch-style natural deduction L without parentheses:

1. which − λxλyλz[(y z) ∧ (x z)]: (CN\CN)/(S/N)
2. John − j: N
3. talked − talk: (N\S)/PP
4. about − about: PP/N
5. |\underline{a − x: N}  H
6. |about + a − (about x): PP  4, 5 E/
7. |talked + about + a − (talk (about x)): N\S  3, 6 E/
8. |John + talked + about + a − ((talk (about x)) j): S  2, 7 E\
9. John + talked + about − λx((talk (about x)) j): S/N  5, 8 I/
10. which + John + talked + about−
(λxλyλz[(x z) ∧ (y z)] λx((talk (about x)) j)): CN\CN 1, 9 E/
11. which + John + talked + about−
λyλz[(y z) ∧ ((talk (about z)) j)]: CN\CN  = 10

(54)

The topicalisation is generated if N•(S/N) is included as a distinguished type (for details see Morrill and Gavarró 1992):

1. Mozart – mozart: N
2. John + talked + about – λx((talk (about x)) j): S/N
3. Mozart + John + talked + about –
(mozart, λx((talk (about x)) j)): N•(S/N)  I• 1, 2

(55)

And also without going into details (but see e.g. Carpenter 1992), the wh-question can be obtained by assignment of the interrogative pronoun to I/(M/(S/N)) where M represents subject-auxiliary inverted sentences, and I interrogatives.

Elegant as such categorial grammar may be, it is more suggestive of an approach to computational linguistic grammar formalism, than actually representative of such. The present approach to left extraction for example is limited to peripheral, as opposed to medial extractions, since S/N represents sentences lacking nominals at the right periphery. For resolution of such matters by means of structural operators, e.g. △ for permutation, whence S/N may become S/△N, see Morrill, Leslie, Hepple and Barry (1990) and Barry, Hepple, Leslie and Morrill (1991). Various other enrichments are proposed in e.g. Moortgat (1988, 1990, 1991a), van Benthem (1989), Morrill (1990a, 1990b, 1990c, 1992a, 1992b) and Moortgat and Morrill (1991). Moortgat (1988) advanced earlier discussion of discontinuity in e.g. Bach (1981, 1984) with a proposal for infixing and wrapping operators. The operators not only provide scope over these particular phenomena but also, as indicated in e.g. Moortgat (1990), seem to provide an underlying basis in terms of which operators for binding phenomena such as quantification and reflexivisation should be definable. The coverage of pied-piping in Morrill (1992b) would also be definable in terms of these primitives, but all this depends on the resolution of certain technical issues which have been to date outstanding.

6 Groupoid Prosodic Interpretation with Identity Element

We already saw use of the empty string in treatment of discontinuity in the PTQ-style fragment. To prepare ground for the treatment of discontinuity, we now incorporate an identity element in associative categorial grammar. Category formulas are freely generated from a set A of atomic category formulas thus:

{F = A | F•F | F\F | F/F | I \atop (56)}

The formula formed by the nullary operator I is a unit for product. We interpret in a monoid (L^{∗}, +, ϵ), i.e. a semigroup (L^{∗}, +) with an element ϵ ∈ L^{∗} such that:

{s + ϵ = ϵ + s = s \atop (57)}

See e.g. Lambek (1988). Then I is made a unit for product by defining its interpretation thus:

{D(I) = \{ϵ\} \atop (58)}

If we interpret the other multiplicatives in L^{∗} we will have ϵ ∈ D(A/A), D(A\A) which, for linguistic reasons (Morrill 1990a), we do not want. Thus we interpret types as subsets of L defined to be L^{∗} − {ϵ}:

\begin{aligned}D(A•B) & = \{s_{1} + s_{2} ∈ L|s_{1} ∈ D(A) ∧ s_{2} ∈ D(B)\} \\ D(A\B) & = \{s ∈ L|∀s′ ∈ D(A), s′ + s ∈ D(B)\} \\ D(B/A) & = \{s ∈ L|∀s′ ∈ D(A), s + s′ ∈ D(B)\} \end{aligned} ; (59)

We will not actually use I here, and will not trouble to formulate rules in such a way as to block assignment to ϵ. What will be important for discontinuity is the presence of ϵ in the algebra of interpretation. The additional apparatus employed will be that of heterogeneous systems of types, that is systems with not just one family of multiplicatives, but with a community of such families.

7 Groupoid Prosodic Interpretation and Communities of Multiplicatives

The essential idea is presented in its generality in Moortgat and Morrill (1991). There it is shown how to give calculi for families of multiplicatives each with their own structural properties, and perhaps with structural interactions. For example, we may juxtapose L and NL (for anticipation of this particular case see Oehrle and Zhang 1989 and Morrill 1990b). More generally, we can define formulas F for n families of multiplicatives thus:

{F = A | F•_{1}F | F\_{1}F | F/_{1}F | F•_{2}F | F\_{2}F | F/_{2}F \atop | … | F•_{n}F | F\_{n}F | F/_{n}F} ; (60)

7.1 Model Theory for Communities of Multiplicatives

Prosodic interpretation is by residuation of each multiplicative with respect to its associated adjunction in an algebra (L, +_{1}, +_{2}, …, +_{n}):

\begin{aligned}D(A•_{i}B) & = \{s_{1} +_{i} s_{2}|s_{1} ∈ D(A) ∧ s_{2} ∈ D(B)\} \\ D(A\_{i}B) & = \{s|∀s′ ∈ D(A), s′ +_{i} s ∈ D(B)\} \\ D(B/_{i}A) & = \{s|∀s′ ∈ D(A), s +_{i} s′ ∈ D(B)\} \end{aligned} ; (61)

As a consequence the residuation laws hold for each family:

{A ⇒ C/_{i}B =|⊧ A•_{i}B ⇒ C =|⊧ B ⇒ A\_{i}C \atop (62)}

The semantic interpretation takes place with respect to cross product and function formation exactly as would be expected.

7.2 Proof Theory for Communities of Multiplicatives

The Fitch-style labelled deduction rules are as before for, but with each connective correlated with its adjunction constructor in the labels.

n.  α – ϕ: A  for any lexical entry
n.  | a_{1} – x_{1}: A_{1} H
| ⋮  ⋮
n + m. | \underline{a_{m} – x_{m}: A_{n}} H
n.  α – ϕ: A
α′ – ϕ′: A  =n, if α = α′ & ϕ = ϕ′

(63)

n. α – ϕ: A
m. γ – χ: A\_{i}B
(α +_{i} γ) – (χ ϕ): B E\_{i} n, m
n. |\underline{a – x: A}  H
m. |(a +_{i} γ) – ϕ: B  unique a as indicated
γ – λxϕ: A\_{i}B  I\_{i} n, m

(64)

n. α – ϕ: A
m. γ – χ: B/_{i}A
(γ +_{i} α) – (χ ϕ): B E/_{i} n, m
n. |\underline{a – x: A}  H
m. |(γ +_{i} a) – ϕ: B  unique a as indicated
γ – λxϕ: B/_{i}A  I/_{i} n, m

(65)

n.  γ – χ: A•_{i}B
m. |a – x: A H
m + 1. |\underline{b – y: B}  H
p.  |δ[(a +_{i} b)] – ω[x, y]: D unique a, b as indicated
δ[γ] – ω[π_{1}χ, π_{2}χ]: D E•_{i} n, m, m + 1, p
n.  α – ϕ: A
m.  β – ψ: B
(α +_{i} β) – (ϕ, ψ): A•_{i}B I•_{i} n, m

(66)

The Gentzen-style labelled sequent rules likwise as before, but with each connective correlated with its adjunction constructor in the prosodic labels.

(67) a. a – x: A ⇒ a – x: A
b. Γ ⇒ α – ϕ: A a – x: A, Δ ⇒ β(a) – ψ(x): BCut Γ, Δ ⇒ β(α) – ψ(ϕ): B
c. Γ ⇒ α – ϕ: A b – y: B, Δ ⇒ γ(b) – χ(y): C \_{i}L Γ, d – w: A\_{i}B, Δ ⇒ γ((α +_{i} d)) – χ((w ϕ)): C
d. Γ, a – x: A ⇒ (a +_{i} γ) – ψ: B\_{i}R Γ ⇒ γ – λxψ: A\_{i}B

e. Γ ⇒ α – ϕ: A b – y: B, Δ ⇒ γ(b) – ψ(y): C /_{i}L Γ, d – w: B/_{i}A, Δ ⇒ γ((d +_{i} α)) – ψ((w ϕ)): C

f. Γ, a – x: A ⇒ (γ +_{i} a) – ψ: B/_{i}R Γ ⇒ γ – λxψ: B/_{i}A

g. a – x: A, b – y: B, Δ ⇒ γ((a +_{i} b)) – χ(x, y): C•_{i}L c – z: A•_{i}B, Δ ⇒ γ(c) – χ(π_{1}z, π_{2}z): C

h. Γ ⇒ α – ϕ: A Δ ⇒ β – ψ: B•_{i}R Γ, Δ ⇒ (α +_{i} β) – (ϕ, ψ): A•_{i}B

We set all this out explicitly in order to facilitate observation that the labelled proof theory for discontinuity will have precisely this pattern of implementation in labelled deduction.

8 Discontinuity

Binary operators ↑ and ↓ are proposed in Moortgat (1988) such that B↑A signifies functors that wrap around their A arguments to form Bs, and (in our notation) A↓B signifies functors that infix themselves in their A arguments to form Bs. Assuming the semigroup algebra of associative Lambek calculus, there are two possibilities in each case, depending on whether we are free to insert anywhere (universal), or whether the relevant insertion points are fixed (existential). We leave semantics aside for the moment.

Existential

D(B↑_{∃}A) = {s|∃s_{1}, s_{2}[s = s_{1} + s_{2} ∧ ∀s′ ∈ D(A), s_{1} + s′ + s_{2} ∈ D(B)]} Universal D(B↑_{∀}A) = {s|∀s_{1}, s_{2}[s = s_{1} + s_{2} → ∀s′ ∈ D(A), s_{1} + s′ + s_{2} ∈ D(B)]} (68)

Existential

D(B↓_{∃}A) = {s|∀s′ ∈ D(A), ∃s_{1}, s_{2}[s′ = s_{1} + s_{2} ∧ s_{1} + s′ + s_{2} ∈ D(B)]} Universal D(B↓_{∀}A) = {s|∀s′ ∈ D(A), ∀s_{1}, s_{2}[s′ = s_{1} + s_{2} → s_{1} + s′ + s_{2} ∈ D(B)]} (69)

Inspecting the possibilities of ordered sequent presentation, of the eight possible rules of inference (use and proof for each of four operators), only ↑_{∃}R and ↓_{∀}L are expressible:

(70) a. Γ_{1}, A, Γ_{2} ⇒ B ↑_{∃}R Γ_{1}, Γ_{2} ⇒ B↑_{∃}A

b. Γ_{1}, Γ_{2} ⇒ A Δ_{1}, B, Δ_{2} ⇒ C↓_{∀}L Δ_{1}, Γ_{1}, A↓_{∀}B, Γ_{2}, Δ_{2} ⇒ C

This is the partial logic of Moortgat (1988). Note that the absence of a rule of use for existential wrapping means that we could not generate from discontinuous elements such as ‘ring up’ and ‘give the cold shoulder’ which we should like to assign lexical category (N\S)↑_{∃}N. (Evidently ↑_{∀} would permit incorrect word order such as *‘Mary gave the John cold shoulder’.) The problem with ordered sequents appears to be that the implicit encoding of prosodic operations is of limited expressivity. Accordingly, Moortgat (1991b) seeks to improve the situation by means of explicit prosodic labelling. This does enable both rules for e.g. ↓_{∀} but still does not enable the useful ↑_{∃}L: the remaining problem is, as noted by Versmissen (1991), that we need to have an insertion point somehow determinate from the prosodic label for an existential wrapper in order to perform a left inference.

In Moortgat (1991a) a discontinuity product is proposed, again implicitly assuming just a semigroup algebra:^{5}

{D(A ⊙ B) = \{s_{1} + s_{2} + s′_{1}|s_{1} + s′_{1} ∈ D(A), s_{2} ∈ D(B)\} \atop (71)}

As for the discontinuity divisions, ordered sequent presentation cannot express rules of both use and proof: only ⊙R can be represented:

(72) Γ_{1}, Γ_{2} ⇒ A Δ ⇒ B⊙R Γ_{1}, Δ, Γ_{2} ⇒ A ⊙ B

Even using labelling, the problem for ⊙L remains and is the same as that before: there is no proper management of separation points. See Hepple (1993) for an attempt to give full logic for Moortgat interpretations via a complex system of labelling.

In Moortgat (1991a) it is observed how the quantifying-in of infix binders such as quantifier phrases seems almost definable as (S↑N)↓S: they infix themselves at N positions in Ss (and take semantic scope at the S level – that is why they must be quantified in). None of the interpretations above however enable the expression of the requirement that the positions referred to by the two operator occurrences are the same. The present proposals will facilitate this definability, and also admit of a full logic. In subsequent sections we deal with examples including the following instances of discontinuity.

5The version given is actually just the existential case of two possibilities, existential and universal, as before. No rules for the universal version can be expressed in ordered sequent calculus, or labelled sequent calculus.

a. Mary rang John up.  Particle verb
b. Mary gave John the cold shoulder. Discontinuous idiom
c. John likes everything  Quantifier raising

Everyone loves something John believes someone walks

d. for whom John works.  Pied-piping

the loss of which after so much wrangling John would finally have to pay for

e. John studies logic and Charles, phonetics.

Gapping

f. John showed Mary herself.  Object antecedent reflexivisation

(73)

9 Model Theory for Discontinuity

To formulate discontinuity we have a community comprising three families of multiplicatives: the usual associative operators, ‘split-point’ non-associative operators, and discontinuity operators. The category formulas are:

{F ::= A | F•F | F\F | F/F | F^{⋄}F | F>F | F<F \atop | F⊙F | F↓F | F↑F} ; (74)

The present proposals differ from Morrill and Solias, and also the original interpretations proposed by Moortgat (1988), in treating wrapping adjunction as a primitive, rather than defined, operation in the prosodic algebra. Corresponding to the three families of multiplicatives there are three adjunctions, and there is an identity element for the associative adjunction +. Thus prosodic interpretation is in an algebra (L^{∗}, +, ϵ, (., .), W) where (L^{∗}, +, ϵ) is a monoid and in addition to the associativity and identity conditions we have:

{(s_{1}, s_{3})W s_{2} = s_{1} + s_{2} + s_{3} \atop (75)}

Spelt out in full the interpretation is as follows by residuation with respect to each adjunction:

\begin{aligned}D(A•B) & = \{s_{1} + s_{2} ∈ L|s_{1} ∈ D(A) ∧ s_{2} ∈ D(B)\} \\ D(A\B) & = \{s ∈ L|∀s′ ∈ D(A), s′ + s ∈ D(B)\} \\ D(B/A) & = \{s ∈ L|∀s′ ∈ D(A), s + s′ ∈ D(B)\} \end{aligned} ; (76)

\begin{aligned}D(A^{⋄}B) & = \{(s_{1}, s_{2}) ∈ L|s_{1} ∈ D(A) ∧ s_{2} ∈ D(B)\} \\ D(A\B) & = \{s ∈ L|∀s′ ∈ D(A), (s′, s) ∈ D(B)\} \\ D(B/A) & = \{s ∈ L|∀s′ ∈ D(A), (s, s′) ∈ D(B)\} \end{aligned} ; (77)

\begin{aligned}D(A⊙B) & = \{s_{1}W s_{2} ∈ L|s_{1} ∈ D(A) ∧ s_{2} ∈ D(B)\} \\ D(A↓B) & = \{s ∈ L|∀s′ ∈ D(A), s′W s ∈ D(B)\} \\ D(B↑A) & = \{s ∈ L|∀s′ ∈ D(A), sW s′ ∈ D(B)\} \end{aligned} ; (78)

As above, L is L^{∗} − {ϵ}.

This is a refinement of the proposal in Morrill and Solias (1993) which is to interpret discontinuous operators in a prosodic algebra (L^{∗}, +, ϵ, ⟨., .⟩, 1, 2) where ⟨., .⟩ is a pairing operator (introduced in Solias 1992) and so has associated projection functions 1 and 2. This defines an algebra of the present form by (s, s′) = ⟨s, s′⟩ and sW s′ = 1s+s′ +2s, but not vice-versa, so that the present form has more general models. The refinement is motivated by the incompleteness of non-associative Lambek calculus for interpretation as ordered trees (see Venema 1993). Since tree formation is isomorphic to pairing, the same incompleteness would arise in the treatment of discontinuity using tupling. The more general models do not impose the structure that validates the non-NL-theorems considered by Venema.

10 Proof Theory for Discontinuity

To avoid having to list too many rules we give just the Fitch-style proof theory in full. The Gentzen formulation is likewise immediately obtained according to the heterogeneous design. Since + is the only associative constructor, we can represent this by ommitting its parentheses. There are the following term label equations:

{((α, γ)W β) = α + β + γ \atop α + ϵ = ϵ + α = α} ; (79)

The lexical assignment, subderivation hypotheses, and term rewriting rules are as usual:

n.  α – ϕ: A  for any lexical entry
n.  | a_{1} – x_{1}: A_{1} H
| ⋮  ⋮
n + m. | \underline{a_{m} – x_{m}: A_{n}} H
n.  α – ϕ: A
α′ – ϕ′: A  =n, if α = α′ & ϕ = ϕ′

(80)

The logical rules are as follows.

n. α – ϕ: A
m. γ – χ: A\B
α + γ – (χ ϕ): B E\ n, m
n. |\underline{a – x: A}  H
m. |a + γ – ϕ: B  unique a as indicated
γ – λxϕ: A\B  I\ n, m

(81)

n. α – ϕ: A
m. γ – χ: B/A
γ + α – (χ ϕ): B E/ n, m
n. |\underline{a – x: A}  H
m. |γ + a – ϕ: B  unique a as indicated
γ – λxϕ: B/A  I/ n, m

(82)

n.  γ – χ: A•B
m. |a – x: A H
m + 1. |\underline{b – y: B}  H
p.  |δ(a + b) – ω(x, y): D unique a, b as indicated
δ(γ) – ω(π_{1}χ, π_{2}χ): D E• n, m, m + 1, p
n.  α – ϕ: A
m.  β – ψ: B
α + β – (ϕ, ψ): A•B I• n, m

(83)

n. α – ϕ: A
m. γ – χ: A>B
(α, γ) – (χ ϕ): B E> n, m
n. |\underline{a – x: A}  H
m. |(a, γ) – ϕ: B  unique a as indicated
γ – λxϕ: A>B I> n, m

(84)

n. α – ϕ: A
m. γ – χ: B<A
(γ, α) – (χ ϕ): B E< n, m
n. |\underline{a – x: A}  H
m. |(γ, a) – ϕ: B  unique a as indicated
γ – λxϕ: B<A I< n, m

(85)

n.  γ – χ: A^{⋄}B
m. |a – x: A H
m + 1. |\underline{b – y: B}  H
p.  |δ((a, b)) – ω(x, y): D unique a, b as indicated
δ(γ) – ω(π_{1}χ, π_{2}χ): D E^{⋄} n, m, m + 1, p
n.  α – ϕ: A
m.  β – ψ: B
(α, β) – (ϕ, ψ): A^{⋄}B I^{⋄} n, m

(86)

n. α – ϕ: A
m. γ – χ: A↓B
(αW γ) – (χ ϕ): B E↓ n, m
n. |\underline{a – x: A}  H
m. |(aW γ) – ϕ: B  unique a as indicated
γ – λxϕ: A↓B  I↓ n, m

(87)

n. α – ϕ: A
m. γ – χ: B↑A
(γW α) – (χ ϕ): B E↑ n, m
n. |\underline{a – x: A}  H
m. |(γW a) – ϕ: B  unique a as indicated
γ – λxϕ: B↑A  I↑ n, m

(88)

n.  γ – χ: A⊙B
m. |a – x: A H
m + 1. |\underline{b – y: B}  H
p.  |δ((aW b)) – ω(x, y): D unique a, b as indicated
δ(γ) – ω(π_{1}χ, π_{2}χ): D E⊙ n, m, m + 1, p
n.  α – ϕ: A
m.  β – ψ: B
(αW β) – (ϕ, ψ): A⊙B I⊙ n, m

(89) The examples in the next section are derived using this format.

11 Linguistic Application

11.1 Particle Verbs

The example ‘Mary rang John up’ is derived as follows. The particle verb has a complex lexical form constructed out of the splitting adjunction, and its lexical type is that of a wrapping functor. After combination with the object at line 3, prosodic evaluation at line 4 give the discontinuous word order.

1. (rang, up) − phone: (N\S)↑N
2. John − j: N
3. Mary − m: N
4. ((rang, up)W John) − (phone j): N\S  1, 2 E↑
5. rang + John + up − (phone j): N\S  =4
6. Mary + rang + John + up − ((phone j) m): S 3, 5 E\

(90)

11.2 Discontinuous Idioms

A discontinuous idiom construction such as ‘Mary gave John the cold shoulder’ is treated in exactly the same way:

1. (gave, the + cold + shoulder) − give-tcs: (N\S)↑N
2. John − j: N
3. Mary − m: N
4. ((gave, the + cold + shoulder)W John) − (give-tcs j): N\S 1, 2 E↑
5. gave + John + the + cold + shoulder − (give-tcs j): N\S =4
6. Mary + gave + John + the + cold + shoulder−
((gave-tcs j) m): S  3, 5 E\

(91)

11.3 Quantifier Raising

In Moortgat (1990) a binary operator which we write here as ⇑ is defined for which the rule of use is essentially quantifying-in, so that a Montagovian treatment of quantifier-scoping is achieved by assignment of a quantifier phrase like ‘something’ to N⇑S, and assignment of determiners like ‘every’ to (N⇑S)/CN. As we already noted, in Moortgat (1991a) it is suggested that a category such as A⇑B might be definable as (B↑A)↓B, but Moortgat observed that this definability does not hold for the given interpretation, for which, furthermore, the logic is problematic. On the present formulation however, these intuitions are realised. The category (S↑N)↓N is a suitable category for a quantifier phrase such as ‘everything’ or ‘some man’, achieving sentential quantifier scope, and quantificational ambiguity. Consider first ‘Every man walks’:

1. every – λxλy∀z((x z) → (y z)): ((S↑N)↓S)/CN
2. man – man: CN
3. walks – walk: N\S
4. every + man – (λxλy∀z((x z) → (y z)) man): (S↑N)↓S E/ 1, 2
5. every + man – λy∀z((man z) → (y z)): (S↑N)↓S  = 4
6. |\underline{a – x: N}  H
7. |a + walks – (walk x): S  E\ 3, 6
8. |ϵ + a + walks – (walk x): S  = 7
9. |((ϵ, walks)W a) – (walk x): S  = 8
10. (ϵ, walks) – λx(walk x): S↑N  I↑ 6, 9
11. ((ϵ, walks)W every + man) –
(λy∀z((man z) → (y z)) λx(walk x)): S  E↓ 5, 10
12. ϵ + every + man + walks – ∀z((man z) → (walk z)): S = 11
13. every + man + walks – ∀z((man z) → (walk z)): S  = 12

(92)

The generation up to line 5 of ‘every man’ with the standard semantics and type (S↑N)↓N is straightforward. In lines 7 to 9 a sentence is constructed on the basis of the nominal a – x hypothesised at line 6. Prosodic equations are used to show that the prosodics can be expressed in a form in which W is the main constructor, and in which, furthermore, a is the right hand operand. The left hand operand is thus a split string term in which a is to be interpolated. Now because the wrap connective is the divisional residuation with respect to the right hand operand of W, this split string term is derivable at line 10 as of the wrap type S↑N, by I↑. Since ‘every man’ is an infix functor over S↑N, it can combine by E↓ (line 11), and on prosodic evaluation interpolates itself at the position in which the hypothesised nominal was used in the subderivational sentence. Thus the quantifier phrase binds semantically a semantic variable for the position in which it occurs prosodically.

There can be no deviance from this pattern, that is, a quantifier phrase cannot bind the wrong position, for there can be no way that the last line of the relevant subderivation can have the form required for I↑, that is (αW a) – ϕ where a – x is the hypothesis, without α being a split string marking the interpolation position for the prosodics that corresponds to semantics ϕ in terms of x: the equations do not allow anything else. So when a quantifier phrase infixes itself, it will semantically bind the position it occupies prosodically.

The following derivation shows the object position binding of ‘John likes everything’.

1. John − j: N
2. likes − like: (N\S)/N
3. everything − λx∀y(x y): (S↑N)↓S
4. |\underline{a − x: N}  H
5. |likes + a − (like x): N\S  2, 4 E/
6. |John + likes + a − ((like x) j): S  1, 5 E\
7. |John + likes + a + ϵ − ((like x) j): S  =6
8. |((John + likes, ϵ)W a) − ((like x) j): S  =7
9. (John + likes, ϵ) − λx((like x) j): S↑N  4, 8 I↑
10. ((John + likes, ϵ)W everything) − (λx∀y(x y) λx((like x) j)): S 3, 9 E↓
11. John + likes + everything − ∀y((like y) j): S  = 10

(93)

The next two derivations deliver the subject wide scope and object wide scope readings of ‘Everyone loves something’.

1. everyone – λx∀z[(person z) → (x z)]: (S↑N)↓S
2. loves – love: (N\S)/N
3. something – λx∃w[(thing w) ∧ (x w)]: (S↑N)↓S
4. |\underline{b – y: N}  H
5. ||\underline{a – x: N}  H
6. ||loves + a – (love x): N\S  E/ 2, 5
7. ||b + loves + a – ((love x) y): S  E\ 4, 6
8. ||((b + loves, ϵ)W a) – ((love x) y): S  = 7
9. |(b + loves, ϵ) – λx((love x) y): S↑N  I↑ 5, 8
10. |((b + loves, ϵ)W something) –
(λx∃w[(thing w) ∧ (x w)] λx((love x) y)): S  E↓ 3, 9
11. |b + loves + something – ∃w[(thing w) ∧ ((love w) y)]: S  = 10
12. |((ϵ, loves + something)W a) – ∃w[(thing w) ∧ ((love w) y)]: S = 11
13. (ϵ, loves + something) – λy∃w[(thing w) ∧ ((love w) y)]: S↑N I↑ 4, 12
14. everyone + loves + something –
∀z[(person z) → ∃w[(thing w) ∧ ((love w) z)]]: S  E↓ 3, 13

(94)

In (94) a nominal hypothesis for the subject is made at line 3, and another subderivation hypothesis for the object at line 4. Since subderivations are firstin-last-out, the subject position is bound last, that is the subject wide scope reading is obtained. The sentence already with the object quantifier phrase is obtained at line 11 just like ‘John likes everything’ in the previous example, but the subject is a hypothesis variable not a lexical form, and we have worked nested one level down.

In (95) the hypothesis of the wider scope subderivation is used in object position, so that the object wide scope reading is obtained.

1. everyone – λx∀z[(person z) → (x z)]: (S↑N)↓S
2. loves – love: (N\S)/N
3. something – λx∃w[(thing w) ∧ (x w)]: (S↑N)↓S
4. |\underline{a – x: N}  H
5. ||\underline{b – y: N}  H
6. ||loves + a – (love x): N\S  E/ 2, 4
7. ||b + loves + a – ((love x) y): S  E\ 5, 6
8. ||((ϵ, loves + a)W b) – ((love x) y): S  = 7
9. |(ϵ, loves + a) – λy((love x) y): S↑N  I↑ 5, 8
10. |((ϵ, loves + a)W everyone) –
(λx∀z[(person z) → (x z)] λy((love x) y)): S  E↓ 1, 9
11. |everyone + loves + a – ∀z[(person z) → ((love x) z)]: S  = 10
12. |((everyone + loves, ϵ)W a) – ∀z[(person z) → ((love x) z)]: S = 11
13. (everyone + loves, ϵ) – λx∀z[(person z) → ((love x) z)]: S↑N I↑ 4, 12
14. everyone + loves + something –
∃w[(thing w) ∧ ∀z[(person z) → ((love w) z)]]: S  E↓ 3, 13

(95)

In the examples so far the quantifier is peripheral in the sentence and (in associative calculus) a category (S/N)\S could have been used for a quantifier phrase to appear in object position and S/(N\S) for the quantifier phrase to appear in subject position. But further assignments still would be required for a quantifier phrase to appear in sentence-medial positions. Some generality with respect to the latter can be achieved by assuming second-order polymorphic categories (see Emms 1990), but two assignments, one forward-looking and another backward looking are nevertheless uniformly required by all quantifiers. The single assignment we have given allows appearance in all N positions without further ado, and allows all the relative quantifier scopings at S nodes. Thus for the example ‘John believes someone walks’, the first derivation to follow gives the narrow scope, non-specific, quantifier reading, but the second, the wide scope, specific reading, which involves the quantifier raising to the superordinate sentence, in which it is medial.

1. John – j: N
2. believes – believe: (N\S)/S
3. someone – λx∃y(x y): (S↑N)↓S
4. walks – walk: N\S
5. |\underline{a – x: N}  H
6. |a + walks – (walk x): S  E\ 4, 5
7. |((ϵ, walks)W a) – (walk x): S  =6
8. (ϵ, walks) – λx(walk x): S↑N  I↑ 5, 7
9. someone + walks – ∃y(walk y): S  E↓ 3, 8
10. believes + someone + walks – (believe ∃y(walk y)): N\S E/ 2, 9
11. John + believes + someone + walks –
((believe ∃y(walk y)) j): S  E\ 1, 10

(96)

1. John – j: N
2. believes – believe: (N\S)/S
3. someone – λx∃y(x y): (S↑N)↓S
4. walks – walk: N\S
5. |\underline{a – x: N}  H
6. |a + walks – (walk x): S  E\ 4, 5
7. |believes + a + walks – (believe (walk x)): N\S  E/ 2, 6
8. |John + believes + a + walks – ((believe (walk x)) j): S E\ 7, 1
9. |((John + believes, walks)W a) – ((believe (walk x)) j): S = 8
10. (John + believes, walk) – λx((believe (walk x)) j): S↑N I↑ 5, 9
11. John + believes + someone + walks –
∃y((believe (walk y)) j): S  E↓ 3, 10

(97)

11.4 Pied-Piping

Historically, pied-piping has played a crucial rôle in the promotion of feature percolation and phrase structural approaches (Gazdar, Klein, Pullum and Sag 1985; Pollard and Sag 1988, 1992) over categorial grammar. Pollard (1988, p.412) for example regards it as exposing a critical inadequacy:

“Evidently, there is no principled analysis of pied piping in an extended categorial framework like Steedman’s without the addition of a feature-passing mechanism for unbounded dependencies.”

(98)

On the phrase structural view, a relative pronoun introduces information which may percolate up normal constituent structure to endow larger phrases with the relativisation property of occurring fronted and binding a gap of the same category as the entire fronted constituent. Cases in which there is no pied-piping are, convincingly, obtained as the special case where the fronted constituent comprises only the relative pronoun. That is, a single categorisation covers both pied-piping and non-pied-piping cases such as (99).

a. (the contract) the loss of which after so much wrangling John

would finally have to pay for b. (the contract) which John would finally have to pay for the

loss of (99)

In Moortgat (1991a) a three-place operator is considered which is like A⇑B, except that quantifying-in changes the category of the context expression. Morrill (1992b) shows that this enables capture of pied-piping. It follows from the nature of the present proposals that (B↑C)↓A presents the desired complicity between the operators. As a result, the treatment of Morrill (1992b) can be presented in these terms.

As a first example, note how the following pied-piping assignment generates ‘about which John talked’ with the same semantics as ‘which John talked about’, considered earlier.

1. about − about: PP/N
2. which − λxλyλzλw[(z w) ∧ (y (x w))]: (PP↑N)↓(R/(S/PP))
3. John − j: N
4. talked − talk: (N\S)/PP
5. |\underline{a − x: N}  H
6. |about + a − (about x): PP  1, 5 E/
7. |about + a + ϵ − (about x): PP  =6
8. |((about, ϵ)W a) − (about x): PP  =7
9. (about, ϵ) − λx(about x): PP↑N  5, 8 I↑
10. ((about, ϵ)W which)−
(λxλyλzλw[(z w) ∧ (y (x w))] λx(about x)): R/(S/PP)  2, 9 E↓
11. about + which − λyλzλw[(z w) ∧ (y (about w)): R/(S/PP) = 10
12. |\underline{a − x: PP}  H
13. |talked + a − (talk x): N\S  4, 12 E/
14. |John + talked + a − ((talk x) j): S  3, 13 E\
15. John + talked − λx((talk x) j): S/PP  12, 14 I/
16. about + which + John + talked−
(λyλzλw[(z w) ∧ (y (for w)) λx((work x) j)): R  11, 15 E/
17. about + which + John + talked−
λzλw[(z w) ∧ ((talk (about w)) j)]: R  =16

(100)

This example is potentially manageable in any categorial grammar with composition, by assignment of type (PP/N)\((CN\CN)/(S/N)). Such assignments are an obvious possibility in the light of Szabolsci (1987) for example, who discusses pied-piping of reflexives, such as to render them direct functors over verbs. Such an assignment must be additional to the regular one, a situation to be improved if possible. But furthermore an example like (99a) where the relative pronoun is not peripheral in the pied-piped material would be problematic. It would need to be arranged by a further lexical assignment that ‘after so much wrangling’ modifies ‘loss’.

In fact, for unclear reasons, it is not easy to find highly acceptable examples of the crucially problematic medial pied-piping cases, but see e.g. (101).

(a statue) for the transport of which by rail John would have to pay $10,000 (101)

In other cases the pied-piped constituent occupies subject position:

a. (a supermarket) the opening of which by the queen/in June

was heralded a moving and historical occassion

b. (a woman) the painting of whom by Matisse fetched a fortune

c. (a boy) the yelling of whom outside could be heard throughout the sermon (102)

If in reality there were no such cases, which would be to say that pied-piping noun phrases always occur right-peripherally in the fronted constituent, a rudimentary treatment like that deriving from Szabolcsi would suffice for categorial grammar. Furthermore all existing phrase structure accounts would be erroneous in that none predict such right-peripherality. Thus for phrase structural approaches there would be “no principled analysis of pied piping” possible without the addition of directional constraints on feature inheritance. Since we regard the examples in the text as acceptable however, we do not take this conditional as going through.

The solution, in terms of infixing and wrapping, is much the same as that for quantification. There is the following derivation for ‘the loss of which after so much wrangling John would finally have to pay for’, given the relative pronoun assignment at line 4.

1. the – λxιy(x y): N/CN
2. loss – loss: CN
3. of – of: (CN\CN)/N
4. which –
λxλyλzλw[(z w) ∧ (y (x w))]: (N↑N)↓((CN\CN)/(S/N))
5. asmw – asmw: CN\CN
6. John – j: N
7. wfhtpf – wfhtpf: (N\S)/N
8. |\underline{a – x: N}  H
9. |of + a – (of x): CN\CN  E/ 3, 8
10. |loss + of + a – ((of x) loss): CN  E\ 2, 9
11. |loss + of + a + asmw – (asmw ((of x) loss)): CN  E\ 5, 10
12. |the + loss + of + a + asmw –
ιy((asmw ((of x) loss)) y): N  E/ 1, 11
13. |(the + loss + of , asmw)W a – ιy((asmw ((of x) loss)) y): N = 12
14. (the + loss + of , asmw) – λxιy((asmw ((of x) loss)) y): N↑N I↑ 8, 13
15. the + loss + of + which + asmw –
λyλzλw[(z w) ∧ (y ιu((asmw ((of w) loss)) u))]:
(CN\CN)/(S/N)
16. |\underline{a – x: N}  H
17. |wfhtpf + a – (wfhtpf x): N\S  E/ 7, 16
18. |John + wfhtpf + a – ((wfhtpf x) j): S  E\ 6, 17
19. John + wfhtpf – λx((wfhtpf x) j): S/N  I/ 16, 18
20. the + loss + of + which + asmw + John + wfhtpf –
λzλw[(z w) ∧ ((wfhtpf ιu((asmw ((of w) loss)) u)) j)]:
CN\CN  E/ 15, 19

(103)

In addition, this same assignment generates non-pied-piping cases, such as ‘which John would finally have to pay for the loss of’. Lines 7 to 11 of the following show that the regular relative pronoun category is derivable from the nominal pied-piping one because (ϵ, ϵ) ∈ D(N↑N).

1. which –
λxλyλzλw[(z w) ∧ (y (x w))]: (N↑N)↓((CN\CN)/(S/N))
2. John – j: N
3. wfhtpf – wfhtpf: (N\S)/N
4. the – λxιy(x y): N/CN
5. loss – loss: CN
6. of – of: (CN\CN)/N
7. |\underline{a – x: N}  H
8. |(ϵ, ϵ)W a – x: N  = 7
9. (ϵ, ϵ) – λxx: N↑N  I↑ 7, 8
10. ((ϵ, ϵ)W which) –
(λxλyλzλw[(z w) ∧ (y (x w))] λxx): (CN\CN)/(S/N)  E↓ 1, 9
11. which – λyλzλw[(z w) ∧ (y w)]: (CN\CN)/(S/N)
12. |\underline{a – x: N}  H
13. |of + a – (of x): CN\CN  E/ 6, 12
14. |loss + of + a – ((of x) loss): CN  E\ 5, 13
15. |the + loss + of + a – ιy(((of x) loss) y): N  E/ 4, 14
16. |(wfhtpf + the + loss + of + a –
(wfhtpf ιy(((of x) loss) y)): N\S  E/ 3, 15
17. (John + wfhtpf + the + loss + of + a –
((wfhtpf ιy(((of x) loss) y)) j): S  E\ 2, 16
18. John + wfhtpf + the + loss + of + a –
λx((wfhtpf ιy(((of x) loss) y)) j): S/N  I/ 12, 17
19. which + John + wfhtpf + the + loss + of –
λzλw[(z w) ∧ ((wfhtpf ιu(((of w) loss) u)) j)]: CN\CN E/ 11, 18

(104)

Thus prepositional pied-piping, nominal pied-piping, and no-pied-piping examples are all obtained by assignment to just the following two types:

(N↑N)↓((CN\CN)/(S/N)) (PP↑N)↓((CN\CN)/(S/PP))

(105)

The semantics is the same in each case, so all the examples considered are obtained by a single restricted second-order quantification assignment as in (106).

which – λxλyλzλw[(z w) ∧ (y (x w))]: ∀^{2}X : {N, PP}((X↑N)↓((CN\CN)/(S/X)))

(106)

The relative pronoun ‘that’ cannot pied-pipe, and so should be assigned the regular type:

(107) that – λxλyλz[(y z) ∧ (x z)]: (CN\CN)/(S/N)

With interrogatives, there is prepositional, but not nominal, pied-piping:

a. Who did John buy the ticket for?
b. For whom did John buy the ticket?
c. *The ticket for whom did John buy?

(108)

Thus each interrogative pronoun should have assignment to some combination of (109), but none a nominal pied-piping assignment.

I/(M/N)

(PP↑N)↓((I/(M/PP))

(109)

Categorial grammar is well-known to provide possibilities for “non-constituent” coordination (see Steedman 1985; Dowty 1988) less accessible in the phrase structure/feature percolation approach. We consider next a coordination construction which is highly problematic from all perspectives, gapping. It is entirely unclear how feature percolation could engage such a construction; but as we shall see the discontinuity apparatus succeeds in doing so.

11.5 Gapping

The proposal to be made here was introduced in Morrill and Solias (1993); see Solias (1993) for an alternative treatment. The kind of example to be considered is:

(110) John studies logic and Charles, phonetics.

Discussion is presented by reference to such a minimal example gapping a transitive verb TV. The construction is characterised by the absence in the right hand conjunct of a verbal element, the understood semantics of which is provided by a corresponding verbal element in the left hand conjunct. Clearly, instanciations of a coordinator category schema (X\X)/X will not generate gapping.

The phenomenon receives categorial attention in Steedman (1990). The approach of Steedman aims to reduce gapping to constituent coordination; furthermore it aims to do this using just the standard division operators of categorial grammar. This involves special treatment of both the right and the left conjunct.

With respect to the right hand conjunct, the initial problem is to give a categorisation at all. Steedman does this by reference to a constituent formed by the subject and object with the coordinator. This constituent is essentially TV\S but with a feature both blocking ordinary application, and licensing coordination with a left hand conjunct of the same category. The blocking is necessary because ‘and Charles, phonetics’ is clearly not of category TV\S: ‘Studies and Charles, phonetics’ is not a sentence. Now, with respect to the left hand conjunct, Steedman invokes a special decomposition of ‘John studies logic’ analysed as S, into TV and TV\S. There is then constituent coordination between TV\S and TV\S.

Finally the coordinate structure of category TV\S combines with TV on the left to give S.

Although this treatment addresses the two problems that any account of gapping must solve, categorisation of the right hand conjunct and access of the verbal semantics in the left hand conjunct, it attempts to do so within a narrow conception of categorial grammar (only division operators) that necessitates invocation of distinctly contrived mechanisms. The radical reconstruals of grammar implicated by this analysis are not necessary given the general framework including discontinuity operators we have set out.

Within the context of categorial grammar we have established, the right hand conjunct is characterisable as S↑TV.^{6} It remains to access the understood verbal semantics from the sentence that is the left hand conjunct. In order to recover from the left hand side the information we miss on the right hand side, we would like to say that this information, the category and semantics of the verb, is made available to the coordinator when it combines with the left conjunct. In accordance with the spirit of Steedman, we can observe that the left hand conjunct contains a part with the category S↑TV of the right hand constituent, but it is discontinuous, being interpolated by TV. But this is precisely what is expressed by the discontinuous product category (S↑TV)⊙TV. Furthermore, an element of such a category has as its semantics a pair the second projection of which is the semantics of the TV, making the verb semantics accessible. Consequently gapping is generated by assignment of ‘and’ to the category (((S↑TV)⊙TV)\S)/(S↑TV) with semantics λxλy[(π_{1}y π_{2}y) ∧ (x π_{2}y)].

6This is not the only possibility; a structural modality could be used as for extraction:

S/△TV.

1. John − j: N
2. studies − study: TV
3. logic − logic: N
4. and − λxλy[(π_{1}y π_{2}y) ∧ (x π_{2}y)]: (((S↑TV)⊙TV)\S)/(S↑TV)
5. Charles − c: N
6. phonetics − phonetics: N
7. |\underline{a − x: TV}  H
8. |a + phonetics − (x phonetics): N\S  6, 7 E/
9. |Charles + a + phonetics − ((x phonetics) c): S  5, 8 E\
10. |((Charles, phonetics)W a) − ((x phonetics) c): S  =9
11. (Charles, phonetics) − λx((x phonetics) c): S↑TV  7, 10 I↑
12. |\underline{a − x: TV}  H
13. |a + logic − (x logic): N\S  3, 12 E/
14. |John + a + logic − ((x logic) j): S  1, 13 E\
15. |((John, logic)W a) − ((x logic) j): S  =14
16. (John, logic) − λx((x logic) j): S↑TV  12, 15 I↑
17. ((John, logic)W studies)−
(λx((x logic) j), study): (S↑TV)⊙TV  2, 17 I⊙
18. John + studies + logic − (λx((x logic) j), study): (S↑TV)⊙TV =17
19. and + (Charles, phonetics)−
λy[(π_{1}y π_{2}y) ∧ ((π_{2}y phonetics) c)]: ((S↑TV)⊙TV)\S  4, 11 E/
20. John + studies + logic + and + (Charles, phonetics)−
(λy[(π_{1}y π_{2}y) ∧ ((π_{2}y phonetics) (λx((x logic) j), study)): S 18, 19 E\
21. John + studies + logic + and + (Charles, phonetics)−
((study logic) j) ∧ ((study phonetics) c): S  =20

(111)

11.6 Object-Antecedent Reflexivisation

Leaving aside locality (but see Morrill 1990a), a subject-oriented reflexive will be able to occur medially if it is assigned the type ((N\S)↑N)↓(N\S) (see Moortgat 1990, 1991a). But we started by noting a difficulty in relation to ordering for object-oriented reflexives. We return finally to the example with which we began. In the following the ditransitive ‘show’ is given a “head-wrapping” assignment (cf. Solias 1993) which forms a split string with its first argument (what will be the remote complement) and then wraps around its second argument (what will be its adjacent complement). Now an object-oriented reflexive can be assigned a category as shown in line 3: i.e. a splitting functor mapping “head-wrapping” ditransitives into wrapping transitives.

1. John − j: N
2. showed − show: ((N\S)↑N)<N
3. herself − λxλy((x y) y): (((N\S)↑N)<N)>((N\S)↑N)
4. Mary − m: N
5. (showed, herself ) − (λxλy((x y) y) show): (N\S)↑N  2, 3 E>
6. (showed, herself ) − λy((show y) y): (N\S)↑N  = 5
7. ((showed, herself )W Mary) − (λy((show y) y) m): N\S 4, 6 E↑
8. showed + Mary + herself − ((show m) m): N\S  = 7
9. John + showed + Mary + herself − (((show m) m) j): S 1, 8 E\

(112)

Note that the duplication of assignments needed for subject-orientation and object-orientation is to some extent redeemed by the distinction in some languages of pronoun forms for the two cases; in English also there is perhaps a difference in feel. Here, as in all the constructions considered, there is a great deal of empirical depth to be considered, as indeed there is technical depth to be considered.

12 Conclusion

Our aim has been to balance logic and linguistics, letting neither get further ahead than the other, to show how the apparatus presented provides the basic tools for a range of discontinuity phenomena. In such an interdisciplinary area it is out of bounds to study more logic than is good for linguistics, or more linguistics than the logic is good for. We hope to have done neither. In relation to computation, little has been said, so let us conclude with these observations on decidability of discontinuity.

The labelled Gentzen sequent proof theory for the three-family discontinuity is, assuming completeness and Cut-elimination, a decision procedure for theoremhood in that for any given conclusion type and multiset of antecedent types, exhaustive backward chaining proof search is terminating. Furthermore each proof constructs the derivational prosodic and semantic terms into which lexical forms are to substituted. For a given input sequence of words, there will be, from a finite lexicon with no assignments to the null element, only a finite number of multisets of lexical assignments the prosodic constant occurrences of which add up exactly to equal the occurrences in the input sequence of words. Thus for parsing, understood as the computation of all meanings for a given word sequence, it suffices as a decision procedure to search in this way and output the semantic forms associated with the prosodic forms evaluating to the right word order.

For generation, understood as the computation of all word sequences for a given semantic form, certain conditions can be observed to similarly suffice for decidability. If all lambda terms are single-bind and none are pure (i.e. constantfree), we can again just try the finite number of multisets of assignments the semantic constant occurrences of which add up exactly to equal those of the input semantic form. With no pure terms and no lexical vacuous abstractions, we still need consider only the finite number of multisets of assignments no semantic constant occurrence count of which exceeds that of the input semantic form.

References

Bach, Emmon: 1981, ‘Discontinuous Constituents in Generalized Categorial Grammars’, NELS, 11, 1–12.

Bach, Emmon: 1984, ’Some Generalizations of Categorial Grammars’, in Fred Landman and Frank Veltman (eds.), Varieties of Formal Semantics, Foris, Dordrecht, pp. 1–23.

Barry, Guy, Mark Hepple, Neil Leslie, and Glyn Morrill: 1991, ‘Proof Figures and Structural Operators for Categorial Grammar’, in Proceedings of the Fifth Conference of the European Chapter of the Association for Computational Linguistics.

van Benthem, Johan: 1989 ‘Categorial Grammar Meets Unification’, ms. Institute for Language, Logic and Information, University of Amsterdam.

van Benthem, Johan: 1991, Language in Action: Categories, Lambdas and Dynamic Logic, North-Holland, Amsterdam.

Buszkowski, W. : 1986, ’Completeness results for Lambek Syntactic Calculus’, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 32, pp. 13–28.

Buszkowski, M.: 1988, ‘Three Theories of Categorial Grammar’, in W. Buszkowski, W. Marciszewski and J. van Benthem (eds.) Categorial Grammar, Linguistic and Literary Studies in Eastern Europe 25, John Benjamins, Amsterdam, pp. 57–84.

Carpenter, Bob: 1992, ‘Categorial Grammars, Lexical Rules and the English Predicative’, in Robert Levine (ed.) Formal Grammar: Theory and Implementation, Cambridge University Press.

Dowty, David R.: 1979, ’Dative ‘Movement’ and Thomason’s Extensions of Montague Grammar’, in S. Davis and M. Methun (eds.) Linguistics, Philosophy and Montague Grammar, University of Texas Press, pp. 153–222.

Dowty, David: 1988 ‘Type Raising, Functional Composition, and Non-Constituent Conjunction’, in R. Oehrle, E. Bach and D. Wheeler (eds.) Categorial Grammars and Natural Language Structures, D. Reidel, Dordrecht, pp. 153–197.

Dowty, David R., Robert E. Wall and Stanley Peters: 1981, Introduction to Montague Semantics, D. Reidel, Dordrecht.

Dunn, J. M.: ‘Gaggle theory: an abstraction of Galois connections and residuation, with applications to negation, implication, and various logical operators’, in van Eijck (ed.) Logics in AI. JELIA Proceedings. Springer, Berlin, pp. 31–51.

Emms, Martin: 1990 ‘Polymorphic Quantifiers’, in Guy Barry and Glyn Morrill (eds.) Studies in Categorial Grammar, Edinburgh Working Papers in Cognitive Science, Volume 5, Centre for Cognitive Science, University of Edinburgh, pp. 65– 111. Also in Proceedings of the Seventh Amsterdam Colloquium.

Gabbay, D.: 1991, Labelled Deductive Systems. To appear, Oxford University Press.

Gazdar, Gerald, Ewan Klein, Geoffrey Pullum, and Ivan Sag: 1985, Generalised Phrase Structure Grammar, Blackwell, Oxford.

Girard, Jean-Yves: 1987, ‘Linear Logic’, Theoretical Computer Science 50, pp. 1–102.

Hepple, Mark: 1993, ‘Labelled Deduction and Discontinuous Constituency, ms. University of Pennsylvania.

Kandulski, M.: 1988, ‘The Non-Associative Lambek Calculus’, in W. Buszkowski, W. Marciszewski and J. van Benthem (eds.) Categorial Grammar, Linguistic and Literary Studies in Eastern Europe 25, John Benjamins, Amsterdam, pp. 141– 151.

Lambek, J.: 1958, ‘The mathematics of sentence structure’, American Mathematical Monthly 65, pp. 154–170.

Lambek, J.: 1961, ‘On the calculus of syntactic types’, in R. Jakobson (ed.) Structure of language and its mathematical aspects, Proceedings of the Symposia in Applied Mathematics XII, American Mathematical Society, pp. 166–178.

Lambek, J.: 1987, ‘Categorial and Categorical Grammars’, in Oehrle, Bach and Wheeler (eds.) Categorial Grammars and Natural Language Structures, D. Reidel, pp. 297–317.

Ludlow, Peter: 1992, ’Topic … Comment: Formal Rigor and Linguistic Theory’, Natural Language and Linguistic Theory, Volume 10 No. 2, pp. 335–344.

Montague, Richard: 1974, ‘Universal Grammar’. Theoria 36, 373–398. Reprinted in R. H. Thomason (ed.) (1974), Formal Philosophy: Selected Papers of Richard Montague, Yale University Press, pp. 222–246.

Montague, Richard: 1973, ‘The proper treatment of quantification in ordinary English’, in J. Hintikka, J. M. E. Moravcsik and P. Suppes Approaches to Natural Language, D. Reidel Dordrecht. Reprinted in R. H. Thomason (ed.) (1974), Formal Philosophy: Selected Papers of Richard Montague, Yale University Press, New Haven, pp. 247–270.

Moortgat, Michael: 1988, Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus, Foris, Dordrecht.

Moortgat, Michael: 1990, ’The Quantification Calculus: Questions of Axiomatisation’, in Deliverable R1.2.A of DYANA Dynamic Interpretation of Natural Language, ESPRIT Basic Research Action BR3175.

Moortgat, Michael: 1991a, ‘Generalised Quantification and Discontinuous Type Constructors’. To appear in Sijtsma & Van Horck (eds.) Proceedings of the Tilburg Symposium on Discontinuous Constituency. De Gruyter, Berlin.

Moortgat, Michael: 1991b, ‘Labelled Deductive Systems for categorial theorem proving, in Proceedings of the Eighth Amsterdam Colloquium.

Moortgat, Michael and Glyn Morrill: 1991, ‘Heads and Phrases: Type Calculus for Dependency and Constituency’, to appear in Journal of Language, Logic and Information.

Morrill, Glyn: 1990a, ‘Intensionality and Boundedness’, Linguistics & Philosophy 13, 699–726.

Morrill, Glyn: 1990b, ‘Rules and Derivations: Binding Phenomena and Coordination in Categorial Logic’, Deliverable R1.2.D of DYANA Dynamic Interpretation of Natural Language, ESPRIT Basic Research Action BR3175.

Morrill, Glyn: 1990c, ‘Grammar and Logical Types’, in Guy Barry and Glyn Morrill (eds.) Studies in Categorial Grammar, Edinburgh Working Papers in Cognitive Science Volume 5. Also in Proceedings of the Seventh Amsterdam Colloquium.

Morrill, Glyn: 1992a, Type-Logical Grammar, Research Report, Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya, and Onderzoeksinstituut voor Taal en Spraak, Universiteit Utrecht. Monograph to appear in Studies in Logic Language and Information, Kluwer, Dordrecht.

Morrill, Glyn: 1992b, ‘Categorial Formalisation of Relativisation: pied piping, islands and extraction sites’, report de recerca LSI–92–23–R, Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya.

Morrill, Glyn and Anna Gavarró: 1992, ‘Catalan Clitics’, in A. Lecomte (eds.) Word Order in Categorial Grammar, Adosa, Clermont-Ferrand, pp. 213–232.

Morrill, Glyn, Neil Leslie, Mark Hepple, and Guy Barry: 1990, ‘Categorial Deductions and Structural Operations’, in Guy Barry and Glyn Morrill (eds.) Studies in Categorial Grammar, Edinburgh Working Papers in Cognitive Science, Volume 5, Centre for Cognitive Science, University of Edinburgh, pp. 1–21.

Morrill, Glyn and Teresa Solias: 1993, ‘Tuples, Discontinuity and Gapping’, in Proceedings of European Chapter of the Association for Computational Linguistics, Utrecht, pp. 287–297.

Oehrle, Richard T. and Shi Zhang: 1989, ‘Lambek Calculus and Preposing of Embedded Subjects’, Chicago Linguistic Society 25.

Pollard, Carl J.: 1988, ’Categorial Grammar and Phrase Structure Grammar: an excursion on the syntax-semantics frontier’, in R. Oehrle, E. Bach and D. Wheeler (eds.) Categorial Grammars and Natural Language Structures, D. Reidel, Dordrecht, pp. 391–415.

Pollard, Carl and Ivan A. Sag: 1988, An Information-Based Approach to Syntax and Semantics, Part 1, Number 13, CSLI Lecture Notes, Center for the Study of Language and Information, Stanford.

Pollard, Carl and Ivan A. Sag: 1992, An Information-Based Approach to Syntax and Semantics, Part 2, Chicago University Press.

Pullum, Geoffrey K.: 1989, ’Topic … Comment: Formal Linguistics Meets the Boojum’, Natural Language and Linguistic Theory Volume 7 No.1, pp. 137–143.

Solias, Teresa: 1992, Gramáticas Categoriales, Coordinación Generalizada y Elisión, doctorate thesis, Departamento de Lingüística, Lógica, Lenguas Modernas y Filosofía de la Ciencia, Universidad Autónoma de Madrid.

Solias, Teresa: 1993, ‘Unassociative Tuple, Sequences, Discontinuity and Gapping in Categorial Grammar’, ms. University of Valladolid.

Steedman, Mark: 1985, ‘Dependency and Coordination in the Grammar of Dutch and English’, Language 61:3, 523–568.

Steedman, Mark: 1990 ‘Gapping as Constituent Coordination’, Linguistics and Philosophy 13, pp. 207–236.

Szabolcsi, Anna: 1987, ‘Bound Variables in Syntax’, Proceedings of the Sixth Amsterdam Colloquium, Institute for Language, Logic and Information, University of Amsterdam, pp.331–351.

Venema, Yde: 1993, ‘Tree Models and (Labelled) Categorial Grammar’, ms. Universiteit Utrecht.

Versmissen, K.: 1991, ‘Discontinuous Type Constructors in Categorial Grammar’, ms. Onderzoeksinstituut voor Taal en Spraak, Universiteit Utrecht.

Wasow, Thomas, Ivan A. Sag and Geoffrey Nunberg: 1983, ‘Idioms: an interim report’, in Shiro Hattori and Kazuko Inoue (eds.), Proceedings of the XIIIth International Congress of Linguists, Tokyo: CIPL, pp. 102–115.

Appendix: Ordered Sequent Calculus for Discontinuity

The general form for heterogeneous ordered sequent calculus from Moortgat and Morrill (1991) is:

(113)  id A ⇒ A  Γ ⇒ A Δ(A) ⇒ BCut Δ(Γ) ⇒ B

(114)a. Γ ⇒ A Δ(B) ⇒ C\_{n} L Δ([_{n}Γ, A\_{n}B]) ⇒ C  [_{n}A, Γ] ⇒ B\_{n} R Γ ⇒ A\_{n}B

b. Γ ⇒ A Δ(B) ⇒ C/_{n}L Δ([_{n}B/_{n}A, Γ]) ⇒ C  [_{n}Γ, A] ⇒ B/_{n}R Γ ⇒ B/_{n}A

c. Γ([_{n}A, B]) ⇒ C•_{n}L Γ(A•_{n}B) ⇒ C  Γ ⇒ A Δ ⇒ B•_{n}R [_{n}Γ, Δ] ⇒ A•_{n}B

In order to deal with with the three-family discontinuity system with identity, we define sequents as of the form Γ ⇒ A where A is a formula and Γ is a configuration, where configurations O are as follows.

{O = ϵ | F | [_{a}O, O] | [_{n}O, O] | [_{w}O, O] \atop (115)}

(116) Γ([_{a}Δ_{1}, [_{a}Δ_{2}, Δ_{3}]]) ⇒ AA_{a} Γ([_{a}[_{a}Δ_{1}, Δ_{2}], Δ_{3}]) ⇒ A

(117) Γ([_{w}Δ_{1}, [_{n}Δ_{2}, Δ_{3}]]) ⇒ AWN Γ([_{a}[_{a}Δ_{1}, Δ_{3}], Δ_{2}]) ⇒ A

(118) Γ([_{a}Δ, ϵ]) ⇒ A ϵ Γ(Δ) ⇒ A

(119) Γ([_{a}Δ, ϵ]) ⇒ A ϵ Γ(Δ) ⇒ A

(120)  id A ⇒ A  Γ ⇒ A Δ(A) ⇒ BCut Δ(Γ) ⇒ B

(121)a. Γ ⇒ A Δ(B) ⇒ C\L Δ([_{a}Γ, A\B]) ⇒ C  [_{a}A, Γ] ⇒ B\R Γ ⇒ A\B

b. Γ ⇒ A Δ(B) ⇒ C/L Δ([_{a}B/A, Γ]) ⇒ C  [_{a}Γ, A] ⇒ B/R Γ ⇒ B/A

c. Γ([_{a}A, B]) ⇒ C•_{n}L Γ(A•B) ⇒ C  Γ ⇒ A Δ ⇒ B•R [_{a}Γ, Δ] ⇒ A•B

(122)a. Γ ⇒ A Δ(B) ⇒ C>L Δ([_{n}Γ, A>B]) ⇒ C  [_{n}A, Γ] ⇒ B>R Γ ⇒ A>B

b. Γ ⇒ A Δ(B) ⇒ C<L Δ([_{n}B<A, Γ]) ⇒ C  [_{n}Γ, A] ⇒ B<R Γ ⇒ B<A

c. Γ([_{n}A, B]) ⇒ C^{⋄}L Γ(A^{⋄}B) ⇒ C  Γ ⇒ A Δ ⇒ B^{⋄}R [_{n}Γ, Δ] ⇒ A^{⋄}B

(123)a. Γ ⇒ A Δ(B) ⇒ C↓L Δ([_{n}Γ, A↓B]) ⇒ C  [_{n}A, Γ] ⇒ B↓R Γ ⇒ A↓B

b. Γ ⇒ A Δ(B) ⇒ C↑L Δ([_{n}B↑A, Γ]) ⇒ C  [_{n}Γ, A] ⇒ B↑R Γ ⇒ B↑A

c. Γ([_{n}A, B]) ⇒ C⊙L Γ(A⊙B) ⇒ C  Γ ⇒ A Δ ⇒ B⊙R [_{n}Γ, Δ] ⇒ A⊙B

Appendix: Generalisation

For generalisation to multiple wrapping we add to the associative binary product and implications n-ary splitting and wrapping multiplicatives for each n ≥ 2 (cf. Buszkowski 1988 for such n-ary generalisations):

F = A | F\F | F/F | F•F | •_{N}(F_{1}, …, F_{n}) | ; →_{N} (F_{1}, …, F_{n})_{i}, i ≤ n | •_{W} (F_{1}, …, F_{n}) | →_{W} ; (F_{1}, …, F_{n})_{i}, i ≤ n ; (124)

Prosodic interpretation is in a monoid with n-ary splitting and wrapping adjunctions for each n ≥ 2:

{(L^{∗}, +, ϵ, \{N_{n}\}_{n∈\{2,3,...\}}, \{W_{n}\}_{n∈\{2,3,...\}}) \atop (125)}

There are the following axioms:

{s_{1} + (s_{2} + s_{3}) = (s_{1} + s_{2}) + s_{3} \atop W_{n}(N_{n}(s_{1}, …, s_{n}), s′_{2}, …, s′_{n}) = s_{1} + s′_{2} + … + s′_{n} + s_{n}} ; (126)

Interpretation is a subsets of L = L^{∗} − {ϵ} by n-ary generalisation of residuation:

\begin{aligned}D(B/A) & = & \{s|∀s′ ∈ D(A), s + s′ ∈ D(B)\} \\ D(A\B) & = & \{s|∀s′ ∈ D(A), s′ + s ∈ D(B)\} \\ D(A•B) & = & \{s_{1} + s_{2}|s_{1} ∈ D(A) ∧ s_{2} ∈ D(B)\} \\ D(•_{N}(A_{1}, …, A_{n})) & = & \{N_{n}(s_{1}, …, s_{n})|s_{1} ∈ D(A_{1}) ∧ … ∧ s_{n} ∈ D(A_{n})\} \\ D(→_{N} (A_{1}, …, A_{n})_{i}) & = & \{s|∀s_{1} ∈ D(A_{1}), …, s_{i−1} ∈ D(A_{i−1}), \\ & & s_{i+1} ∈ D(A_{i+1}), …, s_{n} ∈ D(A_{n}), \\ & & N_{n}(s_{1}, …, s_{i−1}, s, s_{i+1}, …, s_{n}) ∈ D(A_{i})\} \\ D(•_{W} (A_{1}, …, A_{n})) & = & \{W_{n}(s_{1}, …, s_{n})|s_{1} ∈ D(A_{1}) ∧ … ∧ s_{n} ∈ D(A_{n})\} \\ D(→_{W} (A_{1}, …, A_{n})_{i}) & = & \{s|∀s_{1} ∈ D(A_{1}), …, s_{i−1} ∈ D(A_{i−1}), \\ & & s_{i+1} ∈ D(A_{i+1}), …, s_{n} ∈ D(A_{n}), \\ & & W_{n}(s_{1}, …, s_{i−1}, s, s_{i+1}, …, s_{n}) ∈ D(A_{i})\} \end{aligned} ; (127)