Jiří Maršík

Maxime Amblard
email: maxime.amblard@loria.fr

Integration of Multiple Constraints in ACG

Keywords: abstract categorial grammars, grammar engineering, grammatical formalisms, formal grammars, computational linguistics

This proposal is a first step towards a wide-coverage Abstract Categorial Grammar (ACG) that could be used to automatically build discourse-level representations. We focus on the challenge of integrating the treatment of disparate linguistic constraints in a single ACG and propose a generalization of the formalism: Graphical Abstract Categorial Grammars.

Abstract Categorial Grammars (ACGs) [START_REF] De Groote | Towards abstract categorial grammars[END_REF] have shown to be a viable formalism for elegantly encoding the dynamic nature of discourse. Proposals based on continuation semantics [START_REF] De Groote | Towards a montagovian account of dynamics[END_REF] have tackled topics such as event anaphora [START_REF] Qian | Event in compositional dynamic semantics[END_REF], SDRT discourse structure [START_REF] Asher | Sdrt and continuation semantics[END_REF] and modal accessibility constraints [START_REF] Asher | A montagovian treatment of modal subordination[END_REF]. However, all of these treatments only consider tiny fragments of languages. We are interested in building a wide-coverage grammar which integrates and reconciles the existing formal treatments of discourse and allows us to study their interactions and to build discourse representations automatically.

A presupposed condition to actually using an ACG to describe discourse in a large scope is to have a large scale ACG grammar in the first place. The work presented here was motivated by this quest for a wide-coverage ACG grammar, as seen from a point of view of language as a system of largely orthogonal constraints. Encoding ancillary constraints in a type system can make the system hard to read and understand. If multiple constraints written in the style of [START_REF] Pogodalla | Controlling extraction in abstract categorial grammars[END_REF] are to be enforced in the same grammar, we advocate for extending the formalism to prevent the incidental complexity that would otherwise emerge.

We begin with a short review of Abstract Categorial Grammars where we highlight the ways in which Abstract Categorial Grammars facilitate decomposition of linguistic description. We follow that by a closer look at an example of a linguistic constraint. This discussion motivates our proposed extension. We then present the Graphical Abstract Categorial Grammars and consider some of its formal properties. We then finish with an illustration of our approach which incorporates linguistic contributions from multiple sources into a single coherent and simple grammar and examine the limitations and challenges of adopting this approach.

Abstract Categorial Grammars

We first review the grammatical framework in which we conduct our work. Abstract Categorial Grammars are built upon two mathematical structures: (higher-order) signatures and lexicons.

Higher-Order Signatures

A higher-order signature is a set of elements that we call constants, each of which is associated with a type. Formally, it is defined as a triple Σ = <A, C, τ >, where:

-C is the (finite) set of constants -A is a (finite) set of atomic types τ is the type-associating mapping from C to T (A), the set of types built over A

In our case, T (A) is the implicative fragment of linear and intuitionistic logic with A being the atomic propositions. This means that T (A) contains all the a 2 A and all the α -• β and α ! β for α, β 2 T (A).

A signature Σ = <A, C, τ >, by itself, already lets us define an interesting set of structures, that is the set Λ(Σ) of well-typed lambda terms built upon the signature Σ. To make this structure even more useful, we often focus ourselves only on terms that have a specific distinguished type. Using this notion of a signature of typed constants and some distinguished type, we can describe languages of, e.g. tree-like (and by extension string-like), lambda terms.

Lexicons

The idea of a signature is coupled with the one of lexicon, which is a mapping between two different signatures (mapping the constants of one into welltyped terms of the other). Formally speaking, a lexicon L from a signature Σ 1 = <A 1 ,C 1 , τ 1 > (which we call the abstract signature) to a signature Σ 2 = <A 2 ,C 2 , τ 2 > (which we call the object signature) is a pair <F, G> such that:

-G is a mapping from C 1 to Λ(Σ 2 ) assigning to every constant of the abstract signature a term in the object signature, which can be understood as its interpretation/implementation/realization. -F is a mapping from A 1 to T (A 2 ) which links the abstract-level types with the object-level types that they are realized as. -F and G are compatible, meaning that for any c 2 C 1 ,w eh a v e`Σ 2 G(c):

F (τ 1 (c)) (we will be using F and Ĝ to refer to the homomorphic extensions of F and G to T (A 1 ) and Λ(Σ 1 )r e s p e c t i v e l y ) . Now we have enough machinery in hand to describe how ACGs define languages. Given some signature and a distinguished type, we can talk of the abstract language, which is the set of well-typed terms built on the signature and having the distinguished type. If we then also consider a lexicon and its abstract signature, then the language we get by mapping the abstract language of the signature through the lexicon is called an object language.

An ACG for us will then be just a collection of signatures with their distinguished types and the lexicons connecting these signatures, which we will write down in diagrams such as the ones in Figure 1.

The most common pattern will have us using two object signatures, Σ String and Σ Sem , for the surface forms of utterances (strings) and their logical forms (logical propositions) and an abstract signature, Σ Synt , which is connected to both of the object signatures via lexicons (as we can see in Figure 1(a)). Parsing is then just a matter of inverting the surface lexicon to get the abstract term and then applying to it the logical lexicon. Generation is symmetric, we simply invert the logical lexicon and apply the surface lexicon.

Systems of ACGs

Besides the pattern in Figure 1(a), there have been other techniques of decomposing linguistic description in the ACG literature. Here we will focus on two that are relevant to our work.

The first constitutes the Constraint pattern used throughout [START_REF] Pogodalla | Controlling extraction in abstract categorial grammars[END_REF]. Imagine we want our grammar to enforce a particular linguistic constraint, say that tensed clauses form islands for quantifier scope, and suppose we want to proceed by refining our types so as to make linguistic structures violating the constraint untypable. We could dive into our grammar and rewrite it to use the new types. However, we can also keep the existing grammar intact and complement it with a signature and a lexicon that translates that signature to the abstract-most signature of our existing grammar (Figure 1(b)). Usually, the new signature will resemble the prior abstract-most one, albeit with more fine-grained types necessary to express the constraint in question. This pattern is practical for examining linguistic constraints one-by-one and demonstrating that the formalism is capable of expressing them individually. However, this pattern does not serve us much in the context of ACGs when we try to build a grammar which incorporates many of these at the same time. This is due to the fact that after grafting on the first constraint, its added signature now becomes the abstract-most signature in the grammar. Any other constraint that would be added using the Constraint pattern would have to be translated into this new signature. This would mean that the type systems of newly added constraints would have to re-enforce all of the constraints introduced before, therefore nullifying almost any benefit of the pattern.

Another pattern we will briefly mention is the Elaboration pattern in which an edge in the diagram (a lexicon) is expanded into two edges and an intermediate node (signature). We can illustrate this pattern on Tree Adjoining Grammars [START_REF] De Groote | Tree-adjoining grammars as abstract categorial grammars[END_REF]. Suppose we have a signature describing TAG derivation trees and a lexicon which maps them to their yield. We might want to make this grammar richer, and arguably more synoptic, by elaborating the translation from derivation trees to yields by introducing derived trees and describe separately how both derivation trees produce derived trees and how derived trees produce the yields. This way, we can make emerge a potentially useful linguistic structure.

This pattern was used in [START_REF] Pogodalla | Generalizing a proof-theoretic account of scope ambiguity[END_REF] to elaborate the translation from the common Montague-style [START_REF] Montague | The proper treatment of quantification in ordinary english 10[END_REF] higher-order signature to its yield by introducing lower-order syntactic structures more reminiscent of TAG or CFG trees. This helps make a clear distinction between ambiguities caused by syntax and by semantics by segregating the purely syntactic description in the Syntax signature from the issues of operator scope that have to be solved in the SyntSem signature (Figure 1(c)). However, in classical ACGs, we cannot exploit this pattern as much as we would like. If we were to use this grammar as a kernel on top of which we would like to express a syntactic constraint, we would not be able to attach the constraint's signature directly to the Syntax node but we would instead need to attach it to SyntSem4 . This means that the syntactic constraint would end up being expressed in terms of the types of the syntax-semantics interface (SyntSem) rather than just pure syntax (Syntax), which only adds unnecessary complexity.

The Problem of Multiple Constraints

We will consider several linguistic constraints that have been given formal treatments in grammatical formalisms.

In French, negation is signalled by prepending the particle ne to the negated verb in conjunction with using a properly placed accompanying word, such as a negative determiner, in one of the verb's arguments. This phenomenon has been elegantly formalized in the Frigram interaction grammar [10].

(1) Jean ne parle à aucun collègue.

(Jean speaks to no colleague.)

(2) Jean ne parle à la femme d'aucun collègue.

(Jean speaks to the wife of no colleague.)

(3) Aucun collègue de Jean ne parle à sa femme.

(No colleague of Jean's speaks to his wife.)

We see here that the negative determiner aucun can be present in the subject or the object of the negated verb and it can modify the argument directly or be attached to one of its complements. Furthermore, we note that omitting either the word ne or the word aucun while keeping the other produces a sentence which is considered ungrammatical.

This difference in syntactic behavior between noun phrases that contain a negative determiner and those that do not has implications for our grammar. Since two terms that have an identical type in an ACG signature can be freely interchanged in any sentence, we are forced to assign two different types to these two different kinds of noun phrases.

This leads us to a grammar in which we subdivide the atomic types N and NP into subtypes that reflect whether or not they contain a negative determiner inside. Types of the other constants, such as the preposition de seen in ( 2) and (3), will constrain their arguments to have compatible features on their types and will propagate the information carried in the features to its result type, e.g.:

N de1 : NP NEG=F -• N NEG=F -• N NEG=F N de2 : NP NEG=F -• N NEG=T -• N NEG=T N de3 : NP NEG=T -• N NEG=F -• N NEG=T
In the above, we elaborate the types NP and N with features (NEG=F and NEG=T ) and we give the different types for the preposition de in the fragment for negation (N ). The types accept an NP and an N as arguments with any combination of values for the feature NEG, except for the case when both the prepositional NP and the N being modified both contain free negative determiners (i.e. there is no N de4 : NP NEG=T -• N NEG=T -• N NEG= ...). This encodes a constraint that there can be only one free negative determiner per phrase (free as in not hidden inside an embedded clause). Besides this constraint, the types also dictate how the information about negative determiners should propagate from the argument constituent to the complex constituent (in this case, it is simple disjunction).

Enforcing other constraints leads us to subdividing our "atomic" types even further (e.g. the authors of [START_REF] Pogodalla | Controlling extraction in abstract categorial grammars[END_REF] add features to the S and NP types to implement constraints about extraction). Other phenomena, such as agreement on morphological properties like number, gender, person or case, intuitively lead us to make our types even more specific.

If we were to use this approach to write a grammar that enforces multiple constraints at the same time, we would end up with complicated types, like the one below, which provide complete specifications of the various possible situations (in this grammar (C), the preposition de has 12 different types).

C de11 : NP NEG=T ,VAR=F ,NUM=PL -• N NEG=F ,NUM=SG -• N NEG=T ,NUM=SG
This creates two problems. Firstly, the number of such types grows exponentially with the number of features added. This can be fixed by introducing dependent types into the type system as in [START_REF] De Groote | Type-theoretic extensions of abstract categorial grammars[END_REF]. However, while this allows us to abstract over the combinations of feature values and write our grammar down concisely, it does not take away the complexity. The treatments of the various linguistic phenomena are all expressed in the same types making it hard to see whether they are independent or not. Since the treatments cannot be considered in isolation, reasoning about the entire grammar becomes difficult and so does enhancing it with more constraints. This is a fatal problem for a grammar which strives to cover a wide range of linguistic facts. We firmly believe that simplicity is a fundamental requirement for constructing a large and robust grammar and our proposal aims to reclaim that simplicity.

In our grammar, we would like to combine several constraints (Figure 1(b)), and possibly to also separate the syntactic ambiguities from the purely semantic ones (Figure 1(c)). However, trying to mix these strategies in the ACG framework forces us to solve all the constraints in a single type signature or contaminate the syntax-semantics interface with the implementation details of the syntactic layer, both of which introduce incidental complexity we want to avoid.

We would like to have a system which would be characterized by a diagram like the one on Figure 2 where the constraint signatures delimit the legal syntactic structures independently of each other and without interfering with the syntax-semantics interface. However, ACG diagrams are limited to arborescences and we are obliged to generalize them in order to get the expected interpretation.

Graphical ACGs

We define a graphical abstract categorial grammar as a directed acyclic graph (DAG) whose nodes are labeled with signatures (and distinguished types) and whose edges are labeled with lexicons, in other words, a mathematical reification of an ACG diagram that has been generalized from arborescences to DAGs. We then search for an appropriate semantics for these structures, i.e. how to determine what languages are defined by a graphical ACG.

Nodes as Languages

We first follow a paradigm in which nodes of the diagrams are interpreted as languages with the edges telling us how these languages are defined in terms of each other. A single arrow leading to a language means that the target language is produced from the source by mapping it through a lexicon. We now argue that the suitable meaning of two or more edges arriving at the same node is intersection of languages based both on the simplicity of the resulting definitions and on our expectations about the desired semantics. Fig. 2: A graphical ACG that implements two independent syntactic constraints and distinguishes syntactic and semantic ambiguities.

In an ACG diagram, a node with no inbound edges stands for an abstract language. This language is defined as the set of terms having the correct type. If a node has an inbound edge, and therefore a parent, then the elements of its language are also obliged to have an antecedent in the parent language. It is a small step to go from this definition to the following: the language of a node is the set of terms having the correct type and an antecedent in the language of any of its parent nodes. This correctly characterizes the current use of ACG diagrams, recognizing abstract languages as a special case of object languages. Furthermore, this restatement generalizes to DAGs and gives us the desired semantics for implementing multiple constraints: intersection.

We can formalize the above definitions by introducing the notions of intrinsic and extrinsic languages associated with some node v in a graphical ACG G:

I G (v)={t 2 Λ(Σ v ) | `Σv t : S v } E G (v)=I G (v) \ \ (u,v)∈E L (u,v) (E G (u))
The intrinsic language is just the set of terms built on the node's signature and having the node's distinguished type. The extrinsic language is established by taking the extrinsic languages of its predecessors, mapping them through lexicons and taking their intersection, or just taking the node's intrinsic language if it has no predecessors.

We then examine the relationship between the languages defined by ACGs and graphical ACGs (G-ACGs). Intrinsic languages correspond exactly to abstract languages and therefore the sets of languages definable by both are equal.

I = A

G-ACG extrinsic languages correspond to ACG object languages with intersection. More formally, while ACG object languages are ACG abstract languages closed on transformation by a lexicon, G-ACG extrinsic languages are ACG abstract languages closed on transformation by a lexicon and intersection 5 .

O = A L E = A L∩
If we want our grammatical framework to be modular w.r.t. the different linguistic constraints it encodes, we essentially need intersection 6 . Not only would we want a framework in which intersection is possible, we would also like it to be an easy operation. Graphical ACGs make intersections trivial to encode and as for expressive power, we know, from the equations above, that object languages are as expressive as extrinsic languages iff object languages are closed on intersection (which is, at this moment, conjectured to be false). This means that graphical ACGs are either a conservative extension providing a more convenient way of expressing intersection or are extending ACGs by adding only intersection, which enables constraint-based composition of grammars. While the interpretation of G-ACGs given above does have some nice properties, it fails to predict the intuitive understanding of more complex ACG diagrams. This is most visible in the diamond-shaped grammar on Figure 3. If we take a term from E D (Bottom), we know it has antecedents both in E D (Lef t) and E D (Right). However, these two do not have to share an antecedent in E D (Top). This contradicts the generative story one might imagine in which a single term from Top generates terms in Lef t and Right which generate a term in Bottom.

We can observe another peculiarity on a more practical example. Consider the G-ACG in Figure 2. In classical ACGs, one can always take an element in a signature, like Sem, and by transduction find its corresponding element in an another signature, like Syntax. However, in a G-ACG such as this, it is possible that the Syntax term we obtain by transduction does not belong to E G (Syntax) because it lacks antecedents in either Constr 1 or Constr 2 . This means that the notion of an extrinsic language is not capable to give us the set of all meaning terms in Sem which actually correspond to syntactically correct sentences in this G-ACG.

