A Type-Logical Perspective on Minimalist Derivations

Thomas L. Cornell^{∗}

July 17, 1997

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 (e.g., Morrill 1994, Moortgat 1996) We propose to develop ideas from the minimalist program within such a type-logical deductive grammar framework. Simulating minimalist style derivations in a deductive setting turns out to be relatively straightforward, up to a point. Beyond that point, however, problems become quite serious. Nonetheless, the comparison is illuminating, in particular as it sheds some light on the problematical relation of derivational and representational techniques in modern transformational grammar.

The main feature of minimalist derivations which has suggested a connection with categorial grammar is the treatment of feature checking in Chapter 4 of Chomsky (1995). The idea that a feature on a moving phrase might be cancelled against a feature on the structure to which it moves is very reminiscent of the basic cancellation rules of categorial grammar (cf. Stabler forthcoming, 1996). In a type logical setting we would want to implement feature checking as an instance of the application of a rule of use (left rule) for a residual type. To take a somewhat oversimplified example, given a verb which assigns accusative case to its specifier, we can represent the cancellation of the verb’s case (K) feature against the K feature of the object as in the following proof.

K ⇒ K V ⇒ V L\ K, K\V ⇒ V

Roughly, the application of the L\ rule corresponds to the attachment of the object in the specifier position of the V, and the axiom K ⇒ K marks the feature as cancelled.

∗This work has benefitted from the help of many people, in particular Dick Oehrle, Ed Stabler and Uwe Mönnich. Much is due to them, but the errors that remain are all my own. Author’s address: University of Tübingen, Seminar für Sprachwissenschaft; email:

cornell@sfs.nphil.uni-tuebingen.de

There are several points which make this approach to minimalist derivations appealing. Most importantly, this offers an explanation grounded in formal, logical considerations for the idea that transformational derivations should be driven by the need to cancel features. In a deductive setting this means neither more nor less than that proofs encode the need to reduce a theorem to axioms.

Another reason to look closely at type logical grammars as a framework for formal investigations of minimalist ideas has to do with the tension in modern day transformational grammar between derivations and representations. The issue revolves around the relative merits of defining syntactic structures by means of movement-based derivations, or chain-based wellformedness conditions. Two things suggest that a type logical setting may clarify these very murky issues. First, this is a framework in which procedural, proof theoretic approaches are balanced by a careful attention to more declarative, model theoretic techniques. On the other hand, the Curry-Howard morphism, and its generalization to other kinds of labeled deduction, offers a somewhat different, but very direct link between derivations and representations. In this paper we will pay some attention in particular to these latter techniques for relating transformational derivations to chains.

As presented in Chomsky (1995), a derivation proceeds from an initially given numeration, which is supposed to be a multiset of lexical item occurrences. The numeration is then 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. 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 this fundamental decision problem 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. Chomsky’s definition of the numeration as a multiset even gives us a direct indication of which grammar logic we ought to try to use: LP, the Lambekvan Benthem associative and commutative calculus. So our starting point seems clearly given. We begin there and see what kind of trouble we get into.

We present LP here in Gentzen style, with nonassociative, noncommutative sequents (so antecedents are binary trees of formulas), with explicit structural rules of Permutation and Association. This will help us track better what these rules actually get used for and where they are needed. We associate type formulas with “proof terms” which record the structure of the proof. These terms are constructed out of variables, which we will instantiate with lexical term assignments. (To save horizontal space we often write the proof term under the type formula.) Axioms are sequents of the form x : A ⇒ x : A, where x is a fresh variable and A an atomic type.

\begin{aligned}Γ ⇒ {A \atop t} Δ[{A \atop x}] ⇒ {B \atop u} \\ & Cut \\ Δ[Γ] ⇒ {B \atop u[t/x]} \end{aligned}  (1)

\begin{aligned}Γ ⇒ {A \atop t} Δ[{B \atop x}] ⇒ {C \atop u} \\ & L/ \\ Δ[{B/A \atop y}, Γ] ⇒ {C \atop u[y(t)/x]} \end{aligned}  \begin{aligned}Γ ⇒ {A \atop t} Δ[{B \atop x}] ⇒ {C \atop u} \\ & L\ \\ Δ[Γ, {A\B \atop y}] ⇒ {C \atop u[y(t)/x]} \end{aligned}  (2)

