Maxime Amblard
email: amblard@loria.fr

Encoding Phases using Commutativity and Non-commutativity in a Logical Framework

Keywords: type theory, syntax, linguistic modeling, generative theory, phase, Partially Commutative Logic

HAL is a

Generative theory has undergone many changes since Chomsky's Syntactic Structures [START_REF] Chomsky | Syntactic Structures[END_REF] leading up to what is the Minimalist Program (MP) [START_REF] Chomsky | The Minimalist Program[END_REF]. The most frequent criticism made is certainly the non-computational and non-formal nature of such an approach. It is nevertheless rich of a vast literature for the linguistic approach. Fundamentals to the MP are the description of a main calculus which takes into account the syntax, and the production of two forms: one supposed to reflect the sequence of words, and another one for the semantic structure of the utterance. Following the MP, Chomsky claims the identification of phases in the syntactic derivation [START_REF] Chomsky | Derivation by phase. ms[END_REF]. The verb, the main driving force of the analysis, is being transformed, opening the possibility of specific modifications, especially the definition of the Phase Impenetrability Condition (PIC).

The first proposal of formalization for MP was made by Stabler in [START_REF] Stabler | Derivational minimalism[END_REF]. However, this formulation is far from the usual Montagovian approach of semantics. Therefore, translations of this formulation into logic systems have been proposed, in particular [START_REF] Lecomte | Extending Lambek grammars: a logical account of minimalist grammars[END_REF], [START_REF] Lecomte | Categorial grammar for minimalism[END_REF]. Much has been done, exploiting Curry's distinction between the tectogrammatical and the phenogrammatical levels, and this has led to interesting proposals [START_REF] Morrill | Type logical grammar[END_REF], [START_REF] De Groote | Towards abstract categorial grammars[END_REF], [START_REF] Muskens | Languages, lambdas and logic[END_REF], [START_REF] Pollard | Convergent grammars[END_REF]. The latest proposals of extension defined the MCG based on a fragment of Partially Commutative Logic (PCL) [START_REF] Amblard | Calcul de représentations sémantiques et syntaxe générative: les grammaires minimalistes catégorielles[END_REF], [START_REF] Amblard | Categorial minimalist grammars: from generative syntax to logical forms[END_REF]. The authors highlighted the simultaneous need of commutative and non-commutative properties to produce a useful framework .

In this paper, we propose a reconsideration of the properties of commutativity and non-commutativity in MCG to account the concept of phase introduced by Chomsky. Due to space consideration, we will limit ourselves to the problems of parsing, leaving aside the semantic aspects. However, it should be noted that the syntax-semantics interface of MCG contains all the necessary material for its integration.

We first discuss the need for the two different relations in MCG. Then, we define Minimalist Categorial Grammars (MCG). Based on these definitions, the third section presents and encodes phases in MCG, and shows the implementation of the PIC using only logical properties.

Commutativity vs Non-Commutativity in Standard MCG and Phases

To link logic and Generative Theory, MCG's derivations are proofs of a restriction of Partially Commutative Logic (PCL), [START_REF] Retoré | Pomset logic: a non-commutative extension of classical linear logic[END_REF], seen as syntactic representations in generative theory. This logic is an extension of Lambek calculus containing simultaneously commutative and non-commutative connectives (ie introduction and elimination of implication and tensor). To handle the different relations between hypotheses in the same framework, an entropy rule (restriction of order) is added. Moreover, [START_REF] Amblard | Natural deduction and normalisation for partially commutative linear logic and lambek calculus with product[END_REF] shows a weak normalization of this calculus, to produce regular analysis in MCG. All definitions of these grammars are given in [START_REF] Amblard | Calcul de représentations sémantiques et syntaxe générative: les grammaires minimalistes catégorielles[END_REF] 1 , with a composition of rules (note that according to these definitions, normalisation is strong). Moreover, this restriction does not use introduction of hypothesis. They appear in the derivation only from specific lexical entries: in the hypotheses of a given category and that category as a formula. The lexicon will contain the entry φ ⊢ φ with φ as a given category.

The concrete part of the proof is achieved by a merge whose heart is the elimination of / or \ (rules that are found in different versions from categorial grammars , [START_REF] Lambek | The mathematics of sentence structures[END_REF], [START_REF] Steedman | Combinatory grammars and parasitic gaps[END_REF] [16]) plus the entropy rule. This is one point where commutativity and non commutativity play a crucial role. In particular, for the word order, it is clear that the relation is non-commutativite: being on the right or the left of a given word could not just be the same. Non-commutativity is also needed here, because of the second rule in MCG.

The hypotheses are seen as special position markers in the sequence of hypotheses of the proof. They are considered as resources of prominent features related to a phrase. They are unloaded by using the move operation of the generative theory. A direct implication is that the sequence of hypotheses in the proof contains exactly the sequence of available resources for further derivation. In this case, this sequence is a collection of resources and could not be a strict list. Unless a canonical order on the sequence of applied rules is presupposed, the only way to express this is with non-commutativity. The Merge rule must contain a release of the order. Definitions of basic rules of MCG involve commutativity and non-commutativity. We will show how we could use these properties in another perspective to encode a linguistic concept, more precisely by noting that the changing category of the verb controls the process flow.

