Maxime Amblard

Alain Lecomte

Christian Retoré

Categorial minimalist grammars: from generative syntax to logical forms

1. Convergence at first sight, and differences in a second time From the early days of the minimalist program of [START_REF] Chomsky | A minimalist program for linguistic theory[END_REF], a convergence with categorial grammars was noticed by Epstein and Berwick (1995). The striking similarity lies in the merge operation, which looks like the application rule of the AB grammars. In both cases, word order is a consequence of the consumption rules but in categorial grammars being the head of a compound expression also derives from the categories while in a minimalist setting it can be defined independently from the resource consumption. The most striking difference is the absence of movement in categorial grammar: how could this notion be captured? If it can, how could minimality conditions like shortest move be formulated? In the other direction the main difference is the atomicity of minimalist features: merge is not recursive, there cannot be a demand of a category which itself demand another category.

Hence, after quite an optimistic wish of convergence, the task seems so tough that one may wonder why we are willing to do so? There are at least two reasons:

• Of course, the main reason is that categorial grammar easily yield the logical form (or semantic representation) following some of Montague's idea.

• A secondary reason is the formalisation of converging learning algorithms from positive structured examples, which can be defined for categorial grammars, but we shall not speak about it, although one of us did something in this direction [START_REF] Bonato | Learning rigid Lambek grammars and minimalist grammars from structured sentences[END_REF].

Because the categorial tradition is anchored in a formal and logical apparatus, the convergence between generative grammar and categorial grammars benefited from the development of resource logic and from the formalisation of the minimalist program by [START_REF] Stabler | Derivational Minimalism[END_REF] into tree grammars known as minimalist grammars as a special issue of Language and Computation shows (Retoré and Stabler (2004b)).