\begin{aligned}Δ[({A \atop x_{1}} , {B \atop x_{2}} )] ⇒ {C \atop u} \\ & L· \\ Δ[{A·B \atop z}] ⇒ {C \atop u[π_{1}z/x_{1},π_{2}z/x_{2}]} \end{aligned}  (3)

\begin{aligned}(Δ, {A \atop x}) ⇒ {B \atop u} \\ & R/ \\ Δ ⇒ {B/A \atop λx.u} \end{aligned}  \begin{aligned}({A \atop x}, Δ) ⇒ {B \atop u} \\ & R\ \\ Δ ⇒ {A\B \atop λx.u} \end{aligned}  (4)

\begin{aligned}Δ_{1} ⇒ {A \atop x_{1}} Δ_{2} ⇒ {B \atop x_{2}} \\ & R· \\ (Δ_{1}, Δ_{2}) ⇒ {A·B \atop ⟨x_{1},x_{2}⟩} \end{aligned}  (5)

Δ[((Γ_{1}, Γ_{2}), Γ_{3})] ⇒ B A Δ[(Γ_{1}, (Γ_{2}, Γ_{3}))] ⇒ B  \begin{aligned}Δ[(Γ_{2}, Γ_{1})] ⇒ B \\ & P \\ Δ[(Γ_{1}, Γ_{2})] ⇒ B \end{aligned}  (6)

Consider for example the following theorem of LP. (In what follows the feature K is used for “case”, since we are already using C for “complementizer”, and we use W rather than W h for compactness and uniformity.)

{D·K \atop ⟨x_{1},x_{2}⟩}, {(D\V)/V \atop y_{1}} , {(K\V)/D \atop y_{2}} , {D·K \atop ⟨x_{3},x_{4}⟩} ⇒ {K·V \atop ⟨x_{2},y_{1}(y_{2}(x_{3})(x_{4}))(x_{1})⟩}  (7)

Intuitively, this represents the construction of a standard transitive verb phrase in the style of Chomsky (1995).^{1} A light verb (here assigned the type (D\V)/V) selects the external argument (represented here as the first D · K, a determiner phrase needing to check a case feature) and the main verb selects a DP complement (the second D · K) and assigns accusative case to its specifier. The object DP will have to move from complement to specifier of the lower V, and we will end up with a phrase containing two features still needing to be checked: the V feature of the light verb, and the K feature of the external argument. (We do not illustrate the movement of the main verb to adjoin to the light verb; we will discuss head movement in some detail below.) We assume the sequent comma is right branching, and so we can leave out some unnecessary parentheses.

1Or at least, the style arrived at by the end of the book.