Chomsky's theory introduces the notion of phase, which corresponds to the evolution of the verb. Thus, we assume that the lexical item associated with the verb carries only part of its achievement in the sentence. This is an important use in the syntaxsemantic interface for reporting UTAH 2 . The needed hypothesis to introduce a DP is provided by verb lexical items. And this is the correspondence of verb's resources with the DP category which allows the DP to be in the proof.

In the phase's definition, Chomsky assumes that some instance of move (unification of features in our formalism) must be completed before the end of the phase. Once it is reached, the specific resources of the process are no longer accessible to the rest of the analysis. It defines an island in the analysis, called Phase Impenetrability Condition (PIC). Translating this definition into our formalism implies that a phase (or its representation) block access to part of the sequence of hypotheses of the proof. We assume that the interpretation in MCG is a non-commutative point in the sequence of hypotheses.

The direct implication is that the analysis of a sentence simultaneously uses relations to link noun and verb phrases, and non-commutative relations to construct the analysis (changing the category of the verb). The use of non-commutativity involves a strict order to control the verb's role in the analysis. Formal properties used by items of different categories are disjointed and it allows to fully exploit their relations.

Minimalist Categorial Grammars

Minimalist Categorial grammars are based on a fragment of PCL to encode the MP of Chomsky. Then it uses an abstract calculus to produce both a string (sequence of words) and a semantic representation (formula). Word order and semantics are synchronized over the main calculus which uses a structured lexicon and specific rules. First, we briefly present rules of PCL, then we introduce labels which encode word order, then we define lexical items and finally introduce rules of MCG.

Partially Commutative Logic (PCL)

The logic introduced in [START_REF] De Groote | Partially commutative linear logic: sequent calculus and phase semantics[END_REF] and extended in [START_REF] Retoré | A description of the non-sequential execution of petri nets in partially commutative linear logic[END_REF] is a superimposition of the Lambek calculus (Intuitionistic Non-Commutative Multiplicative Linear Logic) and Intuitionistic Commutative Multiplicative Linear Logic. Connectives are:

-the Lambek calculus connectives: ⊙, \ and / (non-commutatives) -commutative multiplicative linear connectives: ⊗ and ⊸ (commutatives)

The use of these connectives is presented in figure 1.

In this logic, commutative and non-commutative relations could be used simultaneously. Then contexts are partially ordered multisets of formulae and in order to relax this order, we need an entropy rule noted ⊏ which is defined as the replacement of ; by ,. The restriction of elimination rules and the entropy rule is called Minimalist Logic (the logic used to define MCG). In the following, we note F the set of categories (F stands for features).

Γ ⊢ A ∆ ⊢ A\C [\e] < Γ ; ∆ >⊢ C ∆ ⊢ A/C Γ ⊢ A [/e] < ∆; Γ >⊢ C Γ ⊢ A ∆ ⊢ A ⊸ C [⊸e] (Γ, ∆) ⊢ C < A; Γ >⊢ C [\i] Γ ⊢ A\C < Γ ; A >⊢ C [/i] Γ ⊢ C/A (A, Γ ) ⊢ C [⊸i] Γ ⊢ A ⊸ C ∆ ⊢ A ⊙ B Γ, < A; B >, Γ ′ ⊢ C [⊙e] Γ, ∆, Γ ′ ⊢ C ∆ ⊢ A ⊗ B Γ, (A, B), Γ ′ ⊢ C [⊗e] Γ, ∆, Γ ′ ⊢ C ∆ ⊢ A Γ ⊢ B [⊙i] < ∆; Γ >⊢ A ⊙ B ∆ ⊢ A Γ ⊢ B [⊗i] (∆, Γ ) ⊢ A ⊗ B [axiom] A ⊢ A Γ ⊢ C [entropy -whenever Γ ′ ⊏ Γ ] Γ ′ ⊢ C

Labels encoding word order

Derivations of MCG are labelled proofs of the PCL. Before defining labelling, we define labels and operations on them. To do this, we use the set of phonological form P h and a set V of variables such that: P h ∩ V = ∅. We note T the union of P h and V . We define the set Σ, called labels set as the set of triplets of elements of T * . Every position in a triplet has a linguistic interpretation: they correspond to specifier/head/complement relations of minimalist trees. A label r will be considered as r = (r s , r h , r c ).

We introduce variables in the string triplets and a substitution operation. They are used to modify a position inside a triplet by a specific material. Intuitively, this is the counterpart in the phonological calculus of the product elimination.

A substitution is a partial function from V to T * . For σ a substitution, s a string of T * and r a label, we note respectively s.σ and r.σ the string and the label obtained by the simultaneous substitution in s and r of the variables with the values associated by σ (variables for which σ is not defined remain the same).