The kind of categorial grammar we are using relies on the outcomes of linear logic [START_REF] Girard | Linear Logic[END_REF], which extends the Lambek calculus [START_REF] Lambek | The mathematics of sentence structure[END_REF] which itself is a logical completion of the AB-grammars (Bar-Hillel, 1953)when the fraction rules are viewed as modus ponens. Lambek calculus is quite a restricted logic: it is an intuitionistic logic, where every hypothesis is used once and exactly once, and where they cannot permute. Our representation uses a mixed system with both commutative and non commutative connectives (de Groote, 1996; [START_REF] Retoré | A description of the non-sequential execution of Petri nets in partially commutative linear logic[END_REF][START_REF] Amblard | Natural Deduction and Normalisation For Partially Commutative Linear Logic and Lambek Calculus with product[END_REF]. Still it is a linear subsystem of intutionistic logic, and this enables to derive semantic interpretation from the syntactic analysis.

There are several ways to represent rather faithfully Edward Stabler's minimalist grammars in categorial grammars and to endow them with an integrated treatment of compositional semantics. Some of them take place in the multimodal framework, like (Cornell, 1999; [START_REF] Vermaat | The Minimalist Move Operation in a Deductive Perspective[END_REF], but here we focus on the one we introduced in the framework of linear logic [START_REF] Lecomte | Semantics in Minimalist Categorial Grammar[END_REF]Retoré (1999, 2001) that we call categorial minimalist grammars. We developed them with others (in particular [START_REF] Anoun | Approche logique des grammaires pour les langues naturelles[END_REF]), but in this presentation, we rather follow the one thoroughly presented in the PhD thesis of the first author, [START_REF] Amblard | Calculs de représentations sémantiques et syntaxe générative : les grammaires minimalistes catégorielles[END_REF].

We first recall some basic notions on minimalist grammars and on categorial grammars. Next we shortly introduce partially commutative linear logic, and our representation of minimalist grammars within this categorial system, the so-called categorial minimalist grammars. Next we briefly present λµ-DRT (Discourse Representation Theory) an extension of λ-DRT (compositional DRT) in the framework of λµ calculus: it avoids type raising and derives different readings from a single semantic representation, in a setting which follows discourse structure. We run a complete example which illustrates the various structures and rules that are needed to derive a semantic representation from the categorial view of a transformational syntactic analysis.

Minimalist grammars

There are actually several variants of minimalist grammars, due to Edward Stabler, whose guidelines are similar. We focus on the initial formulation of [START_REF] Stabler | Derivational Minimalism[END_REF], an important alternative being Stabler (1999) where operations that one may find unpleasant in a categorial setting like head-movement, are simulated by sequences of elementary operations.

As usual in a lexicalised grammar, the lexicon maps each lexical item from Φ = {Peter, sleeps, loves, ...} to a formal encoding of its syntactic behaviour. Here syntactic behaviour is depicted by a sequence of features (category, demand of a category, movement trigger, movement target, see figure 1) followed by the corresponding phonological form. This sequence controls the generating process, which makes use of independent generating functions, only depending on the features of the heads.

(

1) Minimalist lexical entries

The sequence of features preceding the phonological form matches the following regular expression, whose ingredients are depicted in figure 1:

Lex(word) ∈ L = ( = b ∪ b ⇐ ( = b ∪ b ⇐ ∪ +m) * ) * b(-m) *
Such grammars operate on binary trees, the leaves of which are labelled with sequences of features, and the nodes of which are labelled by either "<" or ">". The head of a tree is defined recursively as follows: the head of a tree reduced to a leaf is itself. The head of T 1 < T 2 and of T 2 > T 1 is the head of T 1 . Given a leaf ℓ of a tree T , there always exists a biggest subtree T ′ of T such that l is the head of T ′ : T ′ is said to be the maximal projection of ℓ.

The initial rule says that a tree reduced to a leaf labelled by the lexical entry is itself a derivation tree.

The merge rule, is defined for two trees T 1 and T 2 , one having a head τ 1 = =xτ ′ 1 φ 1 (the demand) and the other having a head τ 2 = xτ ′ 2 φ 2 , where τ ′ 1 , τ ′ 2 are sequences of features and φ 1 , φ 2 are sequences of phonological features. Let us call T ′ 1 and T ′ 2 the trees obtained from T 1 and T 2 by suppressing from their respective heads the first features, that are respectively x and =x. If the demand comes from a lexical item, then the result of the merge operation is

T ′ 1 < T ′ 2 . Otherwise, the result is T ′ 2 > T ′ 1 .
In any case the head of the result comes from T 1 and is τ ′ 1 φ 1 . The head-movement with right adjunction is actually a special merge and not a kind of movement. It is defined for two trees T 1 and T 2 , one having a head τ 1 = x⇐τ ′ 1 φ 1 (the demand) and the other having a head τ 2 = xτ ′ 2 φ 2 , where τ ′ 1 , τ ′ 2 are sequences of features and φ 1 , φ 2 are sequences of phonological features. Let us call T ′ 1 the tree obtained from T 1 by turning its head into τ 1 = τ ′ 1 φ 1 φ 2 i.e. the demand x⇐ has been suppressed and the phonological features are the ones of T 1 's head followed by the one of the head of T 2 . Let us call T ′ 2 the tree obtained from T 2 by turning its head into τ ′ 2 i.e. by suppressing both the x that has been consumed during the merge and the phonological features of the head that have been moved into T ′

1 . If the demand comes from a lexical item, then the result of the merge operation is

T ′ 1 < T ′ 2. Otherwise, the result is T ′ 2 > T ′ 1 .
In any case the head of the result comes from T 1 and is τ ′ 1 φ 1 . As far as strings are concerned, head-movement is not required: grammars with or without head-movement generate the same languages, the simulation of head-movement requires many standard merge and moves to be simulated, and yields different parse trees. For having shorter derivations and standard parse trees, we prefer to use head movement in this paper. There also exists head movement with left adjunction, which is defined symmetrically the phonological features moving before the phonological features of the selector head.

One can also define affix-hopping which is rather similar except that the selectee collects the phonological features of the head of the selector.

The move rule applies to a single tree T whose head is +xτφ i.e. starts with a movement target +x ∈ +m, such that T has a subtree T 1 whose head starts with the corresponding movement trigger -x ∈ -m. Then the result is T ′ 1 > T ′• where T ′ 1 is T 1 without the -x feature and T ′• is T minus the T 1 subtree and minus the +x feature. Observe that the head of the result is the same as the initial one, except that its first feature +x has been erased. 1(2) Language generated by a minimalist grammar A convergent derivation generating the sentence φ 1 • • • φ n ∈ Φ * ends up with a single non phonological feature C on the head, while the leafs read from left to right yield

φ 1 • • • φ n ∈ Φ * .
An important requirement on minimalist grammars, both in the principles of Chomsky and in Stabler's formalisation, is the condition known as the shortest move. In Chomsky's formulation it says that whenever two subtrees have a -xτ head, the first one, that is the closes to the target, moves. In Stabler's view it says that whenever there are two candidates to movement, i.e. when there are two leaves starting with -x, the derivation crashes. Unless otherwise stated, with stick to Stabler's definition.

Minimalist grammars have rather interesting formal properties, some of which are worth quoting. Indeed, Harkema, Kobele, Michaelis, Morawietz, Mönnich, Retoré, Salvati, Stabler studied minimalist grammars from the viewpoint of formal language theory, the main focus being their generative capacity as sets of strings and as sets of trees, the complexity of parsing and learning strategies. We recall here some of the results:

• The generative capacity of minimalist grammars (with shortest move) is equivalent to that of context free linear rewriting system. Michaelis (2001a,b) • In the absence of shortest move, it has been showed that the membership problem is equivalent to the yet unknown decidability of provability of Multiplicative Exponential Linear Logic. [START_REF] Salvati | Minimalist Grammars in the Light of Logic[END_REF] • As far as trees are concerned, we know that the minimalist derived trees, that are the ones depicting syntactic structures can be obtained from a regular tree grammar with a transduction applied thereafter. [START_REF] Mönnich | Derivational Minimalism in Two Regular and Logical Steps[END_REF]; [START_REF] Kobele | An automata-theoretic approach to minimalism[END_REF] Although there are some semantic concerns in minimalist grammars as rewriting systems e.g. in [START_REF] Kobele | Generating Copies: An investigation into Structural Identity in Language and Grammar[END_REF] what is a logical form and how it could be computed is not as clear as it is in the logical approach to categorial grammars. This is likely to be the most frustrating limit of minimalist grammars and the main reason for studying them from a categorial perspective.

For us, the main advantage of minimalist grammars (or in a broader perspective, generative grammar, transformational grammars, etc.) is their linguistic richness and soundness, which is attested by the relation they are able to draw between sentences (questions and related declarative sentences for instance) or between languages (the differences among features are a way to explain language variation).

Categorial grammars

A categorial grammar consists in a lexicon which associates with every lexical item a finite set of categories (propositional logical formulae). In the case of AB grammars categories are finitely generated by the connectives / and \ from a set of base categories: S (sentence), np (or dp for noun phrase or determiner phrase), n (common noun) etc. A sequence of words w 1 • • • w n is in L(Lex) whenever ∀i∃t i ∈ Lex(w i ) such that t 1 , . . . , t n ⊢ S is derivable in a logical calculus. For AB grammars the calculus simply consists in the two famous residuation laws, which are elimination rules from the logical viewpoint, i.e. when / and \ are viewed as non commutative linear implications.

Alternatively, one could also label the formulae in the proofs as follows:

(w : word, with A ∈ Lex(w) ) axiom ⊢ w : A ⊢ w 1 . . . w n : A ⊢ m 1 • • • m p : A \ B \ e ⊢ w 1 • • • w n m 1 • • • m p : B ⊢ t : B / A ⊢ u : A / e ⊢ tu : B
This lead to a definition of the generated language as typable strings:

(3) Language generated by an AB grammar

(*) w 1 • • • w n ∈ L(Lex) whenever ⊢ w 1 • • • w n : S .
The logical calculus we are to use for categorial minimalist grammars is close to the one above since we shall consider labels and only elimination rules. But it also resembles the Lambek calculus since we have more logical rules and one of them, namely product elimination, requires axioms and variables. 2One can wonder why moving out the mathematical paradise provided by usual categorial grammars, AB grammars or Lambek grammars, which are very neat and elegant, especially the Lambek calculus. The main reason is that the syntactic abilities of categorial grammars are limited. A formal way to say so is that they only describe context-free languages, which are commonly assumed to be insufficient to describe natural language syntax, but a more empirical one is their difficulty to describe various syntactic phenomena, like discontinuous constituent, or to relate declarative sentence and questions. 3 Therefore, one has to extend such systems, either by extending the logic by modalities and postulates, as [START_REF] Moortgat | Categorial Investigations[END_REF] did, thus sticking to the parsing as deduction paradigm, or to have a logical basis providing the deep structure and an extra mechanism computing word order.

Despite their syntactic limitations, categorial formalisms nevertheless allow an appealing direct computation of (usual) logical formulae from a syntactic analysis. The deep reason, already noticed by the Ancients is that syntactic categories correspond to semantic types, see e.g. [START_REF] Baratin | L'analyse linguistique dans l'antiquité classique -I Les théories[END_REF]: a sentence S is a proposition t, a definite np is an individual e, a common noun n or an intransitive verb np \ S is a one place predicate, a transitive verb is a two place predicate etc. Without providing the details, since we are going to present a similar process for categorial minimalist grammars, let us explain how it works.

In order to compute the semantic formula associated with a sentence, we have:

• A lexicon that provides each word with a syntactic category c and a lambda term whose type is the semantic translation t = c * .

• A syntactic analysis that is a proof in the Lambek calculus of S under the assumption t 1 , . . . , t n , each t i being a possible category for the word w i .

The algorithm which computes the associated logical formula is quite simple:

(i) Convert the syntactic categories into semantic types as follows: np * = e, S * = t, n * = e → t, (A\ B) * = (B/ A) * = e → t: this yields a proof in intuitionistic logic of S * = t under the assumption c * 1 = t 1 , . . . , c * n = t * n . This proof is a proof that the lambda term hereby defined corresponds to a formulae (is of type t), whose free variables are of type t i .

(ii) Replacing each variable with the corresponding term of type t i provided by the lexicon provide a close term of type t, that is a logical formulae.

Categorial minimalist grammars

Labels encoding word order

Let us consider a set of variables V (for expressing hypothesis and encoding movement) and a (disjoint) set of phonological forms Φ (words, lexical items) The labels we are to use are slightly more complicated than sequences of words. A label r is a triple each component being a sequence of variables and phonological forms

r = (r spec | r head | r comp ) = (r s | r h | r c ) ∈ (V ∪ Φ) * 3
Intuitively, these three strings are the yields of the three subtrees respectively corresponding to the head (r h ), the specifier (r s ) and the complement (r c ). The following notations are convenient to denote the suppression of one of the components:

r -h = (r s | ǫ | r c ) ∈ [(V ∪ Φ) * ] 3 , r -s = (ǫ | r h | r c ) ∈ [(V ∪ Φ) * ] 3 , r -c = (r s | r h | ǫ) ∈ [(V ∪ Φ) * ] 3 . With these notations r -h = r s r c ∈ (V ∪ Φ) * Given a label r = (r s | r h | r c
) we denote by r the concatenation of its three components:

r = r s r h r c ∈ (V ∪ Φ) *

A restricted fragment of partially commutative logic

To represent minimalist grammars we make use of a very restricted fragment of partially commutative linear logic. This later system introduced by de Groote in de Groote (1996) 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. The connectives are both the ones of the Lambek calculus (•, \, /) and the ones of (commutative)multiplicative linear logic (⊗, ⊸).

We only consider a particular formulation of a restricted fragment of the calculus to encode minimalist grammars:

• We use natural deduction as in [START_REF] Amblard | Natural Deduction and Normalisation For Partially Commutative Linear Logic and Lambek Calculus with product[END_REF].

• We only use the commutative conjunction (⊗) and the two non commutative implications (/, \).

• We only use elimination rules. • Contexts will simply be multisets of formulae. Usually, for such calculi, contexts are partially ordered multisets of formulae and a rule called entropy allows to relax such order. In the restricted calculus we use, we systematically use the full strength of entropy just after the eliminations of / and \ which usually introduce order between the assumptions. Hence contexts are simply multisets of formulae.

∆ ⊢ z : A ⊗ B Γ[(x : A, y : B)] ⊢ t : C [⊗ e ] Γ[∆] ⊢ (let (x, y) = z in t) : C
The product elimination rule is especially important, because it enables a coding of movement (or rather copy theory of Brody (1994)) from one hypothesis to the other one. It is a free adaptation of the product elimination rule to the proof expressions of Abramsky (1993) (see figure 2).

The formulae we use have a definition that follows rather precisely the sequences of features that are used in minimalist grammars, i.e. in the set L defined in 1:

(4) Logical formulae in a categorial minimalist lexicon

F ::= x / b | x / ⇐ b | c x ::= b \ x | b ⇒ \ x | m \ x | c c ::= m ⊗ c | b
The rules which control the labelling are presented in figure 4.2 -observe that labels do not control the deductive process but are derived from deductive process.

The rules of figure 4.2 will be used as a group of rules which corresponds to the main operations of minimalist grammars, namely merge and move given in ( 5) and [START_REF] Bar-Hillel | A quasi arithmetical notation for syntactic description[END_REF].

We also need to distinguish different \, /-eliminations because head-movement with right adjunction is as far as logical types are concerned a merge but is has a different effect on word order. The two rules corresponding to lexical merge / head-movement with

s, A ∈ Lex [Lex] ⊢ G (ǫ | s | ǫ) : A x ∈ V [axiome] x : A ⊢ G (ǫ | x | ǫ) : A Γ ⊢ G r 1 : A / B ∆ ⊢ G r 2 : B [/ e ] Γ; ∆ ⊢ G (r 1s | r 1t | r 1c r 2 ) : A ∆ ⊢ G r 2 : B Γ ⊢ G r 1 : B \ A [\ e ] Γ; ∆ ⊢ G (r 2 r 1 s | r 1h | r 1c ) : A Γ ⊢ G r 1 : A ⊗ B ∆[x : A, y : B] ⊢ G r 2 : C [⊗ e ] ∆[Γ] ⊢ G r 2 [r 1 /x, ǫ/y] : C Γ ⊢ G r : A Γ ′ ⊏ Γ [⊏] Γ ′ ⊢ G r : A Figure 3: Labelled PCMLL deductions.
As renaming allows, it is assumed that no variable is common to two labels from different premises: Var( r 1 ) ∩ Var( r 2 ) = ∅. In the ⊗ e rule, A is usually a movement feature. right adjunction / ⇐ or the non lexical variant are provided in figure 7 This is the reason why we use the symbols ⇒ \ and / ⇐ corresponding to head-movement with right adjunction. Clearly, this is a weakness of the system, because as far as proofs are concerned it is weird to have different connectives with the same rules. We can answer to the possible protests that:

• As for minimalist grammars, head-movement is not really required since it can be simulated with regular movement, hence merge and move which are completely directed by the formulae

• Because the system does not contain the introduction rules, the system is unable to prove A\ B ≡ A ⇒ \ B nor A/ B ≡ A/ ⇐ B which would be quite a problem.

(5) The operation merge in a categorial setting

sem, A ∈ Lex [Lex] ⊢ s em : A ⊢ g : A / B ∆ ⊢ u : B [mg] ∆ ⊢ (g(u)) : A ∆ ⊢ u : B Γ ⊢ g : B \ A [mg] ∆, Γ ⊢ (g(u)) : A (6) The operation move in categorial setting Γ ⊢ s : A ⊗ B ∆[u : A, v : B] ⊢ r : C [mv] ∆[Γ] ⊢ r[u := s, v := ǫ] : C (7) Head-movement with right adjunction in a categorial setting Γ ⊢ (r s | r h | r c ) : A / ⇐ B ∆ ⊢ (s s | s h | s c ) : B [mghdr] Γ, ∆ ⊢ (r s | r h s h | r c s s s c ) : A ∆ ⊢ (s s | s h | s c ) : B Γ ⊢ (r s | r h | r c ) : B ⇒ \ A [mghdr] ∆, Γ ⊢ (s s s c r s | r h s h | r c ) : A

Grammars

As earlier said, the definition of the generated language resembles the one of categorial grammar given in 3, although here it encompasses a broader notion of label.

(8) Language generated by a categorial minimalist grammars

A grammar produces a sentence φ 1 . . . φ n ∈ Φ * whenever there exists a derivation of ⊢ r : C with r = φ 1 . . . φ n (remember that r is the concatenation of the three components of r). This definition entails among others that variables must disappear with product elimination rules encoding movement during the derivation process.

A natural question is whether minimalist grammars and categorial grammars generate the same strings and derived trees. The answer is yes, and the proof may be found in Amblard (2007), 4 . It relies on translations from one king of lexicon to the other: [START_REF] Brody | Lexico-logical form: a radically minimalist theory[END_REF] The translation ( ) α from a lexicon à la Stabler into a categorial minimalist lexicon

(γ -f ) α = ( f ⊗ (γ) δ ) (= f γ) α = (γ) β / f ( f ⇐γ) α = (γ) β / ⇐ f ( f ) α = f (= f γ) β = f \ (γ) β ( f ⇐ γ) α = f ⇒ \ (γ) β (+ f γ) β = f \ (γ) β (γ -f ) β = ( f ⊗ (γ) δ ) ( f ) β = f (γ -f ) δ = ( f ⊗ (γ) δ ) ( f ) δ = f (10)
The translation ( ) α ′ from a categorial minimalist lexicon into a lexicon à la Stabler

(F / f ) α ′ = = f (F) β ′ (F / ⇐ f ) α ′ = f ⇐ (F) β ′ ( f ⊗ F) α ′ = (F) δ ′ -f ( f ) α ′ = f ( f \ F) β ′ = = f (F) β ′ si f ∈p 1 + f (F) β ′ si f ∈p 2 ( f ⇒ \ F) β ′ = f ⇐ (F) β ′ ( f ) β ′ = f ( f ⊗ F) β ′ = (F) δ ′ -f ( f ⊗ F) δ ′ = (F) δ ′ -f ( f ) δ ′ = f (11) Equivalence of

categorial minimalist grammars and minimalist grammars

If a minimalist grammar à la Stabler is turned into a categorial minimalist lexicon according to the rules in figure 9, then the generated sentences are the same and even parse trees are almost the same (provided the subtree undergoing movement is correctly placed). Conversely, if one turns a categorial minimalist lexicon (only containing formulae in CMG defined in figure 4) into a minimalist lexicon according to the rules in 10, then one also gets the same generated sentences and parse trees.

A remaining question is how constraints on derivations, like shortest move, could be formulated in a deductive setting. This is a weakness of the system: the only way to formulate these restrictions is to impose constraints on derivations, and this is not so appealing from a logical viewpoint since rule are usually context free, i.e. apply locally without referring to the history of the deduction -unless one goes to dependent types, which are complicated and not yet explored for linear calculi.

Syntax and semantics in categorial minimalist grammars

The purpose of viewing minimalist grammars as a categorial system is to have an automatic conversion of syntactic compositions into semantic composition. We firstly present the semantic types and their relation to syntactic categories, then a variant of λ-DRT with µ constructs in order to obtain the different scope readings from a single semantic representation, and finally sum up the algorithm producing semantic analyses.

From syntactic categories to semantic types

The formulae that we infer as semantic representations are first order, because we are going to use DRT which better matches the discourse structure. Therefore we reify predicates, we use variables to express high order properties: we write run(e, Rex) ∧ f ast(e) instead of f ast(run(Rex)). Consequently we have the following three base types t the standard Montague type, for truth values and propositions (that will be used as ⊥ from the µ-calculus viewpoint).

e the standard Montague type, for entities.

v the type for reifying events and predicates in order to remain in first order logic.

The standard translation H of a syntactic category x into the corresponding semantic type H(x) has to be slightly extended, because in addition to the syntactic connectives /, \ we have ⊗, together with an extra basic type for reifications. [START_REF] Epstein | On the Convergence of 'Minimalist' Syntax and Categorial Grammar[END_REF] Converting syntactic categories into semantic types

H(C) = t H(v) = v → t H(t) = v → t H(V) = e → (v → t) H(d) = e H(n) = e → t H(x ⊗ y) = H(y) ifa ∈ m = H(x) if a m H(x \ y) = H(x) → H(y) H(y / x) = H(x) → H(y) H(x ⇒ \ y) = H(x) → H(y) H(y / ⇐ x) = H(x) → H(y)
This translation can be illustrated on the syntactic categories we are to use in the example of section 6.

H(k ⊗ d) = e H(V / d) = (v→t)→e→v→t H((k\(d\v)) / ⇐ V) = (e→v→t)→e→e→v→t H((k \ t) / ⇐ v) = (v → t) → e → v → t H(k ⊗ d / n) = (e → t) → e H(C / t) = (v → t) → t

λµ-calculus

Semantics can be computed in standard Montagovian terms and types, as did [START_REF] Amblard | Syntax and Semantics interacting in a minimalist theory[END_REF] or Lecomte and Retoré (2002) We extend a bit this process, by moving from λ-calculus to λµ calculus, a λ calculus for depicting classical proofs (while standard λcalculus correspond to proofs in intuitionistic propositional logic). The advantage is that quantifiers do not need to be type raised and that the different scopes are obtained from a single syntactic semantic analysis, by different λµ computations, as initiated by de Groote (2001) and developed for categorial minimalist grammars in Amblard (2007) or Lecomte (2008).

The µ calculus is strongly related to the formulation of classical logic in natural deduction using reductio as absurdum: instead of concluding ¬¬A = (A → ⊥) → ⊥ from ⊥ under the assumption ¬A one concludes A. Provided one does not use the ⊥ rule (ex falso quod libet sequitur), this can be done with any constant type for ⊥. Here, as in de Groote (2001), we shall use Montague t type (truth values, propositions) for the ⊥ of the glue language that is the λµcalculus. As opposed to common intuitions, this is really harmless! We will use a restricted calculus, whose typing rules are very easy: basic types are the aforementioned t, e, v and, as said above, t will be used as ⊥. Types are defined as usual, with the arrow (intuitionistic implication) only.

For each type Z, we have a denumerable set of λ-variables of type Z.

We have µ variables with type X → t for some type X.

There are three kinds of terms, Values V, Unamed Terms v and Named Terms c with V ⊂ v, which are defined as the smallest sets closed under the following operations:

• a λ-variable x : X is a value and an unnamed term.

• if u : U is an unnamed term and x a λ variable then λx. u : X → U is a value and an unnamed term

• if v 1 : X → U and v 2 : X are unnamed terms, (v 1 (v 2 )) : U is an unnamed term

• if v : X is an unnamed term and α : X → t a µ-variables, than (α(v)) : X is a named term

• if v : X is a named term and α : X → t is a µ-variable then (µα. v) : X is an unnamed term.

• Any term of type t is a named term (this follows from ⊥ = t).

The reduction patterns for λµ-calculus include the usual β conversion as well as reductions concerning µ variables and the µbinder:

(13) λµ reductions (β) ((λx. t)(u)) β t[u/x] (µ) ((µα. T [(α Q)])P) µ µα. T [(α(Q P))] (µ ′ ) (P(µα. T [(α Q)])) µ ′ µα. T [(α(P Q))] (ς) ((µα. T [(α Q)]) ς T [Q] only for Q : t
Let us recall that λµ calculus, with the given reductions, is not confluent. This will be useful to obtain the many readings of a given sentence, as first observed by de Groote (2001).

λµ-DRS

Instead of standard Montague semantics, we prefer to produce Discourse Representation Structures (DRS), whose dynamics better matches the one of sentences and discourse. Of course, given the wished correspondence with the categorial framework, we use a compositional presentation of DRT, like λ-DRT. But, because we also wish to have µ reductions for avoiding type raising and solving scope questions, we use a generalisation of λ-DRT that we call λµ-DRT.

Basically, we consider DRS with λ and µ variables (all µ variables will be of type X → t), using freely both λ and µ abstractions, and we refer to these structures as λµ-DRS (Discourse Representation Structure) In addition to the λ and µ variables and the variables used for movement which can be considered as free λ variables we need a set of discourse refrents V D of type e (some could be of type v) denoted by

d 1 , • • • , d n .
The lexicon in addition to the syntactic categories maps each lexical item to a λµ-DRS. A λµ-DRS is typed term with three different kinds of variables V λ (containing movement variable, which have nothing special except that they are not bound by any λ), V µ and V D and three corresponding kinds of binders the later one allowing dynamic binding. Variables that are µ or λ bound can be suppressed from the context, while discourse referents of V D should remain in the context until some simplifications are performed, as their binding is sophisticated, see 14.

Types for these terms are defined as usual, from three base types B = {e, v, t} (entities, events, truth-values) by the arrow:

T = B | T → T We have constants, namely predicates of type υ → (υ → (υ → • • • t))
where υ is either e or v -there is no need to systematically force that a predicate only involves one event, itself. As usual, an intransitive verb has type v → e → t, a transitive verbe v → e → e → t, a ditransitive verbe v → e → e → e → t, and a property e → t.

We also have logical constants:

• ∧ : t → t → t • ∧ : t → t → t • ⇒ : t → t → t • = : e → e → t There is no constant for ∃ ([d|F] is close to ∃d F) nor for ∀ ([|[d|F] ⇒ [|G]] is close to ∀d (F ⇒ G)
), since we thus obtain better scope properties. The variant of ∧ named ∧ has a slightly different behaviour with respect to discourse variables. The operation ∧ concerns DRS as well as formulae, and is a kind of a fusion, similar to the merge operations explored by [START_REF] Muskens | Combining Montague Semantics and Discourse Representation[END_REF].

Variable Term Result α : (X → t) ∈ V µ u : X µα. u : X x : X ∈ V λ u : U (λx.u) : X → U d : e ∈ V d d : v ∈ V d u : t [d|u] : t
We also have applications:

First Term Second Term Application Result α : (X → t) u : X (α(u)) : t u : X → Y v : X (u(v)) : Y
Given a formula F : t we use the following shorthands:

• let F : t then [|F] = F in the very same context. In particular F → G can be viewed as [|F] ⇒ [|G]. • let F : t then [d 1 |[d 2 [d 3 |[• • • [d n [|F]]]]]] = [d 1 • • • d n |F] the context being unchanged.
A λµ-DRS is a typed term of this calculus. When it is of type t, without µ-binder nor µ-variable, it is an ordinary λ DRS, and when, furthermore, there is neither λ binder nor λ variables, it is an ordinary DRS (provided formulae involved in implications are viewed as short hands for DRS without discourse variables). In order to formulate the reduction of ∧ which encodes dynamic binding, we need some standard notions on DRS and subDRSs.

A sub DRS is simply a subterm. A subDRS G of a DRS H is said to be a positive (resp. negative) subDRS of H written ≺ + (resp. ≺ -) whenever:

• G = H • H = [d|K] and G ≺ + K (resp. G ≺ -K)). • H = K ∧ L or H = K ∧ L and G ≺ + K (resp. G ≺ -K) • H = K ⇒ L and G ≺ + K or G ≺ -L (resp. G ≺ + L or G ≺ -K) The reference markers associated to a DRS [d 1 • • • d n |F] are the discourse refrents d 1 • • • d n .
The accessibility relation is the closure of (≺) ∪ (տ) where F տ G whenever F → G. The accessible referent markers of a DRS are the referent markers of the accessible DRS.

As said above, ∧ operation is close to the DRS merge in the literature, but here it will be called fusion because we use merge as a term denoting a syntactic operation. Although it could be defined on the run, the reduction of ∧ is easier to define on a normal λµ-DRS, that is a DRS without λ abstraction nor µ abstractions. It can be reduced when it applies to a DRS D and a single formula F with free discourse variables fdv(F). To view this reduction as a fusion (merge), firstly turn F into [ fdv(F)|F]: then the resemblance should be clear.

(14) Internalisation

If there exist one largest

K = [k 1 • • • k s |G] positive subDRS of D whose accessible referent markers includes fdv(F) then D∧ F reduces to D with subDRS K replaced with K = [k 1 • • • k s |G ∧ F].
If there is no such positive subDRS, or if there is no largest one, no internalisation is possible.

The process of syntactic and semantic derivation

Assume we have a lexicon which maps a word to its syntactic category x (that can be inferred from a minimalist grammar) together with the corresponding λµ-DRS with the semantic type H(x) defined in 5. Firstly, we should provide the semantic counter part of the syntactic rules. Merge does, as usual, correspond to λ application: the head is the semantic function which is applied to the semantics of the argument. Head movement with right adjunction, is just a merge from the semantic viewpoint -indeed the resource consumption is just the same, only word order is different from standard merge.

(15) Semantic counterpart of merge and of head-movement

In the merge and hdr rules of figures 5 and 7 let H(s) : H(B) be the semantic term corresponding to s : B i and let H(r) : H(A) → H(B) be the one corresponding to r : A / B (or

A / ⇐ B or B \ A or B ⇒ \ A) (

all the possible syntactic categories for r translated into the semantic type H(A) → H(B)).

Then the semantic term associated with the resulting category A is H(r)(H(s)) : H(A) -the functional application of the semantic term associated with the function-category to the semantic term associated with the argument.

The semantic counterpart of the move rule of figure 6 is more complex. As may be observed in the syntactic rule, move connects two places of respective categories A and B, in an elimination rule with main premise A ⊗ B. These two places corresponds to two λ-variables u and v that by construction also appear in the semantic term. Items that can undergo movement, typically determiner phrases missing a case, or wh constituents, have a semantic term s associated with a particular discourse variable d(s) introduced in the lexicon within the semantic term of the determiner. Move consists in replacing the first variable u with the semantic term s, and the second, v with the corresponding discourse variable d(s). The internalisation process described above in 14 is precisely made to connect the formula in which d(s) appears and the DRS that derives from s and which is meant to bound the discourse referent d(s). [START_REF] Kobele | Generating Copies: An investigation into Structural Identity in Language and Grammar[END_REF] The semantic counterpart of move In the rule below d(s) is the distinguished discourse variable associated with the movable semantic term s.

Γ ⊢ H(s):A ⊗ B ∆[u:H(A), v:H(B)] ⊢ H(r)[u, v]:H(C) [mv] ∆[Γ] ⊢ H(r)[u:=H(s), v:=d(s)]:H(C)

To sum up, how do we proceed to compute both the syntactic and the semantic structure associated to a sentence φ 1 • • • φ n ∈ Φ * ? [START_REF] Kobele | An automata-theoretic approach to minimalism[END_REF] Computing the parse structure and the logical forms in a categorial minimalist grammar (i) Firstly, we construct a proof with the rules mv, mg and hdr of r

: C with r = φ 1 • • • φ n .
(ii) Afterwards or in parallel steps, this provides a λµ-DRS of type t without free λ variables, nor with free µ variables, that is nearly what we were looking for: we only have to internalise the formulae concerning some discourse variable d that lie outside the corresponding box which bounds d. This may seem problematic because it turns some free variables into bounded ones but as we proceed just after the derivation, before any renaming takes place, this is harmless. Also by construction, there cannot be conflict about in which box the formula must be moved.

[d, f |P(d, f )] ∧ Q( f ) [d, f |P(d, f ) ∧ Q( f )]
Hence we end up with a λµ DRS D of type t without free variables of any kind, and we may call The next section provides detail on all these steps by running a complete example.

D

A complete example of a syntactic and semantic analysis

Here is a samble lexicon from which we will derive the two reading of the ambiguous sentence: the children ate a pizza.

lexical λµ-DRS & semantic type syntactic item category the λQ.µδ.[|[d|(Q d)] ⇒ [(δ d)]] (e → t) → e k ⊗ d / n specific discourse variable: d a λQ.µγ.[p|(Q p) ∧ (γ p)] (e → t)
(v → t) → e → v → t (k \ t) / ⇐ v comp λQ.[e|(Q(e))] (v → t) → t C / t
In order to complete both the syntactic and the semantic process, described in the previous section on this example, we are to use the following structure: declaration of the syntactic variables declaration of the corresponding semantic variables

⊢                label, triple of phonological forms syntactic category semantic type DRS ⊢                (ε | a | ε) (k ⊗ d) / n (e → t) → e λQ.µγ.[p | Q(p) ∧ γ(p)] ⊢                (ε | pizza | ε) n e → t λz.piz(z) mg ⊢                    (ε | a | pizza) k ⊗ d e µγ. [p | piz(p)∧γ(p)] ⊢                (ε | the | ε) (k ⊗ d) / n (e → t) → e λQµδ.[ | [d | Q(d)]⇒[δ(d)]] ⊢                (ε | children | ε) n e → t λz.child(z) mg ⊢                    (ε | the | children) k ⊗ d e µδ.[ | [d | child(d)] ⇒[ | δ(d)]]
Figure 4: Constructing the two d p's: Two steps of the derivation may be performed independently. They both consist in constructing a determiner phrase by a merge rule and semantically the determiner (some or all) applies to the predicate. Notice that the semantic of quantifiers include a µ-abstraction.

The first step is a lexical merge with a variable that will be used later on for movement. On the semantic side merge corresponds to the application of the verbal lambda term to the variable.

⊢                (ε | eat | ε) V / d e → e → v → t λxλyλe.eat(e, x, y) u:d u:e ⊢                (ε | u | ε) d e u mg u:d u:e ⊢                    (ε | eat | u) V e → v → t λyλe.
eat(e, u, y)

Next step is a head-movement with right adjunction triggered by modif . Semantically it is also an application, which introduces the Pa thematic role:

⊢                    (ε | ε | ε) (k\(d\v)) / ⇐ V (e→v→t)→e→e→v→t λRλx 2 λyλe. R(y, e) ∧ Pa(e, x 2 ) u:d u:e ⊢                    (ε | eat | u) V e → v → t λyλe.
eat(e, u, y)

hdr u:d u:e ⊢                    (ε | eat | u) k\(d\v)
e → e → v → t λx 2 λyλe.eat(e, u, y) ∧Pa(e, x 2 )

Next step introduces in a merge rule a variable for case that will be used for movement. On the semantic side, the variable gets the patient role.

v:k v:e ⊢                (ε | v | ε) k e v u:d u:e ⊢                    (ε | eat | u) k\(d\v)
e → e → v → t λx 2 λyλe.eat(e, u, y) ∧Pa(e, x 2 )

mg v:k, u:d v:e, u:e ⊢                          (v | eat | u) d\v e → v → t λyλe.
eat(e, u, y) ∧Pa(e, v)

A move inserts the d p a pizza (computed in figure 6) into the main derivation. Syntactically, the movement checks the case, and the phonological string replaces the variable. Semantically the λµ-DRS replaces the variable u, and the specific discourse referent p replaces v. Next a variable corresponding to the subject (another dp) is introduced in a non-lexical merge-rule. Semantically, we just apply a λ-expression to the variable:

⊢                    (ε | a | pizza) k ⊗ d e µγ. [p | piz(p)∧γ(p)] v:k, u:d v:e, u:e ⊢                          (v | eat | u) d\v e → v → t λyλe. eat(e, u, y) ∧Pa(e, v) mv ⊢                          (a pizza | eat | ε) d\v e → v
w:d w:e ⊢                (ε | w | ε) d e w ⊢                          (a pizza | eat | ε) d\v e → v →
⊢                          (w a pizza | eat | ε) v v → t λe. eat(e, µγ.[p | piz(p)∧γ(p)], w)∧Pa(e, p)
The verb is now ready to receive its inflection. Syntactically it is a head movement with right-adjunction that glues the inflection mark to the right of the verb (eat in f l should be understood as ate). Semantically, the λ-term associated with the inflection is applied to the term we derived so far. A variable is introduced to enable the subsequent movement of the subject. Semantically, the application assigns the agent role to the subject. The subject that is the d p we derived in figure 6, is inserted in the main derivation by a move. Replacing the variables attracts the subject to the left most position, and on the semantic side, the λµ-DRS associated with the d p replaces the variable w, while the other semantic variable y is replaced with the specific discourse referent d.

⊢                          (ε | infl | ε) (k \ t) / ⇐ v (v→t)→e→v→t λQλy 2 λe. Q(e)∧P(e) ∧agent(e, y 2 ) w:d w:e ⊢                          (w a pizza | eat | ε) v v → t
⊢                              (ε | ate | w a pizza) k \ t e → v →
y:k y:e ⊢                (ε | y | ε) k e y w:d w:e ⊢                              (ε | ate | w a pizza) k \ t e → v →
⊢                                          (y |
⊢                    (ε | the | children) k ⊗ d e µδ.[ | [d | child(d)] ⇒[ | δ(d)]] w:d, y:k w:e, y:e ⊢                                          (y |
⊢                          (the children | ate | a pizza) t v → t λe.eat(e, µγ.[p | piz(p) ∧ γ(p)], µδ.[ | [d | child(d)]⇒[ | δ(d)]]) ∧Pa(e, p)

∧P(e)∧Ag(e, d)

Finally, the complementiser turns the whole sentence into a complement by a merge, and semantically reifies the whole formula.

⊢                (ε | ε | ε) C / t (v → t) → t λQ.[e | (Q(e))] ⊢                          (the children | ate | a pizza) t v → t λe.eat(e, µγ.[p | piz(p) ∧ γ(p)], µδ.[ | [d | child(d)]⇒[ | δ(d)]]) ∧Pa(e, p)∧P(e)∧Ag(e, d) mg ⊢                          (ε | ε | the children ate a pizza) C t [e | eat(e, µγ.[p | piz(p) ∧ γ(p)], µδ.[ | [d | child(d)]⇒[ | δ(d)]]) ∧Pa(e, p)

∧P(e)∧Ag(e, d)]

Thus the syntactic derivation yields the following λµ-DRS:

[e|eat(e, µγ.[p|piz(p) ∧ γ(p)], µδ.[|[d|child(d)]⇒[|(δ d)]])
∧Pa(e, p)∧P(e)∧Ag(e, d)] Yet we need to internalise the predicates, as explained in 14, i.e. to move inside the scope of quantifiers the formulae involving these variables (notice that this is harmless, because we just performed the derivation, and the variables do not have the same name by coincidence nor by renaming) and this leads to the following λµ-DRS: For computing this term, we can drop the final ∧P(e) and the e box, since it is not going to interfere with the µ reductions. But we must be slightly cautious and write the λµ-DRS in the λ applicative style (((eate)p)d) rather than predicate logic, to make µ reduction more visible.

W = (((eat e)(µγ.[p|(piz p) ∧ (γ p)∧((Pa e)p)))(µδ.Y)) with Y = [|[d|(child d)]⇒[|(δ d)∧((Ag e)d)]]

We now have to reduce acording to the reduction rules in 13 this λµ-term and this will lead to the two readings. The first one is that the children shared a pizza, while the second one says that for every child there is a pizza that he ate. As λµ-reduction is not convergent, other readings may be obtained by applying different reductions when possible. For instance, after step 1 for which there is no choice, yielding W (µγ ′ .Z)(µδ.

Perspectives

The purpose of this paper was to describe a state of our work on categorial representation of generative grammars, which enables the automated computation of semantic representation, here viewed as DRSs. Nevertheless, some intriguing questions remain.

On the syntactic side, what would be a proof theoretical version of shortest move? As such conditions involve the history of proofs, that are proof terms, dependant types should provide a way to formulate such condition, but for linear logic they have not yet been much studied. Still on the syntactic side, representation of minimalist grammars with remnant movement (which leaves out headmovement) for which the correspondence is tighter by our work should be developed on particular phenomena, like VP rolls from Hungarian: as derivation intends to be quite lengthy, possibly some predetermined sequences or rules should be used, if they are prooftheoretically meaningful.

On the semantic side, some aspects deserve further study and improvement. The internalisation process, although harmless because it is performed just after parsing, is not to be recommended. Indeed, it depends on the name of the variable and modifies variable binding. Correlated to this issue, rules that depend on the name of a bound variable, the one associated with a movable constituent, should be avoided.

We nevertheless hope that this movement inside the categorial community will make colleagues happy, and especially Jim Lambek.

Works Cited

Figure 1 :

 1 Figure 1: Features and lexical entries in minimalist grammars

Figure 2 :

 2 Figure 2: Labels for product elimination rule.

  the semantic representation of the sentence [[φ]]. (iii) Nevertheless [[φ]] still contains µ variables and abstractions, which prevents us from interpreting directly [[φ]] as a formulae. Performing β and µ reductions (µ, µ ′ , ς) yields ordinary DRS that are usual the semantic representations of the sentence. The different scope readings result from the non confluence of µ reductions, as in de Groote (2001).

[

  e|eat(e, µγ.[p|piz(p) ∧ γ(p)∧Pa(e, p)], µδ.[|[d|child(d)]⇒[|δ(d)∧Ag(e, d)]]) ∧P(e)]

  (i) µ ′ reduction with α = γ (µ-variable), V = (eat e) and (α T ) = (γ p) replaced by (V(α ′ T )) = (γ ′ ((eat e)p)) yields: W (µγ ′ .[p|(piz p) ∧ (γ ′ ((eat e)p))∧((Pa e)p))(µδ.Y) (ii) A µ reduction with α = γ ′ (µ-variables), V = (µδ.Y) and (α T ) = (γ ′ ((eat e)p)) replaced by ((α ′ T )V) = ((γ ′′ ((eat e)p))(µδ.Y)) yields: W (µγ ′′ .[p|(piz p)∧((γ ′′ (((eat e)p)(µδ.Y)))∧((Pa e)p))]) (iii) Next we apply a ς-rule on γ ′′ , yielding: W [p|(piz p) ∧ (((eat e)p)(µδ.Y)) X ∧((Pa e)p)] (iv) The underbraced subterm: X = (((eat e)p)(µδ.Y)) is actually: (((eat e)p)(µδ.[|[d|(child d)]⇒[|(δ d)∧((Ag e)d)]])) and it can undergo a µ ′ -reduction with α = δ (µ-variable) and V = ((eat e)p) in which (α T ) = (δ d) is replaced with (α ′ (V T )) = (δ ′ ′ (((eat e)p)d)), thus yielding: X (µδ ′ .[|[d|(child d)]⇒[|(δ ′ (((eat e)p)d))∧((Ag e)d)]]) (v) finally a simplification by the ς-rule yields: X [|[d|(child d)]⇒[|(((eat e)p)d)∧((Ag e)d)]] If we insert the result of X into the result of W and add the final P(e) we obtain: [e|[p|(piz p) ∧ [|[d|(child d)]⇒ [|(((eat e)p)d)∧((Ag e)d)]]∧((Pa e)p)] ∧ P(e)] that is ∃e.P(e) ∧ ∃p (piz(p)∧Pa(e, p) ∧ ∀d (child(d) ⇒ (eat(e, p, d) ∧ Ag(e, d))))

  [|[d|(child d)]⇒[|(δ d)∧((Ag e)d)]])with Z = [p|(piz p) ∧ (γ ′ ((eat e)p))∧((Pa e)p)] instead of the µ reduction used in the first derivation, we can apply a µ ′ rule.(ii) A µ ′ -rule with α = δ, and V = (µγ ′ .Z)(α T ) = (δ d) replaced with (α ′ (V T )) = (δ ′ ((µγ ′ .Z)d)) yields: W µδ ′ .[|[d|(child d)]⇒[|(δ ′ ((µγ ′ . Z)d))∧((Ag e)d)]](iii) next we can apply a simplification ς rule for µδ ′ yielding:W [|[d|(child d)]⇒[| ((µγ ′ .Z)d) S ∧((Ag e)d)]]• the underbraced subterm S = ((µγ ′ .Z)d) that is S = ((µγ ′ .[p|(piz p) ∧ (γ ′ ((eat e)p))∧((Pa e)p)])d) can undergo a µ-reduction with α = γ ′ , β = γ ′′ (µ-variables) and V = d in which (αT ) = (γ ′ ((eat e)p)) replaced with (α(T V)) = (γ ′ (((eat e)p)d)) yielding: S (µγ ′′ .[p|(piz p) ∧ ((γ ′′ ((eat e)p))d)∧((Pa e)p)]) (iv) next we can apply to S a µγ ′′ simplification, yielding: S [p|(piz p) ∧ (((eat e)p)d)∧((Pa e)p)] If we insert the reduct of S into what we reduced W to, we get: W [|[d|(child d)] ⇒[|[p|(piz p) ∧ (((eat e)p)d)∧((Pa e)p)]∧((Ag e)d)]] If we add the [e|P(e) ∧ • • • that has been left out, we obtain: ∃e P(e) ∧ ∀dchild(d) ⇒ Ag(e, d) ∧ ∃p(piz(p) ∧ eat(e, p, d) ∧ Pa(e, p))

  ate | w a pizza)

	t
	v → t
	λe.
	eat(e, µγ.
	[p | piz(p)∧γ(p)],
	w)
	∧Pa(e, p)∧P(e)
	∧Ag(e, y)

It is possible to also consider weak movement, which leaves the -x subtree at is pace, but suppress the semantic information, and makes a copy of the tree structure with only the semantic features and moves it as we did. As we do not speak about semantic features, we skipped this possible rule.

Can one extends this definition of the generated language to Lambek grammars? Lambek calculus extends the above calculus with the introduction rules (or abstraction), and this requires to have context and variables (introduced by the axiom x : A ⊢ x : A). Since variables are abstracted only from leftmost or rightmost positions, one has to carry over context with words to prohibit illicit abstractions, hence the lightness of the above system without contexts is

lost.[START_REF] Amblard | Syntax and Semantics interacting in a minimalist theory[END_REF] Although Lambek grammars only describe context free languages, if the grammar is not compiled into a context free grammar, parsing by proof search is NP complete.

Actually Amblard (2007) does not include the head movemen case, but especially for this construct, the two kind grammars work just the same, mutatis mutandi.


Cyril Cohen
email: cyril.cohen@inria.fr

Formalizing real analysis for polynomials

When reasoning formally with polynomials over real numbers, or more generally real closed fields, we need to be able to manipulate easily statements featuring an order relation, either in their conditions or in their conclusion. For instance, we need to state the intermediate value theorem and the mean value theorem and we need tools to ease both their proof and their further use. For that purpose we propose a Coq library for ordered integral domains and ordered fields with decidable comparison. In this paper we present the design choices of this libraries, and show how it has been used as a basis for developing a fare amount of basic real algebraic geometry.

Introduction

The purpose of this work is to show how to formalize some real analysis. We particularly would like to point out how important are the choices we make in stating single lemmas. We also describe the basis we could have chosen to built the theory we describe, and why we think we made a good choice.

In order to achieve this goal, we reuse techniques from the mathematical components team to build a little bit of analysis, but only with polynomials for now. This allows to use only algebraic properties to express and prove analytic theorems. We hope these techniques ease the formalisation and the manipulations inside a Type Theoretic proof assistant such as Coq. And Coq's system is based on an intuitionistic logic.

When working in such an intuitionistic context, we don't have the excluded middle axiom anymore. However, this axiom is extensively used in standard mathematical reasoning and mathematical theorems are usually proved without wondering whether their proof is constructive or not.

A first solution would be to add the excluded middle to Coq. But this has two major drawbacks. The first one is that Coq is also a programming language, and supposing excluded middle is like supposing the existence of a program which doesn't exist. The second one is that it could introduce inconsistencies in the system, enabling us to prove the false, and thus prove anything.

An alternative, proposed by the SSReflect extension for Coq, is to have classical reasoning with a better granularity. Indeed, instead of supposing the excluded middle true for any property, we work with structures that provide a restricted version of excluded middle. For example, we define a structure of discrete type by requiring it to have decidable equality (this is an excluded middle limited to equality predicate on a given type).

This means that if we can find such a type, we just see it as an instance of this structure. For example, equality on natural number is decidable and thus we can view natural numbers as an instance of discrete type). This means that this restricted kind of excluded middle can be instantiated by the decision procedure of equality on the given type. Moreover, this introduces no inconsistency in the system because we never supposed there were an instance of the structure.

A third advantage is that we can represent decidable propositions as booleans. Since equality on boolean is decidable, the proof that two given booleans are equal is unique. This implies we can prove equivalence between two boolean predicate by proving the equality of these two predicate. That's why we use boolean predicates as much as we can, instead of propositions.

These techniques come historically from the proof of the four color theorem (cf [START_REF] Gonthier | A computer-checked proof of the four-colour theorem[END_REF]), which relies on combinatorics. This is a domain where boolean reflexion proved very useful.

The first part of this paper will describe what are the basis we took for our development. Then we discuss the importance of the way we stated lemmas, from a user point of view, and how we should consider it from a developing point of view. In a third part, we show how far we can go into mathematics of the theory we deal with. Finally we show an overview of some work in progress we derive from the latter theory.

We here do not pretend to build a notion of topology nor covering the basis for entire analysis. In fact, we intend to prove specific mathematics results, but we try to remain generic with regard to the way we enunciate notions and theorems. We then still have some hope the notions could be generalized to a bit more analysis, keeping the same kind of light formulation.

Disambiguation of the meaning of axiom When talking about axioms, one has to be careful whether he talks about an axiom of the system in which he is working (for example Coq), or an axiom of the theory on which he is working (for example, the axioms of the theory of groups, or of real closed field ). We will call global axiom the axioms of our system (which correspond to the Axiom command in Coq), and use axiom for the properties that generate some theory.

A representation for discrete real closed fields

Real analysis requires fixing a representation of real numbers. However, from a constructive perspective real numbers are not an easy topic. There are multiple possible implementations of R.

Implementation of real numbers

We discuss here the troubles we may encounter with real numbers, depending on the implementation we choose.

Classical Real numbers These are the real numbers we use in mathematics. They could be classically built as the completion of Q.

They are currently integrated in Coq by several global axioms (cf Coq standard library Coq.Reals.Raxioms). These global axioms give us the decidability and the totality of the order, archimedean property and the completeness property.

They are nevertheless pretty unsatisfactory because they have no implementation in Coq. No one could provide axiom-free Coq proof terms that satisfies these. No one could rely on them to compute or extract a program. It could even be considered as unsafe because when we load these real numbers into the system, we add definitively new global axioms. This endangers the consistency of the system. Indeed, adding global axioms incompatible with the system or incompatible between themselves leads to the ability to prove False.

Constructive Real Numbers There is also a constructive point of view of reals, as done in CoRN. Real numbers are here represented by functions outputting an approximation of the number. This has the good property to be constructible and hence have a concrete implementation. The construction could be made out of Cauchy sequences among other ways, as explained in [START_REF] Geuvers | Constructive reals in coq: Axioms and categoricity[END_REF].

There is even a work (cf [START_REF] Kaliszyk | Computing with classical real numbers[END_REF]) which relates the axiomatizes real numbers with the constructive one from CoRN, in a specific context. However, equality is not decidable in general. Hence ordering is not decidable either. Thus, we are not in the framework we chose.

Algebraic Real Numbers

The most satisfying model one for our purpose are algebraic real numbers. They are real roots of polynomials with coefficients in Q. They are a subset of constructive real numbers and have stronger properties. They still are contructive but they have also decidable equality, and also decidable order.

These kind of real numbers seem to fit our requirements. So we may decide to base our development onto them. However, no implementation of algebraic real numbers has been, to our best knowledge, done in Coq.

An interface for real numbers

However, we don't really need an implementation for our purpose. We are only interested in the first order theory of algebraic real numbers. That's why we formalize the theory of discrete real closed fields. This mean we only have to specify a structure requiring the real closed fields axioms. Then, the result we prove is valid for any model of real closed fields, including an implementation of real algebraic numbers. Moreover, giving such an implementation will validate our results, which all have the existence of real algebraic numbers as an hypothesis.

A real closed field is an ordered field where the intermediate value theorem holds for polynomials. We thus have to dispose of a representation of (discrete) ordered fields or more generally (discrete) ordered integral domains. Indeed, this allows to cover the case of relative numbers, which are a model of discrete ordered integral domains. And also rational numbers, which are a model of discrete ordered fields.

We then add the intermediate value theorem (abbrev. IVT ) as an axiom to get the theory of real closed field. This enables the possibility to do analysis. The IVT states that if a polynomial P changes its sign between a and b, then it has a root between a and b. We see in Section 4 that all this allows us to prove basic real analysis results, for polynomials. This is the least we could expect from this structure in order to do analysis.

About implementation techniques 3.1 Ordering and real closed fields in Coq

SSReflect libraries features an algebraic hierarchy (defining Rings, Integral Domains, and Fields for example). This hierarchy contains everything we need to formalize real closed fields except for the part which deals with ordering. Thus, we extend this hierarchy by adding an order structure on it. To build the hierarchy, the choice for representing the abstractions of Rings and Integral Domains (etc ...) has been to use Canonical Structures and Coercions (cf [START_REF] Garillot | Packaging mathematical structures[END_REF]).

The algebraic hierarchy has been built out of components called classes. A class is simply a record containing the laws and properties of a given structure. A class is made of what we call mixins. Mixins are the laws and properties we must add to a class, to make it a sub-class. For example the class of a fields, is made of the class of integral domains plus a mixin telling that units are the non null elements.

Mixin for Ordering Since we want our order to be decidable, we choose le to be a boolean predicate, this choice is justified in 3.2/ The order relation symbol is the only one required since we can deduce the strict inequality lt from the large one le and equality. The additional axioms for ordering say that le has to be a antisymmetric, transitive and total, and must be compatible with + and *.

Here is the order mixin we chose.

Record mixin_of (R : ringType) := Mixin { le : R -> R -> bool; _ : antisymmetric le; _ : transitive le; _ : total le; _ : forall z x y, le x y -> le (x + z) (y + z); _ : forall x y, le 0 x -> le 0 y -> le 0 (x * y) }.

with a notation x <= y for le and x < y for lt.

Integration in algebraic hierarchy

We have now to decide where to add this mixin in the existing algebraic hierarchy. Since we have no example of ordered ring below integral domains, and the relative numbers are an ordered integral domain, we chose to extend the hierarchy with an ordered integral domain structure, an ordered field structure and a real closed field structure:

Pragmatic formalization of lemmas

While building a library, the way functions and lemma are stated is as important as the content they provide. The key point is that the objects of the library should be as easy as possible to use. Choosing the way to state a lemma should depend on the advantages it provides.

We try here to make a list of principles we used and that makes life easier for the user. These principles are folklore for SSReflect advanced users but are not necessarily obvious. We illustrate these principles on examples either from SSReflect library or from our development about ordered rings.

Boolean reflexion Since we try to use as much as boolean predicates as we can to represent proposition, we need tools to ease the use of such lemmas. First we would really want that boolean properties make sense as statements. Indeed if eqT : T -> T -> bool is a decision procedure for some equality over the type T, we would like to state properties like that : Lemma eqT_correct : forall x y, (x = y) <-> (eqT x y).

But this makes no sense as such because eqT x y has type bool, not Prop. However, using Coq coercion system, we can define the following function as an implicit coercion. This enables us to state the previous lemma, which is in fact the following one, but where is_true has been automatically inferred, and hidden at pretty printing.

Lemma eqT_correct : forall x y, (x = y) <-> is_true (eqT x y).

The example eqT_correct we showed is what we call a reflexion lemma. This kind of lemma relates the boolean construction with an equivalent propositional formulation. And there are facilities to go from one representation to the other. The purpose of the equivalent proposition formulation is to provide new functionalities. For example, rewriting with e : eqT x y rewrites subterms eqT x y to true, whereas eqT_correct e rewrites x to y.

Privileging rewriting As a side effect and feature of the previous principle, equality is used instead of equivalence as much as possible and hence rewriting becomes one of the most used tactic in SSReflect.

Applied to our development, rewriting with a boolean property exy : x <= y which is in fact exy : x <= y = true replaces every occurrences of x <= y by true, in any context. This is easier than trying to isolate the predicate using a lot of case analysis and constructor introductions to try to apply it at the right places. This also enables us to use equivalence lemmas stated as equalities, such as ~~(x <= y)= (y < x) and replace occurrences of ~~(x <= y) by y < x (where ~~is the boolean not).

Combining rewrites

The SSReflect rewrite tactic has a different behavior than Coq standard one. We can give it pairs of lemmas to rewrite with. For example, if we have lxy : x <= y and lyz : y <= z, we can write rewrite (lxy, lyz).. The term (lxy, lyz) has type (x <= y)* (y <= z). Rewriting with this product will try to rewrite with the first element of the pair, and if it fails, the second one.

We used this feature to encode intervals. To state that x is between a and b, we can write a <= x <= b, which is a notation for a <= x && x <= b. This has the nice property to be a boolean, so we can combine it with boolean operators and equate it with another boolean to state some equivalence. However, once we have it in our hypotheses, it becomes less useful. Imagine we have the following goal. We can also chain rewriting, by rewrite lemma_1 lemma_2. . .lemma_n.

Conditional rewriting When we rewrite with a lemma such as

Lemma ltrW : forall (x y : R), x < y -> x <= y , if it successes, it will generate a new subgoal, asking for us to show x < y. For example, with the following goal But the rewrite command has a special syntax // to eliminate trivial subgoals. And in the previous example, both are trivial. Thus, rewrite ltrW // will solve the entire goal. However, if the subgoals are more complicated, // doesn't work anymore. For example with the following goal. Hopefully, the ? modifier allows to try to rewrite. For example if we do rewrite ltrW ?(ltr_trans lac)// (where ltr_trans is the transitivity lemma for <) , we get only one subgoal : Factorizing Lemmas and Naming conventions Due to these principles we end up with a large amount of lemmas. For example in our development about ordered rings, we have actually about 140 lemmas available to the user.

However, there could have been a lot more if we didn't use the previous and the following principles. Nevertheless, 140 is still huge, and we really don't want the user to get lost in the labyrinth of lemmas of the library. A good way to help him is to adopt systematic naming convention. This idea comes also from the four color theorem formalization (cf [START_REF] Gonthier | Notations of the four colour theorem proof[END_REF]).

The basis of this convention is naming the lemma by the defined symbols that appear in its statement, generally in order of appearance. For example:

Lemma sgr_mul : forall x y, sgr (x * y) = sgr x * sgr y.

is named as such because it involves sgr and mul.

We can put suffixes to add some more information when needed. For example, in Lemma ler_add2r : forall z x y, (x + z <= y + z) = (x <= y). Lemma ler_add2l : forall z x y, (z + x <= z + y) = (x <= y).

the suffix 2r (resp. 2l) means that we add on both sides of the inequality (2) and on the right side of the addition (r) (resp. on the left side of the addition (l)).

Having these systematic naming conventions have two major advantages. The first one is that user in the know can almost guess the statement associated to the lemma without having to Check or Print it. The second one is that a user looking for a lemma that talks about some defined symbols only has to do a Search on these names to find quickly the right one. We think this methodology has been so far very efficient.

Positioning arguments correctly When we write a lemma, we could place the arguments in almost any order we want as long as it respects dependencies. Whereas it doesn't matter in a mathematical point of view, it matters while concretely using the lemma in another proof. We must place in the first positions what the user needs to provide the most.

For example, the following Lemma ler_add2r : forall (x y z : R), (x + z <= y + z) = (x <= y) should be rewritten this way :

Lemma ltr_add2r : forall (z x y : R), (x + z <= y + z) = (x <= y) because if we want to rewrite from left to right, we would like to be able to explicit z without giving explicitly additional arguments (or put _).

Destructing with a specification

For case analysis over the trichotomy (x < y or x = y or x ≥ y) we use a feature of the destruct Coq tactic. This works by building the following inductive along with a lemma Lemma ltrgtP : forall x y, ltrgt_spec x y (x < y) (x > y) (x == y ).

Then, destructing ltrgtP automatically produces three subgoal with the corresponding hypothesis on top of the stack. Moreover, this destruction replaces occurrences of x < y, x > y and x == y.

For example while proving Lemma mulf_gt0 : forall x y, (0 < x * y) = ((0 < x && 0 < y) || ( x < 0 && y < 0)).

Once we introduce x and y, we get the subgoal

x y : R ==================================================== (0 < x * y) = ((0 < x && 0 < y) || (x < 0 && y < 0))

If we do case: (ltrgtP 0 y) we get three following subgoals. What's interesting here is to see how much work it did in only one case analysis : it generated three subgoals with a usable hypothesis on the left, and it substituted 0 < y, y < 0 and y == 0 by true or false, depending on the case.

An attempt to a little more automation

In an attempt to decrease the number of lemma, we tried to regroup some lemmas that could talk both about <= and <. For example, we could make one lemma gathering the two following results :

Lemma ler_add2r : forall (z x y : R), (x + z <= y + z) = (x <= y) . Lemma ltr_add2r : forall (z x y : R), (x + z < y + z) = (x < y).

into this only one lemma :

Lemma lter_add2r : forall (c : lter R) (z x y : R), c (x + z) (y + z) = c x y.

Where lter R is a structure capturing both < and <=. the good c is then inferred while rewriting.

After using it a little, we discovered it was not as easy to use as it seemed to be in the beginning. Indeed, rewriting with such lemmas allowed to factorize a little more. But with undesirable side effects, both in understanding and in practicing. The lemmas are more difficult to understand, and rewriting with them leads to a term with a beta-redex that we'd never want to see.

This design choice will be removed while updating this part of the order extension.

Into the basic theory of real closed fields

Basing ourselves on the theory of real closed fields, we'd like to show we can derive the basic facts about real analysis for polynomials.

Rolle's theorem and Mean Value theorem

The first thing is that we can quite easily prove constructively Rolle's theorem for polynomials which is a basic theorem in real analysis. (where p.[a] is the evaluation of a polynomial p and p^()' is its derivative).

But to prove it, we had to prove an intermediate lemma: which states that we can find c where either the derivative is null, or the polynomial itself is. Fortunately, we can prove that any polynomial has a number of root lower that its degree. So we can iterate the previous lemma a finite number of times (bounded by the degree), to prove Rolle's theorem.

Sketch of the proof of rolle_week We factorise P into P = (X -a) n+1 (Xb) m+1 Q Then there are two cases :

• Either Q(a)Q(b) ≤ 0, and by IVT, we can find c such that a < c < b and Q(c) = 0.

We conclude that P (c) = 0

• Or Q(a)Q(b) > 0.
We have

P = (X -a) n (X -b) m R with R = (X -a)(X -b)Q + (m + 1)(X -a)Q + (n + 1)(X -b)Q
Then we notice that R(a)R(b) < 0.

Hence there exists c such that a < c < b and R(c) = 0. Thus P (c) = 0

Sign on the right of root Let sgp right (P, x) be a function that gives the sign of a function in the right neighborhood of x. This means sgp right (P, x) is the sign of P (y) on any y between x and the first root of P from x (excluded).

There is also an algebraic characterisation of sgp right . Indeed, sgp right (x) is the sign of P (n) (x) for the first natural number n such that P n (x) = 0. So the following program computes this sign. And at some point we need to relate the specification we required at first with the definition we finally stated. We would like a lemma of this form ∃η x , ∀y, x < y < x + η x ⇒ sgp right (x) = sign(P (y))

.

To prove this constructively, we need to build a good η x . Thanks to the root isolation procedure we can find such an η x . For example, η x = x -x where x is the first root of P between x and b for any b such that x < b. (Thus b could be x + 1 as well as the upper bound of an interval on which we may be working).

Some experimentations showed that proofs seemed to be easier if we leave the choice of b to the user. This makes an η x,b dependent not only from x but also from b. Moreover, we decided to turn x < y < x+η x,b into a predicate on y, to make statements more readable. This corresponds to the right neighborhood of x in ]x, b[.

Defining neighborhood predicates

This leads us to define a neighborhood predicate, rather than defining a bound (η x,b ). This neighborhood predicate's graph is the set of y that are close enough of x on the right. Close enough in the sense their image by P all have the same sign.

We also need the same reasoning on the left. Here are the definitions we finally posed.

Definition neighpr p x b := (fun y => x < y < head b (roots_of p x b)). Definition neighpl p a x := (fun y => last a (roots_of p a x) < y < x).

Since this part of the work is still in progress, this is subject to change. But since the rest of the development (cf 5.2) that already uses these notion is almost done. But we can already guess they are a good abstraction over neighborhood for our particular purpose.

Towards quantifier elimination

As an application of the previous developments, we build a certified Quantifier elimination procedure for real closed field. Quantifier elimination is a standard way of proving the decidability of first order theories. The original result is from Tarski (cf [START_REF] Tarski | A decision method for elementary algebra and geometry[END_REF])

We base the development of this procedure and its certificate on a paper proof that can be found at the beginning of [START_REF] Basu | Algorithms in Real Algebraic Geometry[END_REF]. The method consists in eliminating one existential variable at a time. We first consider the case of one variable, and generalize to the case of multiple variable. However, this generalization poses problems in encoding the good structures to make the induction possible. But we have great hopes that the method we used for quantifier elimination on algebraically closed fields will work (cf [START_REF] Cohen | A formal quantifier elimination for algebraically closed fields[END_REF]). This proof will ensure the decidability of the first order theory of real closed field. However, this procedure is not efficient enough to compute the solution of basic concrete problems. But we hope the development of this library will ease the proof of more subtle quantifier elimination. One example of such procedures is the cylindrical algebraic decomposition, already implemented in Coq, but not yet certified (cf [START_REF] Mahboubi | Implementing the cylindrical algebraic decomposition within the coq system[END_REF]).

Conclusion

We showed how we took advantage of boolean reflexion to ease reasoning over these structure where at least equality and ordering are decidable. We also showed that the way we state the lemmas is very important from a user point of view. We saw that we should state as much equalities as possible. That we may sometimes introduce some inductive type to write a specification and use it to make case analysis. But also that naming conventions are important for the user to find its path. We also propose some ways to state concepts like neighborhood and interval in a way that eases its use as much as possible.

The major drawback of this work is the lack of automation. But we hope that the constructions it still helps to make leads to the formalization of a reflexive procedure for deciding formula with comparison (like the cylindrical algebraic decomposition). This seems to be a natural and very powerful enhancing of this work. Nevertheless, before building such a tactic, we can hope for some incomplete automation that would be able to solve simpler facts. An example of such a tactic already implemented in Coq is the fourier tactic, but it is not yet compatible with our development for technical reasons.

A good thing to make this work a little more concrete would be to instantiate the structure of real closed field we defined. This can be done by building the real closure of rational numbers, for example.

Another natural extension of this work would be to generalize the analytic part of the formalization. This means we could try to do a little more than analysis for polynomials. We showed how some standard notions of real analysis can be represented in Coq, but when its formalization is constructive. To achieve that, we exploited the very strong properties of polynomials, but it may be possible to abstract a bit more from this properties. For example, we could use polynomial approximations to extend our results. We could head to uniform polynomial approximation or to approximation using series (cf [START_REF] Boldo | Formal Proof of a Wave Equation Resolution Scheme: the Method Error[END_REF])

  Coercion is_true (b : bool) : Prop := (b = true).

  a b x : R x_in_ab : a <= x <= b ===================== a <= x This goal seems trivial, however, to solve it, we still have to translate the boolean conjunction into a propositional one, split it and rewrite with the left part. Now, if we state intervals in this way : x_in_ab : (a <= x)* (x <= b), thanks to pair rewriting, we just have to rewrite with x_in_ab. Moreover, we can define the following reflexion lemma : Lemma ccintP : (a <= x) * (x <= b) <-> a <= x <= b. And in the previous goal a b x : R x_in_ab : a <= x <= b ===================== a <= x rewriting with (ccintP x_in_ab) turns the goal to true.

  b) && (a + c < 2 * b) rewrite ltrW as well as rewrite ltrW // will both lead to the two subgoals : a b c: R lac : a < c lcb : c < b ======================= true && (a + c < 2 * b) ===== a < b

  true && (a + c < 2 * b)

  CoInductive ltrgt_spec x y : bool -> bool -> bool -> Set := | LtrgtLt of x < y : ltrgt_spec x y true false false | LtrgtGt of x > y : ltrgt_spec x y false true false | LtrgtEq of x = y : ltrgt_spec x y false false true.

  -> (0 < x * y) = ((0 < x && true) || (x < 0 && false)) ============================================================ y < 0 -> (0 < x * y) = ((0 < x && false) || (x < 0 && true)) ============================================================= y = 0 -> (0 < x * y) = ((0 < x && false) || (x < 0 && false))

  ∀a, b ∈ R, p ∈ R[X], a ≤ b∧p(a) = p(b) = 0 ⇒ ∃c, a < c < b∧p(b)-p(a) = p (c)•(b-a)And the Mean Value Theorem, which is a corollary to Rolle's Theorem. It is five lines of SSReflect proof script.∀a, b ∈ R, p ∈ R[X], a ≤ b ⇒ ∃c, a < c < b ∧ p(b) -p(a) = p (c) • (b -a)A constructive proof of Rolle's theorem for polynomials The statement of Rolle's theorem in SSReflect is Lemma rolle : forall a b p, a < b -> p.[a] = 0 -> p.[b] = 0 -> exists c, a < c < b /\ p^'().[c] = 0.

  Lemma rolle_weak : forall a b p, a < b -> p.[a] = 0 -> p.[b] = 0 -> exists c, a < c < b /\ (p^'().[c] = 0 \/ p.[c] = 0).

Fixpoint

  sgp_right (p : {poly R}) x := if p.[x] != 0 then sign p.[x] else sgp_right p^'()

Acknowledgments

The author wish to thank Assia Mahboubi for her regular feedback and contributions, both for the order library and its applications to real closed fields. But also for numerous comments and suggestions she made about this paper. I also which to thank George Gonthier for the discussions we had that helped the development, thanks to his advises and knowledge. Finally, I which to thank François Bobot for his last minute relecture and suggestions.

Root isolation

Given a and b (such that a < b), we are also able to compute the list of the roots of a non zero polynomial, that are between a and b (excluded).

The method is the following, we proceed by induction on the degree of the polynomial. Since P is non null, the base case is deg(P ) = 0. In this case, there are no roots, we return the empty list.

The induction hypothesis is "for all P such that deg(P) ≤ n, we can compute the roots of P ". Let's take P such that deg(P ) = n + 1, we have to show that we can compute its roots.

We can apply the induction hypothesis to P whose degree is n < n, and get the list x 1 , . . . , x m of the roots of P . Let's pose x 0 = a and x m+1 = b. For all 0 ≤ i ≤ m, P has the same sign between x i and x i+1 , hence P is monotonic on [x i , x i+1 ]. This means it has a root on [x i , x i+1 ] iff P (x i ) and P (x i+1 ) have different signs (by IVT and monotonicity). Moreover, if it has one, it's the only one (by monotonicity). Let z i be the root if it exists. the z i for i such that z i is well-defined plus the x i that are also roots of P are the roots of P . Qed.

Works in progress

Root isolation allows to define a constructive notion of neighbourhood for polynomial properties.

Neighborhood reasonning

At some point we'd like to reason about what happens near a point. This notion isn't straightforward to formalize because mathematician use sometimes the expression "near enough" without taking care to mention with regard to what. And even if they say ∀ε, ∃η(ε), s.t.P (ε, η(ε)), this doesn't mean that η : R + → R + is computable. This seems to prevent us from building an equivalent. While this may be true in the general case, in some cases where the η function is computable, we'd like to be able to handle it. For example, if the property that characterizes the neighborhood is that some polynomial P doesn't have a root, since we can isolate roots, we can explicit things.

Here is an example where such reasoning is needed