The above characteristics motivated us to explore alternative interpretations of G-ACGs. We will present one such alternative now, which exchanges the language-algebraic point of view for a generative one.

Nodes as Terms

In the new paradigm, we interpret the nodes of the graph as terms and the edges as statements that one term is mapped into another using a lexicon. This leads us to the definition of the pangraphical7 language of a node u in a G-ACG G.

A term t belongs to P G (u) whenever there exists a labeling T of the nodes of the graph such that:

-T u = t. -For all v 2 V (G), `Σv T v : S v . -For all (v, w) 2 E(G), L (v,w) (T v )=T w .
If we compare this new interpretation of G-ACGs to the former one, we find out that in the case when the graph of the grammar is an arborescence, they are actually equivalent. This means that in classical ACGs, where all the diagrams are arborescences, the two metaphors (nodes as languages and nodes as terms) can be, and are, used interchangeably. However, as we start to consider nonarborescent graphs, we find, interestingly, that the two paradigms diverge (i.e. 9G,u. E G (u) 6 = P G (u)).

The newly defined pangraphical languages solve the problem of extrinsic languages giving us counter-intuitive interpretations for some specific G-ACGs. Specifically, the members of P D (Bottom) in the diamond grammar have a single antecedent in P D (Top) and the language P G (Sem) (from Figure 2) contains only meanings expressible by syntactically correct sentences.

Pangraphical languages turn out to be at least as expressive as the extrinsic languages 8 . The proof is carried out by transforming a G-ACG such that a particular node will have the same pangraphical language in the latter G-ACG as the extrinsic language it had in the former. The nodes of the newly constructed G-ACG correspond to paths in the former one terminating in the node in question 9 . Thus the labelling of nodes with terms which certifies a given term's presence in the pangraphical language of the new G-ACG also serves as a proof of its presence in the extrinsic language of the old G-ACG and vice versa. This gives us the following ladder of expressivity

I ✓ E ✓ P
which can be complemented with the following series

I G (u) ◆ E G (u) ◆ P G (u)

Illustration

In this final section, we assemble a G-ACG which integrates the French negation constraint discussed in Section 2, the constraints on extraction introduced in [START_REF] Pogodalla | Controlling extraction in abstract categorial grammars[END_REF] and a constraint handling agreement in a single grammar specification to demonstrate our approach. We start with the extraction constraints. [START_REF] Pogodalla | Controlling extraction in abstract categorial grammars[END_REF] describes three different constraints on extraction, all of them expressed using the Constraint pattern (Figure 4(a)). We can take the union of these three G-ACGs to get the G-ACG on Figure 4(b). Next, we can incorporate knowledge from [START_REF] Pogodalla | Generalizing a proof-theoretic account of scope ambiguity[END_REF], by splitting the L Syn lexicon and introducing a new intermediate signature (Figure 5(a)). The new signature, Syntax, deals purely with syntax without any issues of operator scope and its functions have lower-order types than those in Syn. We will finally We notice that while the three constraints introduced in [START_REF] Pogodalla | Controlling extraction in abstract categorial grammars[END_REF] are expressed in terms of the Syn signature, our constraints Agr and Neg use a different interface, the Syntax signature, to constrain the languages being defined. The Cont i constraints are not actually constraining syntax itself, but the syntaxsemantics interface. This is in some cases a deliberate decision, since e.g. Cont 1 is the constraint enforcing that quantifier scope must not escape outside of tensed clauses. The Syntax signature is not equipped to talk about operator scope and so the constraint is expressed above the Syn signature. On the other hand, constraints Cont 2 and Cont 3 from [START_REF] Pogodalla | Controlling extraction in abstract categorial grammars[END_REF] are purely syntactic and therefore could be more easily expressed in terms of Syntax instead of Syn. However, we see it as a perk of our approach that we can ignore that and import the constraints wholesale without having to adapt them.

The Neg Signature

We will now look under the covers of the two signatures implementing the constraints, starting with negation and the Neg signature.

As was said in Section 2, we will proceed by splitting the atomic types N and NP into N NEG=F and N NEG=T , and NP NEG=F and NP NEG=T ,r e s p e c t i v e l y . We will use these new types to distinguish whether an N or NP phrase contains a negative determiner that can pair up with a negated verb. Where before we had a single type, we will now have possibly multiple types to account for the different values of the arguments' NEG features. Here are some representative examples:

N aucun : N NEG=F -• NP NEG=T N le1 : N NEG=F -• NP NEG=F N le2 : N NEG=T -• NP NEG=T N ne tv 1 :(NP NEG=F -• NP NEG=F -• S) -• (NP NEG=T -• NP NEG=F -• S) N ne tv 2 :(NP NEG=F -• NP NEG=F -• S) -• (NP NEG=F -• NP NEG=T -• S) N ne tv 3 :(NP NEG=F -• NP NEG=F -• S) -• (NP NEG=T -• NP NEG=T -• S) N aime : NP NEG=F -• NP NEG=F -• S N que1 :(NP NEG=F -• S) -• N NEG=F -• N NEG=F N que2 :(NP NEG=F -• S) -• N NEG=T -• N NEG=T
We see that the negative determiner aucun can only attach to phrases which do not already contain a free negative determiner and that the resulting phrase is marked as having a free negative determiner. On the other hand, the determiner le does not have any interaction with the new NEG feature and is still able to take any N phrase, preserving any free negative determiners inside. The type of the negative particle ne modifies a verb (in the example above, N ne tv i , a transitive verb) and produces a new verb that makes sure that at least one of its arguments contains a negative determiner. Verbs are not agnostic about the NEG feature. By default, they specifically demand it to be false, since a negative determiner cannot be coupled with a non-negated verb. Finally, the types of the relativizer que tell us two other things: the NP trace is considered as containing no negative determiners, and a relative clause does not care about or alter the presence of free negative determiners in the N it modifies.

The lexicon which translates from this signature to Syntax is a straightforward relabeling. Its items can be characterized by the following schema:

L N eg (N wordformi )=C wordform
where C wordform is the constant in Syntax corresponding to the wordform.

The Agr Signature

The Agr signature will be constructed using the same strategy as Neg. N and NP will be subdivided into N NUM=SG , N NUM=PL , NP NUM=SG and NP NUM=PL (we only treat number agreement in this example). Here are some example types:

A tatou : N NUM=SG A tatous : N NUM=PL A le : N NUM=SG -• NP NUM=SG A les : N NUM=PL -• NP NUM=PL A aime1 : NP NUM=SG -• NP NUM=SG -• S A aime2 : NP NUM=SG -• NP NUM=PL -• S A qui1 :(NP NUM=SG -• S) -• N NUM=SG -• N NUM=SG A qui2 :(NP NUM=PL -• S) -• N NUM=PL -• N NUM=PL
The types for nouns and determiners are quite predictable. For the transitive verb aime, we see that we need a second type to account for the fact that aime does not care about the number of the object. Finally, the relativizer qui enforces that the number of the trace NP in the relative clause must be the same as the number of the N being modified.

The lexicon L Agr follows exactly the same schema as that of L N eg .

Limits of Modularity

We have decomposed our grammar into 9 signatures and 8 lexicons. Besides making the grammar more readable and easily navigable, it also makes the grammar more attractive from a computational point of view. The complexity of parsing the highest abstract-most structures and verifying all the constraints is decomposed into smaller subtasks. A string can be parsed into its representation at the Syntax level fairly easily (compared to parsing it at the higher levels) since Syntax employs types of lower orders than the more abstract signatures. Finding the syntactic structure for a string is thus feasible. We then proceed to verifying the syntactic constraints. Here we can observe that the lexicons L N eg and L Agr are mere relabelings and therefore parsing (i.e. constraint verification) is trivial (i.e. decidable). Now in order to determine the meaning of our sentence, we have to continue parsing by finding an antecedent in Syn. This involves higher-order types used to encode the various scope-bearing operators. Finally, we can opt in to verify the high-level syntax-semantics constraints which employ dependent types. However, the lexicons in this case resemble relabelings and a semi-decidable procedure could be used to solve the problem. Having the grammar decomposed like this opens it up for computational processing by letting us engage in different tactics at different stages instead of having to parse a single hidden structure which enforces grammaticality w.r.t. every constraint. G-ACGs share these perks also with classical ACGs but they let use this composition in another dimension, which facilitates the writing of multiple constraints. However, it is important to keep in mind that the composability demonstrated above is limited only to the composition of constraints. If we would like to extend our language with, e.g., a new lexical category, then every signature and every lexicon would have to be extended to cover this new category. It is also important to point out that the constraint signatures that we have been composing are not light-weight objects. They are usually defined by taking an existing signature that describes the language at a relevant level and by strengthening (usually all) the types of that signature to enforce the constraint 10 . However, most of these type alterations are mundane and we believe that this is fertile ground for applying metagrammars.

Conclusion

We have considered the problem of building a wide-coverage ACG, specifically the problem of expressing a multitude of linguistic constraints. We have examined previous techniques and found no satisfying solution. We have thus provided an extension of the ACG formalism to solve the problem and justified the need for the increased expressivity. This embedding of syntactic constraints will contribute to an effort to define a syntax-semantics interface and later to build discourse structures.

In the end, our approach lets us define the syntax in a clean way using the idiomatic style of categorial grammars (simple atomic types like N , NP and S) and then define the constraints themselves the same way as they are defined in ACG research (such as is the case with [START_REF] Pogodalla | Controlling extraction in abstract categorial grammars[END_REF]).

Interesting avenues of future work include: digging deeper into the languagetheoretical properties of G-ACGs (Are ACG object languages closed on intersection? Are extrinsic languages as expressive as pangraphical languages?), searching for a metagrammatical description of constraint signatures to ease work on G-ACG grammars, and finally building large-scale grammars to verify the usability of our approach.

Fig. 1 :

 1 Fig. 1: Diagrams of systems of ACGs.

Fig. 3 :

 3 Fig. 3: The diamond-shaped G-ACG D.

  G-ACG merging the three extraction constraints.

Fig. 4 :

 4 Fig. 4: Combining the constraints on extraction.

  Adding our own syntactic constraints, Neg and Agr.

Fig. 5 :

 5 Fig. 5: Building the example grammar up to its final state.

This is due to the fact that ACG diagrams are always arborescences, in which the root node represents the abstract language from whose terms are generated the terms of all the object languages.

Can be shown by induction on the topological ordering of any given graphical ACG.

If I have a grammar that enforces A and a grammar that enforces B,t h e nIw a n tt o have access to the grammar of the language where both A and B are enforced.

As opposed to extrinsic languages, which are constrained only by their predecessors in the graph, pangraphical languages are constrained by the entire graph.

This might come as no surprise given the extended domain of constraints compared to extrinsic languages (constrained by the entire graph as opposed to just the node's predecessors).

This means that when the G-ACG is D, the diamond grammar, and the node in question is Bottom,t h e nw ew i l lh a v et w od i fferent nodes for the two paths [Top,Left,Bottom]a n d[ Top,Right,Bottom].

This makes the expressivity of model-theoretic syntactic formalisms such as Interaction Grammars, in which adding the lexical items for ne and aucun along with enforcing the Neg constraint takes only two tree descriptions [10], even more striking when compared to our approach.


Emmanuel Hainry
email: emmanuel.hainry@loria.fr

Jean-Yves Marion
email: jean-yves.marion@loria.fr

Romain Péchoux
email: romain.pechoux@loria.fr

Type-based complexity analysis for fork processes

Keywords: Implicit Computational Complexity, Tiering, Secure Information Flow, Concurrent Programming, PSpace

We introduce a type system for concurrent programs described as a parallel imperative language using while-loops and fork/wait instructions, in which processes do not share a global memory, in order to analyze computational complexity. The type system provides an analysis of the data-flow based both on a data ramification principle related to tiering discipline and on secure typed languages. The main result states that well-typed processes characterize exactly the set of functions computable in polynomial space under termination, confluence and lock-freedom assumptions. More precisely, each process computes in polynomial time so that the evaluation of a process may be performed in polynomial time on a parallel model of computation. Type inference of the presented analysis is decidable in linear time provided that basic operator semantics is known.

Introduction

We propose a type system for an imperative language with while loops and forks calls, which provides an upper bound on the complexity of a process by controlling its data flow. Threads are created dynamically and they do not share a global memory. Each fork call creates a new child process with a distinct identifier (id) and duplicates the execution context including the program counter. The parent process keeps the ids of its children (but not the converse). Communications between children and their parent are performed through the use of a wait instruction that allows a returning child to pass a value to its parent process. The domain of computation is, in essence, the set of strings, on which various admissible operators can be defined. Thus, we are able to use arrays of strings with respect to the typing limitation as in Example 1.

We demonstrate that each subprocess generated by a well-typed process (under some restrictions) runs in polynomial time (Proposition 2) and that the number of process offsprings is bounded by a polynomial (Proposition 3). As a result, the amount of interactions between two processes is also bounded by a polynomial. Thanks to Savitch's Theorem [START_REF] Savitch | Relationship between nondeterministic and deterministic tape classes[END_REF], we show that a program runs in polynomial space on a sequential machine (Theorem 2), and conversely (Theorem 3). This result is expressed in the central Theorem 1. As far as we know, it is the first characterization of FPSpace based on a typed system for an imperative language. The type inference procedure is computable in linear time in the program size (Proposition 1). As a result, applications about the complexity measure of process calculi may be considered. We refer to the conclusion for a discussion about practical issues.

That said, one of our main motivation is to understand the relationship between data flow control and computational complexity. In [START_REF] Marion | A type system for complexity flow analysis[END_REF], a type system was introduced for a sequential imperative programming language, characterizing the set of polynomial time computable functions. The idea behind such a typing system is to control the information flow in an execution by enforcing a data tiering discipline. The idea is that data are ramified into tiers in such a way that data at a given tier may only produce information at the same tier or at a lower tier. Thus, the type system prevents the alteration of upper tier data by lower tier data, following the principle of an integrity policy [START_REF] Biba | Integrity considerations for secure computer systems[END_REF]. From this observation, there is only a small step to do in order to devise a type system based on works on type-based information flow analysis. We refer to the survey [START_REF] Sabelfeld | Language-based information-flow security[END_REF] for further explanations. The type system assigns tiers (which are similar to security levels) to variables. As in [START_REF] Volpano | A sound type system for secure flow analysis[END_REF][START_REF] Smith | Secure information flow in a multi-threaded imperative language[END_REF], the type system prevents information to flow from lower tier variables to higher tier variables by direct or indirect assignments. From a complexity point of view, the main novelty here is that we have to control the information that flows between processes so that the termination of a father process does not depend on the return values of its children. For this, we suggest a three-tier lattice, {-1, 0, 1}, where tier 1 variables control the while loops, tier 0 variables are working data, and tier -1 variables are output values. Consequently, we prevent an unsafe declassification due to the termination of a process through the wait/return mechanism. Lastly, it is worth noticing that we establish a non-interference property (Proposition 2), which expresses the relationship between information flow and complexity.

There are several works, which are directly related to our results. On function algebra, a characterization of Pspace has been provided by ramified recursion with parameter substitutions [START_REF] Leivant | Ramified recurrence and computational complexity II: Substitution and poly-space[END_REF] and by ramified recurrence over functions [START_REF] Leivant | Predicative functional recurrence and poly-space[END_REF]. For lambda calculus, [START_REF] Gaboardi | A logical account of PSPACE[END_REF] introduced a typed lambda calculus based on Soft Linear Logic [START_REF] Lafont | Soft linear logic and polynomial time[END_REF], which identifies exactly Pspace. On functional languages, several characterizations of Pspace have been provided in [START_REF] Jones | The expressive power of higher-order types or, life without cons[END_REF] consisting in restrictions on data manipulation and on recursion schemes. The completeness proofs of the aforementioned works simulate alternating polynomial time Turing machines [START_REF] Chandra | [END_REF]. Another approach is the one of Pola [START_REF] Cockett | A categorical setting for lower complexity[END_REF] which relates complexity and category theory. On imperative languages, an approach consists in analyzing the growth of the data flow by means of a matrix calculus propagating constraints between variables [START_REF] Niggl | Certifying polynomial time and linear/polynomial space for imperative programs[END_REF][START_REF] Jones | A flow calculus of wp-bounds for complexity analysis[END_REF][START_REF] Moyen | Resource control graphs[END_REF]. Thus, Niggl and Wunderlich gave a characterization of Pspace [START_REF] Niggl | Certifying polynomial time and linear/polynomial space for imperative programs[END_REF]. On the complexity of message passing languages based on implicit computational complexity, Amadio and Dabrowski show how to obtain an upper bound on instants for synchronous languages by using quasi-interpretation based tools [START_REF] Amadio | Feasible reactivity for synchronous cooperative threads[END_REF][START_REF] Amadio | Feasible reactivity in a synchronous pi-calculus[END_REF]. More recently, Dal Lago et al proposed to polynomially bound process interactions by type systems based on Light Linear Logic [START_REF] Lago | Light logics and higher-order processes[END_REF][START_REF] Lago | Soft session types[END_REF]. Notice that the fragment of the process calculi is too weak to establish a completeness result. Lastly, the recent work of Madet [START_REF] Madet | A polynomial time lambda-calculus with multithreading and side effects[END_REF] proposes a multithreaded program with side effects also based on light linear logic which are polynomial.

2 Imperative language with forks 2.1 Syntax of processes Expressions, instructions, commands and processes are defined by the following grammar, where V is the set of variables and O is the set of operators. The size of an expression is

|X | = 1 and |op(E 1 , . . . , E n )| = n i=1 |E i | + 1. We note V(K), K ∈ Exp ∪ Proc the set of variables occurring in K. E , E 1 , . . . , E n ∈ Exp ::= X | op(E 1 , . . . , E n ) X ∈ V, op ∈ O I ∈ Inst ::= fork() | wait(E ) C , C ∈ Cmd ::= X :=E | C ; C | while E do C | skip | X :=I | if E then C else C P ∈ Proc ::= return X | C ; P

Informal semantics

The semantics is similar to the one of C programs and Unix processes. Each process has an id (a pid). When a fork command is executed, a new child process is created, that will run concurrently with its parent process with its own duplicated memory. The parent process knows the child id, whereas a child has no knowledge of its parent process id. A process P is evaluated inside a configuration, a triple (P, µ) ρ consisting of a process, a store µ mapping each variable to a value of the computational domain and a set of ids ρ. In a configuration, the process can be viewed as the code that remains to be executed, and ρ stores the children process id's. At the creation of a child process, the store µ and the program counter are duplicated, and ρ is ∅. The main process id is always 1. When a new child is created by a fork its id is automatically set to a new integer and it is recorded in the set ρ of the father's configuration. All the configurations corresponding to the main process and its subprocesses are stored inside an environment E , a partial function mapping the process id to a configuration. Processes do not share a global memory. Consequently, the only way for a process to communicate with its children is through the use of a wait(E ) instruction, which provides a one-way communication. The following program illustrates how to define distinct code that will be executed by the child but not the parent process and conversely.

For the parent, X contains the pid of its child, for the child, X contains 0.

P : X := f o r k ( ) ; // X contains the child pid i f X > 0 then { // father's code (X>0) Y := w a i t (X ) ; Y := " f a t h e r " } e l s e { // child's code (X=0) Y := " c h i l d " } return Y // The father returns "father" and the child returns "child" 2.3 Semantics of expressions, configurations and environments Domain. Let W be the set of words over a finite alphabet Σ including two symbols tt and ff that denote truth values true and false. Let ε be the empty word. The length of a word d is denoted |d |. As usual, we set |ε| = 0. Define as the sub-word relation over W, by v w , iff there are u and u of W s.t. w = u.v .u , where '.' is the concatenation. We write n to mean the binary word encoding the natural number n. Store. A store µ is a total function from process variables in V to words in W. Let µ{X 1 ← d 1 , . . . , X n ← d n }, with X i pairwise distinct, denote the store µ where the value stored by X i is updated to d i , for each i ∈ {1, . . . , n}. The size of a store µ, denoted |µ| is defined by |µ| = X ∈V |µ(X )|. Configuration. Given a store µ and a process P, the triplet c = (P, µ) ρ , where ρ is an element of P(N), is called a configuration. Let ⊥ be a special erased configuration that will be used to replace the content of a configuration once it has terminated: it no longer uses space. The size of a configuration is defined by |⊥| = 0 and |(P, µ) ρ | = |µ| + ρ, where ρ is the cardinality of ρ. Environments. An environment E is a partial function from N to configurations. The domain of E is denoted dom(E ) and we denote E its cardinal when it is finite. We abbreviate E (n) by E n . The size of a finite environment E is defined by

(X :=E ; P, µ)ρ c → (P, µ{X ← d })ρ if (E , µ) e → d (Assign) (if E then Ctt else Cff; P, µ)ρ c → (Ctt; P, µ)ρ if (E , µ) e → tt (Iftt) (if E then Ctt else Cff; P, µ)ρ c → (Cff; P, µ)ρ if (E , µ) e → ff (Ifff) (while E do C ; P, µ)ρ c → (P, µ)ρ if (E , µ) e → ff (While ff ) (while E do C ; P, µ)ρ c → (C ; while E do C ; P, µ)ρ if (E , µ) e → tt (While tt )
E = i∈dom(E ) |E i |. The notation E [i := c] is the environment E defined by E (j) = E (j) for all j = i ∈ dom(E ) and E (i) = c. As usual E [i 1 := c 1 , . . . , i k := c k ] is a shortcut for E [i 1 := c 1 ] . . . [i k := c k ]. The initial environment is noted E init [P, µ]
and consists in the main process with no child.

That is

E init [P, µ](1) = (P, µ) ∅ and dom(E init [P, µ]) = {1}. An environment E is terminal if the root process satisfies E 1 = (return X , µ) ρ .
Semantics. The transition → for process evaluation is provided in Figure 2. The (Fork) rule creates a new configuration, a new process, say of id n, with a new store, and adds it to the environment. The parent process records its child id n into the variable X on which the fork instruction has been called and the child id set of the parent is updated to ρ ∪ {n}. Note also that X is assigned to 0 in the child configuration. The (Wait) commands Z:=wait(E ) evaluates the expression E to some binary numeral n. If the process n is a terminating configuration E n with n ∈ ρ, then the output value µ (Y ) is transmitted and stored in the variable Z. Finally, the returning process n is killed by erasing it through the following operation E [n := ⊥]. Note that the side condition n ∈ ρ prevents locks.

E [i := c] → E [i := c ] if c c → c (Conf) E [i := (X :=fork(); P, µ)ρ] → E [i := (P, µ{X ← n}) ρ∪{n} , n := (P, µ{X ← 0}) ∅ ] (Fork) with n = E + 1 E [i := (X :=wait(E); P, µ)ρ] → E [i := (P, µ{X ← µ (Y )})ρ, n := ⊥] (Wait) if (E , µ) e → n,

Strong normalization, lock-freedom and confluence

Throughout the paper, given a relation →, let → * be the reflexive and transitive closure of → and let → k denote the k-fold self composition of →. A process P is strongly normalizing if there is no infinite reduction starting from the initial environment E init [P, µ] through the relation →, for any store µ. Given an initial environment E init [P, µ], for some strongly normalizing process P and some store µ, if

E init [P, µ] → * E , for some environment E such that there is no environment E , E → E , then either E is terminal, i.e. E 1 = (return X , µ ) ρ (the main process is returning) or E 1 = (X :=wait(E); C , µ ) ρ (we say that the environment E is locked). A process P = C ; return X is lock-free if for any initial environment E init [P, µ], there is no locked environment E such that E init [P, µ] * → E . A process P is confluent if for each initial environment E init [P,
µ] and any reductions E init [P, µ] → * E and E init [P, µ] → * E there exists an environment E 3 such that E → * E 3 and E → * E 3 . A strongly normalizing, lock free and confluent process P computes a total function f : W n → W defined:

∀d 1 , . . . , d n ∈ W, f (d 1 , . . . , d n ) = w if E init [P, µ[X i ← d i ]] → * E , for some terminal environment E with E 1 = (return X , µ ) ρ and µ (X ) = w .
3 Type system 3.1 Tiers and typing environments.

Tiers are elements of the lattice ({-1, 0, 1}, ∨, ∧) where ∨ and ∧ are the least upper bound operator and the greatest lower bound operator, respectively. The induced order, denoted , is such that -1 0 1. In what follows, let α, β, . . . denote tiers in {-1, 0, 1}. Tiers will be used to type both expressions and commands. Operator types τ are defined by τ ::= α | α -→ τ . As usual, we will use right associativity for -→. A variable typing environment Γ maps each variable in V to a tier. An operator typing environment ∆ maps each operator op to a set of operator types ∆(op), where the operator types corresponding to an operator of arity n are of the shape

τ = α 1 -→ . . . -→ α n -→ α.
Intuitively, each tier variable has a specific role to play:

tier 1 variables will be used as guards of while loops. They should not be allowed to take more than a polynomial number of distinct values; tier 0 variables may increase and cannot be used as while loop guards; tier -1 variables will store values returned by child processes and cannot increase. Intuitively, they play the role of an output tape.

3.2 Well-typed processes.

Typing rules. Figure 3 provides the typing rules for expressions, commands and processes. Typing rules consist in judgments of the shape Γ, ∆ K : α, K ∈ Exp ∪ Cmd, meaning that K has type α under variable and operator typing environments Γ and ∆, respectively. There are some important points to explain in this type system. First, the typing discipline precludes values from flowing from tier α to tier β, whenever α β and α = β. Consequently, the guards of while loops are enforced to be of tier 1 in rule (CW). Moreover, in a (CB) rule, we enforce the tier of the guard to be equal to the tier of both branches. Also note that the subtyping rule (CSub) is restricted to commands in order not to break this preclusion. On the opposite, information may flow from tier 1 to tier 0 then to tier -1. This point is underlined by the side condition of the (CA) rule. The (F) rule enforces the tier of the variable storing the process id to be of tier 0 since the value stored 3. Type system for expressions, instructions, commands and processes will increase dynamically during the process execution. Finally, the tier of the variable storing the result returned by a child process (rule (W)) has to be of tier -1, which means that no information may flow from a variable of a child process to tier 0 and tier 1 variables of its parent process. Notations. In practice, we write C : α to say that C is of type α, and E α to says that E is of type α under the considered environments.

Γ (X ) = α (EV) Γ, ∆ X : α Γ, ∆ Ei : αi α1 -→ . . . -→ αn -→ α ∈ ∆(op) (EO) Γ, ∆ op(E1, . . . , En) : α Γ, ∆ X : 0 (F) Γ, ∆ X :=fork() : 0 Γ, ∆ E : 0 Γ, ∆ X : -1 (W) Γ, ∆ X :=wait(E ) : -1 Γ, ∆ X : α Γ, ∆ E : α E ∈ Exp α α (CA) Γ, ∆ X :=E : α Γ, ∆ C : α Γ, ∆ C : α (CC) Γ, ∆ C ; C : α ∨ α Γ, ∆ E : 1 Γ, ∆ C : α (CW) Γ, ∆ while(E )do{C } : 1 Γ, ∆ E : α Γ, ∆ C : α Γ, ∆ C : α (CB) Γ, ∆ if E then C else C : α (CS) Γ, ∆ skip : α Γ, ∆ C : α α β (CSub) Γ, ∆ C : β Γ, ∆ X : β (R) Γ, ∆ return X : β Fig.
Example 1. The following example illustrates how we can program a reduce operation used in parallel prefix sum [START_REF] Ladner | Parallel prefix computation[END_REF]. The problem consists in computing the greatest element among n integers in an array-like structure (A[0], . . . , A[n -1]).

max reduce ( n 1 , A 0 ) : : = r 0 := 0 : 0 ; f -1 := A[ r ] 0 : -1 ; f l a g 0 := t t : 0 ; while (n 1 = 1)

1 do { i f f l a g 0 then { // not finished p i d l 0 := f o r k ( ) : 0 i f ( p i d l >0) 0 then { // father process r 0 := 2 * r +2: 0 ; p i d r 0 := f o r k ( ) : 0} e l s e { r 0 := 2 * r +1: 0 } // left son i f ( p i d r ==0) 0 o r ( p i d l ==0) 0 then { f -1 := A[ r ] 0 : 0 ; } e l s e { f l a g 0 := f f : 0 ; // father x l -1 := w a i t ( p i d l ) : 0 ; xr -1 := w a i t ( p i d r ) : 0 ; f -1 := max( f -1 , max( x l , xr ) ) : 0 ; } } n 1 := h a l f ( n ) 1 : 1 } // end of while return f : -1
The notation A[r] simply denotes the access to cell r of the array A. The program queries the first element of the array A[0] then will spawn two children subprocesses, each one exploring one half of the array (the left son will compute the max of [START_REF] Cockett | A categorical setting for lower complexity[END_REF], A [START_REF] Lafont | Soft linear logic and polynomial time[END_REF], . . .}). When labelling the nodes of the subprocesses tree with the character each process checks by itself, it is such that the array is a breadth first search of it.

{A[i]; 2 k -1 ≤ i ≤ 2 k + 2 k-1 -2, k ≥ 1} = {A[1], A[3], A[4], A[7], . . .}, the right son computing the max of {A[i]; 2 k + 2 k-1 - 1 ≤ i ≤ 2 k+1 -2, k ≥ 1} = {A[2], A[5], A
Notice that the typing of commands uses the subtyping rule CSub.

We find convenient to describe now the nature of operators used, that will be presented in the next section (Definitions 1 and 2). The get operation on arrays, expressed above by the assignment f := A[r], is a neutral operation of type 0 -→ 0 -→ 0 and it can be in Ntr because of its type. The length n and the index r are identified by their binary notations. So the operators 2 * r + 2 and 2 * r + 1 increase the length by 1 and are positive operators of type 0, 0 -→ 0, and so are in Pos. Similarly, the operator half(n) divides the length n by two, that is it deletes a letter. So, it is a neutral operator of type 1 -→ 1 and is in Ntr. The predicates or, = are typical neutral operators of types resp. 0 -→ 0 -→ 0 and 1 -→ 1 -→ 1. However the typing implies that or ∈ Ntr ∪ Pos, and = ∈ Ntr. Lastly, max is a max operator of type -1 -→ -1 -→ -1 and is in Max.

Safe processes, type inference and complexity

Neutral, max, and positive operators

The type system guarantees that information flow goes from tier 1 to tier -1, and prevents any flow in the other way from a lower tier to higher tier. But this is not sufficient to bound process resources. We need to fix the class of operator interpretations based on their typing. For that we define neutral operators (that make the variables decrease and preserve tier), max operators (that do not make variables grow and preserve lower tiers but not tier 1), and positive operators (that can only produce a result of tier 0 as they can create something bigger than their arguments). Definition 1.

An operator op is neutral if:

(a) either op computes a binary predicate (i.e. the codomain of op is {tt, ff}).

(b) or ∀d 1 , . . . , d n , ∃i ∈ {1, . . . , n}, op (d 1 , . . . , d n ) d i . 2. An operator op is max if ∀(d i ) 1,n | op (d 1 , . . . , d n )| ≤ max i∈[1,n] |d i |. 3. An operator op is positive if ∀(d i ) 1,n , | op (d 1 , . . . , d n )| ≤ max i∈[1,n] |d i | + c, for a constant c ≥ 0.
Say that a type α 1 -→ . . . -→ α n -→ α is decreasing if α ∧ i=1,n α i . We now give a partition of operators into three classes which depend both on their types and on their growth rates.

Definition 2 (Safe operator typing environment). An operator typing environment ∆ is safe if each type given by ∆ is decreasing and there exist three disjoint classes of operators Ntr, Max and Pos such that for any operator op and ∀α 1 -→ . . . -→ α n -→ α ∈ ∆(op), the following conditions hold:

-If op ∈ Ntr then op is a neutral operator.

-If op ∈ Max then op is a max operator and α = 1.

-If op ∈ Pos then op is a positive operator and α = 0.

Intuitively, expressions in while guards are of tier 1 and so the iteration length just depends on the number of possible tier 1 configurations. Inside a while loop, we can perform operations on variables of other tiers. The tier -1 values are return values and processes are confined in the sense that the information flow of a process does not depend on a return value.

Main result

Proposition 1 (Type inference). Given a safe operator typing environment ∆, deciding if there exists a variable typing environment Γ such that the typing rules are satisfied can be done in time linear in the size of the program.

Proof. We encode the tier of each variable X by 3 boolean variables x 1 , x 0 and x -1 . We enforce that variable X is of exactly one tier will be encoded by (¬x 0 ∨¬x 1 )∧(¬x 0 ∨¬x -1 )∧(¬x 1 ∨¬x -1 ). Each command gives some constraints. Thus, in the case of an assignment X := op(Y ), we need to encode Γ (Y ) ≥ Γ (X ), which can be represented as (¬y -1 ∨ x -1 ) ∧ (¬y 0 ∨ ¬x 1 ) ∧ (¬x 1 ∨ y 1 ). As a result, the type inference problem is reduced to 2-SAT.

Definition 3 (Safe process). Given Γ a variable typing environment and ∆ an operator typing environment, we say that a process P is a safe process if:

-P is well-typed with respect to Γ and ∆, i.e. Γ, ∆ P : β; -∆ is safe.

The main result below is a consequence of the soundness Theorem 2 and the completeness Theorem 3 Theorem 1. The set of polynomial space computable functions is exactly the set of functions computed by strongly normalizing, lock-free, confluent and safe processes, where a unit-cost is taken as the cost of an operator computation.

Therefore, the process in example 1 can run within a polynomial space. It is worth noticing that the demonstration below says more about process interaction and runtime, which are, in fact, polynomially bounded as we shall see.

Complexity soundness

Process runtime

We establish that each process runs in polynomial time if the time measure is the number of reductions. We follow the line of the soundness proof of [START_REF] Volpano | A sound type system for secure flow analysis[END_REF] to demonstrate a non-interference property. We first prove two lemmas 1 and 2 in order to express that an expression of tier 1 just depends on tier 1 variables, and not on lower tier variables. As a result, there is only a polynomial number of tier 1 configurations, because of neutral operator growth rate. From the security point of view, this means that a variable of tier (level) 1 can be updated by information of the same tier of integrity. Proposition 2 corresponds to the non-interference property. Intuitively, it says that the complexity of a process depends only on tier 1 variables, and so it is not modified if values of lower tiers are updated and so the process runtime does not interfere with lower tier values.

Lemma 1 (Simple security). Given a safe process P wrt typing environments Γ and ∆, if Γ, ∆ E : 1, for an expression E in P, then for each X ∈ V(E ), Γ (X ) = 1 and all operators in E are neutral.

Proof. By induction on E .

Given a typing environment Γ say that |µ| i = Γ (X )=i |µ(X )|. We will first prove that that the values taken by each tier 1 expression are at most in polynomial number.

Lemma 2. Given a safe process P wrt typing environments Γ and ∆, for each expression E in P such that Γ, ∆ E : 1, the number of distinct values taken by E during the evaluation of the initial environment E init [P, µ] is bounded polynomially in |µ| 1 .

Proof. A store can be updated either (i) by using a fork instruction, (ii) by using a wait instruction or (iii) by assigning the result of an expression. The typing discipline prevents variables assigned to in (i) and (ii) to be of tier 1. For (iii), we have E = op(E 1 , . . . , E n ), for some neutral operator op, by Lemma 1. Consequently, the result of the computation is either tt or ff or a subword of the initial values. The number of sub-words being quadratic in the size, the number of distinct values of tier 1 variables is at most quadratic in |µ| 1 .

The relations ⇒ i are defined to express the computation of the process of id i. Definition 4 (⇒ i ). Given two environments E and E such that E → E , we write E → i E if the transition → corresponds to the evaluation of the process in the configuration E i of E . In the same way define the transition

E → =i E if there exists k = i such that E → k E . Now define ⇒ i by E ⇒ i E if there are environments E 1 , E 2 such that E → * =i E 1 → i E 2 → * =i E .
The proposition below expresses that the number of instructions performed by a single process is bounded by a polynomial in the tier 1 initial values. Intuitively, this means that each process runs in polynomial time, in the tier 1 initial values, if we do not count the waiting time due to forks.

Proposition 2 (Non-interference wrt time). Given a strongly normalizing and safe process P, there is a polynomial Q such that, for each initial environment

E init [P, µ], ∀i ∈ N, if E init [P, µ] ⇒ k i E then k ≤ Q(|µ| 1 ).
Proof. The typing discipline enforces all the expressions in while-loop guards of a safe process to be of tier 1. The evaluation of tier 1 values does not depend on lower tier values. By Lemma 2, the number of values taken by tier 1 variables during the evaluation is bounded by Q(|µ| 1 ) for some polynomial Q. If a process enters twice in the same configuration with the same tier 1 values, then the computation loops forever. Consequently, if P is strongly normalizing then all the while loops are executed at most Q(|µ| 1 ) times.

Process spawning

Now, we demonstrate that given a strongly normalizing and safe process the number of children of a process (Lemma 3), the number of process generations (Lemma 4) and the size of a configuration (Lemma 5) are polynomially bounded.

Definition 5. Given a finite environment E , the process tree T (E ) is defined:

the nodes are the configurations {E 1 , . . . , E E } and the root is

E 1 ; -for each l ∈ [1, E ], there is an edge from E l = (P, µ) ρ to E k , if k ∈ ρ.
The degree d(T ) corresponds to the number of children generated by fork instructions of a given process. The height h(T ) is the number of nested processes.

Lemma 3. Given a strongly normalizing and safe process P, there exists a polynomial Q such that, for each initial environment

E init [P, µ], if E init [P, µ] → * E then d(T (E )) ≤ Q(|µ| 1
). In other words, for each E i = (P i , µ i ) ρi , i ≤ E , the number of subprocesses is bounded by Q(|µ| 1 ), i.e. ρ i ≤ Q(|µ| 1 ).

Proof. By Proposition 2, there is a polynomial Q such that the transition → i is taken at most Q(|µ| 1 ) times, which bounds the number of executed fork instructions.

Lemma 4. Given a strongly normalizing and safe process P, there exists a polynomial Q such that, for each initial environment

E init [P, µ], if E init [P, µ] → * E then h(T (E )) ≤ Q(|µ| 1 ).
Proof. By Proposition 2, there is a polynomial Q which bounds the number of executed instructions and which just depends on the size of tier 1 initial values. Now, when X := fork() is performed, the parent process store is duplicated in the child process store, except for the value of X . But X is of tier 0 and so has no impact on the computational time of both processes. Next, a fork command has been executed in the parent process. So, the runtime of the child generated is strictly less than the runtime of its father. Therefore, we deduce that Q bounds the height of the process tree.

We end by showing that subprocess stores are polynomially bounded in the size of the initial store, which is a consequence of the non-interference property, as stated in Proposition 2.

Lemma 5. Given a strongly normalizing and safe process P, there exists a polynomial S such that, for each initial environment

E init [P, µ], if E init [P, µ] → * E then ∀i ≤ E , if E i = (P i , µ i ) ρi then |µ i | ≤ S(|µ| 1 ) + |µ| 0 + |µ| -1 .
Proof. There are three cases to consider. First, a variable of tier 1 is updated by an expression of tier

PSpace abiding evaluation strategy

We define a deterministic evaluation strategy starting from the initial environment and evaluating it until it reaches a wait instruction for a process n. Then, the strategy runs the process n until it returns a value. Formally, define a state s = (E , l) to be a pair of an environment E and a stack l of ids representing the queued processes. The initial state is (E init [P, µ], [START_REF] Amadio | Feasible reactivity for synchronous cooperative threads[END_REF]). We denote :: the stack constructor.

1. If E → h E for some rule (R) of Figure 2, R = W ait, then (E , h :: q) (E , h :: q) 2. If E h = (X := wait(E ); P, µ) ρ and (E , µ) e → n then (E , h :: q) (E , n :: h :: q) 3. If E n = (return X , µ) ρ and E h = (Y :=wait(E ); P, µ ) ρ then (E , n :: h :: q) (E , h :: q) where E → h E for the (Wait) rule of Figure 2.

Notice that the rule (2) implies that (E , µ ) e → n in rule (3).

Lemma 6 (Correction Lemma). Given a strongly normalizing and confluent process P and an initial environment E init [P, µ], if there exists E such that [START_REF] Amadio | Feasible reactivity for synchronous cooperative threads[END_REF]) and µ (X ) = µ (X ), where [START_REF] Amadio | Feasible reactivity for synchronous cooperative threads[END_REF] is the stack containing the single process 1.

E init [P, µ] → * E [1 := (return X , µ ) ρ ] then there exists E s.t. (E init [P, µ], [1]) * (E [1 := (return X , µ ) ρ ],
The size of a stack |l| is the number of elements in it (e.g. |[1]| = 1).

Lemma 7. Given a strongly normalizing and safe process P, there is a polynomial Q such that for each initial environment E init [P, µ] and each stack l, if

(E init [P, µ], [1]) * (E , l) then (i) |l| ≤ Q(|µ|) and (ii) E ≤ Q(|µ|).
Proof. The strategy explores the process tree using a stack. The height of the stack corresponds to the number of nested processes. The first inequality follows Lemma 4. Next, by combining Lemmata 3 and 5, we obtain the second inequality.

Theorem 2 (Soundness). A strongly normalizing, confluent and safe process P can be evaluated in polynomially bounded space using strategy , where a unit-cost is taken as the cost of an operator computation.

Completeness

Let us show that each polynomial space computable function can be computed by a strongly normalizing and safe process. Theorem 3. Every polynomial space function is computable by a strongly normalizing, lock-free and safe process P.

Proof. We present how to compute the value of a quantified boolean formula (QBF). The program below may be seen as a skeleton from which we may simulate, for example, an alternating Turing machine running in polynomial time. Consequently, the computation of a polynomial space function necessitates to compute its output bit by bit, which may be uniformly performed by generating each address and querying the output bit. The program below generates 2 n forks where n is the number of variables. We suppose that the concrete syntax of a QBF is implemented as a string phi of tier 1. Two neutral operators kind and variable of type 1 -→ 1 return the quantifier kind and the variable bound at the root of phi. The neutral operator next of type 1 -→ 1 erases the root quantifier and moves to the next one. The positive operator evaluate of type 1, 0 -→ 0 computes a boolean formula with respect to an evaluation encoded as an array of booleans, which is an NC 1 complete problem [START_REF] Buss | The boolean formula value problem is in ALOGTIME[END_REF]. As in example 1, arrays are words of type 0, whose length is bounded by phi. The set array operator, that we conveniently note vartab[x] := tt, is a positive operator of type 0, 0 -→ 0. We consider the array to be pre-allocated using a calloc operator that can be implemented using a positive operator in a loop.

This program has two big while loops: the first one generates 2 n subprocesses, one for each possible variable configuration, for each variable, the father will assign tt and the son will assign ff; the second one gathers the results of the children, making a disjonction with the parent if they correspond to a ∃, a conjonction for a ∀. qbf (phi) ::= p s i 1 := p h i 1 : 1 ; q 1 := kind ( p h i 1 ) : 1 ;

x 1 := v a r i a b l e ( p h i 1 ) : 1 ; i 0 := 0 0 : 0 ; // son number of a process p i d t a b 0 := c a l l o c ( p h i 1 , p h i 1 ) : 0; v a r t a b 0 := c a l l o c ( p h i 1 , t t ) : 0; while ( q 1 == ' ∃ ' ) o r ( q 1 == ' ∀ ' ) do { p h i 1 := next ( p h i 1 ) : 1 ; p i d 0 := f o r k ( ) : 0 ; i f p i d 0 >0 then { // father process p i d t a b [ i ] := ( pid , q ) : 0 ; v a r t a b [ x ] := t t : 0 ; i 0 := i + 1 0 : 0 } e l s e { // son process v a r t a b [ x ] := f f : 0 ; i 0 := 0 0 : 0} // end of else q 1 := kind ( p h i 1 ) : 1 ; x 1 := v a r i a b l e ( p h i 1 ) : 1 ; } // end of while r e s -1 := e v a l u a t e ( p h i 1 , v a r t a b ) 0 : 0 ; while ( s t a t e ( p s i 1 ) == ' ∃ ' ) o r ( s t a t e ( p s i 1 ) == ' ∀ ' ) do { p s i 1 := next ( p s i

Conclusion

We established that a typed process will generate only a polynomial number of offspring processes and that each process runs within polynomial time bounds. This work may have practical applications to determine whether or not a process runs within certain limited computing resources. Indeed, it may be a tool to control the spawning mechanism, and so to prevent, for example, denial of service attacks.

Let us come back to Example 1 describing a max-reduce algorithm. The runtime is O(log 2 (n)). The reason of this apparent shortcoming is that we can not allow a break instruction inside a while-loop. In this case, a return instruction would "disrupt" the information flow and would interfere with tier 1 values. As a result, the runtime would not be anymore bounded. However, if the goal is to analyze program complexity, then we can devise a program transformation Θ, which, approximately, moves break instructions outside while loops, whenever it is possible. Such program transformation may be efficiently performed by a tree transducer. Moreover, there is no reason to preserve the program semantics because we are just interested in resource bounds. So, we may omit implementation details, which may increase drastically the expressivity of the considered programs. Therefore, we may think of this overall scenario: A system receives a process P to run. First, it computes an abstraction of P using a program transformation Θ. Second, it checks that the abstraction is well-typed. As a result, and even if the system does not know precisely an upper-bound on the complexity, it gets efficiently some confidence on the resource usage of P .

The program solving QBF gives another limitation because we are not allowed to make a loop bounded by the number of subprocesses, which is a tier 0 value. However, we know that this number is bounded by a tier 1 value. To solve this, Hofmann suggested to manage the garbage collector thanks to a type system. We may think to allow iterations on controlled unsafe values by a kind of declassification rule.

The above questions suggest the need to delve deeper into the question of determining the amount of information, which can be declassified while guarantying complexity. In regards to future research, the relationship between information, information flow control and complexity should be better understood.

  Expressions and configurations. Each operator of arity n is interpreted by a total function op : W n → W. The expression evaluation relation e → and the sequential command evaluation relation c → are described in Figure 1.

  E1, . . . , En), µ) e → op (d1, . . . , dn), if ∀i, (Ei, µ) e → di (Operator) (skip; P, µ)ρ c → (P, µ)ρ (Skip)

Fig. 1 .

 1 Fig. 1. Small step semantics of expressions and configurations

Fig. 2 .

 2 Fig. 2. Semantics of Environments

  1 ) : 1 ; i f ( i >0) then { // for each son i 0 := i -1 0 : 0 ; ( p i d 0 , op 0 ) := p i d t a b [ i ] : 0 ; r e s s o n -1 := w a i t ( p i d 0 ) -1 : -1 i f op 0 == ' ∃ ' then r es -1 := o r ( r e s , r e s s o n ) -1 : 0 ; e l s e r e s -1 := and ( r e s , r e s s o n ) -1 : 0 ; } } return r e s -1

  [START_REF] Amadio | Feasible reactivity for synchronous cooperative threads[END_REF]. By Lemma 1, a tier 1 expression just consists in neutral operators and tier 1 variables. So, tier 1 variables are always sub-words of tier 1 initial values. Thus, the size of a variable of tier 1 is always bounded by |µ| 1 . Second, take a tier 0 variable X , which is either updated inside a process by a composition of operators or updated by a pid return of a fork. By combining Proposition 2 and lemmas 3 and 4, we obtain a polynomial R which depends on operators and on the program such that the size of X is bounded by R(Q(|µ| 1 )) + |µ| 0 in each process computation. Third, take a tier -1 variable Y . Suppose that the variable Y is assigned to max operators and variables of any tier. Observe that the case when Y := wait(E ) is a particular case of an assignment if we see globally all processes together. Hence Y is bounded by R(Q(|µ| 1 ) + |µ| 0 + |µ| -1 .