If the domain of definition of a substitution σ is finite and equal to x 1 , . . . , x n and σ(x i ) = t i , then σ is denoted by [t 1 /x 1 , . . . , t n /x n ]. Moreover, for a sequence s and a label r, s.σ and r.σ are respectively denoted s[t 1 /x 1 , . . . , t n /x n ] and r[t 1 /x 1 , . . . , t n /x n ]. Every injective substitution which takes values in V is called renaming. Two labels r 1 and r 2 (respectively two strings s 1 and s 2 ) are equal modulo a renaming of variables if there exists a renaming σ such that r 1 .σ = r 2 (resp.

s 1 .σ = s 2 ).
Finally, we need another operation on string triplets which allows to combine them together: the string concatenation of T * is noted •. Let Concat be the operation of concatenation on labels which concatenates the three components in the linear order:

for r ∈ Σ, Concat(r) = r s • r h • r c .
We then have defined a word order structure which encodes specifier/complement/head relations and two operations (substitution and concatenation). These two operations will be counterparts in the phonological calculus of merge and move.

Labelled proofs. Before exhibiting the rules of MCG, we need to define the concept of labelling on a subset of rules of the Minimalist Logic (\ e , / e , ⊗ e and ⊏).

For a given MCG G, let a G-background be x : A with x ∈ V and A ∈ F , or

G 1 ; G 2 or else (G 1 , G 2 )
with G 1 and G 2 some G-backgrounds which are defined on two disjoint sets of variables. G-backgrounds are series-parallel orders on subsets of V × F . They are naturally extended to the entropy rule, noted ⊏. A G-sequent is a sequent of the form:

Γ ⊢ G (r s , r t , r c ) : B where Γ is a G-background, B ∈ F and (r s , r t , r c ) ∈ Σ.
A G-labelling is a derivation of a G-sequent obtained with the following rules:

Γ ⊢ G r 1 : A ⊗ B ∆[x : A, y : B] ⊢ G r 2 : C V ar(r 1 ) ∩ V ar(r 2 ) = ∅ A ∈ P 2 [⊗ e ] ∆[Γ ] ⊢ G r 2 [Concat(r 1 )/x, ǫ/y] : C Γ ⊢ G r : A Γ ′ ⊏ Γ [⊏] Γ ′ ⊢ G r : A
Note that a G-labelling is a proof tree of the Minimalist Logic on which sequent hypotheses are decorated with variables and sequent conclusions are decorated with labels. Product elimination is applied with a substitution on labels and implication connectors with concatenation (a triplet is introduced in another one by concatenating its three components).

Lexicon

MCG encodes informations in the lexicon with types. They are defined over two sets, one of linguistic categories and the other of move features. Lexical items associate a label and a formula of PCL with respect to the following grammar:

L ::= (B) / P 1 | C B ::= P 1 \ (B) | P 2 \ (B) | C | D C ::= P 2 ⊗ (C) | C 1 D ::= P 2 ⊙ (D) | C 1 C 1 ::= P 1
where L is the starting non-terminal and P 1 and P 2 are atomic formulae belonging to set of features of the MCG (features which trigger merge or move rules).

Formulae of lexical items get started with a / as the first connective, and continue with a sequence of \. This corresponds to the sequence of selectors and licensors in MG lexical items. These are trigger rule features of MCGs. They give the concrete part of the derivation. A formula is ended with an atomic type, the category of the phrase, or a sequence of ⊙ (which contains at least a specific type, which is also the main category).

For example, the following formula could be the one of an MCG entry:

(d \ h \ j \ k \ (a ⊗ b ⊗ c)) / m, whereas this is not : (d \ h \ j \ k \ (a ⊗ b ⊗ c)) / m /
p, because it has two /. These formulae have the following structure :

(c m \ . . . \c 1 \(b 1 ⊗ . . . ⊗ b n ⊗ a))/d with a ∈ P 1 , b i ∈ P 2 , c j ∈ P and d ∈ P 1 .
The morphism from MG lexicon to MCG ones is defined in [START_REF] Amblard | Calcul de représentations sémantiques et syntaxe générative: les grammaires minimalistes catégorielles[END_REF].

Rules of MCG

In the same way as for MG, [START_REF] Stabler | Derivational minimalism[END_REF], rules of MCG are defined over two principles:

-combining two pieces of derivation: merge -redefining internal relations in a derivation: move

As we have mentioned before, MCG is defined over a restriction of PCL: elimination of / and \, and ⊗. In the following, in order to distinguish relations in the sequence of hypotheses, a commutative relation will be marked with ',' and a non-one with ';'.

-Merge is the function which combines two pieces of proofs together and it needs an non-commutative relation to correctly encode relations among words. But in the same application, merge will also combine hypothesis of different proofs. And from a linguistic point of view, relations between these hypothesis should be commutative because there is no reason to block access to them. Then, merge combines an elimination of \ or / with the application of an entropy rule. For the same linguistic reasons as in MG, MCG use two different kinds of merge depending on the lexical/non-lexical status of the trigger. For the word order, merge is simply the concatenation of the string of one phrase in the label of the other one (depending of right/left relation): Lexical trigger:

