A Deductive Calculus of Categories and Transformations

Thomas L. Cornell^{∗} University of Tübingen Seminar für Sprachwissenschaft

           cornell@sfs.nphil.uni-tuebingen.de

March 10, 1998

1 Introduction

Many researchers in the past few years have remarked on the apparent relation between ideas from Chomsky’s minimalist program (Chomsky 1995) and fundamental ideas in categorial grammar.^{1} In this paper we investigate this connection in some detail. We present a formalization of some ideas from Chomsky (1995) in the framework of multimodal type logical grammar (e.g., Morrill 1994, Moortgat 1996, and refs.). This project is in many respects rather straightforward, but makes use of aspects of the type logical machinery which are generally not used, or at least not used for these purposes, in categorial grammar. This allows us to investigate to some degree the relation between analyses of extraction phenomena based on hypothetical reasoning—the classical categorial approach—and those based on movement, seen here as a complex of structural rules. Besides these concerns relating different frameworks we can also use these techniques to deal with theory internal questions. In this paper we will use this framework to investigate some questions that have dogged transformational grammar since the introduction of trace theory in the early 1970s. In particular, we investigate the relations between derivational and representational means for expressing properties of syntactic structures and observe, via the well-known Curry-Howard correspondence between proofs and terms, an extremely tight connection between chain-based approaches—especially as developed in recent work by Brody (see esp. Brody 1997)—and movement based approaches such as that of Chomsky (1995).

∗This paper began life as an extended version of the handout for a talk presented at the Formal Grammar conference in Aix-en-Provence on August 10, 1997. A preconference proceedings paper is available as Cornell (1997). However, very many improvements have been made since then. This research in all its phases has benefitted tremendously from the help of many people, in particular Dick Oehrle, Michael Moortgat, Ed Stabler and Uwe Mönnich. Much is due to them, but the errors that remain are all my own.

1See especially Stabler (forthcoming), but also Berwick and Epstein (1995), and Lecomte (1997) address these issues as well.

1.1 Features and Formulas

The main feature of minimalist derivations which has suggested a connection with categorial grammar is the treatment of feature checking in Chomsky (1995), which is very reminiscent of the basic cancellation rules of categorial grammar. Consider the following instance of a L\ rule, a “rule of use” in a Gentzen style presentation of a Lambek calculus.

\begin{aligned}K ⊢ K V ⊢ V \\ & L\ \\ (K, K\V) ⊢ V \end{aligned}  (1)

Suppose we interpret K as the case feature of a DP, and the structure (K, K\V) to be a checking configuration. Then this instance of a L\ rule corresponds fairly closely to the minimalist idea that an expression marked with a case feature can cancel that feature in a checking configuration (e.g., the specifier position) with a head marked with the same feature. In effect, then, the axiom K ⊢ K marks the feature as cancelled.

Chomsky’s principle of Last Resort, though it appears in several forms in Chomsky (1995), essentially amounts to the following once a theory of feature checking is in place.

Transformational derivations should be driven by the need to check features.

In a deductive setting, with feature checking implemented along the lines sketched above, this means neither more nor less than that:

Proofs are driven by the need to reduce a theorem to axioms.

so this key idea of the minimalist program would receive a purely formal explanation in a deductive setting. Seen in this light, certain aspects of minimalist machinery may appear as special cases of more general mechanisms with a broader foundation in mathematics and logic. It should benefit current syntactic theorizing to know to what extent the theory of syntax can call upon well established techniques and results, the better to isolate what makes the formal system of grammar special.

The L\ rule exemplified above is just a directional variant of a rule essentially corresponding to Modus Ponens (“Given A and the implication A ⇒ B, conclude B,”) and so common to a great many deductive systems. What sets categorial grammar style deduction apart in this universe is its strict attention to the way in which deductions consume resources. In particular, an assumption once used cannot normally be used again; a feature once cancelled remains cancelled, in effect. This attention to the consumption of resources adds another dimension to the sense in which notions of economy are critical to the minimalist program.

This idea of resource sensitivity can be made precise by comparing the following two variants of a rule for drawing conclusions of the form “A and B.”

\begin{aligned}Γ ⊢ A Γ′ ⊢ B \\ & R× \\ Γ, Γ′ ⊢ A × B \end{aligned}  \begin{aligned}Γ ⊢ A Γ ⊢ B \\ & R⊓ \\ Γ ⊢ A ⊓ B \end{aligned}  (2)

In the R× rule, we must divide up our antecedent hypotheses into those which we will use to prove A and those which we will use to prove B. In the R⊓ rule, we need not do this. Later on we will simply throw away any elements of Γ which we do not need; in the meantime we are free to use the same assumption to prove both A and B, if that is useful.

In linear logic (Girard 1987, Troelstra 1992), one systematically splits the familiar logical connectives like conjunction in just this way, into a “multiplicative” variant, like our ×, and an “additive” variant, like our ⊓. In this context, the very resource conscious logics of categorial grammar can be seen as implementing a multiplicative fragment of linear logic.

In contrast to derivations in categorial grammar, the features which drive minimalist transformational derivations are often subcategorial, “morphological” features like Case or Wh. Typically, lexical items must be assigned to multiple types, but in implementing the minimalist approach to features and derivations they must be assigned to multiple types in a resource sensitive manner. So we are led to conclude that,

Subcategorial features can be resources, too.

at least insofar as they drive derivations.

Accordingly, we allow mulitplicative product types in our lexicon. For example, a Wh determiner like which, needing case and selecting a noun type complement might be represented with a formula like

(D • K • W)/N,  (3)

where we use K for Case and W for Wh. (We treat • as right branching by default, so as to avoid unnecessary parentheses.) This formula represents a function which takes an argument of type N and returns a value whose type is given by the tuple of features D • K • W, the type of elements which have all three characteristics, but where those characteristics may have effects on different parts of the syntax.^{2}

Just as in categorial grammar the local combinatorial potential of phrases is given in advance by the type of the lexical head, so in this system the movement potential of a phrase (i.e., its nonlocal combinatorial potential) is given in advance by the type of its head. For example, the WhP headed by which, given the type assignment in (3), will have to occupy three possibly distinct syntactic positions in order to cancel its three “chain” features.

2Other approaches to multiple type assignment, such as Bayer and Johnson (1995) do so in an essentially additive manner, so that extra features can be thrown away. Heylen (1997) uses unary modal operators to implement features, but again in such a way that extra features can simply be disregarded. The problems these authors address are common to all frameworks, and so we cannot ignore the necessity of some resource insensitive treatment of features. Clearly both treatments can coexist, but we cannot at this point offer any systematic or predictive theory of how they do so.

Roughly: ‘/’ and ‘\’ say how to build phrases, ‘•’ says how to build chains.

In this sense, the approach to features in the minimalist program represents a sort of extension to the approach to features in categorial grammar. One can be more concrete: for Chomsky, the operation Merge is cost-free, but it is subject to some sort of selectional/thematic restrictions which are extra syntactical. For categorial grammarians, the main focus is on (categorial) selection properties of heads: selection features are in an interesting sense logically dual to the notion of syntactic category. Avoiding an argument—for the moment at least—over who gets to be Syntax, we can see here an interesting complementarity of focus: on selection and local grammatical relationships on the part of categorial grammar and on extraction and nonlocal grammatical relationships on the part of the minimalist program. It now appears that both a categorial theory of selection and a minimalist theory of movement can live together within the same logical framework, which we will try to develop in some detail in this paper.^{3}

This complementarity of focus is already knitted together to a considerable degree in the work of Michael Brody. Brody develops a theory of chains in which the root position (the deepest chain position) is constrained to be the sole position at which a number of properties including selection can hold (and refs. Brody 1995a, 1997). (This is the Generalized Projection Principle of Brody (1997).) Chomsky, on the other hand, has his theory of feature-driven derivation explicitly given as primarily a theory of the relation between specifically nonroot chain positions and functional categories.

1.2 Numerations and Sequents

As presented in Chomsky (1995), a derivation proceeds from an initially given numeration, which is supposed to be a multiset of lexical item occurrences. Lexical elements are withdrawn from the numeration and subjected to the action of a pair of generalized transformations, Merge and Move, which transform the raw lexical resources of the numeration into an LF representation, delivering an intermediate representation for PF spell-out along the way. The operation of Select forms syntactic objects from numeration items and the operations of Merge and Move form new syntactic objects from old. We observe that there is in fact no formal difference between the numeration and the set of syntactic items: both are multisets, in particular, so for the purposes of this paper we will not distinguish between these two structures, using the term “numeration” indiscriminately for both. At the same time, we do away with the Select operation.

3In this we are essentially following Stabler (1997b,a, forthcoming), who incorporates a theory of selection based on Koopman (1994) in his algebraic formalization of minimalist derivations.

In the setting of a grammar logic we want the lexical item instances to be type formulas, and we want to isolate in particular collections of such lexical formulas which can be combined to form sentences. We represent the fundamental decision problem of a grammar logic as the question of whether or not a sequent of the form

lexical resources ⊢ sentence-category

is derivable.

Grafting minimalist ideas into this setting seems fairly natural: we are interested in sequents of the form

Numeration ⊢ C

where C (complementizer) is the sentence category.

1.3 Checking Configurations

Chomsky (1995) defines the checking domain of a head in such a way that it includes all head-internal positions and specifier positions, and it excludes the complement position, which becomes the attraction domain. The flow of movement is then from the attraction domain and into the checking domain.

Chomsky (1995) lacks a theory of selection. To a point one can imagine categorial grammar as providing a theory of selection and the minimalist program as providing a theory of attraction. We wish to combine both theories here, to obtain a theory which is more uniformly resource conscious. So here even the complement position will be a checking position, but only for selection features. Note however that we will not trouble ourselves much here over the distinction between features belonging to these two systems, except to suggest along the way how it could be done.

As we will see, the standard L/ and L\ rules of the Lambek calculus require that the functor and its argument be sisters in the sequent antecedent. In minimalist syntactic structures, on the other hand, in the typical case of the Spec-Head configuration and even—following head movement—in some cases of the Complement-Head configuration as well cancelling pairs of features are not in a sisterhood configuration. That is, there is a mismatch between the definition of checking configuration in the minimalist program and the definition of the equivalent notion in proof theory. Moortgat and Oehrle (1997) offer two sorts of solutions for this sort of problem: “structural normalization” and “structural transparency”. The former adds controlled structural rules so as to allow the relevant resources to be placed into the canonical sister configuration; the latter allows intervening structure to be ignored in the relevant cases. Here we use the former approach: once the generalized transformation Move has acted to place features in checking configurations, a further suite of structural rules allows the feature to be cancelled to move into position as a sister of the cancelling functor. We think of this extra set of structural rules as providing a definition of minimalist checking configuration in terms of the more local configurations which are more convenient to proof theory.

2 The Grammar Logic

We introduce the logic which implements the ideas of section 1 in two pieces. In modern proof theory it is quite common to separate the inference rules of a logic into two components: the “logical” or “connective” rules and the “structural” rules. The logical rules are the rules which implement the definitions of the logical operators, that is, which assure us that a conjunction operator behaves like conjunction, an implication operator like implication and so forth. Structural rules deal with the relations among formulas, in ignorance of the logical connectives from which those formulas are built. For example, the rule of Exchange allows us to take a pair of formulas (A, B) and proceed with the proof by replacing that pair with the permuted pair (B, A). Whether A is a conjunction or an implication or whatever makes no difference to the applicability of Exchange. For example, the calculus presented in Lambek (1961) has the same connectives as the calculus presented in Lambek (1958), but it is a different logic because it lacks the structural rule of Associativity.