\begin{matrix}{D \atop x_{3}} ⇒ {D \atop x_{3}}  \begin{aligned}{K \atop x_{4}} ⇒ {K \atop x_{4}}  {V \atop x_{5}} ⇒ {V \atop x_{5}} \\ & L\ \\ {K \atop x_{4}} , {K\V \atop y_{3}} ⇒ {V \atop y_{3}(x_{4})} \end{aligned} ; P,A ; {K\V \atop y_{3}} , {K \atop x_{4}} ⇒ {V \atop y_{3}(x_{4})} \\ L/ \\ ({(K\V)/D \atop y_{2}} , {D \atop x_{3}} ), {K \atop x_{4}} ⇒ {V \atop y_{2}(x_{3})(x_{4})} \end{matrix} ; A ; {(K\V)/D \atop y_{2}} , {D \atop x_{3}} , {K \atop x_{4}} ⇒ {V \atop y_{2}(x_{3})(x_{4})} ; L· ; {(K\V)/D \atop y_{2}} , {D·K \atop ⟨x_{3},x_{4}⟩}, ⇒ {V \atop y_{2}(x_{3})(x_{4})}  (8)
\begin{aligned}(8) & \begin{matrix}{V \atop x_{7}} ⇒ {V \atop x_{7}}  \begin{aligned}{D \atop x_{6}} ⇒ {D \atop x_{6}}  {V \atop x_{8}} ⇒ {V \atop x_{8}} \\ & L\ \\ {D \atop x_{6}} , {D\V \atop y_{4}} ⇒ {V \atop y_{4}(x_{6})} \end{aligned} ; R\ ; {D\V \atop y_{4}} ⇒ {D\V \atop λx_{6}.y_{4}(x_{6})} \\ L/ \\ {(D\V)/V \atop y_{1}} , {V \atop x_{7}} ⇒ {D\V \atop λx_{6}.y_{1}(x_{7})(x_{6})} \end{matrix} \\ & Cut \\ {(D\V)/V \atop y_{1}} , {(K\V)/D \atop y_{2}} , {D·K \atop ⟨x_{3},x_{4}⟩} ⇒ {D\V \atop λx_{6}.(y_{1}(y_{2}(x_{3})(x_{4}))(x_{6}))} \end{aligned}  (9)
\begin{aligned}(9) & \begin{matrix}{K \atop x_{2}} ⇒ {K \atop x_{2}}  \begin{aligned}{D \atop x_{1}} ⇒ {D \atop x_{1}}  {V \atop x_{9}} ⇒ {V \atop x_{9}} \\ & L\ \\ {D \atop x_{1}} , {D\V \atop y_{5}} ⇒ {V \atop y_{5}(x_{1})} \end{aligned} \\ R· \\ {K \atop x_{2}} , {D \atop x_{1}} , {D\V \atop y_{5}} ⇒ {K·V \atop ⟨x_{2},y_{5}(x_{1})⟩} \end{matrix} ; P,A ; ({D \atop x_{1}} , {K \atop x_{2}} ), {D\V \atop y_{5}} ⇒ {K·V \atop ⟨x_{2},y_{5}(x_{1})⟩} ; L· ; {D·K \atop ⟨x_{1},x_{2}⟩}, {D\V \atop y_{5}} ⇒ {K·V \atop ⟨x_{2},y_{5}(x_{1})⟩} \\ & Cut \\ {D·K \atop ⟨x_{1},x_{2}⟩}, {(D\V)/V \atop y_{1}} , {(K\V)/D \atop y_{2}} , {D·K \atop ⟨x_{3},x_{4}⟩} ⇒ {K·V \atop ⟨x_{2},y_{1}(y_{2}(x_{3})(x_{4}))(x_{1})⟩} \end{aligned}  (10)

Figure 1: Sketching a minimalist derivation as a proof in LP.

The subproof in (8) represents the result of merging the direct object as complement of the main verb, cancelling the categorial feature against the verb’s selection feature. Then the direct object’s surviving K feature moves to the specifier position of the verb, which is a checking configuration for formal features. As one would expect, the operation of the generalized transformation Move is implemented via a series of applications of the structural rules A and P.

The subproof in (9) merges the lower VP (now just containing the main verb’s uncancelled V feature) with the light verb that selects it. Then finally the subproof in (10) merges the subject DP with the light verb as its specifier. We cancel the categorial D feature against that verb’s selection feature, leaving the K uncancelled.

Such a derivation would normally proceed by moving the K feature of the subject to attach to Tense or some other case-assigning functional projection. Additionally we might have a W feature on either the subject or the object, which would need to be cancelled against a corresponding feature of the complementizer.

In this example we use our structural rules in three places, only one of which corresponds to an application of Move in the corresponding minimalist style derivation. A fourth case is not represented here, mainly because we have presented the numeration in the order in which its contents would be used in a minimalist derivation. In the missing case, an entire feature complex would be moved to the point at which its first feature is used. This should also not be confused with syntactic movement, since it is in principle completely free of constraints, which only begin to apply once we have detached the first feature from the product or, in the case of a functor, applied it to its first argument. The other two cases are forced on us by our use of product types to represent lexical items with multiple features, and by the fact that the logical inference rules can only apply to adjacent, bracketed pairs of formulas. This creates a point of friction with the minimalist program as, for example, the Specifier-Head configuration, which is perhaps the paradigm case of a checking configuration in the minimalist program, does not form an appropriate environment for the application of the L\ rule.

One way to reduce this friction might be to adopt a multimodal approach with (at least) two products: one corresponding to “true” structure building, the other a “utility product” used for shuttling features around.