⊢ (r s , r h , r c ) : A / B ∆ ⊢ s : B [/ e ] ∆ ⊢ (r s , r h , r c • Concat(s)) : A [entropy] ∆ ⊢ (r s , r h , r c • Concat(s)) : A =⇒ ⊢ (r s , r h , r c ) : A / B ∆ ⊢ s : B [mg] ∆ ⊢ (r s , r h , r c • Concat(s)) : A
A merge with a lexical item do not explicitly show the order between hypotheses. But here, the entropy rule is the replacement of a ; by a , Non-lexical trigger:

∆ ⊢ s : B Γ ⊢ (r s , r h , r c ) : B \ A [\ e ] ∆; Γ ⊢ (Concat(s) • r s , r h , r c ) : A [entropy] ∆, Γ ⊢ (Concat(s) • r s , r h , r c ) : A =⇒ ∆ ⊢ s : B Γ ⊢ (r s , r h , r c ) : B \ A [mg] ∆, Γ ⊢ (Concat(s) • r s , r h , r c ) : A -The encoding of Move in MCG is structurally different from the one in MG.
Here, it assumes that a phrase is included in the proof if and only if all its hypotheses are. Then, we do not really reinterpret the local tree as in MG, but we directly produce the final derivation tree. In this way, a move is the discharge of hypotheses by a ⊗.

For word order, the concatenation of the moved phrase is substituted in the position of the newest hypothesis:

Γ ⊢ r 1 : A ⊗ B ∆[u : A, v : B] ⊢ r 2 : C [mv] ∆[Γ ] ⊢ r 2 [Concat(r 1 )/u, ǫ/v] : C
Finally, to give account of [START_REF] Stabler | Recognizing head movement[END_REF], the framework is enriched with rules which modifies the position of the string in the label. There are two kinds of rules:

-head movement where the head of the merged element is concatenated in the final head. This implies four rules: two to distinguish left and right concatenation and two over the lexical status of the trigger of merge. -Affix hopping where the head of the trigger is concatenated with the head of the merged element. In the same way, there are four rules to distinguish left from right concatenations and lexical status of the trigger.

We use a simple way to encode the different possibilities of merging with < and >. Pointing to the connective indicates head-movement and outside defines affix hopping. The lexical status does not need to be represented. In the following of this paper, only head movement will be used, thus we give this four rules:

Head-Movement: Γ ⊢ (r spec , r tete , r comp ) : A / < B ∆ ⊢ s : B [mg] Γ, ∆ ⊢ (r spec , r tete • s tete , r comp • Concat(s -tete )) : A Γ ⊢ (r spec , r tete , r comp ) : A > / B ∆ ⊢ s : B [mg] Γ, ∆ ⊢ (r spec , s tete • r tete , r comp • Concat(s -tete )) : A ∆ ⊢ s : B Γ ⊢ (r spec , r tete , r comp ) : B > \ A [mg] ∆, Γ ⊢ (Concat(s -tete ) • r spec , s tete • r tete , r comp ) : A ∆ ⊢ s : B Γ ⊢ (r spec , r tete , r comp ) : B \ < A [mg] ∆, Γ ⊢ (Concat(s -tete ) • r spec , r tete • s tete , r comp ) : A 3 Phases

Encoding Phases in MCG

Following [START_REF] Chomsky | Derivation by phase. ms[END_REF], Chomsky assumes that the analysis of a sentence is driven by the verb which goes by two specific states: the phases VP and cP. Note that neither tP nor the decomposition over simple verb form as it is used in usual MCG are phases (this is illustrated in figure 2). Moreover, Chomsky claims that syntactic islands are defined by phases. That is, the content of a phase must be moved to its left-hand side in order to let it accessible. This step of the phase is called a transfer. According to this structure, items on the right side of the phase can not be moved again. This syntactic island is called the Phase Impenetrability Condition (PIC). The definition of phases and the PIC are still under debate. Nevertheless, an interesting point for MCG is the simultaneous use of commutative and non-commutative properties of the framework to recognize them.

According to Chomsky, a phase is a node of the syntactic tree which triggers allowed moves. Because it is a node, this implies for MCG to combine two subproofs. It is not possible to simulate this with a single lexical item (which implies a terminal node). Also transfering is the realization of possible moves and the direct linking of hypotheses in a cyclic move.

Another argument in support of phases is in the semantic counterpart. This article does not present this second synchronized part of the calculus in MCG. Many different works claim that at particular step of the verb derivation some specific thematic roles could be assigned as in [START_REF] Hale | On argument structure and the lexical expression of syntactic relations[END_REF], [START_REF] Kratzer | External arguments[END_REF] and [START_REF] Baker | Thematic Roles and Syntactic Structure[END_REF]. [START_REF] Amblard | Calcul de représentations sémantiques et syntaxe générative: les grammaires minimalistes catégorielles[END_REF] and [START_REF] Lecomte | Semantics in minimalist-categorial grammars[END_REF] describe both arguments for this and the semantic tiers according to these assumptions. But, they do not include the idea of phases. Only remarks that simplification of derivation requires specific points in which continuation reductions must occur. We leave the presentation of consequences of phases on semantics to future works.