In a fairly natural sense, the nonassociative Lambek calculus NL of Lambek (1961) is the minimal grammar logic, in that it contains no structural rules at all. We will lay out its logical inference rules in the next subsection but consider for now one of these rules, called L• because it tells us how to proceed with a proof search when we encounter a formula with a • connective on the left of the ⊢ symbol. (Here the notation Δ[X] means a collection of formulas in which there is a distinguished occurrence of X; subsequent use of Δ[Y] should be taken to mean the same structure but with Y in place of that occurrence of X.)

\begin{aligned}Δ[(A, B)] ⊢ C \\ & L• \\ Δ[A • B] ⊢ C \end{aligned}  (4)

We eliminate an occurrence of • in this rule, but we introduce at the same time a pair of parentheses. Without Associativity, the sequent D, (A, B) is not at all the same as the sequent (D, A), B, so we have to keep track of the associations between our formulas. In effect our sequents are no longer made out of simple sequences of formulas (the notion of “sequence” being inherently associative) but rather out of trees of formulas, and a sequent is a pair consising of a tree on the one hand and a formula on the other.

A significant recent innovation in this family of rather weak logics has been the development of multimodal grammar logics (see Moortgat 1996, for an overview). In these logics we can have more than one product operator, and so more than one kind of slash as well. In addition one can have “product” operators which are not binary. By far the most common extension in this direction has been the use of unary modal operators. The key to allowing these various different “modes of grammatical composition” to live together in a single sound and complete logic is to label the parentheses introduced by the various L•_{i} rules (and L◇_{i} rules for the “unary products”) with an indication of which product introduced them. For example:

\begin{aligned}Δ[(A, B)^{i}] ⊢ C \\ & L•_{i} \\ Δ[A •_{i} B] ⊢ C \end{aligned}  (5)

or the following:

\begin{aligned}Δ[⟨A⟩^{i}] ⊢ C \\ & L◇_{i} \\ Δ[◇_{i}A] ⊢ C \end{aligned}  (6)

Then the rules governing the corresponding residuals require that the active formulas be associated with the correct brackets. For example:

\begin{aligned}Γ ⊢ A Δ[B] ⊢ C \\ & L\_{i} \\ Δ[(Γ, A\_{i}B)^{i}] ⊢ C \end{aligned}  \begin{aligned}(A, Δ)^{i} ⊢ B \\ & R\_{i} \\ Δ ⊢ A\_{i}B \end{aligned}  (7)

In effect we have several different sorts of functions (depending on the number of products, i.e., the number of subscripts) and corresponding to this we have several different sorts of function application. Now a function of a certain sort can only be applied to an argument if it is applied in the right way. We can do nothing with a configuration of the form (A, A\_{i}B)^{j}, for example.

Given such labeled trees of formulas, one can write structural rules which relate them. For example, a subtree of the form ⟨Δ⟩^{1} might be allowed to permute with another subtree where permutation was barred for all other structures. Or to consider our previous example, we might in certain circumstances be able to convert a j type application to an i type application, allowing us to use a configuration like (A, A\_{i}B)^{j} after all. Our implementations of Chomsky’s Merge and Move will be constructed out of precisely such modally controlled packages of structural rules, which we will describe in section 2.2, after we introduce the basic logic.

2.1 Connectives of the Grammar Logic and Their Inference Rules

Formally, the language of our logic is defined as follows. (This is an utterly standard definition and we present it rather tersely here. The interested reader is refered to Moortgat (1996) for a more detailed treatment.) We assume given a set of basic type symbols Basic. We define the well-formed type formulas with the following little grammar.

F ⟶ Basic | F •_{i} F | F\_{i}F | F/_{i}F | ◇_{i}F | □_{i}^{↓}F  (8)

We refer to \_{i} and /_{i} as the (left and right) residuals of •_{i}, and to □_{i}^{↓} as the residual of ◇_{i}. They are required to obey the following residuation laws.

B ⊢ A\_{i}C ⟷ A •_{i} B ⊢ C ⟷ A ⊢ C/_{i}B  (9)
◇_{i}A ⊢ B ⟷ A ⊢ □_{i}^{↓}B  (10)

Here the i are taken to range over some index set, but in practice we will often substitute different symbols for the different •_{i}. For example we might write •_{0} as ⊗ and /_{0} as /_{⊗}.

From formulas in F we construct structured configurations of formulas (sometimes called “structured databases of resources”) as follows.

S ⟶ F | (S, S)^{i} | ⟨S⟩^{i}  (11)

A sequent here will be a pair consisting of a configuration and a formula, written S ⊢ F. Inference rules will then be templates with one or two upper sequents (“premises”) and one goal sequent (“conclusion”), and proofs will be trees labeled with sequents all of whose local trees are instances of inference rules or else (at the leaves) of axiom schemata.

We will present our inference rules and proofs in the style of a Gentzen sequent calculus. This means that every connective will have a “left rule” and “right rule” for dealing with sequents in which that connective appears either to the left or right of the ⊢ symbol. The Gentzen system was originally developed because it makes searching for a proof of a given sequent much easier than a Hilbert system or a Natural Deduction system. Because of this emphasis on proof search, rather than proof per se, we typically read Gentzen inferences from the bottom up, even though logically the direction of inference is from the top down. So, for example, we tend to think of the L•_{i} rule as telling us what to do when a •_{i} appears on the left in the goal sequent, though logically it is telling us under what structural conditions in the premises we can infer a L•_{i} on the left in the conclusion. The left and right rules are sometimes referred to as “rules of use” and “rules of proof”, respectively. The left rule L•_{i} tells us under what structural conditions we can use a •_{i} to prove a consequent, and the right rule R•_{i} tells us under what structural conditions we can prove a consequent with a •_{i} as its main connective.

The logical inference rules for constructing derivations over such formulas are given in figure 1. Note that, read bottom up, each rule (other than the Cut rule) removes a logical operation from the sequent to be proved, so at each step the problem of finding a proof gets strictly smaller. We chose this format here because in addition to making it easier to construct proofs it also makes much clearer the role which the structure of antecedent formulas plays in the proof. As a result, again reading bottom up in the direction of proof search rather than of inference, Gentzen style proofs will be seen to look very similar to minimalist derivations (see section 3).

So far we have presented the logic completely abstractly, without regard for the inventory of connectives we will actually need. The considerations of section 1 lead us to adopt a basic language with the product connectives in table 1. Keep in mind that these are just convenient symbols for the “official” •_{i} notation, so (a) they all have residuals and (b) the rules of figure 1 apply to all of them and to all of their residuals.

In fact, however, though we will make use of all of these products, we will make use of the residuals of only • and ◇_{0}. That is, the logic allows us to reason

A ⊢ A Axiom  \begin{aligned}Γ ⊢ A Δ[A] ⊢ B \\ & Cut \\ Δ[Γ] ⊢ B \end{aligned}  (12)
\begin{aligned}Γ ⊢ A Δ[B] ⊢ C \\ & L/_{i} \\ Δ[(B/_{i}A, Γ)^{i}] ⊢ C \end{aligned}  \begin{aligned}(Δ, A)^{i} ⊢ B \\ & R/_{i} \\ Δ ⊢ B/_{i}A \end{aligned}  (13)
\begin{aligned}Γ ⊢ A Δ[B] ⊢ C \\ & L\_{i} \\ Δ[(Γ, A\_{i}B)^{i}] ⊢ C \end{aligned}  \begin{aligned}(A, Δ)^{i} ⊢ B \\ & R\_{i} \\ Δ ⊢ A\_{i}B \end{aligned}  (14)
\begin{aligned}Δ[(A, B)^{i}] ⊢ C \\ & L•_{i} \\ Δ[A •_{i} B] ⊢ C \end{aligned}  \begin{aligned}Δ_{1} ⊢ A Δ_{2} ⊢ B \\ & R•_{i} \\ (Δ_{1}, Δ_{2})^{i} ⊢ A •_{i} B \end{aligned}  (15)
\begin{aligned}Γ[A] ⊢ B \\ & L□_{i}^{↓} \\ Γ[(□_{i}^{↓}A)^{i}] ⊢ B \end{aligned}  \begin{aligned}(Γ)^{i} ⊢ A \\ & R□_{i}^{↓} \\ Γ ⊢ □_{i}^{↓}A \end{aligned}  (16)
\begin{aligned}Γ[(A)^{i}] ⊢ B \\ & L◇_{i} \\ Γ[◇_{i}A] ⊢ B \end{aligned}  \begin{aligned}Γ ⊢ A \\ & R◇_{i} \\ (Γ)^{i} ⊢ ◇_{i}A \end{aligned}  (17)

Figure 1: Logical rules for a general multimodal type logic.

⊗ — The numeration forming operator.
• — The lexical product.
◇_{0} — For feature checking.
◇_{1} — For implementing Move.
<, ⊳ — Complement and specifier attachment products.

Table 1: Connectives of the Grammar Logic. about and calculate with the full range of connectives, but we will be interested only in lexical type formulas, that is, type formulas assigned to lexical items, and in our minimalist lexicons only the residuals of • (written simply \ and /) and of ◇_{0} (written □_{0}^{↓}) will appear. (The unary modal ◇_{1} will also appear, but not its residual.) No rule introduces a connective into a premise, so in general our formulas will be restricted to connectives appearing in the lexicon. The extra products will appear only as labels on structured configurations, and will be put there by structural rules, considered in the next section. It is important to keep in mind that this system is investigated here as a useful device for doing scientific calculations and not as a set of formal universals expressing a theory of Universal Grammar. No special claims are being made here about formal properties of UG. Indeed, any attempt to stipulatively restrict allowable proofs to use only left rules would destroy any chance at completeness for the logic and we would also lose the ability to construct proofs which will be very useful to us below. We will see when we consider the relation of transformational derivations to categorial derivations in section 5 that we can make very good use of the fact that our derivations are embedded in a full grammar logic.

2.2 Packages of Structural Rules

As far as the rules in (12)–(17) are concerned, any binary product is like any other binary product and so also for unary products and all associated residual operators. It is in their access to structural rules that the different connectives differ in more than just typography. We discuss briefly here what we intend for all of these connectives, and then present the actual packages of structural rules which implement these intentions.

Numerations are meant to be multisets, that is, the only thing that matters is the number of times a given structure occurs. Order and hierarchy are irrelevant there. Accordingly, we want the numeration forming product ⊗ (and its corresponding “comma”, (·, ·)^{⊗}) to allow freely the permutation and reassociation of its arguments. Because of this, there is no real need to write the parentheses in a structure built up in the ⊗ mode, and the order of formulas is a strictly typographical necessity. Accordingly, we will use a “sugared notation” for the corresponding resource structures. That is, we use unbracketed commas to concretely present the numeration part of a sequent, writing A, B ⊢ C, rather than (A, B)^{⊗} ⊢ C. For example, the antecedent of the sequent A, B, (C, D)^{<} ⊢ E is a numeration with 3 elements: two formulas and the tree (C, D)^{<}. Unbracketed substructures are granted free access to permutation and association rules, making numerations behave as multisets, as in Chomsky (1995).

For our purposes the most important connectives are • and its residuals \ and /. These are the connectives which glue features together in lexical items, and they govern the projection of lexical properties into the syntax. This introduces a few special technical problems which have to be dealt with. Formally, the rule cancelling a feature A against a head marked B/A can only take place in a structure with the bracketing (B/A, A)^{•}, because / is the residual of •. The configuration (B/A, A)^{•} is, then, the checking configuration which we get, for free, from the logic of residuation. From Chomsky (1995), however, we already have a notion of checking configuration given to us. For example—and indeed this is taken as the paradigm example—the specifier-head configuration is a checking configuration for formal features. In our language we could represent such configurations as resource structures (A, (A\B, C)^{<})^{⊳} . This is not the configuration we want, on two counts: first it is structurally wrong, in that the functor and its argument are not structurally adjacent, and second it is mistyped, since \ is neither the residual of ⊳ nor of <. Formally, the notion of residuation gives us a primitive, mathematically elegant basis for investigating feature cancellation, but we still have to say explicitly, in these terms, what we mean a checking configuration in natural language syntax to be. It is for this reason that we provide the unary modal ◇_{0}. This will allow us to say exactly what we mean by a checking configuration (see below, in section 2.2.4), in a way which can change as we gain new empirical insights without changing the underlying mathematical basis of our calculational machinery. Looking ahead, ◇_{0} will give features access to restricted forms of associativity and permutation, which will allow them to move about the resource structure to find the head in whose checking domain they are. In this sense feature cancellation is very much like movement, and in particular it may help to clarify the intuition that, if it weren’t for the externally imposed necessity to pied pipe elaborate interface structures, then feature cancellation would just be head movement (as it is supposed to be in covert cases). The relation between ◇_{0} and ◇_{1}, which licenses access to movement rules, will be laid out in section 2.2.3.