Another direction in which these simple ideas can be refined is suggested by the following. Consider how we might assign values to the proof terms in the goal sequent. At the moment, we would like the proof term associated with the consequent to represent the LF structure we have built. We will assign to the functor categories structure building functions. We use a variant of the notation used in Stabler (1996, forthcoming) for representing minimalist phrase structures. We use the symbols ⊲, >, ▶, ◀ to indicate which of two subexpressions is the head of the whole (the head is always greater than the nonhead), whether the configuration so formed is a checking configuration (closed triangles represent checking configurations) and whether the configuration is regarded as internal to the X0 or external to it (black triangles are head internal). In traditional terminology, ⊲ represents specifier attachment, > complement attachment and ◀ and ▶ represent prefix and suffix attachment, respectively. We prefer this notation to Chomsky’s set-theoretic notation at very least for readability reasons, but even more so, in the current context, because it treats all the interior nodes of a phrase structure tree as being labeled with operation symbols that essentially correspond to various sorts of headed concatenation operators. So this notation makes it clear that we are dealing with structures built up from lexical material by the application of product operators, though we will not develop the full fledged multimodal system that this promises in this preliminary investigation.

To arrive at the kinds of trees one finds in Stabler’s work, we simply install the first argument in the complement position and the remaining arguments in specifier positions. (We consider X0 internal positions below.) This would give us the following assignments for our two verb formulas, which are essentially structurally identical.

(D\V)/V : y_{1} = λu_{1}.λu_{2}.(u_{2} ⊲ (v_{1} > u_{1}))  (11)
(K\V)/D : y_{2} = λu_{1}.λu_{2}.(u_{2} ⊲ (v_{2} > u_{1}))  (12)

(We will use subscripted v’s and d’s as placeholders for whatever lexical information may need to be associated with the head position.) In light of these assignments, we can think of \ as the residual of the specifier attaching product ⊲ and / as the residual of the complement attaching product >. It is with an eye towards this move that we have presented a version of LP with slashes in both directions: normally, with permutation, these distinctions are irrelevant.

An interesting possibility presents itself when we consider how to assign proof terms to our product categories, the feature complexes D · K. We associate them with chains, that is,

(D · K)_{Subj} : ⟨x_{1}, x_{2}⟩ = ⟨t_{S}, d_{S}⟩,  (13)
(D · K)_{Obj} : ⟨x_{3}, x_{4}⟩ = ⟨t_{O}, d_{O}⟩.  (14)

This move is pretty much forced on us by a type logical perspective. The choice of a product type to represent bundles of formal features is the most natural way to accommodate the resource sensitive treatment of formal features in the minimalist program. But in turn the most natural way to treat a product type as a structure is, well, as a product, that is, a pair or more generally an n-tuple. Intuitively, if we have two types, we ought to have two things belonging to those types. The object which we think of as being both of type K and type D is a complex object, in other words, and the syntax cares about how it was made. In particular, those parts may be associated with different licensing heads, or with the same head but in different structural relations. So together with the procedural idea of feature driven movement we are given as its declarative counterpart the idea of a feature bearing chain.

Particularly interesting in this regard is the fact that the chain associated with a lexical item is, in fact, associated with the lexical item. That is, it is present in the derivation from the very beginning, even before the proof steps corresponding to movement have been executed. This idea, that chains can be formed “presyntactically,” is already present in the literature in work by Michael Brody (e.g., Brody 1995), though it does not seem to have received very much attention to date.^{2}

So, as the reader can readily verify, the proof term associated with the final VP works out to the following.

⟨d_{S}, (t_{S} ⊲ (v_{1} > (d_{O} ⊲ (v_{2} > t_{O}))))⟩  (15)

This structure, in which we simply pair an otherwise unattached expression with an otherwise complete tree, has no counterpart in standard syntax. It appears here because we could not use up all our lexical material in a single verb phrase, and because we have to package the consequent of our intuitionistic sequents into a single formula. Whether such a “storage construction” would ever find a use in ordinary syntax remains to be seen.

The main point to observe here is that, given a theory of feature driven movement, the movement potential of a given lexical item is largely given by its lexical makeup. This observation assimilates very nicely with the classical categorial observation that the combinatory potential of a lexical item is essentially given in advance by its syntactic category. And because it is embedded in a grammar logic, this idea receives immediately, via the Curry-Howard morphism, both a declarative and a procedural encoding.