The analysis of a simple sentence derivation in standard MSG uses 4 items. In the following, the verb read will be used to illustrate this presentation for a simple active affirmative sentence.

1. The deep syntactic build of the verb: the verb and all its arguments (except the subject). ⊢ v / < d 2. Mode: introduces the subject category and, at least, the accusative case.

⊢ k \ d \ V / < v 3. Inflection: brings the inflection to the verb.

⊢ k \ t / < V 4. Comp: fully completes the analysis (a question mark, insert in relative clause, etc.) ⊢ c / t

In order to keep control on the string associate to the verb, the derivation systematically uses head movement except comp which ends the derivation. We claim that phases can be encoded in MCG with a non-commutative order. The lexical realization of a phase item explicitly contains hypotheses in a non-commutative order.

∆ 1 , H 1 ; H 2 ∆ 2 ⊢ A (1)
This order makes a strong boundary in the derivation of the phase. It blocks move of elements in complement position to specifier. These are the only items that are lexically built with hypothesis different from the original definition of MCG [START_REF] Lecomte | Extending Lambek grammars: a logical account of minimalist grammars[END_REF], [START_REF] Amblard | Calcul de représentations sémantiques et syntaxe générative: les grammaires minimalistes catégorielles[END_REF] and [START_REF] Amblard | Categorial minimalist grammars: from generative syntax to logical forms[END_REF]. Using the ⊙ e rule of the PCL, the phase rule is defined as:

∆ s , ∆ h , ∆ c ⊢ (s s , s h , s c ) : X ⊙ Y Γ s , X; Y, Γ c ⊢ (r s , r h , r c ) : Z [phase] Γ s , ∆ s , ∆ h ⊢ (r s • s s , r h , s h • s c • r c ) : Z
The phase rule is the combination of a discharge of hypothesis in non-commutative order and a transfer step. This transfer is the realization of all possible moves and parts of cyclic ones. This new rule assembles several individual rules of PCL proof. It may be difficult to follow the derivation step by step. In the following, phases are given with more details. Thus, we note [phase 1 ] the substitution part of the phase (the use of ⊙ e which combines two proofs) and [phase trans ] moves which can be achieved after [phase 1 ]. The main condition to validate a phase is ∆ c and Γ c are empty after [phase trans ]. This correspond to a phrase in complement position of a phase does not stand accessible. We note MCG phase , MCG wit phases.

There is a direct consequence of this encoding of phase on the structure of the lexical item Hypotheses on its left-hand side of take the place of the complement of the head. Thus, all elements with which it should be combined must be in a specifier position. A more complex formula as in (1) will be built only with \ :

∆ 1 , H 1 ; H 2 ∆ 2 ⊢ (s s , s h , s c )B n \ . . . \ B 0 \ A (2)
To take into account of the definition of the phases theory and the proposed encoding in MCG, a simple sentence will be divided into two phases: one with the mode and another with comp. Their lexical items are modified in this way into:

-mode: ⊢ k \ d \ V / v ⇒ V ; v ⊢ k \ d \ V -comp: ⊢ c / t ⇒ c; t ⊢ c
Hypotheses on the left-hand side of formulae receive a straightforward interpretation. They correspond to the conversion of a proof of a v to a proof of a V (or from a t to a c in the second one). Thus, we need to update the two other formulae in order to combine them with the two previous ones:

-verb: ⊢ v / d ⇒ ⊢ (V ⊙ v) / d -inflection: ⊢ k \ t / V ⇒ ⊢ k \ (c ⊙ t) / V
Note that the use of ⊙ in a formula do not imply that this item is one of a phase. It means that they take an active part in the construction of the verb. Here, we have extended the main category of the item to the previous one, combined with the category of the following phase category with a ⊙.

In fact, each head item drives a specific part of all elements are included under their relation to the head. But, the unloading of hypotheses (the realization of the phase) occurs later. Here, the logical account of the framework updates the derivation in a way that there is no direct intuition with the syntactic tree. We present a simple example of interpretation of a phase in a proof into a tree: on one hand the starting part of the derivation and on the other the proof which results in the phase:

⊢ (A ⊙ B) / C C ⊢ C [mg] C ⊢ (A ⊙ B) A; B ⊢ D \ E D ⊢ D [mg] D, A; B ⊢ E Which correspond to the two following syntactic trees: < ¨¨¨¨r r r r ⊢ (A ⊙ B) / C C ⊢ C > ¨¨¨¨r r r r r D ⊢ D < ¨¨¨¨r r r r A; B ⊢ D \ E ǫ
The syntactic tree of the phase is not a simple leaf but a tree with an empty position in which the other derivation is substitued:

> ¨¨¨¨r r r r r D ⊢ D < ¨¨¨¨r r r r A; B ⊢ D \ E < ¨¨¨¨r r r r ⊢ (A ⊙ B) / C C ⊢ C
And it is clear that all information derived in the second tree before the phase combination must be updated after. Finally, for the same reasons as for merge, Head Movement and Affix Hopping are needed through the phase. The same connectives are used with the same effects. One instance is:

∆ s , ∆ h , ∆ c ⊢ (s s , s h , s c ) : X ⊙ < Y Γ s , X; Y, Γ c ⊢ (r s , r h , r c ) : Z [phase] Γ s ∆ s , ∆ h ⊢ (r s • s s , s h • r h , s c • r c ) : Z
where the head of the triplet is the concatenation of the two heads. The following section presents an application of this rules in a full analysis of a simple sentence.

Derivation of a simple sentence

To illustrate derivation with phases, this section presents the complete derivation of a simple sentence. However, extending the analysis to more complex syntactic structures has resulted in defining the lexical entries corresponding with the same principles. We present the analysis of the following example:

(1) The children read a book. This simple sentence uses the affirmative form, the verb will take the four previous steps. In order to build noun phrase with MCG with generative theory, we combine a determiner ⊢ (k ⊗ d) / n with a noun ⊢ n. It produces a constituent of category d (for determinal phrase) which lacks the assignment of syntactic case (k). Then, the following lexicon is used:

articles ⊢ (ǫ, the, ǫ) : k ⊗ d / n ⊢ (ǫ, a, ǫ) : k ⊗ d / n noun ⊢ (ǫ, chlidren, ǫ) : n ⊢ (ǫ, book, ǫ) : n verb ⊢ (ǫ, read, ǫ) : (V ⊙ v) < / d (mode) V ; v ⊢ (ǫ, ǫ, ǫ) : k \ d \ V (inf lection) ⊢ (ǫ, -, ǫ) : k \ (c ⊙ t) / < V (comp) c; t ⊢ (ǫ, ǫ, ǫ) : c
The derivation is a proof, so each main element (the head of each phrases) drives its subproof. The consequence is that the proof is built in several parts adjusted against each other by the discharge of hypotheses. This property makes the presentation more complex, but the search for proofs (i.e. the parsing) could be done in parallel. In the following, each verb step is presented. Note that the normalization of PCL from [START_REF] Amblard | Natural deduction and normalisation for partially commutative linear logic and lambek calculus with product[END_REF] ensures that we could combine each step one by one as presented here.

Step 1 In the first verb step of the derivation, the first position of the verb is saturated by a hypothesis of category d. It corresponds to the position of the main component that occupies the object position in the sentence. The object is not directly inserted in the derivation because all its features are not yet marked by hypotheses: the position of k (mark of the syntactic case assignment3 ) is missed. This is a departure from MG, in which all phrases are directly inserted in the derivation. Here, we only mark positions for insertion.

⊢ (ǫ, read, ǫ) : (V ⊙ v) < / d d ⊢ (ǫ, u, ǫ) : d [mg] d ⊢ (ǫ, read, u) : (V ⊙ v)
This is the end of the first verb step. The result must be inserted in another proof which contains hypothesis V and v. On one hand, the interpretation of the non-commutative relation between V and v in the type could be the saturation of all arguments of an element of type v to produce a V .

Step 2 These hypotheses are in the proof driven by the second entry of the verb: mode which ends the first phase. First, we need to saturate all positions of mode with lexical hypothesis, and then we could:

1. combine the result with the first verb step, 2. introduce the object of the sentence with a move in the transfer part of the phase.

The lexical item of mode is merged with a hypothesis k and next a d:

d ⊢ (ǫ, w, ǫ) : d k ⊢ (ǫ, v, ǫ) : k V ; v ⊢ (ǫ, ǫ, ǫ) : k \ d \ V [mg] k, V ; v ⊢ (v, ǫ, ǫ) : d \ V [mg] d, k, V ; v ⊢ (w v, ǫ, ǫ) : V
At this point of the derivation, this result is combined with the first verb step with a [phase] with head movement. Note that the string of the head of the discharged is concatenated to the string of the head position in order to keep all structural information over the verb accessible to the full derivation. The substitution part of the phase produces:

d ⊢ (ǫ, read, u) : (V ⊙ v) < d, k, V ; v ⊢ (w v, ǫ, ǫ) : V [phase 1 ] d, k, d ⊢ (w v, read, u) : V
Before ending the phase, we perform a move with all positions of the utterance's object (they are now in the proof). Then it could be introduced in the derivation with a transfer. In parallel, the determiner phrase is built with the two lexical entries "a" and "book" by a merge:

⊢ (ǫ, a, ǫ) : (k ⊗ d) / n ⊢ (ǫ, book, ǫ) : n [mg] ⊢ (ǫ, a, book) : k ⊗ d
Thereby, it is discharged in the main proof. The choice of the d with which to carry out the unloading is not left by chance. The derivation must be continued with the one which empties the previous verb step with a move. This is exactly the interpretation of transfer part in [START_REF] Chomsky | Derivation by phase. ms[END_REF].

⊢ (ǫ, a, book)

: k ⊗ d d, k, d ⊢ (w v, read, u) : V [phase trans ] d ⊢ (w a book, read, ǫ) : V
This move substitute in the newest variable as define in [START_REF] Amblard | Calcul de représentations sémantiques et syntaxe générative: les grammaires minimalistes catégorielles[END_REF]. It is the full realization of the constituent. In this phase, non-commutativity and commutativity are both used. Non-commutativity in order to keep the structure of the verb and commutativity to unload hypotheses of the nominal phrase. This underlies the assumption that the order of the features of the noun could not be presupposed. This is reinforced by the analysis of questions where that object constituent undergoes one more move and then must be explicitly transfered from right to left part of the phase. Now, it is the end of the second verb step. The derivation continues by preparing the third one.

Step 3 This part of the derivation must be combined with the next lexical entry of the verb, the inflection. In this part of the verb step, it was merged with the previous result and next with a k hypothesis -the position of the subject case:

k ⊢ (ǫ, z, ǫ) : k ⊢ (ǫ, -, ǫ) : k \ (c ⊙ t) / < V d ⊢ (w a book, read, ǫ) : V [mg] d ⊢ (ǫ, read, w a book) : k \ (c ⊙ t) [mg] k, d ⊢ (z, read, w a book) : (c ⊙ t)
This allows to discharge hypothesis about the subject constituent which it also build:

⊢ (ǫ, the, ǫ) : (k ⊗ d) / n ⊢ (ǫ, children, ǫ) : n [mg] ⊢ (ǫ, the, children) : k ⊗ d
And unloaded:

⊢ (ǫ, the, children) : k ⊗ d k, d ⊢ (z, read, w a book) : (c ⊙ t)
[mv] ⊢ (the children, read, a book) : (c ⊙ t)

Step 4 This example stands for a very simple sentence, then the last verb step corresponds only to the combination of the current bypass with the lexical entry comp by a phase with nothing in the transfer part: ⊢ (the children, read, a book) : (c ⊙ t) c; t ⊢ (ǫ, ǫ, ǫ) : c

[phase] ⊢ (ǫ, ǫ, the children read a book) : c This ends the last phase and thus the derivation. The proof matches the string The children read a book. An important distinction with the previous versions of these grammars is in the use of lexical item without phonological part. Here, only the lexical items used in the phase process are necessary, but the structure of items for phases imposes a strict order in their pooling.

Question

In the previous example, the transfer part of the two phases is not really efficient. The first one introduced the object of the utterance and the second only ended the derivation. For questions, the comp item is more complex because it introduces the last feature of the object. This time, its lexical item is : c; t ⊢ (ǫ, ǫ, ǫ) : wh \ c. And it is only afterward that a hypothesis wh is introduced that the object could be introduced in the derivation. But it means that in the previous phase, the constituent mark must be transferred from the left to the right part of the first phase. This is done with a cyclic move: the introduction of a new hypothesis k ⊗ d ⊢ k ⊗ d, which explicitly connect the two hypotheses.

In the lexicon, only comp is modified and an item for which is added :

which ⊢ (ǫ, ǫ, ǫ) : (wh ⊗ (k ⊗ d))
The derivation before the phase is still the same.

1. First step procedure:

⊢ (ǫ, read, ǫ) : (V ⊙ v) < / d d ⊢ (ǫ, u, ǫ) : d [mg] d ⊢ (ǫ, read, u) : (V ⊙ v) 2. Saturation of positions of mode: d ⊢ (ǫ, w, ǫ) : d k ⊢ (ǫ, v, ǫ) : k V ; v ⊢ (ǫ, ǫ, ǫ) : k \ d \ V [mg] k, V ; v ⊢ (v, ǫ, ǫ) : d \ V [mg] d, k, V ; v ⊢ (w v, ǫ, ǫ) : V 3. Construction of the object constituent: ⊢ (ǫ, which, ǫ) : (wh ⊗ (k ⊗ d)) / n ⊢ (ǫ, book, ǫ) : n [mg] ⊢ (ǫ, which, book) : (wh ⊗ (k ⊗ d))
We get all the necessary material to process the phase. Its first part combines:

d ⊢ (ǫ, read, u) : (V ⊙ v) d, k, V ; v ⊢ (w v, ǫ, ǫ) : V [phase 1 ] d, k, d ⊢ (w v, read, u) : V
In the treatment of this utterance, the transfer part is not able to directly discharge the two hypotheses of the determiner phrase. A cyclic move is used in order to store the access to this element. At the same time, the phase move it on its left part:

k ⊗ d ⊢ (ǫ, W, ǫ) : k ⊗ d d, k, d ⊢ (w v, read, u) : V [phase trans ] d, k ⊗ d ⊢ (w W, read, ǫ) : V
The derivation continues with the same third step and produces:

k ⊗ d ⊢ (the children, read, W ) : (c ⊙ t)
Finally, before the last phase, the derivation introduces a wh hypothesis which will allow the move of object after the first part of the phase realization. The move of the transfer part is:

⊢ (ǫ, which, book) : (wh ⊗ (k ⊗ d)) wh, k ⊗ d ⊢ (y the children, read, W ) : c
[phase trans ] ⊢ (which book, ǫ, the children read) : c

In this example, only the transfer in the first phase, which accounts for the cyclic move of the constituent allows to complete the derivation.

Blocked derivation with PIC

A very important point in the definition of the phase rule is the fact that the complementizer part of hypothesis must be removed. This property encodes the Phase Impenetrability Condition. The previous one does not contain such problem because the transfer part of the first phase achieves all moves which empty complementizer hypotheses.

A simple example extracted from the previous one is the case where the k hypothesis in the second step of the verb is not included. Thus the derivation must failed because one hypothesis is away. The lexical entry corresponding to mode is: And the transfer part does not contribute to this step. The part of the Γ c of the phase rule is not removed. The structure of the proof which blocks the derivation is the case where the constituent is in complementizer position of the head.

We would remark that derivations with phases immediately block the process unlike traditional MCG or MG which perform the full derivation before concluding that a specific feature stand at the end (and reject the derivation).

Even if this example is quite simple, it shows that the encoding of PIC directly uses properties of the MCG. Unlike the other constraints, we do not need to propose new rules. That insure to keep the same generative power for MCG phase . The derivation strictly controls the structure and check internal relations.

Conclusion

The main aim of this paper is to introduce the concept of phase from minimalism into type logical grammars, simulating the generative theory of Chomsky which has been an open question since [START_REF] Chomsky | Derivation by phase. ms[END_REF]. It involves the introduction of a new rule into the system, and highlights commutative and non-commutative relationships between elements of the parsing process. Moreover, this addition is not ad hoc as it allows full use of the properties of PCL underlying the formalism. This new rule is the composition of a substitution of hypotheses in commutative relations, followed by a transfer that is either the realization of a move became possible, or a cyclic move. This proposal also involves a new linguistic interpretation of cyclic move.

A full description of the system would require additional details [START_REF] Amblard | Calcul de représentations sémantiques et syntaxe générative: les grammaires minimalistes catégorielles[END_REF]. However, we emphasize the role played by phases at the syntactic level to define islands where the encoding of PIC is simply the use of logical properties of the framework. Furthermore, we claim that the use of phases at semantic level corresponds to the introduction of thematic role predicates (variables related to the reification of formulas and substitution of variables). They also mark points in the semantic tiers where the context must be reduced. It plays a crucial role at the semantic level by marking reduction point for continuations.

The introduction of these phases confirms the use of a logical system simultaneously handling relations commutative and non-commutative at plays in linguistic analysis. Distributing the properties on each component used in this analysis can produce fine performances A remaining issue for this description is the formalization of the phase as reduction point at the semantic level that would reduce ambiguities of scope of quantifiers. In addition, the study of equivalence between the MCG with phases and MG remains an open question.

Fig. 1 .

 1 Fig. 1. Partially Commutative Logic rules.

Fig. 2 .

 2 Fig. 2. Phases in verb structure

V

  ; v ⊢ (ǫ, ǫ, ǫ) : d \ Vwhich produces a conclusion of a proof of type V with only d in the left hand side:d, V ; v ⊢ (wǫ, ǫ) : VThe result of the first part of the phase is:d ⊢ (ǫ, read, u) : (V ⊙ v) d, V ; v ⊢ (w v, ǫ, ǫ) : V [phase 1 ] d, d ⊢ (w v, read, u) : V

These definitions contain also a syntax / semantic interface. However, we leave this part out of this article due to space.

Uniform Theta Assignment Hypothesis or assignment of thematic roles.

s, A ∈ Lex [Lex] ⊢ G (ǫ, s, ǫ) : A x ∈ V [axiom] x : A ⊢ G (ǫ, x, ǫ) : A Γ ⊢ G r 1 : A / B ∆ ⊢ G r 2 : B V ar(r 1 ) ∩ V ar(r 2 ) = ∅ [/ e ] Γ ; ∆ ⊢ G (r 1s , r 1t , r 1c • Concat(r 2 )) : A ∆ ⊢ G r 2 : B Γ ⊢ G r 1 : B \ A V ar(r 1 ) ∩ V ar(r 2 ) = ∅ [\ e ] Γ ; ∆ ⊢ G (Concat(r 2 ) • r 1s , r 1t , r 1c ) : A

in the semantic part of the calculus, this position is also used for the thematic role assignement.

Acknowledgments

The author would like to express his gratitude to reviewers for their precise remarks, Corinna Anderson, Sai Qian and Sandrine Ribeau for their readings.