The notation for the last two “tree-building” products ⊳ and < is derived from the algebraic systems for minimalist derivations of Stabler (Stabler 1997b,a, forthcoming). They can be thought of as headed operators, which point in the direction of the head, so that a structure written (α < β) would correspond to the structure, written Chomsky-style as {α, {α, β}}, in which α and β were merged with α projecting over β.

2.2.1 The Numeration Package

We have already noted that the numeration forming product ⊗ is associative and commutative. Formally we have the following rules. (The double line in rule ⊗A means that the inference can go in either direction.)

\begin{aligned}Γ[(Δ_{1}, Δ_{2})^{⊗}] ⊢ A \\ & ⊗P \\ Γ[(Δ_{2}, Δ_{1})^{⊗}] ⊢ A \end{aligned}  (18)

Γ[(Δ_{1}, (Δ_{2}, Δ_{3})^{⊗})^{⊗}] ⊢ A

⊗A

Γ[((Δ_{1}, Δ_{2})^{⊗}, Δ_{3})^{⊗}] ⊢ A (19)

As noted above, we will use a syntactically sugared presentation of these structures and just as we will typically not bother to write the parentheses we will also typically not mention the implicit application of these rules, except where confusion may arise.

The rules ⊗P and ⊗A have a special feature: ⊗, or rather its associated configuration-forming comma and brackets, is the only connective which appears. Many of the structural rules to be introduced in the following subsections involve several products at a time, in one of two ways. Some rules simply allow us to convert one product to another. Logically, this represents the claim that the individuals constructed with the first product form a subset of the individuals constructed with the second. The most important rules from the standpoint of transformational grammar, however, are the rules which govern the interaction of several products. We will see many examples of these inclusion and interaction rules in what follows.^{4}

2.2.2 Merge Package

Our next example is only slightly more complex: the generalized transformation Merge. The essential idea is that Merge takes a pair of resources which are more or less free-floating in the numeration and freezes them in a structure in which their sequential and hierarchichal positions are fixed.

\begin{aligned}Γ, (Δ_{1}, Δ_{2})^{<} ⊢ A \\ & Mg1 \\ Γ, Δ_{1}, Δ_{2} ⊢ A \end{aligned}  (20)

\begin{aligned}Γ, (Δ_{2}, Δ_{1})^{⊳} ⊢ A \\ & Mg2 \\ Γ, Δ_{2}, Δ_{1} ⊢ A \end{aligned}  (21)

Rule Mg1 corresponds to the attachment of a complment and Mg2 to the attachment of a specifier. Which rule we use depends on features of the head (Δ_{1} in both cases): if Δ_{1} is a formula of the form B/A, then Mg1 applies. Otherwise Mg2 applies. We require in addition that the Δ_{i} not contain any instances of ⊗ formulas or ⊗ structures. Intuitively, we should only be able to merge structures which were themselves built up by Merge. We can impose this condition by considering Mg2 to depict a family of rules in which Δ_{1} is given either as a formula other than B/A or A ⊗ B, or a structural configuration annotated with

\begin{aligned}& Axiom \\ A ⊗ (B ⊗ C) ⊢ ((A ⊗ B) ⊗ C) \end{aligned} ⋮ ; Γ[((A ⊗ B) ⊗ C)] ⊢ D

Cut Γ[A ⊗ (B ⊗ C)] ⊢ D

4Note that, logically, all of these structural rules are postulates, that is, new axiom schemata. We can convert such postulates into inference rules by “compiling in a Cut” as follows. Suppose we have the postulate

A ⊗ (B ⊗ C) ⟶ (A ⊗ B) ⊗ C Then subproofs of the following form are always possible.

Essentially the same technique allows us to generalize to resource structures of the form ((Δ_{1}, Δ_{2})^{⊗}, Δ_{3})^{⊗} in place of ((A ⊗ B) ⊗ C), for example, giving us the form of the inference rule as it is presented here.

a product other than ⊗. Because such products cannot be introduced except by converting a ⊗ product, a simple induction shows that such an approach does indeed implement this side condition in the logic. Such an approach is cleaner because we actually can prove theorems in which ⊗ configurations do appear embedded in, say, < configurations, but only when the theorem is of that form to start with. We are only assured that when the antecedent of the theorem is a numeration, i.e., a pure ⊗-structure of lexical type formulas, then our side condition above is guaranteed to hold.^{5}

2.2.3 Move (XP) Package

This package implements XP movement, and can be used to implement a very restricted form of head movement.^{6} Out approach implements a technique which is quite often used in applications of multimodal calculi to linguistic problems. The basic idea is to observe first that the sequent ◇_{i}□_{i}^{↓}A ⊢ A is valid, for all formulas A in F.

\begin{aligned}A ⊢ A \\ & L□_{i}^{↓} \\ ⟨□_{i}^{↓}A⟩^{i} ⊢ A \end{aligned} ; L◇_{i} ; ◇_{i}□_{i}^{↓}A ⊢ A  (22)

Now suppose we have some structural rules which are sensitive to the presence of these ⟨·⟩^{i} structures, for example the following.

\begin{matrix}Γ[(Δ_{1}, ⟨Δ_{2}⟩^{i})^{j}] ⊢ A \\ Γ[(⟨Δ_{2}⟩^{i}, Δ_{1})^{j}] ⊢ A \end{matrix}  (23)

If we provide a feature B in the lexicon with the prefix “◇_{i}□_{i}^{↓}”, then we have in effect given it a license to permute, after which the diamond that allowed permutation is removed and the position of the feature is fixed. Given such a rule the sequent

(A\_{j}B, ◇_{i}□_{i}^{↓}A)^{j} ⊢ B

is valid but

(A\_{j}B, A)^{j} ⊢ B

is not valid, nor is

(A\_{j}B, ◇_{i}□_{i}^{↓}A)^{k≠j} ⊢ B.

5Such a move would allow us to investigate, for example, grammars in which completely nonconfigurational domains could be embedded in much more rigid structures. Such an investigation could then be carried out in a uniform framework in which the rest of the implementations of minimalist ideas were left intact and only this one condition allowed to vary.

6We will see examples of this in section 3. Basically, we will only be able to move heads when they are linearly adjacent to their targets. This may be good enough, since cancelled material does not count for adjacency. We discuss head movement on its own in some detail in Cornell (1997).

The unary operator ◇_{1} licenses access to this package, so all moveable lexical material must be marked with the ◇_{1} in the lexicon. If we think of a lexical formula like (D•K•W)/N as denoting a function from N’s to (D•K•W) chains, and in general if we think of products in the lexicon as indicating that an item may have an effect on several different points of syntactic structure, then clearly we want the chain portion of this formula to be given access to the movement package: ◇_{1}(D•K•W)/N. But we have also to provide the lexical item with the means to stop moving. Since each feature can stop at a different point, we place a box operator before each individual feature: ◇_{1}(□_{1}^{↓}D • □_{1}^{↓}K • □_{1}^{↓}W)/N. This would be enough if movement always placed features right next to the heads they cancel against. Because we must say more about what structural positions are actually considered close enough to count as being “logically adjacent”, we will ultimately need our boxes to be the residuals of a different diamond, ◇_{0}, and we provide an inclusion rule which converts ◇_{1} to ◇_{0} when the derivation goes from a movement phase to a feature cancellation phase. So our final lexical formula for a Wh determiner like which will be: ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K • □_{0}^{↓}W)/N.

The main rules of this package which actually execute movement transformations are the rules Mv1–3 given below.

\begin{aligned}Γ[(⟨Δ_{2}⟩^{1}, Δ_{1})^{⊳} ] ⊢ A \\ & Mv1 \\ Γ[(Δ_{1}, ⟨Δ_{2}⟩^{1})^{<}] ⊢ A \end{aligned}  (24)

Rule Mv1 moves an entire complement expression, Δ_{2}, across a head Δ_{1} to specifier position.

Γ[(⟨Δ_{2}⟩^{1}, (Δ_{1}, Δ_{3})^{<})^{⊳} ] ⊢ A

Mv2 Γ[(Δ_{1}, (⟨Δ_{2}⟩^{1}, Δ_{3})^{⊳} )^{<}] ⊢ A (25)

Rule Mv2 moves only the specifier of a complement to the (lowest) specifier position of a governing head.

Γ[(⟨Δ_{2}⟩^{1}, (Δ_{1}, Δ_{3})^{⊳} )^{⊳} ] ⊢ A

Mv3 Γ[(Δ_{1}, (⟨Δ_{2}⟩^{1}, Δ_{3})^{⊳} )^{⊳} ] ⊢ A (26)

Rule Mv3 moves a phrase from a lower specifier position to a higher. Unlike the other movement rules, which can implement what we intuitively think of as entire movement steps, Mv3 does not correspond to any entire movement step in a derivation. Rather, it is used because we have no other way of stating that a moving expression may move across any number of intervening specifiers (as long as locality or economy conditions are satisfied, see below). For example, there is no other way for a moving phrase to reach the highest of multiple specifier positions without Mv3, nor is there any way for a moving phrase to escape from the domain of a head with another specifier. Absence of this rule would prevent an object Wh phrase from moving over the subject to reach the specifier of CP position, for example.

However, presence of this rule does permit multiple specifiers to appear in virtually any order. Some control over this situation can be recovered, if necessary, by appeal to the feature cancellation system (see below on movement extending a structure). As we are about to see, the feature cancellation process cannot start until an expression gives up its license to move.^{7}

\begin{aligned}Γ[(⟨Δ_{1}⟩^{1}, ⟨Δ_{2}⟩^{1})^{i}] ⊢ A \\ & K \\ Γ[⟨(Δ_{1}, Δ_{2})^{i}⟩^{1}] ⊢ A \end{aligned}  (27)

\begin{aligned}Γ[⟨Δ⟩^{0}] ⊢ A \\ & Mm \\ Γ[⟨Δ⟩^{1}] ⊢ A \end{aligned}  (28)

The final two rules in the package provide an exit from a movement subproof. The rule K is simply a rule of distributivity, which allows us in effect to peel a feature off of a larger complex of features. In particular, it allows us to peel off a feature which we intend to cancel in this position.^{8} Then rule Mm, a containment rule, says in effect that anything that has access to movement rules has access to cancellation rules as well, converting a structure ⟨Δ⟩^{1} to a structure ⟨Δ⟩^{0}.

Our system always restricts inference rules to act on very local configurations of resources. Long distance effects are obtained from the recursive structure of proofs, and by the corresponding iteration of a number of very local rules. As a result this system looks rather different in detail than a traditional transformational approach. For purposes of comparison, it is best not to think of the application of individual Mv rules as each implementing a movement step. Rather, an application of the generalized transformation Move corresponds to the entire subproof between the application of the first Mv rule to an expression to the application of the Mm rule, which switches the system from Move mode to feature cancellation mode.

Locality conditions may be placed as side conditions on these rules. For example, suppose we assume that (reading bottom up) a formula cannot cross another (c-commanding) formula with the same feature (with the same polarity). Nor can it move away from a head with an oppositely charged version of the same feature. Take for example Mv2, repeated below.