Unfortunately, however appealing these observations may be, serious and immediate problems remain which suggest that there are important ways in which minimalist derivations are not like type logical deductions. In order to make something like Merge emerge in this deduction, we focused on a very particular sort of proof, which is not in fact very typical of proofs in LP and its cousins. Obviously, completely Cut-free proofs are also available. We could, for example, prove the theorem in (7) by first breaking up all lexical feature-complexes with applications of the L· rule, and then merging the individual features in with their licensing functors. However, this allows several other related theorems as well. One is just the version in which subject and object roles are switched and this is okay, we want that one. But another represents the illegal derivation in which we put t_{S} in Spec of the higher V, by cancelling the subject’s D feature there as before, and we put its “antecedent” d_{S} in Spec of the lower V, by permuting and reassociating the K feature rightwards.

2Note that Brody assumes that chains are copies of a phrasal structure; here we use traditional traces. In Cornell (1997) we consider chains as sequences of abstract syntactic positions rather than phrasal copies, and this is the syntactic theory that is really lurking in the background here.

We could rule this out by placing the traditional sort of c-command requirements on chains as they appear in our proof terms, but up until now we have not used our labeling algebra as a source of constraint; it is used solely to provide a declarative perspective on the derivation. Nor would this be an appropriate use of this constraining device: a lack of independence between derivation and representation spoils their correspondence by the same token. In any case it is a rather important claim of derivational minimalism that such conditions as the c-command condition are unnecessary when we are always adding to the tree at its root. Our Cut-based “derivational deduction” in (8)–(10) imposes just this sort of ordering constraint. As long as we are always combining two lexical formulas at a time, and as long as we use up all the features we can in each subproof then the ill formed chains observed above will simply never occur. However, we cannot simply stipulate that we are interested only in proofs of a certain kind, and still claim the benefits of working in a grammar logic.

We can construct at least a partial solution by making use of Moortgat’s unary modality operators ◇ and □^{↓}. (Cf. Moortgat (1996). The basic idea we use here is due originally to Morrill (1994).) The logical rules for this “unary product” and its residual are given below.

\begin{aligned}Δ[(A)^{◇}] ⇒ B \\ & L◇ \\ Δ[◇A] ⇒ B \end{aligned}  \begin{aligned}Δ[A] ⇒ B \\ & L□^{↓} \\ Δ[(□^{↓}A)^{◇}] ⇒ B \end{aligned}  (16)

\begin{aligned}Δ ⇒ A \\ & R◇ \\ (Δ)^{◇} ⇒ ◇A \end{aligned}  \begin{aligned}(Δ)^{◇} ⇒ A \\ & R□^{↓} \\ Δ ⇒ □^{↓}A \end{aligned}  (17)

We also make use of the following two “weak distributivity” postulates governing the interaction of the unary and binary modality.

\begin{aligned}Δ[((Γ_{1})^{◇}, Γ_{2})] ⇒ A \\ & K1 \\ Δ[((Γ_{1}, Γ_{2}))^{◇}] ⇒ A \end{aligned}  \begin{aligned}Δ[(Γ_{1}, (Γ_{2})^{◇})] ⇒ A \\ & K2 \\ Δ[((Γ_{1}, Γ_{2}))^{◇}] ⇒ A \end{aligned}  (18)

Suppose now that we revise our lexical type formulas so that the heads of functors are marked with a □^{↓}. We furthermore insist that every functor be contained in a (·)^{◇} bracketing which contains no other functor not contained in a smaller such bracketing. More simply: a ◇ must intervene between every pair of functor categories. Only certain such bracketings can lead to successful derivations, namely those which capture enough lexical material in their scope to cancel all antecedent features of the functor. Once we