Γ[(⟨Δ_{2}⟩^{1}, (Δ_{1}, Δ_{3})^{<})^{⊳} ] ⊢ A

Mv2 Γ[(Δ_{1}, (⟨Δ_{2}⟩^{1}, Δ_{3})^{⊳} )^{<}] ⊢ A (29)

If Δ_{2} = A and Δ_{3} = A\B, for example, then the application of Mv2 should be blocked. In Mv3, if (the head of) Δ_{3} contains an oppositely charged version of a feature found in Δ_{2}, or Δ_{1} contains a similarly charged feature, then the application of the rule is blocked. In all these cases we would be violating Shortest Move, alias the Minimal Link Condition.

7Of course, placing a limit on the number of specifiers that can appear would allow us to write finitely many rules which would move expressions across sequences of specifiers.

However, if that bound were greater than 1, we would run afoul of the “Syntax can’t count”

doctrine.

8The name of this rule is traditional, stemming from classical modal logic. It should not be confused with our use of K as an abbreviation for a Case feature.

Also so far nothing has required that movement extend the structure, i.e., that all movement should be to the root. Here it is particularly important that we keep the notion of a Move step in a transformational derivation separate from the notion of the application of a Mv rule. Conditions on the target of Move should in general be translated as conditions on Mm, since this marks the end of a movement subproof. For example, if we rewrite Mm as a family of rules like the following

Γ[(Δ_{1}, (⟨Δ_{2}⟩^{0}, Δ_{3})^{⊳} )^{⊗}] ⊢ A

Mm′ Γ[(Δ_{1}, (⟨Δ_{2}⟩^{1}, Δ_{3})^{⊳} )^{⊗}] ⊢ A (30)

with variations for all the possible local configurations in which ⟨Δ_{2}⟩^{1} could appear, then we could prevent movement from halting prematurely. (Recall that ⊗ is the numeration forming connective, so this expression depicts the interface between a syntactic object and the collection of syntactic objects in the numeration.) Movement could still halt prematurely, but the feature(s) being moved could not ever cancel, since now Mm could not apply, and so no proof could ever be found that way.

There is one further feature of the Move package which deserves comment, but we postpone discussion until section 4: movement here leaves no traces. It actually destroys embedded structure in order to create new structure. The reason for this is straightforward. This is a calculus of syntactic features, and traces, being syntactically inert, have no syntactic (or rather, syntactically active) features. Nonetheless we have spoken frequently of tuples of features as being the types of chains, and we have not (knowingly) spoken this way irresponsibly. Again, the reader is referred to section 4, where we will discuss in some detail the formal relation between derivations and representations, and show how derivations as we have presented them here are mapped to “T-markers”, in which traces, indices and chains all appear in their familiar roles.

2.2.4 Feature Checking Package (“Micro-Movement”)

These rules act to break up a lexical product in one place, and form a new one in another. The c variants act to remove a feature from complement position, and the s variants act in the same way on specifiers. Note however that there can be multiple specifiers in Chomsky’s system, but only a single complement. So the rules which (read bottom up) move a feature from the specifier to the head are somewhat more complex than those moving a feature from the complement to the head.^{9}

9We have done nothing here to assure that only selectional requirements of a head can be satisfied in a complement configuration, that is, that the head-complement configuration is not a checking configuration for formal features. Probably the best way to do this would be to distinguish selectional and categorial features from formal and licensing features in the lexicon, by using either separate unary modalities or by splitting the • product in two. The increase in precision would be valuable, but we postpone its implementation for now.

Rules F 0c and F 0s handle the case where the feature to be cancelled is already adjacent to the feature it is to be cancelled against, so these take the form of embedding rules, but in a contextually restricted form.

\begin{aligned}Γ[(Δ_{1}, ⟨Δ_{2}⟩^{0})^{•}] ⊢ A \\ & F 0c \\ Γ[(Δ_{1}, ⟨Δ_{2}⟩^{0})^{<}] ⊢ A \end{aligned}  \begin{aligned}Γ[(⟨Δ_{1}⟩^{0}, Δ_{2})^{•}] ⊢ A \\ & F 0s \\ Γ[(⟨Δ_{1}⟩^{0}, Δ_{2})^{⊳} ] ⊢ A \end{aligned}  (31)

Rule F 1c acts in structurally similar circumstances to rule F 0c; the difference is that in this case the complement is a complex of features, from which we detach one (Δ_{2}). Rule F 1s is similar: it detaches Δ_{1} from a complex of features in specifier position but again, as in F 0s, a specifier of a head with no complements. (Recall that our system can’t see traces, so it is possible, after movement, to have a head with a specifier but no complement.) Note however that in this case the result is another specifier configuration, rather than a (·, ·)^{•} configuration. This is because the head could have several specifiers (and still no complement), and our feature has to work its way across all of them to find the head (at which point F 0s applies).

Γ[((Δ_{1}, ⟨Δ_{2}⟩^{0})^{•}, Δ_{3})^{<}] ⊢ A F 1c Γ[(Δ_{1}, (⟨Δ_{2}⟩^{0}, Δ_{3})^{•})^{<}] ⊢ A Γ[(Δ_{2}, (⟨Δ_{1}⟩^{0}, Δ_{3})^{⊳} )^{⊳} ] ⊢ A F 1s Γ[((⟨Δ_{1}⟩^{0}, Δ_{2})^{•}, Δ_{3})^{⊳} ] ⊢ A (32)

Rule F 2 handles moving across multiple intervening specifiers, and rule F 3 handles the cancelation of a feature originating in a specifier in the case where the head does have a complement.

Γ[(Δ_{2}, (⟨Δ_{1}⟩^{0}, Δ_{3})^{⊳} )^{⊳} ] ⊢ A

F 2 Γ[(⟨Δ_{1}⟩^{0}, (Δ_{2}, Δ_{3})^{⊳} )^{⊳} ] ⊢ A (33)

Γ[((⟨Δ_{1}⟩^{0}, Δ_{2})^{•}, Δ_{3})^{<}] ⊢ A

F 3 Γ[(⟨Δ_{1}⟩^{0}, (Δ_{2}, Δ_{3})^{<})^{⊳} ] ⊢ A (34)

3 (Minimalist) Derivation as Proof Search

In figure 2 we see a very simple example of some of this machinery at work. The derivation here is the trivial derivation which merges a D with a V that selects a D, canceling the categorial D feature against the selection feature of the V. In passing we note again that the minimalist program proper, as laid out in Chomsky (1995), does not include selection in the syntax. The conditions under which it is okay to merge a nominal complement with a predicate are offloaded to the interpretive components. Here we treat both systems together, noting only that both phenomena associated with the lowest chain position (e.g., selection) and phenomena associated with higher chain positions can be accommodated in a single residuation calculus with a single primary product (•), supported by a number of control modalities.

D ⊢ D V ⊢ V L/ (V/D, D)^{•} ⊢ V

L□_{0}^{↓}

(V/D, ⟨□_{0}^{↓}D⟩^{0})^{•} ⊢ V

F 0c

(V/D, ⟨□_{0}^{↓}D⟩^{0})^{<} ⊢ V

Mm

(V/D, ⟨□_{0}^{↓}D⟩^{1})^{<} ⊢ V

L◇_{1}

(V/D, ◇_{1}□_{0}^{↓}D)^{<} ⊢ V

Mg1

V/D, ◇_{1}□_{0}^{↓}D ⊢ V

Figure 2: An elementary derivation, cancelling one selection feature.

In the proof in figure 2, read bottom up as a proof-search, we could have equally well started with rule L◇_{1} and then afterwards used Mg1. The real action begins with the application of rule Mm. We decide that we have established a checking configuration (the head-complement configuration is certainly a checking configuration for selection features) and so we convert ⟨□_{0}^{↓}D⟩^{1} to ⟨□_{0}^{↓}D⟩^{0}.

At this point we have a formula to which we could apply L□_{0}^{↓}. However, if we did so we would be left with a configuration of resources (V/D, D)^{<}. Keep in mind that all of our slashes are shorthand for /_{•}, that is, they are the residuals of • , not of <. So this configuration does not allow the application of L/. We can, however, apply F 0c, which tells us that a single feature in a complement configuration can be considered adjacent to a functor for purposes of feature cancellation. Now that we have applied F 0c, it is safe to remove the protective wrapping from the D feature, leaving us with the configuration (V/D, D)^{•}, as desired. From there the proof is by the application of L/.

The dependencies between the various packages can be seen as follows. The Merge package gives us access to all of the Move package by converting numeration configurations into specifier or complement configurations; then the Move package—which applies trivially in figure 2—gives access to the Feature Cancellation package, which converts specifier and complement configurations into function application configurations and so finally gives access to the base logic of residuation.

In figure 3 we see a slightly more complex derivation, which includes a simple but not quite trivial instance of Move. Here we have a V which selects a D complement and assigns case to its specifier, together with a nominal with a categorial D feature and a K formal feature both of which must be canceled. The type formula ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K) is the type of a simple nominal A-chain.

The beginning of the proof search is similar to the one in figure 2. The main difference is that now our complement contains two features, so we have to do some extra work to peel off the D feature. This accounts for the two

D ⊢ D  \begin{aligned}K ⊢ K V ⊢ V \\ & L\ \\ (K, K\V)^{•} ⊢ V \end{aligned} ; L□_{0}^{↓} ; (⟨□_{0}^{↓}K⟩^{◇_{0}} , K\V)^{•} ⊢ V ; F 0s ; (⟨□_{0}^{↓}K⟩^{0}, K\V)^{⊳} ⊢ V ; Mm ; (⟨□_{0}^{↓}K⟩^{1}, K\V)^{⊳} ⊢ V ; Mv1 ; (K\V, ⟨□_{0}^{↓}K⟩^{1})^{<} ⊢ V

L/

(((K\V)/D, D)^{•}, ⟨□_{0}^{↓}K⟩^{1})^{<} ⊢ V

L□_{0}^{↓}

(((K\V)/D, ⟨□_{0}^{↓}D⟩^{0})^{•}, ⟨□_{0}^{↓}K⟩^{1})^{<} ⊢ V

F 1c

((K\V)/D, (⟨□_{0}^{↓}D⟩^{0}, ⟨□_{0}^{↓}K⟩^{1})^{•})^{<} ⊢ V

Mm

((K\V)/D, (⟨□_{0}^{↓}D⟩^{1}, ⟨□_{0}^{↓}K⟩^{1})^{•})^{<} ⊢ V

K

((K\V)/D, ⟨(□_{0}^{↓}D, □_{0}^{↓}K)^{•}⟩^{1})^{<} ⊢ V

L•

((K\V)/D, ⟨(□_{0}^{↓}D • □_{0}^{↓}K)⟩^{1})^{<} ⊢ V

L◇_{1}

((K\V)/D, ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K))^{<} ⊢ V

Mg1

(K\V)/D, ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K) ⊢ V

Figure 3: A slightly more complex derivation, canceling one selection feature and one formal feature. new steps—the applications of rules L• and K—that now intervene between the L◇_{1} and Mm steps. Also we now have to use F 1c rather than F 0c to feed the L/ rule that cancels the D feature.

We are then left with a verb which assigns case to its left (K\V), and a case-needing chain element (⟨□_{0}^{↓}K⟩^{1}) to its right. All we really need to do here is simply to permute the functor and its argument, but since we cannot allow the permutation rule P to apply indiscriminately we first have to check that the potential argument formula really is allowed to permute. This is indeed the case: the ⟨·⟩^{1} wrapper fits the requirements of the Mv1 rule on its output. The rest of the proof is similar to the cancellation of D feature, except that we move the K feature in from the left instead of from the right.

3.1 A More Elaborate Derivation

So far we have considered derivations in which we only ever have one instance of any given feature. The hard problems arise when we have more than one. For example, suppose we have two nominal expressions, both with type ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K). It is in principle always possible to use our proof machinery to break up such feature clusters into separately movable pieces, and there is always a danger that the pieces we free up in this way may attach to the wrong places (cf. Cornell 1997). A classic example would be the case where the external argument robs the accusative case of an active voice verb from the internal argument, which then has to raise to subject position to get case, creating in effect a passive structure based on an active voice verb.

In Chomsky (1995), the following structure is considered for ordinary transitive clauses (disregarding head movement, and assuming overt object raising), along with a variant in which the overt object outscopes the subject trace.

⊳
Subj  \begin{aligned}& < \\ Tns & \begin{aligned}& ⊳ \\ t_{Subj} & \begin{aligned}& ⊳ \\ Obj & \begin{aligned}& < \\ v & \begin{aligned}& < \\ V & & t_{Obj} \end{aligned} \end{aligned} \end{aligned} \end{aligned} \end{aligned}

Assuming that accusative case is assigned by the “light verb” v, we need

D ⊢ D V ⊢ V K ⊢ K \begin{matrix}D ⊢ D\begin{matrix}V ⊢ V \begin{matrix}K ⊢ K \begin{aligned}T ⊢ T \\ & L◇_{1}, Mm, L□_{0}^{↓} \\ ◇_{1}□_{0}^{↓}T ⊢ T \end{aligned} \\ F 0s, L□_{0}^{↓}, L\ \\ (⟨□_{0}^{↓}K⟩^{0}, K\◇_{1}□_{0}^{↓}T)^{⊳} ⊢ T \end{matrix} \\ L◇_{1}, Mm, F 0c, L□_{0}^{↓}, L/ \\ (⟨□_{0}^{↓}K⟩^{0}, ((K\◇_{1}□_{0}^{↓}T)/V, ◇_{1}□_{0}^{↓}V)^{<})^{⊳} ⊢ T \end{matrix} ; Mv2, Mm ; ((K\◇_{1}□_{0}^{↓}T)/V, (⟨□_{0}^{↓}K⟩^{1}, ◇_{1}□_{0}^{↓}V)^{⊳} )^{<} ⊢ T ; Mg1 ; Tns, (⟨□_{0}^{↓}K⟩^{1}, ◇_{1}□_{0}^{↓}V)^{⊳} ⊢ T \\ L◇_{1}, L•, K, Mm, F 1s, F 0s, L□_{0}^{↓}, L\ \\ Tns, (◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K), D\◇_{1}□_{0}^{↓}V)^{⊳} ⊢ T \end{matrix} Mg2 Tns, Subj, D\◇_{1}□_{0}^{↓}V ⊢ T F 0s, L□_{0}^{↓}, L\ Tns, Subj, (⟨□_{0}^{↓}K⟩^{0}, K\(D\◇_{1}□_{0}^{↓}V))^{⊳} ⊢ T L◇_{1}, Mm, F 0c, L□_{0}^{↓}, L/ Tns, Subj, (⟨□_{0}^{↓}K⟩^{0}, ((K\(D\◇_{1}□_{0}^{↓}V))/V, ◇_{1}□_{0}^{↓}V)^{<})^{⊳} ⊢ T Mv1, Mv2, Mm Tns, Subj, ((K\(D\◇_{1}□_{0}^{↓}V))/V, (◇_{1}□_{0}^{↓}V, ⟨□_{0}^{↓}K⟩^{1})^{<})^{<} ⊢ T Mg1 Tns, Subj, v, (◇_{1}□_{0}^{↓}V, ⟨□_{0}^{↓}K⟩^{1})^{<} ⊢ T

L◇_{1}, L•, K, Mm, F 1c, L□_{0}^{↓}, L/

Tns, Subj, v, (◇_{1}□_{0}^{↓}V/D, ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K))^{<} ⊢ T

Mg1
Tns, Subj, v, V, Obj ⊢ T

Figure 4: An abbreviated derivation with two DPs.

something like the following lexical assignments.

Tns ↦ (K\T)/V  (35)
v ↦ (K\(D\◇_{1}□_{0}^{↓}V))/V  (36)
V ↦ ◇_{1}□_{0}^{↓}V/D  (37)
Subj, Obj ↦ ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K)  (38)

The following is a theorem in our system. (The subscripts Subj and Obj have no status in our system. They are just here for readability.)

(K\T)/V, ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K)_{Subj}, (K\(D\(◇_{1}□_{0}^{↓}V)))/V,

(◇_{1}□_{0}^{↓}V)/D, ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K)_{Obj} ⊢ T (39)

A proof is given in figure 4. Note that we collapse entire sequences of rule applications where these do things we have already seen examples of. We employ here an abbreviatory convention according to which we use the lexical item in place of its type formula until the type formula is actually needed.

Observe that the first feature to be cancelled must be the D feature of one of the two DPs. Choosing the one marked “Obj”, that leaves us with the following goal sequent.

Tns, Subj, v, (◇_{1}□_{0}^{↓}V, ⟨□_{0}^{↓}K⟩^{1})^{<} ⊢ T  (40)

Note that we could at this point (after some permutations and reassociations) merge the subject formula with the tree we have built so far. That would put it closer to the light verb’s K feature, blocking movement of the object’s K feature. But the subject cannot cancel the the verb’s K feature itself: it has to discharge its D feature in order to “release” its K feature. So that move is blocked by the nonassociative and noncommutative nature of the • product. Instead we merge the current tree with the light verb.

Tns, Subj, ((K\(D\(◇_{1}□_{0}^{↓}V)))/V, (◇_{1}□_{0}^{↓}V, ⟨□_{0}^{↓}K⟩^{1})^{<})^{<} ⊢ T  (41)

Now we can move the object K feature out of the lower VP.

(K\T)/V, ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K)_{Subj},

(⟨□_{0}^{↓}K⟩^{1}, ((K\(D\(◇_{1}□_{0}^{↓}V)))/V, ⟨□_{0}^{↓}V ⟩^{1})^{<})^{⊳} ⊢ T (42)

Now we can cancel the V feature. Note that, without a Head Movement package, we could not do this until we had evacuated all uncancelled features from around the head. This trick works, but note that it runs counter to proposals in Chomsky (1995), according to which the head should move first. The rest of the derivation offers nothing new; relevant snapshots of the main goal sequent are given below.

Tns, Subj, (⟨□_{0}^{↓}K⟩^{1}, K\(D\(◇_{1}□_{0}^{↓}V)))^{⊳} ⊢ T  (43)
Tns, (◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K)_{Subj}, D\(◇_{1}□_{0}^{↓}V))^{⊳} ⊢ T  (44)
Tns, (⟨□_{0}^{↓}K⟩^{1}, ⟨□_{0}^{↓}V ⟩^{1})^{⊳} ⊢ T  (45)
(⟨□_{0}^{↓}K⟩^{1}, ((K\T)/V, ⟨□_{0}^{↓}V ⟩^{1})^{<})^{⊳} ⊢ T  (46)

Step (43) is the result of cancelling the lower V feature. Step (44) is the resultof cancelling the object’s K feature against the higher verb. Then the subject’s D feature is cancelled against the verb leading to (45). Finally, after some applications of rules from the Merge package, the subject’s K feature can move to specifier of T, leaving the verb free to cancel its V feature against the V feature of T, which will then allow the cancellation of the subject’s K feature, finishing the proof.

4 Derivation and Representation

In this section we consider the structure of proofs in our system, using techniques of labeled deduction (Gabbay 1994) generalizing the well-known Curry-Howard correspondence between proofs and terms of the lambda calculus. A generative linguist can see in these techniques a generalization of the familiar idea that a phrase structure tree for a sentence can be extracted from a phrase structure derivation serving at once as a record of that derivation and as a static analysis of the sentence so derived. Here we will use the record of a transformational derivation to provide a static analysis of the sentence so derived. Since the derivation here is a transformational one, and not a phrase structure derivation, we can think of the term representing the essential structure of the derivation as a T-marker, to revive some terminology from Chomsky (1975/1955).

In the structural rules which implement the Move transformation we saw a version of movement which destroys the local structure in which the moving expression is initially embedded. So, to take a very simple example, movement from complement to specifier of a single head takes a configuration like (Γ, Δ)^{<} as input and produces a configuration like (Δ, Γ)^{⊳} as output, crucially without leaving a trace behind. The reason for this is that this is a calculus of syntactically active features. Syntactic structure which is inactive is invisible to this system. In particular, traces—which bear no features that might still need to be checked—are invisible to the derivational machinery. However, if we examine the structure of the derivations themselves, rather than the transient structures that they create, we can recover our familiar traces, chains and indices and study them. In a sense, we can use the Curry-Howard morphism to connect derivations with the flavor of the 60’s era Standard Theory of transformational grammar to representations with more of the flavor of 80’s era Government-Binding Theory and the minimalist program.

The assignment of proof terms to formulas works as follows in the setting of a Gentzen sequent calculus. With each basic type appearing in an axiom we associate a variable, so that the axiom A ⊢ A is now written x:A ⊢ x:A. Then the inference rules tell us how to manipulate these variables so as to record the essential structure of the proof. Note in particular the following property of our new labeled rules, which is an invariant on the recursive structure of proofs: the formulas of sequent antecedents are always labeled with variables (which may be fresh variables introduced by the inference rule). The consequence, on the other hand, gets increasingly complex at each step. When we are done, we have a sequent with a numeration of lexical type formulas in the antecedent—each labeled with a variable—and the sentence category in the consequence, labeled with a lambda term built out of those variables.

This device is familiar from formal semantics, where we can use it to derive the semantics of a sentence by assigning to the variables in the goal sequent terms drawn from the lexicon giving the semantics of individual words. The proof term assigned to the consequence of the goal sequent then provides a recipe or program for constructing the semantics of the sentence from the semantics of its constituent lexical items. One can, however, just as easily assign to these variables terms which reflect the theory of syntax in such a way that the lambda term will be converted to an LF level syntactic structure. On the surface this may not seem like a very interesting thing to do: the lambda term itself is already a tree structure with obvious and transparent relations to the kinds of trees one is familiar with from the syntax literature. However, we will see that this gives us a nice, rigorous mathematical framework for investigating questions like the copy theory of movement, spell out, and reconstruction, that is, questions proper to the theory of chains. We derive in this way a clean break between the theory of chains on the one hand and the theory of movement on the other, which we take to have to do with locality or economy conditions restricting

A : x ⊢ A : x Axiom  \begin{aligned}Γ ⊢ t:A Δ[x:A] ⊢ u:B \\ & Cut \\ Δ[Γ] ⊢ u[t/x]:B \end{aligned}  (47)

\begin{aligned}Γ ⊢ t:A Δ[x:B] ⊢ u:C \\ & L/_{i} \\ Δ[(y:B/_{i}A, Γ)^{i}] ⊢ u[y(t)/x]:C \end{aligned}  \begin{aligned}(Δ, x:A)^{i} ⊢ u:B \\ & R/_{i} \\ Δ ⊢ λx.u:B/_{i}A \end{aligned} (48)

\begin{aligned}Γ ⊢ t:A Δ[x:B] ⊢ u:C \\ & L\_{i} \\ Δ[(Γ, y:A\_{i}B)^{i}] ⊢ u[y(t)/x]:C \end{aligned}  \begin{aligned}(x:A, Δ)^{i} ⊢ u:B \\ & R\_{i} \\ Δ ⊢ λx.u:A\_{i}B \end{aligned} (49)

\begin{aligned}Δ[(x_{1} :A, x_{2} :B)^{i}] ⊢ u:C \\ & L•_{i} \\ Δ[z:A •_{i} B] ⊢ u[(z)_{1}/x_{1}, (z)_{2}/x_{2}]:C \end{aligned} \begin{aligned}Δ_{1} ⊢ x_{1} :A Δ_{2} ⊢ x_{2} :B \\ & R•_{i} \\ (Δ_{1}, Δ_{2})^{i} ⊢ ⟨x_{1}, x_{2}⟩:A •_{i} B \end{aligned} (50)