D ⇒ D \begin{matrix}K ⇒ K \begin{matrix}etc. \\ V, W ⇒ V · W \end{matrix} ; L□^{↓} ; (□^{↓}V)^{◇}, W ⇒ V · W ; K1 ; (□^{↓}V, W)^{◇} ⇒ V · W \\ L\ \\ ((K, K\□^{↓}V), W)^{◇} ⇒ V · W \end{matrix} ; P, A ; (K\□^{↓}V, K, W)^{◇} ⇒ V · W ; L· ; (K\□^{↓}V, K · W)^{◇} ⇒ V · W L/ (((K\□^{↓}V)/D, D), K · W)^{◇} ⇒ V · W A ((K\□^{↓}V)/D, D, K · W)^{◇} ⇒ V · W L· ((K\□^{↓}V)/D, D · K · W)^{◇} ⇒ V · W

Figure 2: A derivation within a domain of freedom.

have managed to cancel all the antecedent features of the functor, possibly after some application of K1 or K2, we will be able to apply the L□^{↓} rule to remove the modals, now that their work is done. The point of this operation is that the ◇ modal effectively seals off its scope from the application of A or P. Now the entire subconstruction can be permuted or reassociated, and its contents can also move freely within the scope of the operator, but structural rules, limited to binary contexts, cannot apply across this unary barrier. Then the embedded □^{↓} operator functions as a key to unlock this barrier, but a key which can only be accessed once all the other features of the head have been used up. In figure 2, we assume that the object is a Wh phrase, to illustrate the use of the K1 rule.

This is a step in the right direction. However, it involves considerable use of force, since now we must assume a degree of structure in the numeration which is apparently not required in ordinary minimalist derivations. In fact, the ◇ domains have essentially the effect of selecting a particular order of processing for elements in a numeration, so the freedom of choice that is supposed to hold in the introduction of numeration items into the derivation is lost. To some extent all of this control information is lexically based, by virtue of the fact that every ◇ must balance against a □^{↓}. Still it does not appear to us as neat a solution to the problem of control as the minimalist requirement that all transformations should extend their target, and work remains to be done.

Let us turn now to problems posed by head movement constructions. We take as our example here an artificial language, the “copy language” over the alphabet {0, 1}. We will derive the strings of this (non-context free) language using head movement in a minimalist derivational style. The idea is to simulate in this artificial language the formation of head (e.g., verb) clusters in natural languages. These are supposed to pose serious problems for representational variants of GB and minimalism, and so they are of special interest in the study of the relations between derivational and representational approaches.

We will assume, as a point of departure, a theory in which head movement is triggered by the selectional requirements of the host head. As overt XP movement is triggered by strong formal features, we will follow Stabler (following Koopman 1994) in treating overt head movement as triggered by strong selection features. A theory of selection is conspicously missing from Chomsky (1995). Merge is supposed to be free to apply at any time, and is not required to cancel any features. To achieve a more uniformly resource-conscious theory we have been tacitly assuming all along a categorial style theory of selection to go with our minimalist style theory of attraction. Up to this point those systems have been essentially modular: selection is concerned with categorial features and attraction with “inflectional” features like case. Here, however, those systems overlap, and not without some tricky formal problems.

For our lexicon for the copy language we make use of four atomic features, {S, F, A, B}. From these we construct the following lexical items, with term assignments as given.

S/F : λu_{1}.((ϵ ▶ π_{1}u_{1}) > π_{2}u_{1})  (19)
((A\F)/F)_{i} : λu_{1}.λu_{2}.⟨(u_{2} ⊲ (t_{i} > π_{1}u_{1})), (0 ▶ π_{2}u_{1})⟩  (20)
((B\F)/F)_{i} : λu_{1}.λu_{2}.⟨(u_{2} ⊲ (t_{i} > π_{1}u_{1})), (1 ▶ π_{2}u_{1})⟩  (21)
F_{i} : ⟨t_{i}, ϵ⟩  (22)
A : 0  (23)
B : 1  (24)

The strings of the copy language will be the yield of the proof terms for category S. Intuitively, the various F categories form a recursive spine, with A and B specifiers which “agree” with their heads on the symbol they dominate. We consider all antecedent occurrences of F to be strong selectors. This has the effect of cyclically extracting every second occurrence of a 1 or 0 and collecting them under the head of the matrix S.

As usual the terms associated with nonfunctors are chains. Up until now, however, the length of the chain has been a function of the number of features in the type or, to put it the other way around, the type formula has accurately reflected the structure of the chain: a chain is a tuple, so its type is a tuple. Here we have a proof object with the formal properties of a nontrivial chain but which is assigned a single type. This works because of the tight connection between complement taking and complex head formation. For example, Stabler (1996) treats them as part of the same algebraic operation.