\begin{aligned}Γ[x:A] ⊢ u:B \\ & L□_{i}^{↓} \\ Γ[⟨y:□_{i}^{↓}A⟩^{i}] ⊢ u[^{∨}y/x]:B \end{aligned}  \begin{aligned}⟨Γ⟩^{i} ⊢ t:A \\ & R□_{i}^{↓} \\ Γ ⊢ ^{∧}t:□_{i}^{↓}A \end{aligned}  (51)

\begin{aligned}Γ[⟨x:A⟩^{i}] ⊢ u:B \\ & L◇_{i} \\ Γ[y:◇_{i}A] ⊢ u[^{∪}y/x]:B \end{aligned}  \begin{aligned}Γ ⊢ t:A \\ & R◇_{i} \\ ⟨Γ⟩^{i} ⊢ ^{∩}t:◇_{i}A \end{aligned}  (52)

Figure 5: Logical inference rules, annotated with proof term labels.

derivations. It is in many ways easier to deal with chains representationally and locality derivationally, so it is nice to have a single system in which these two approaches are not merely compatible but actually two sides of the same coin.

The logical rules of figure 1 are given in their labeled forms in figure 5. In figure 5 we use the following notational conventions. Given a term u, the notation u[t/x] denotes the substitution of t for x, x a leaf node in the term u. Given a term z, which should represent an ordered pair, (z)_{1} and (z)_{2} represent the first and second projections of that pair, i.e., its first and second coordinates, respectively. We use x, y and z to represent variables, that is, terms assigned to type formulas in sequent antecedents, and we use s, t and u to represent proper terms, that is, terms associated with type formulas in sequent consequences. Note that proof terms are associated with formulas, not with configurations, so that we might have, for instance, x_{1} :◇A but ⟨x_{2} :A⟩.

The proof terms for the binary products are based on the familiar Curry-Howard correspondence between proofs and lambda terms: the left slash rules correspond to function application, the right slash rules to lambda abstraction, the left product rules to projection and the right product rules to pairing. We observe the following formal generalization: the right rules implement what we might think of abstractly as constructor functions (which construct function types and product types in these cases), while the left rules implement what we might think of as the corresponding destructor rules. This pattern is carried over to the unary modalities, where the ^{∩} and ^{∧} functions stand for constructors for the diamonds and their residuals, respectively, and the ^{∪} and ^{∨} functions stand for corresponding destructors. Unlike the case for binary modes of combination there is no traditional concrete instantiation of this notion of constructor and destructor. They can be anything, as long as destructors and constructors cancel each other out. Because the unary modals play such a large role in the theory of movement, we will consider below how these abstract functions might be realized in the context of the theory of chains.

As usual in a Gentzen calculus, the left slash rules are probably the most difficult to understand. Take for example the L/_{i} rule.

Γ ⊢ t:A Δ[x:B] ⊢ u:C

L/_{i} Δ[(y:B/_{i}A, Γ)^{i}] ⊢ u[y(t)/x]:C

The key idea is that constructing a C from Δ[B] will insert an occurrence of B’s associated variable (here x) somewhere in the term associated with C (here u). That is, we know that u contains an object x of type B. We also know at least one way to construct new objects of type B, namely by applying a function of type B/A to an object of type A. So if we have an object y of type B/A and an object t of type A (or rather, the resources Γ that we know are sufficient to build such a thing), then y(t) must be an object of type B. Therefore we can substitute it for x in u, which is what we do in the conclusion of the L/_{i} rule.

The way in which proofs and proof terms are related is relatively fixed. It is at the level of the lexical term assignments that we can examine the effects of different theoretical proposals. We have already observed that lexical type formulas represent “in miniature” the phrases and chains into which the syntax will extend them. In general, lexical types represent functions from phrases to chains. Consider again the assignment to the Wh determiner which, ignoring the control modals for the moment:

which ↦ (D • K • W)/N  (53)

Any lexical term assignment which we might consider must make sense as an object of this type. That is, it should take a single argument and return a triple of objects.^{10} Observe that we can compute a general form for such a term by labeling the proof of the “complex axiom”

(D • K • W)/N ⊢ (D • K • W)/N.

This yields the following labeled sequent as a theorem of our system (the proof is left as a simple and useful exercise).^{11}

10Actually the situation is slightly more complicated because of the presence of the control modals. We will consider their added effects below.

y:(D • (K • W))/N ⊢ λx.⟨(y(x))_{1}, (y(x))_{2}, (y(x))_{3}⟩:(D • (K • W))/N (54)

Accordingly we derive the equation

y = λx.⟨(y(x))_{1}, (y(x))_{2}, (y(x))_{3}⟩.

This equation is satisfied by any function which maps a single argument to a triple, and so gives a general form for such functions.

One possible term assignment would then be something like the following, where α represents the lexical determiner.

(D • K • W)/N : λy.⟨(α < y), (α < y), (α < y)⟩  (55)

(We use Stabler’s notation here rather than Chomsky’s; to recover that notation, substitute {α, {α, x}} for (α < x).) Here we are treating the application of α to x as literal head-complement formation. Such a term implements the Copy Theory of movement or chain formation. Cancelling the N feature with the L/ rule will have the effect of applying this function to the proof term of the NP, making 3 copies of it. Then as each of the DP’s own features are cancelled, one copy will be peeled off of the tuple and attached into the phrase of the cancelling head.

Note that this offers a solution to a problem of Brody’s (Brody 1997). The theory presented there, like the theory underlying Brody (1995a), combines the idea of presyntactic chain formation with the copy theory of movement. A problem for such a theory is that, presyntactically, it is not yet known what material will be attached into the X-bar projection of the head. Accordingly Brody must place well-formedness conditions on his representations which assure that all information adhering to one copy is propagated to all the others. These conditions are rather complex and intricate. Here we see that nothing extra is really required. The feature makeup of the Wh determiner determines its type: features which it can cancel appear under the slash and features which need to be cancelled appear over the slash. The elements of the chain appearing over the slash can really be anything: the stipulation that they be identical is a substantive condition which forms the core assumption of the copy theory of movement. Given that assumption, and stating things with reference to the proof term in (54), we know that (y(x))_{1} equals (y(x))_{2} equals (y(x))_{3}. All that is left is to decide what structure should be built when a determiner combines with its (internal) argument. Again, the stipulation that that should be a headcomplement configuration seems entirely unproblematic. So we are driven to a representation which, when combined with an argument, will propagate the structure of that argument to all chain positions without further stipulation. In particular, the fact that the λx takes scope over three copies of x simply falls out of the structure of the formula and the way it is used in proofs.

11Note that this proof is not, technically, a derivation, since it is not a proof of a basic category from a numeration. We see again the utility of being able to do proofs beyond just derivations.

It is interesting that, as far as proof terms are concerned, it is the L/ and L\ rules which implement Merge. That is, these are the rules which implement function application, and therefore which will trigger the application of structure building functions to their arguments. Indeed, the proportion “Merge is to Application as Move is to Abstraction” is another reason why the relationship of the minimalist program to categorial grammar has been so compelling. However, this means that it is really Merge which is responsible for feature cancellation, whereas in Chomsky (1995) feature cancellation is supposed to be an essential part of Move. However, this connection between Merge and feature cancellation, or something very much like it, has already been proposed in other minimalist literature (Collins 1997, Bobaljik 1995). In particular, it has been proposed that Move should be treated as removing uncancelled features from the tree and returning them to the numeration, whence they are later merged again at a higher point, or that Move at very least includes Merge as a suboperation. On such a view it will always be Merge which (a) builds structure and (b) in so doing places features in checking configurations.

This relationship of our calculational machinery and the theoretical literature is especially interesting inasmuch as Brody espouses a representational, chain-based perspective on extraction while Collins, Bobaljik and company embrace a derivational, movement-based perspective. Normally, these two perspectives are taken to be competing theories, but in the light of a deductive approach they appear as two sides of the same coin.

A more traditional view of chains would be obtained with an assignment like the following.

(D • K • W)/N : λx.⟨t_{α}, t′_{α}, α < x⟩  (56)

In this version we have committed to interpreting the DP in its highest position, though without saying whether we mean this to represent its LF interpretation, its PF interpretation, or both. We might consider how we would go about representing a DP chain in which distinct positions were interpreted at PF and LF, respectively. One way to do this would be to assign to each lexical item a pair of proof terms. This would implement in a minimalist setting a research program like Oehrle’s (Oehrle 1994, , and refs.). An alternative, inspired by Stabler’s proposals for “one-pass” derivations (Stabler forthcoming, 1997a), would be to use the same proof term but with subexpressions like [[α]] and /α/, for the LF and PF interpretations of α respectively, and similarly for [[x]] and /x/.

One would like to be able to explore positions intermediate between the copy theory and more traditional theories about chains. One possibility is suggested by Collins (1997): starting with a copying operation, we then apply partial deletion to the copies (“up to recoverability”). In effect, we just have to be sure that, knitting all the copies back together again, we obtain the features of the original lexical item. For studying these rather more complex theories it becomes important to look again at our control modals and their effects on the proof.

In figure 6 we exhibit the simple derivation from figure 3, this time with labels. The essential point is the proof term we derive in the consequent of the

x_{4} :D ⊢ x_{4} :D \begin{aligned}x_{1} :K ⊢ x_{1} :K x_{2} :V ⊢ x_{2} :V \\ & L\ \\ (x_{1} :K, f′:(K\V))^{•} ⊢ f′(x_{1}):V \end{aligned} ; L□_{0}^{↓} ; (⟨x_{3} :□_{0}^{↓}K⟩^{0}, f′:K\V)^{•} ⊢ f′(^{∨}x_{3}):V ; Ψ ; f′:(K\V), ⟨x_{3} :□_{0}^{↓}K⟩^{1} ⊢ f′(^{∨}x_{3}):V

L/

(f:(K\V)/D, x_{4} :D)^{•}, ⟨x_{3} :□_{0}^{↓}K⟩^{1} ⊢ f(x_{4})(^{∨}x_{3}):V

L□_{0}^{↓}

(f:(K\V)/D, ⟨x_{5} :□_{0}^{↓}D⟩^{0})^{•}, ⟨x_{3} :□_{0}^{↓}K⟩^{1} ⊢ f(^{∨}x_{5})(^{∨}x_{3}):V

Φ

f:(K\V)/D, ⟨(x_{5} :□_{0}^{↓}D, x_{3} :□_{0}^{↓}K)^{•}⟩^{1} ⊢ f(^{∨}x_{5})(^{∨}x_{3}):V

L•

f:(K\V)/D, ⟨x′:□_{0}^{↓}D • □_{0}^{↓}K⟩^{1} ⊢ f(^{∨}(x′)_{1})(^{∨}(x′)_{2}):V

L◇_{1}

f:(K\V)/D, x:◇_{1}(□_{0}^{↓}D • □_{0}^{↓}K) ⊢ f(^{∨}(^{∪}x)_{1})(^{∨}(^{∪}x)_{2}):V

Figure 6: The derivation of figure 3 with labels.

goal sequent, repeated below.

f(^{∨}(^{∪}x)_{1})(^{∨}(^{∪}x)_{2})

In particular, notice that the ^{∪} function, which represents the destructor for the ◇_{1} modal, which in turn marks chains as moveable, appears under the scope of the projection functions which break up the chain for attachment in multiple locations. We have (^{∪}x)_{1} and (^{∪}x)_{2}. The variable x corresponds to the proof term for the argument DP, in this case a two element chain. If we think of ^{∪}x as representing the application of a partial deletion function to a chain, then we can read full proof term for the VP in the following way. We calculate the effects of partial deletion on the chain x, then peel off the root of that chain and apply f to it, making it the verb’s structural complement in the T-marker. We then apply the resulting function to the head of the chain, or what is left of the head after partial deletion, yielding a specifier construction. Note that we must be sure that ^{∪} cancels with ^{∩}. One way to do that might be to implement the constructor ^{∩} as the (bidirectional) propagation of information along a chain. In this way we force the condition of recoverability on partial deletion: if too much is deleted then propagation will not recover the original chain.

In this section we have seen how chains arise out of the primitive assumption that features are resources which are consumed by a derivation. The resource conscious approach to formal features characteristic of the minimalist program forces us to admit lexical type formulas containing tuples of features. As soon as we try to say what kinds of syntactic objects these tuples may be the types of, we arrive at chains. Finally, the mechanisms of modal control over movement provide us at the same time with devices which can be used in the theory of chain formation to regulate the distribution of syntactic information among the various chain positions. In this way we derive the mathematical foundations of a syntactic theory which uses both movement and chains, as the theory of Chomsky (1995) does, while at the same time keeping them separate and synchronized. Brody (1995b) is critical of the minimalist program as it was developing at the time precisely because it mixed chains and movement transformations, which Brody argued were redundant. We claim here, on the strength of these investigations, that the problems with such redundancies can be tamed if there is a precise correspondence between chains and movement so that they are in fact, as they are here, two aspects of the same mathematical object. Chains may be seen as the static reflex of the way in which features are cancelled in a derivation, or derivations may be seen as the way in which conditions on the interaction of chains and chain elements are verified. As these perspectives are equivalent, neither can really be more correct than the other, and both become more useful as it becomes possible to use whichever one is better suited to the purpose at hand.

5 On the Relation Between Movement and Hypothetical Reasoning

In figure 7 we see an example of a classical derivation of a relative clause in the associative Lambek calculus L. We see that the relative pronoun which is assigned in the lexicon the type of a function from 1-place predicates needing an argument on their right (S/NP) to whatever type (complete) relative clauses should have. The bulk of the proof involves proving that the resources of the clause other than the relative pronoun are sufficient to construct an instance of its argument type. Since that argument type is higher order (it is the type of a function and not just a basic type) the main subproof is a proof of a formula on the right of the ⊢ whose main functor is /, so we require the use of the R/ rule to deal with this. The R/ rule is the Gentzen version of “hypothetical reasoning”: we prove that we can construct a functional type by proving that, if we had its argument type on the left of the ⊢, then we could construct the type of its output. In type-logical terms, then, the left residual rules correspond to the application of a function to its argument and the right residual rules tell us how to construct a function by abstraction over its argument. (In terms of more traditional implicational logic, the left residual rules correspond to modus ponens while the right rules correspond to the deduction theorem.)

It is the introduction of hypothetical reasoning into categorial grammar which distinguishes the systems derived from Lambek’s calculi L and NL from the Ajdukiewicz-Bar Hillel system (AB), which has only function application without abstraction. It is this move which really turns a rule based grammar formalism into a logic, and so the utility of hypothetical reasoning for handling linguistic extraction phenomena has been an important argument over the years for this approach to categorial grammar.

However, in our minimalist-style derivations we have made no use of hypo-

NP ⊢ NP NP ⊢ NP S ⊢ S L\ NP, NP\S ⊢ S L/ NP, (NP\S)/NP, NP ⊢ S R/ NP, (NP\S)/NP ⊢ S/NP R ⊢ R

L/ R/(S/NP), NP, (NP\S)/NP ⊢ R

Lookup

which mary proved ⊢ R

Figure 7: which Mary proved ⊢ R in L.

thetical reasoning. We have used only left rules.^{12} This is because our grammar makes no use of higher order types: there are no types in minimalist lexicons which take functions as arguments.^{13} So it is important to examine at this point in more detail just how we manage to derive extraction phenomena without appeal to hypothetical reasoning. We will see immediately that certain features of transformational grammar are rather surprisingly not relevant to distinguishing it from categorial grammar. For example, the appeal to empty trace categories is irrelevant: we have seen already that these have no place in the derivational calculus in any case. The appeal to movement is also irrelevant: in order to deal with a host of real syntactic phenomena, hypothetical reasoning in categorial derivations must also be augmented with modally controlled access to permutation and association, though typically the direction of movement is the reverse of our system. Perhaps most surprisingly, the appeal to hypothetical reasoning itself is not particularly significant. We will see that this is essentially an artifact of the hierarchical order in which we wish to combine resources.

In figures 9 and 10 we present sketches of the labeled derivations of a subjectrelative clause like … who sneezed … in CG and TG. The CG type for an English-style relative clause should be something like N\N, the type of a nominal post modifier, hower we write it here simply as R. Variables have been given suggestive names to help in comparing the actions of the two different derivation systems. The main thing to observe is the way in which the TG derivation uses the resource W (for the Wh feature) and the null Comp (W \C)/V.

In figure 10 we have suppressed Tense and Case, allowing the complementizer to select a verb directly. We have in both cases also suppressed the application of structural rules and the modal operators needed to control access to those rules. The structural rules, in particular, have no effect on the proof terms we derive. These proof terms are repeated below for convenience.

12Note that our heavy use of structural rules is not really relevant to this discussion. Indeed the multimodal control of structural rule packages was developed within categorial grammar because proofs like that in figure 7, with relatively light and uniform use of structural rules, proved deceptively simple and inadequate in the face of natural language data.

13There may be an exception to this. If a head can raise to adjoin to another head bringing some uncancelled features along with it, to be cancelled in its new position as part of a complex head, then the higher head may need to select the lower as a functional type.

\underline{CG}  \underline{TG}
who  R/(NP \S) D • W
sneezed  NP \S  D\V
Comp  —  (W \C)/V

Figure 8: Lexica for the CG and TG derivations.

\begin{aligned}Nom:NP ⊢ Nom:NP x_{1} :S ⊢ x_{1} :S \\ & L\ \\ Nom:NP , P red:NP \S ⊢ P red(Nom):S \end{aligned} ; R\ ; P red:NP \S ⊢ λNom.P red(Nom):NP \S x_{2} :R ⊢ x_{2} :R

L/ W h:R/(NP \S), P red:NP \S ⊢ W h(λNom.P red(Nom)):R

Figure 9: CG derivation of who sneezed.

Nom:D ⊢ Nom:D \begin{matrix}x_{3} :V ⊢ x_{3} :V \begin{aligned}W h:W ⊢ W h:W x_{1} :C ⊢ x_{1} :C \\ & L\ \\ W h:W , x_{2} :W \C ⊢ x_{2}(W h):C \end{aligned} \\ L/ \\ W h:W , App:(W \C)/V , x_{3} :V ⊢ App(x_{3})(W h):C \end{matrix}

L\ W h:W , App:(W \C)/V , Nom:D, P red:D\V ⊢ App(P red(Nom))(W h):C

L• App:(W \C)/V , Subj:D • W , P red:D\V ⊢ App(P red((Subj)_{1}))((Subj)_{2}):C

Figure 10: TG derivation of who sneezed.

\begin{matrix}Fig. 9: & W h(λNom.P red(Nom)) \\ Fig. 10: & App(P red(Nom))(W h) \end{matrix}

The main ways in which the TG term differs from the CG term are the appearance of the variable App, which corresponds in the syntax to the presence of the null complementizer, the reduction of W h from a function to a constant of some sort and the lack of a λ abstractor in front of the P red(Nom) expression. The first two differences are exactly what we would expect, given that the Wh operator has been given an atomic type. When we “reify” function symbols (such as variable binding operators) as individuals then we need to provide a new explicit function symbol to represent the application of a functor to its arguments. Where the CG derivation constructs a term which represents directly the application of a W h operator to a one place predicate, the TG derivation yields instead a term which requires further interpretation, in particular a term in which App must still be interpreted as function application in order to derive the semantics.

The third distinction goes deeper into the relations between these approaches. The TG term lacks the λ abstractor because the derivation uses only application (L/, L\) steps with no abstraction (R/, R\) steps. These abstraction steps are certainly required in a syntax without explicit chains: this is the mechanism whereby the W h operator will bind the variable Nom without knowing the variable’s name in advance. Suppose we interpret W h as

λP.which is the x such that P (x)

and apply it to λNom.sneezed(Nom). We get

which is the x such that (λNom.Nom sneezed)(x)

which reduces to

which is the x such that x sneezed.  (57)

That is, we have managed to rename the variable in the predicate to the variable bound by the Wh operator.

Chain formation is supposed to solve the problem of variable binding in a rather different way. The idea is essentially to rely on movement or chain formation to assure that the operator and bound variable are appropriately named. We can think of the identity of the occurrence of ⟨Nom, Wh⟩ (call it “Subj ”) as the “index” which is born by Nom and Wh. We thus have enough information to ensure that Wh can be interpreted as something which binds occurrences of the variable named Subj in its scope. For example, if we wished to derive something like the semantic logical form “which is the x such that x sneezed,” from the proof term App(P red(Nom))(W h), we could try to make the following assignments.

App ↦ λP.λQ.Q(P)
P red ↦ λx.x sneezed
Nom ↦ x_{Subj}
W h ↦ ‘λ’R.which is the x_{Subj} such that R

The λ in the assignment to Wh is in scare quotes because we must violate a condition on the reduction of lambda terms in order to obtain the expression we want. Normally, it is not allowed to substitute one expression into another in such a way that a variable free in the former becomes bound in the result. That is precisely what we want to have happen here: we want x_{Subj} in “x_{Subj} sneezed” to be bound by the Wh operator “which is the x_{Subj} such that” when the former is substituted for R. We have taken great pains in the naming of the variable corresponding to Nom with just this end in view. Interestingly, this approach shows some similarities to a recent approach to categorial deduction developed by Mark Hepple (Hepple 1997, 1996). Hepple presents specialized deduction rules which allow him to go from higher order types to first order types. These devices crucially rely on a variant of substitution into lambda terms which allows variable capture by a variable binder, which is exactly the mechanism we are relying on here. Again, the magic works because of the care we have taken with the naming of our variables, via coindexation, so that variable capture should never be accidental.

These distinctions seem to derive rather directly from the focus in CG on semantics and in TG on syntax. In particular, CG avoids headaches of variable naming and intentional variable capture by making sure that the syntactic type of the relative pronoun reflects its semantic type. The TG approach on the other hand focuses on building up a strictly syntactic structure to serve as the LF interface. For example, the TG approach bears strong similarities to the way in which well formed formulas are built up in first order logic. There for example we have a rule of formation which says that if ϕ is a wff, then so is ∀xϕ, together with a definition of bound and free variables which assures that ∀x will capture all occurrences of x free in ϕ. There is no concern here for the eventual interpretation of ∀x as the universal quantifier. In particular, if we try to implement this formation rule as a structure building function λP.∀xP, then we risk, indeed we really intend, exactly the kind of variable capture that we have seen above. In effect, these differences reflect the fundamental idea in TG that scope-taking is a matter of syntactic configuration, whereas in CG (with its close ties to generalized quantifier theory) scope-taking is really an instance of the function-argument relation.

This is not by any means the end of the story, however, or even of such a story as can be told in this limited space. We have a calculus which is a real grammar logic, complete with left and right rules for all connectives. To be sure, we have focused our attention on a particular class of lexicons, which have properties reflecting ideas of the minimalist program, and these lexica do not require us to use right rules in grammatical derivations. However, we can easily extend our investigation, holding the grammar logic constant. In particular, we can ask what would happen if we did use hypothetical reasoning in the derivation of extraction phenomena.

For example, it is a theorem of our system that the partial clause [Comp sneezed] can be assigned the type C/_{⊗}◇_{1}(□_{0}^{↓}D • □_{0}^{↓}W).

(W \C)/V, D\◇_{1}□_{0}^{↓}V ⊢ C/_{⊗}◇_{1}(□_{0}^{↓}D • □_{0}^{↓}W)

The proof search is elementary and obvious after its first step: we must start with an application of R/_{⊗}. This gives us as the immediate premise of the goal sequent the very same numeration we would have started from in the transformational derivation restricted to first order types.