So now, for example, the following is an NL theorem, that is, we could derive it even in the absence of any structural rules.

{S/F \atop y_{1}} , {A \atop x_{1}} , {(A\F)/F \atop y_{2}} , {B \atop x_{2}} , {(B\F)/F \atop y_{3}} , {F \atop x_{3}} ⇒ {S \atop y_{1}(y_{2}(y_{3}(x_{3})(x_{2}))(x_{1}))}  (25)

With the term assignment in (19)–(24) this evaluates to the following, which yields the string 0101.

((ϵ ▶ (0 ▶ (1 ▶ ϵ))) > (0 ⊲ (t_{0} > (1 ⊲ (t_{1} > t_{ϵ})))))  (26)

It might be preferable from a formal standpoint to make our treatment of head chains more consistent with our treatment of XP chains. That is, if there are two elements of the head chain, each should have a type, a grammatical resource which is used in the construction of that chain. The problem is that there is no compelling theory of head movement which identifies it with some feature distinct from the category of the head. For the moment we will propose a formal solution in advance of any theory, using X as our mystery feature (which might well simply be a second copy of F). In this setting we no longer require projection functions in our proof terms: in a derivation, the head chain is broken up by L· as with XP chains. However, now the sequent corresponding to (25) no longer has a proof in NL: we require associativity to reassociate a feature from the rest of its lexical bundle to the functor against which it cancels.

(S/X)/F : λu_{1}.λu_{2}.((ϵ ▶ u_{2}) > u_{1})  (27)
(((A\(F · X))/X)/F)_{i} : λu_{1}.λu_{2}.λu_{3}.⟨(u_{3} ⊲ (t_{i} > u_{1})), (0 ▶ u_{2})⟩ (28)
(((B\(F · X))/X)/F)_{i} : λu_{1}.λu_{2}.λu_{3}.⟨(u_{3} ⊲ (t_{i} > u_{1})), (1 ▶ u_{2})⟩ (29)
(F · X)_{i} : ⟨t_{i}, ϵ⟩  (30)
A : 0  (31)
B : 1  (32)

We must distinguish features which attract heads from features which attract phrases. As with ⊲ and >, then, we might treat the / over the X feature as the residual of the suffix attaching ▶ product. Then a tuple of features corresponds to two chains, whose members are interleaved; but the two distinct chains are easily recovered by considering the type of each link. One further point about the representation of chains needs to be made: the initial position of the X0 chain is always embedded in the XP. So in fact each of the 2-tuples depicted above represent at once a one-position XP chain and a two-position X0 chain.

We have at various points alluded to a multimodal version of this system, which is lurking behind the structure forming operators of the term algebra. Such a system would give us much more detailed control over derivations, control which we will probably need to deal with locality problems adequately. But this system is clearly going to be quite complex. One needs four products for the structure forming operations, a lexical product, for forming chains, and a “utility” product for converting checking configurations like Spec-Head to pairs which can trigger a L/ rule. These various products interact in very complex ways, and much of the complexity has to do with low-level details, like overcoming the structural distance between a specifier and its head, which are not of much linguistic interest. Therefore we thought it best to start with the simplest ideas, since these already present us with a good collection of hard problems to solve. Nonetheless it is already fairly clear in what directions these simple ideas can be elaborated. We can continue to follow the basic technique of using the desired structures as proof terms, gradually unpacking them so that less of the syntax is done there and more is done in the type system. In effect, we follow a model theoretic program in which the proof terms represent the structures we desire to isolate and reason about, and we develop linguistic and proof theoretic resources to accomplish this. However, the flow of ideas is not at all oneway. For example, it is the resource-consciousness of the proof system that suggests the necessity of Brody-style presyntactic chain formation.

References

Brody, M. (1995). Lexico-Logical Form, MIT Press, Cambridge, MA.

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

Cornell, T. (1997). Representational minimalism, Technical Report 83, SFB 340, University of Tübingen.

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

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

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

Stabler, E. P. (1996). Derivational minimalism, Proceedings of LACL-96, Nancy, France.

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