(W \C)/V, D\◇_{1}□_{0}^{↓}V, ◇_{1}(□_{0}^{↓}D • □_{0}^{↓}W) ⊢ C

We can conclude, then, that we could assign to the relative WhP the higher order type

C/_{⊗}(C/_{⊗}◇_{1}(□_{0}^{↓}D • □_{0}^{↓}W)).

This allows it to combine with a partial relative clause in the same way in which the categorial relative pronoun combines with its clause (see figure 9). That is, the goal sequent is derived by the application of L/_{⊗}, with the left premise being the claim that the material in the scope of the pronoun is sufficient to provide it with its argument. Again, the key step of that proof will be the derivation of the goal’s left premise by the application of R/_{⊗}. In this case, the main subproof down to the application of R/_{⊗}, is the same as the proof in figure 10. Therefore, we know that the proof term assigned to the succedent type before the application of R/_{⊗} will be of the form

App(P red((Subj)_{1}))((Subj)_{2})

(plus constructors and destructors corresponding to the unary control modals). The action of the R/_{⊗} rule will cause the chain-variable Subj to be bound, yielding the following labelled sequent.

App:(W \C)/V , P red:D\◇_{1}□_{0}^{↓}V ⊢

λSubj.App(P red((Subj)_{1}))((Subj)_{2}):C/_{⊗}◇_{1}(□_{0}^{↓}D • □_{0}^{↓}W) (58)

If we associate our new higher-order relative pronoun with a fresh variable F then the entire relative clause is of type C with proof term

F (λSubj.App(P red((Subj)_{1}))((Subj)_{2}))

The F here is strongly analogous to the role of the functional variable W h in the proof term assigned by the CG proof in figure 9. Semantically, we want to assign it the same kind of value, namely a function which applies another function to its bound variable. So, given that Subj was, in our first-order type based derivation, assigned to the pair

⟨x, λS.which is the x such that S⟩

then F should be assigned the following logical form.

λR.R(⟨x, λS.which is the x such that S⟩)  (59)

All this should be completely unsurprising, despite the sheer weight of mathematical ink, since the type C/_{⊗}(C/_{⊗}◇_{1}(□_{0}^{↓}D • □_{0}^{↓}W)) is just an instance of a type formula of the general form B/_{⊗}B/_{⊗}A, and we have as a theorem that the following sequent

A ⊢ B/_{⊗}B/_{⊗}A

is valid in the associative, commutative calculus LP (recall that ⊗ is just the LP product, with free access to permutation and association rules). This is just type raising, and the expression in (59), though made somewhat obscure by the appeal to pairing and projection, is just the semantics of a type-raised argument, taking a function and applying it to itself. The important point here is that, because this is a valid sequent, we do not even need to modify our lexicons in order to accommodate approaches to extraction based on hypothetical reasoning. Once we have a definition of who which works in a transformational derivation without hypothetical reasoning, we automatically can derive a type assignment and logical form assignment which works with hypothetical reasoning. In particular, core ideas about the locality of possible movement transformations remain in place.

However, the appeal to hypothetical reasoning on its own does not turn TG into CG, really because we do not have to make any modifications to our lexica. In particular, chains persist, leaving us with expressions like

⟨x, λS.which is the x such that S⟩

where we have an occurrence of x outside scope of the Wh operator which we intend ultimately to place within that scope. Embedding this in layers of applications and abstractions does not change things, and transformational grammar remains a theory of formation distinct from a theory of interpretation. In light of this, a distinction which reflects concerns of very long standing in both traditions, it is somewhat remarkable to observe once again that the appearance of chains in this system stems directly from the resource conscious use of features which is a very recent feature of transformational grammar, belonging specifically to the minimalist program. That is, our multiplicative treatment of multiple feature assignment leads us to type formulas whose natural structural interpretation is as tuples of syntactic objects all extending a single lexical head, that is, chains. The more things change, the more they stay the same.

The most important lesson here is then that the use of hypothetical reasoning per se does not appear to be really relevant to the comparison of CG and TG. We need modify neither our logic nor our lexicons to support CG-style derivations of relative clauses in TG, and our approach to TG derivations uses no resources which are not in principle available to CG. However, it seems fairly clear that the introduction of product types into a categorial lexicon would have profound effects on the hitherto very tight connections in that framework between syntax and semantics.

6 Missing Pieces, Future Work

A number of important gaps remain in these proposals which will have to be filled in future work. We have so far done nothing to implement successive cyclic movement, for example. In Chomsky (1995) this is done by deleting (or erasing) only the feature on the target. In our terms this amounts to allowing moving features access to the structural rule of Contraction as well as movement.

\begin{aligned}Γ[(Δ, Δ)^{j}] \\ & Contraction \\ Γ[⟨Δ⟩^{i}] ⊢ A \end{aligned}

There is also another way to give a formula more restricted access to Contraction “through the back door”, namely via structural rules of (reverse) distributivity.

Γ[((Δ_{1}, Δ_{2})^{i}, (Δ_{1}, Δ_{3})^{i})^{j}] ⊢ A

Distributivity^{−1} Γ[(Δ_{1}, (Δ_{2}, Δ_{3})^{j})^{i}] ⊢ A

Here the required presence of a j type configuration adds a certain amount of context sensitivity to the multiplication of the resources in Δ_{1}. However, it is not at this point clear how this can be employed in the context of a movement derivation.

We have also done nothing to implement the distinction between overt and covert movement. In particular, we have not implemented the minimalist idea that features come in strong and weak varieties, and that only strong features force overt movement. Part of the reason for this is that the theory is somewhat vague on this point. In various places, Chomsky seems to want “strength” itself to be a feature. So it is not yet clear whether “strength” should be treated in a resource conscious manner, or rather in an additive manner, or by some other means completely (e.g., with yet more modal control).

Finally, our implementation of locality conditions on movement as side conditions on the application of structural inference rules leaves a good deal to be desired. In particular such side conditions threaten the compleness of the grammar logic, and in general have a sort of extra logical flavor. Ideally the same conditions should be implemented directly in the logic via structural postulates and corresponding inference rules. It is not guaranteed that this is possible. For example, global economy conditions are unlikely to be implementable except as extra conditions on which otherwise well formed proofs are admissible. However, local conditions, in particular c-command based conditions like the versions of Minimal Link found towards the end of Chomsky (1995) look more tractable, since in a strictly binary branching structure such as our resource configurations the c-command configuration is relatively easy to describe.

In spite of these shortcomings of what is after all still a very preliminary investigation, it seems likely that the devices of multimodal type logics can provide us with an extremely useful tool for investigating different theories within a transformational framework, and also for investigating different frameworks whose fundamental biases are rather different. It is important to keep in mind that the system we have presented here is like other type logical grammatical calculi in the Lambek tradition in that it is not meant as a formal theory of Universal Grammar. The logic itself is useful precisely because it is not restrictive. This is what allows such different syntactic theories as categorial grammar and transformational grammar to be embedded within it. It is not a formal theory of Universal Grammar, but rather a tool for performing precise scientific calculations within the theory of grammar, very broadly construed. Because this system is intended as a very general grammatical calculus, and because it is founded on mathematical principles as well as grammatical ones, it helps to dissolve the barriers between frameworks which restrictive formalisms impose, and is thus a healthy antidote to (but not a replacement for) formalistic theories of Universal Grammar. We have seen, for example, that different theories of chains can be compared without regard for whether they approach chains derivationally or representationally, because both derivations and representations are simultaneously present and synchronized in type logical grammar. This approach remains useful even when we are considering extraction phenomena more abstractly, and in particular theoretical approaches to them which do not utilize chains at all. We have seen that we can gain considerable precision in meta-theoretic investigations, isolating deep pretheoretical commitments from the mechanisms which help to realize them. Perhaps the best way to see the utility of a general grammatical calculus is to view it as an approach which respects individual ideas about syntax as paramount, taking precedence over the larger frameworks which knit them together in various ways.

References

Bayer, S. and Johnson, M. (1995). Features and agreement, Proceedings of the ACL, Association for Computational Linguistics, pp. 70–76.

Berwick, R. C. and Epstein, S. D. (1995). Computational minimalism: The convergence of the minimalist syntactic program and categorial grammar, TWLT-10: Algebraic Methods in Language Processing, AMAST, Faculty of Computer Science, University of Twente, Enschede, the Netherlands.

Bobaljik, J. (1995). In terms of merge: Copy and head movement, MIT Working Papers in Linguistics 27, MIT Linguistics Dept., pp. 41–64.

Brody, M. (1995a). Lexico-Logical Form: A Radically Minimalist Theory, MIT Press, Cambridge, MA.

Brody, M. (1995b). Perfect syntax, Colloquium talk given at the University of Tübingen.

Brody, M. (1997). Projection and phrase structure, Technical Report 98, SFB 340, University of Tübingen. Draft of an article forthcoming in Linguistic Inquiry.

Chomsky, N. (1975/1955). The Logical Structure of Linguistic Theory, University of Chicago Press, Chicago.

Chomsky, N. (1995). The Minimalist Program, MIT Press, Cambridge, MA.

Collins, C. (1997). Local Economy, MIT Press, Cambridge, MA.

Cornell, T. L. (1997). A type-logical perspective on minimalist derivations, Proceedings of Formal Grammar ’97, Aix-en-Provence, France.

Gabbay, D. M. (1994). Lds—labeled deduction systems, Technical Report MPI-I-94-223, Max Planck Institut für Informatik, Saarbrücken. To appear from Oxford University Press.

Girard, J.-Y. (1987). Linear logic, Theoretical Computer Science 50: 1–102.

Hepple, M. (1996). A compilation-chart method for linear categorial deduction, Proceedings of COLING-96.

Hepple, M. (1997). Maximal incrementality in linear categorial deduction, ACL-EACL ’97 Proceedings, ACL and EACL, pp. 344–351.

Heylen, D. (1997). Generalisation and coordination in categorial grammar, in G.-J. M. Kruijff, G. V. Morrill and R. T. Oehrle (eds), Formal Grammar 1997, Aix-en-Provence, France.

Koopman, H. (1994). Licensing heads, in D. Lightfoot and N. Hornstein (eds), Verb Movement, Cambridge University Press, Cambridge, pp. 261–296.

Lambek, J. (1958). The mathematics of sentence structure, American Mathematical Monthly 65: 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 Twelfth Symposium in Applied Mathematics, Providence, Rhode Island.

Lecomte, A. (1997). POM-nets and minimalism, in C. Casadio (ed.), Proceedings of the IV Roma Workshop: Dynamic Perspectives in Logic and Linguistics, SILPS Group in Logic and Natural Languages.

Moortgat, M. (1996). Categorial type logics, in J. van Benthem and A. ter Meulen (eds), Handbook of Logic and Language, Elsevier, chapter 2.

Moortgat, M. and Oehrle, R. T. (1997). Structural abstractions, in V. M. Abrusci and C. Casadio (eds), Proceedings of the 1996 Roma Workshop: Proofs and Linguistic Categories, Dept. of Philosophy, Univ. of Bologna, Bologna, Italy.

Morrill, G. (1994). Type Logical Grammar, Kluwer, Dordrecht.

Oehrle, R. T. (1994). Term-labeled categorial type systems, Linguistics and Philosophy 17(6): 633.

Stabler, E. (1997a). Derivational minimalism, in C. Retoré (ed.), Logical Aspects of Computational Linguistics, Springer, Berlin, pp. 68–95. LNAI 1328.

Stabler, E. P. (1997b). Computing quantifier scope, in A. Szabolcsi (ed.), Ways of Scope Taking, Kluwer, Boston.

Stabler, E. P. (forthcoming). Acquiring and Parsing Languages with Movement, Basil Blackwell, Oxford.

Troelstra, A. S. (1992). Lectures on Linear Logic, Vol. 29 of Lecture Notes, CSLI, Stanford.