Claire Laudy
email: claire.laudy@thalesgroup.com

Simon Fossier
email: simon.fossier@thalesgroup.com

Johann Dreo
email: johann.dreo@pasteur.fr

Tackling Threatening behavior through a Semantic Approach

Keywords: Trajectory Fusion, Optimization, Motion Planning, Semantization, Threat Detection, Situation Awareness

We introduce a new approach to characterize and detect threatening behaviors in surveillance systems, without relying on history or expertise. This approach consists in simulating the worst-case attack plans, fusing their semantic descriptions and using the produced patterns to raise alerts in operational conditions. We demonstrate our set of tools on a simple scenario involving geolocated sensors looking for moving vehicles targeting a protected objective. We find that the system is able to recover well-grounded graph patterns defining detection rules which make sense in the operational context. We believe that our approach achieves a relevant compromise between data-based and expertise-based systems, and allows for a good balance between efficiency and understandability.

I. INTRODUCTION

Surveillance systems are typically composed of a set of sensors that track targets on the zone, in the objective of raising alerts when a "threatening" behavior is detected. These systems are typically designed by an expert who knows the operational context and the definition of targeted behaviors. Modern approaches may also make use of data captured by an existing system in order to learn the targeted behaviors, and possibly improve the system design iteratively [START_REF] Verma | A review of supervised and unsupervised machine learning techniques for suspicious behavior[END_REF]. These approaches require to be able to actually identify a threatening behavior in a database of situations. Once a set of threatening behaviors is identified, it can be used to train a classifier, which will be able to detect if a given situation is threatening or not [START_REF] Joshi | Smart surveillance system for detection of suspicious behaviour using machine learning[END_REF]. However, most classification approaches would not be able to easily transfer their knowledge to an explainable form, such as a geometric definition of a behavior [START_REF] Verma | A review of supervised and unsupervised machine learning techniques for suspicious behavior[END_REF].

In this work, we propose an intermediate approach which substitutes the need for an explicit definition of a specific behavior with an implicit characterization based on the sole definition of the target's objectives. A simulator generates expected behaviors by optimizing the attainment of the threat's objective and these optimal simulations are interpreted as a base of probable behaviors to reach the objectives. This is close to goal-based analysis [START_REF] Tung | Goal-based trajectory analysis for unusual behaviour detection in intelligent surveillance[END_REF], but the simulator models the whole behavior, instead of letting an expert defining key points on the trajectories. These optimized situations are then discretized, semantic information is attached to them thanks to the use of a generic ontology, and common explicit patterns are finally extracted among the threatening behaviors, which constitutes an explicit basis for generating alerts.

We thus provide a new way to raise alerts on threatening behaviors, which may complement more classical rulebased [START_REF] Lee | Archcam: Real time expert system for suspicious behaviour detection in atm site[END_REF] or learning-based approaches [START_REF] Wiliem | A suspicious behaviour detection using a context space model for smart surveillance systems[END_REF]. This is particularly important for situations where no sufficient observations or expertise is available, which is a common real-life occurrence in surveillance systems [START_REF] Torres | Online learning of contexts for detecting suspicious behaviors in surveillance videos[END_REF].

We rely on the assumption that a threatening target, that aims at traversing the system with a given objective, will try to avoid detection while being efficient (typically, fast) in its traversal [START_REF] Dreo | Netted multi-function radars positioning and modes selection by non-holonomic fast marching computation of highest threatening trajectories by cma-es optimization[END_REF]. For instance, a vehicle will try to traverse a monitored area as fast as possible, in order to reach the exit point which allows for an escape [START_REF] Strode | Optimising multistatic sensor locations using path planning and game theory[END_REF].

The objective is to help surveillance operators in intercepting a target before it reaches a goal or hides. Technically, this translates into: how to automatically trigger relevant alerts, when there is no historical records of nefarious activity, and no expert to explicitly design the alert system? This forces to think in terms of states and optimal behaviors: how can we design a system that anticipates the behaviors of the antagonist, while focusing on the surveillance sensors that are available, and that raises an alert when the measurements match a behavior pattern? Moreover, how can we predict an intercept state and/or a goal state in which the target may be present in the future, to be able to stop it?

The advantage of our approach is that it tackles the problem by answering the following questions:

• What are the possible plans an attacker would follow if they wanted to attack the system? • What would be the common features between these possible plans? • How to leverage these commonalities to catch the attacker?

Prior art only considers learning approaches on raw data from the sensors, explicit rules, or discretization of features in a human behavior video [START_REF] Verma | A review of supervised and unsupervised machine learning techniques for suspicious behavior[END_REF]. To our knowledge, this work is the first to compensate for the lack of real labeled data by using fully optimized simulation, and semantic graph fusion to raise alerts.

II. COUPLING OPTIMIZATION AND FUSION TO PARAMETERIZE AN ALERTING SYSTEM

Our approach relies on the synergy of three elements:

• Simulation of threatening targets by a planning optimizer, which computes a set of possible plans of attacks on the system. A large set of simulations, involving different threat assumptions, provides a consequently large set of attack plans. • Semantization of those plans, i.e. their transformation into a concept-centric description, using a given ontology, which leads to a large set of semantic graphs describing the plans of attack. This graph set is then fused to obtain a description of the most common elements that characterize threats, i.e. the elements that the alerting system should try to identify -in other words, patterns of attack. • When the system is in use, these patterns of detection are correlated with the sensor measurements: the measurements first go through the same semantization process, then are correlated with the fused patterns. When this behavior matching method returns a high level of correlation, it is interpreted as a potential threat, which triggers the raising of an alert. In this work, we consider a geolocated system, which threat vehicles traversing a given zone. Sensors are placed to detect moving threats in their assigned detection area, are usually characterized by a detection range and sensitivity, but can also have highly anisotropic capabilities by design or due to the terrain (for instance, range difference in plains vs. forests). On the attacker side, the threat can move more or less easily, depending on its location (e.g. move fast on a road with a car, move slowly while walking in the forest). The target behavior itself can be summarized by a trajectory, from a boundary of the system's domain to another boundary. During detection, there are remaining unknowns regarding the attacker's capabilities (e.g. the type of vehicle they will use), and it can be necessary to enumerate and work with several options (e.g. the attacker would use either a car or a truck).

The overall process can be summarized as follows:

1) Threats are simulated by a motion planning optimizer that computes attack trajectories on the system. A large set of simulations, involving different threat assumptions, provides a consequently large set of plans of attack. This is our base dataset for describing the possible threats. 2) These plans are then semantized with the support of an ontology (description of the different elements that appear in the domain), which leads to a large set of semantic graphs. This is a simpler representation of the threats, which has the advantage of being discrete and understandable in terms of concepts, zones, speeds, etc.

3) The set of graphs is then fused, so as to obtain the common and/or most threatening parts in the semantic graphs. Each fused graph forms a pattern of attack. This is our reference information to raise alerts.

4) When the system is in use, the sensors provide a characterisation of the threat behavior (e.g. a trajectory, a type of vehicle. . . ). This behavior is passed through the same semantization process, leading to a set of realtime semantized detections, now expressed in the same formalism as the patterns of attack. 5) The detections are finally matched with the patterns of attack, in order to raise progressively increasing alerts as the measured semantic graph matches an increasing sub-part of a pattern of attack.

At first glance, it could be thought that most of these steps have implementations in the state of the art. However, when taking into account the input-output formalism of the successive steps, as well as the required association of these steps with the constraints associated to the problem, this creates a new implementation problem in itself and specific challenges. More specifically:

• 1) + 2) : The semantization of plans of attacks into conceptual graphs is highly unusual, since plans are usually processed at the event level or at the kinematics level.

• 3) + 4) + 5): Matching real-life detections with semantic graphs without expert transformation rules is a challenge in itself, made possible by the semantization module that couples the zone/subnetwork description with attack paths and transforms them into a semantized graph, allowing for graph matching algorithms to be applied on this coherent dataset.

A. Semantic Trajectory Modelling

One key aspect of our approach is the semantic modelling of the trajectories. We choose to model them using conceptual graphs. Conceptual graphs [START_REF] Chein | A Graph-Based Approach to Knowledge Representation: Computational Foundations of Conceptual Graphs[END_REF] are a family of formalisms for knowledge representation, made of ontological and factual knowledge. A CG is a bipartite graph representing factual knowledge referring to a vocabulary that represents the ontological knowledge.

A vocabulary is a 5-tuple V = (T C , T R , σ, I, τ ). T C and T R , that respectively correspond to concept and relation types, are two partially ordered disjoint finite sets, where ordering corresponds to generalisation. T C contains a greatest element ⊤. Each relation type has an associated arity. A signature specifies the arity and the maximal concept type of each argument of a given relation type. σ maps to each relation type r its signature σ(r), i.e. a tuple (t 1 , ...t n ) where each t i ∈ T C , thus specifying its arity, n, and the most general concept type t i for each of its argument. I is a set of individual markers used to instantiate concept nodes. τ is a mapping from I to T C that defines the type instantiated by each individual marker.

A CG is a bipartite labeled multigraph represented as a 4tuple G = (C, R, E, label) defined over such a vocabulary V. C and R correspond to concept and relation nodes, E denotes the set of the edges connecting elements of C and R. label is a labelling function from C to T C × I and from R to T R . For any r ∈ R, label(r) = t r ∈ T R is the type of r and for

any c ∈ C, label(c) = (t c , i c ) ∈ T C × I where t c is the type of c
The vocabulary we developed to model semantic trajectories is made of an ontology and a set of signatures associated with the relations types defined in the ontology. The ontology is depicted on Figure 1 We define the following relation signature in order to express the trajectories.

• in(Presence, Area, Duration),

• with speed(Presence, Speed ),

• precedes(Presence, Presence, Delay). An elementary unit of a trajectory (EUT) of a vehicle is defined by its presence in a given area for a given duration and with a given speed. A trajectory is defined as the succession of such EUTs, this succession being defined using the precedes relation defined above. Figure 2 depicts an example with a trajectory composed of a succession of Presence in the radar2 zone and in the uav1 zone.

B. Threat Planning Optimization

In this work, the objective of the threat model is to provide a set of paths which captures the worst case scenario, where the threat behaves optimally. This set Γ * ⊂ Γ encloses paths going from a "source" set of EUTs Υ ∈ Ω (i.e. where the threat comes from), to a "targeted" set of EUTs Θ ∈ ∂Ω (i.e. what the threat wants to reach by traversing the domain).

In this setting, the navigation of threats are a priori completely free, in the sense that it only has to satisfy a transport equation and thus satisfy locally the conservation of energy. More realistically, though, paths may be subject to momentumrelated or environmental constraints, such as obstacles, radius of curvature (depending on the speed), bounded accelerations, bounded speed, etc. The model of navigation should thus be able to capture the characteristics of different vehicles. The following section introduces such models, and we refer the reader to [START_REF] Mirebeau | Numerical schemes for anisotropic PDEs on cartesian grid domains[END_REF] for more details.

1) Eikonal model: Solving such a constrained navigation problem is equivalent to solving the eikonal equation:

|∇u(p)| = 1 c(p) ∀p ∈ Ω, u(∂Ω) = 0 (1)
for a given speed function c : Ω →]0, ∞[. The goal thus becomes to recover the value function u : Ω → [0, ∞]:

u(p) := inf length F (γ) γ : [0, 1] → Ω, γ(0) ∈ Υ, γ(1) ∈ Θ
In the general sense, the path length should be measured as the sum of the length of (arbitrarily small) legs (i.e. sequence of two EUTs), with respect to a given metric

F : Ω × E d → [0, ∞]: length F (γ) := 1 0 F γ(t) (γ(t)) dt
F may be a conformal metric (locally proportional to the Euclidean one) of the form F(p) = ∥p∥/c(p) (similar to equation 1).

The (generalized) eikonal equation then reads:

F * p (du(p)) = 1, where F * p := sup{⟨ p, ⃗ p⟩ | F p (⃗ p) ≤ 1} (2)
which allows to capture several anisotropic navigation constraints (e.g. radius of curvature, drift, detection probability, etc.) within F, at each area of the domain.

It is worth noting that solving the eikonal equation 2 can be done efficiently in O(n log n) by causal eikonal solvers, while also computing the vector field of optimal control v : R → S n-1 at no additional cost, as:

⃗ v(p) = -∇u(p) |∇u(p)| (3)
Integrating the vector field (3) from some sources ψ ∈ Υ effectively recovers the optimal paths that reach the nearest -in the sense of the metric Ftargeted locations θ ∈ Θ. Note that the number of recovered paths is the same as the number of sources, effectively limiting the space of threat's behavior.

2) Sensor Network Traversal: Since we consider the problem of a threat traversing a domain on which a network of sensors is located, we define a "track" as a path linking a source point to the nearest entry in an area that the system is watching over. Sensors are modelled as areas where the system has a high probability of detecting (some kind of) vehicles. The cost metric F thus models the probability of detecting the threat for each point of the domain.

If F(p) > 0 ∀p ∈ Ω (i.e. if there is a non-null probability of detecting a threat out of any sensor field of view), then the optimal paths resulting from integrating (3) are unique. Note that, in that case, if the threat does not traverse a sensor's field of view, then the problem falls back to a shortest path problem, hence producing realistic paths [START_REF] Renau | Landscape-Aware Selection of Metaheuristics for the Optimization of Radar Networks[END_REF].

As an extension of this model, it is possible to set up a two players game model where a player optimizes the sensor network configuration against the player who optimizes the threat paths, without loss of generality (see [START_REF] Mirebeau | Automatic differentiation of nonholonomic fast marching for computing most threatening trajectories under sensors surveillance[END_REF] for an example).

In this work, we either use the HFM solver [START_REF] Mirebeau | Hamiltonian Fast Marching: A Numerical Solver for Anisotropic and Non-Holonomic Eikonal PDEs[END_REF] to optimize threat tracks, or produce hand-made tracks with realistic shapes honoring equation 2.

C. Plans Semantization

The semantization consists in transforming a given threat plan into a graph representation following the ontology and relational structure defined in section II-A.

First, we use layers covering the navigation domain. Each layer is linked to a specific semantic meaning, such as the operational boundaries, the navigation speeds, or the probabilities of detection. Each layer is a partition of the domain, i.e. a set of non-overlapping layer subzones. Each layer subzone in those partitions is thus holding an atom of data with a semantic meaning ("detection = 50%", "boat speed = 12 kts", or even "no data").

The union of all layers produces a new partitioning of the domain in a set of non-overlapping areas of interest, each of which holds a list of data atoms, with one atom for each layer. An event is defined as an entry of a threat into an area of interest, or an exit from this area. The semantization then transforms a path traversing the navigation domain into a sequence of events.

In summary, the semantization process consists in: 1) computing the union of all layers, 2) discretizing the input threat track in a list of entry/exit events in/out of the traversed areas, 3) transforming this discrete sequence of events in a conceptual graph. This results in tracks defined in the conceptual graph formalism, e.g., as "Presence of a SpeedBoat in MonitoredArea zone X1, with average speed 25, during a time period of 9, followed by a presence in zone Y2, with [etc.]".

The computational geometry functions are implemented with the CGAL library [START_REF] Fabri | Cgal: The computational geometry algorithms library[END_REF], using the kernel with exact predicates & exact constructions, and the 2D arrangements package [START_REF] Wein | Advanced programming techniques applied to CGAL's arrangement package[END_REF].

D. Semantic Trajectory Fusion

The fusion process developed in the semantic information fusion module is a hybrid between the Apriori algorithm [START_REF] Agrawal | Fast algorithms for mining association rules in large databases[END_REF] and Taxogram [START_REF] Cakmak | Taxonomy-superimposed graph mining[END_REF].

Agrawal and Srikant [START_REF] Agrawal | Fast algorithms for mining association rules in large databases[END_REF] proposed the Apriori algorithm, for frequent item set mining and association rule learning from transactional databases. It operates on databases containing transactions (i.e. collections of items). Each transaction is seen as a set of items (an "itemset").

The algorithm discovers frequent item sets in the database in a "bottom up" approach. It extends already processed frequent item sets with new items. Thus, the algorithm first processes the frequent item sets of length 1 and then extends them one item at a time. The frequency condition is tested by processing the support of an item set in the database and comparing it to a threshold. The support of an item set is the number of times this item set appears in the database. Given a threshold ϵ, the Apriori algorithm identifies the item sets which are subsets of at least ϵ transactions in the database.

Taxogram is a taxonomy-superimposed graph-mining algorithm that can efficiently discover frequent graph structures in a database of taxonomy-superimposed graphs. Taxonomysuperimposed graph describes graphs which nodes take value in a taxonomy. It is very close to our conceptual graphs, the nodes of which take types in the taxonomy part of an ontology. However, in conceptual graphs, concept nodes are not only composed of types, but also value, that are not defined in the taxonomy part of the ontology.

Taxogram has two main properties. First, it performs a subgraph isomorphism test once per class of patterns, which are structurally isomorphic, but have different labels. Then, it reconciles standard graph mining methods with taxonomybased graph mining and takes advantage of well-studied methods in the literature.

The Taxogram algorithm is composed of three stages: 1) relabelling nodes in the input database, 2) mining pattern classes/families and constructing associated occurrence indices, and 3) computing patterns and eliminating useless (i.e., overgeneralized) patterns by post-processing occurrence indices. In the Semantic Information fusion module, as in Taxogram, the graph data base is first generalised. Each concept of each graph of the database is generalised. That is to say that the type of concept is replaced by its most general super-type in the ontology that is also a subtype of Entity.

Once the graphs of the database are generalised, they are transformed into itemsets, in order to be processed by Apriori. Each relation of the graph, with its linked concept nodes is transformed into an item. The set of relations composing each track graph is thus transformed as an itemset. The Apriori algorithms processes a set of itemsets, searching for frequent patterns into these itemsets.

Once frequent generalised patterns are provided by Apriori, we use the approach described in [START_REF] Cakmak | Taxonomy-superimposed graph mining[END_REF] in order to process the specific patterns.

E. Attacks Detection

The challenge of this final step is twofold: align the real trajectories with the frequent patterns extracted by Semantic Fusion, and define the explicit rules for triggering alerts.

Actual trajectories are provided by the different sensors on the monitored zone. Here, our base material is system tracks, which stem from the kinematic fusion of sets of sensor tracks associated with a single object detected by multiple sensors. For this paper, we make the assumption that there is a single system track per actual moving object, although our tests showed that, more often than not, an important preprocessing work is required, e.g. to manage track drops due to blind zones or objects closer than sensor resolution.

To align the system tracks with the semantic frequent patterns, we first use the same semantization tool as described in II-C. This ensures that the semantized version of the system trajectory follows the same ontology as the frequent patterns.

Then, we need to match zone transition sequences, i.e. the semantized track, with the frequent patterns which characterize the threat. Though seemingly straightforward, this matching is affected by:

• variability: the threat patterns provide hints about, e.g., expected speeds during a zone crossing, or time necessary to cross a zone, but the actual detections will never perfectly these average/median/fused times. It is therefore not possible to use purely Boolean predicatebased matching systems, and we need to rely on probabilistic or threshold-parameterized rule systems. • observability: threat models are based on motion planning in a fully modelled zone, but in actual contexts the threats are not guaranteed to be observable with 100% uptime. If a given zone is not or poorly covered by the detection tools available to the system, the track will either lack a portion of the plots that in this zone (best case) or even be discarded, leading to a new track created when newly re-detected in the next zone, with a new identifier. This is linked to the preprocessing mentioned earlier.

Typically, a mitigation system has to be put in place, so as to both manage the inobservable zones and perform an hypothesis-based matching between partial tracks so as to recreate the full behavior of the threats. • quantization/sampling side effects: the fact that the observations and the threats are described in a discrete paradigm results in classical time-space alignment issues, and some measure of interpolation is necessary. After alignment, we define a set of metrics from the pattern/track correlation, which include: track vs. pattern speed alignment; zone traversal time alignment; presence/absence of missing segments in tracks vs. patterns.

Moreover, a dynamic alert system requires timeliness, i.e. the capability to raise alerts at the right time, with as much early notice as possible. By design, the threat patterns span the whole threat behavior, from early detection to threat realization. Therefore, we cannot wait until the whole threat pattern is matched by a trajectory to raise the alarm. This is managed by defining a level of completion of the patterns, i.e. a current position in the threat pattern (close or far to the objective).

The track is also complemented with contextual information, issued from the system identification capabilities. This information is either (1) controlled/measured -based on sensor measurements, e.g. video-extracted; (2) declarative -retrieved directly or indirectly from reports from the objects, e.g. AIS;

(3) curated -aggregated in trustworthy databases with some human verification involved, e.g. ship registration databases.

Finally, all these metrics are merged into a rule system tuned with the stakeholders, to trigger alerts. These alerts are raised or dropped dynamically, and complemented with high-level indicators, such as a confidence level, an estimated time to completion, or hints on targets or geographical elements to be highlighted, based on the part of the frequent patterns which is still to happen.

III. EXAMPLE

We applied the approach on several scenarios, with contexts ranging from a couple of departure and target points, to much bigger ones. We describe in the following section one of our middle size scenarios and present the results we obtained in terms of detection rules.

A. Scenario

The scenario depicted on Figure 3 The area is too large to be fully covered by detection systems. Two fixed-position radars are located in the outwards coast, depicted in light blue circular sectors and referred as F1 and F2 in the following. In addition, depicted in darker blue rectangles, two uncrewed aerial vehicles (UAV) provide dynamic detection systems, referred to as D1 and D2, and patrol within the gulf in predetermined flight patterns. Notably, it can be assumed that potential attackers are aware of the radars range and detection efficiency, since they are permanently installed, but not of the UAVs.

B. Threats simulation and tracks semantization

In order to keep the example visually interpretable, we generated only a few threatening tracks for this example. These tracks are depicted on figure 3 as the green lines between the possible departure and target points.

The tracks are then semantized so that they are transformed into semantic graphs before the fusion step. Figure 2 depicts the resulting semantic graph for the track depicted in plain line. This track first crosses the F1 detection area, then avoids the D1 area by bypassing it on the right and finally crosses the D3 detection area.

C. Track fusion

The fusion module aims at finding recurrent patterns across the different tracks, in order to generate detection rules from them. We want to detect with the same rule all tracks that have close trajectories; therefore, the patterns have to be underspecified, with regards to the input semantic tracks. However, as depicted on figure 2 each graph track has specific (and usually different) values for the duration of the presence of the vehicle in an area, speed of the vehicle and delay between the crossing of two successive areas. Therefore, the fusion algorithm needs to integrate a set of parametered fusion heuristics, which fuzzify the values by associating them to ranges of speed, duration and delay.

Second, the fusion algorithm needs to be parametered with the minimal support desired for each pattern graph (and thus detection rule), over the initial data set of input tracks. Here, a graph pattern is said to be supported by a set of input graphs if it represents these input graphs, i.e. the support of a graph pattern is the proportion of graphs in the input data set that are more specific than the graph pattern.

Obviously, we don't want to have too many rules, since it would reduce the interpretability of the detection rule set by operators. On the other hand, if rules are too generic and support too many threat configurations, the information they carry may be of little use to the operator: a rule being triggered would not give enough specific information on the behavior of the vehicle for an appropriate action to be taken.

For this example, if we target a minimum support of 50% for the graph pattern, we obtain only one frequent pattern, representing tracks that cross the D2 and then the D3 areas. This pattern is depicted on figure 4. None of the northern tracks are represented, and no difference is made between tracks coming from the east (not crossing F2) and the ones coming from the south (crossing F2).

When we lower the minimum support for graph patterns to 25%, two additional patterns are found (and depicted on Each elementary unit of trajectory (EUT, linked by precedes) involves multiple values. Atomically, the comparison is straightforward when the values associated to the extracted concepts are fuzzified (here, Duration or Delay intervals) and imply a notion of membership of the semantized value to the fuzzified value. When the fused value is sharp (here, Speed), the comparison will require a heuristic membership criterion, typically a fuzzy or sharp threshold in the difference between values.

Then, at a given point in time, a potential threat will have matched a certain number of sequential EUTs. We check whether the threat pattern is matched from the beginning, if there are additional or missing EUTs, and how many EUTs in the pattern have been matched at that instant. From these criteria, we build, in link with the stakeholders, an aggregated threat level and a scale of operational alert levels.

Finally, during operation, threats will be continuously matched against patterns, their threat levels evaluated, and alerts raised with the appropriate levels, with the estimated time to completion, and with the estimated end zone (linkable to the targeted asset).

IV. CONCLUSION AND PERSPECTIVES

In this paper we presented an approach for building a surveillance system based on simulation of attacks rather than on the expertise of an operator defining specific threatening behaviors within specific contexts, or on a labeled dataset. The process we propose follows 5 steps:

1) the simulation of threatening behaviors (tracks generation), 2) the semantization of these tracks, 3) the fusion of the semantized tracks during the system preparation phase, 4) the semantization of tracks provided by sensors during operation, 5) the detection of threatening vehicles which behavior matches the behavior patterns found on step 3. While we present here the use of the process with the aim of automatically generating behavior rules that are understandable by a human operator, a perspective of our work is to use it in order to configure the sensors as well. To do so, we can take advantage of the fact that threatening tracks are simulated. The idea is to add a system that will automatically optimize sensors positioning, in order to maximise the probability of detection of a vehicle (see [START_REF] Renau | Landscape-Aware Selection of Metaheuristics for the Optimization of Radar Networks[END_REF], [START_REF] Mirebeau | Automatic differentiation of nonholonomic fast marching for computing most threatening trajectories under sensors surveillance[END_REF] for examples, albeit not involving semantic fusion). The process described here then remains unchanged: semantic behavior rules, associated with the best sensor positioning will be generated, and the final probability of raising an alert will be used as an objective function of a high-level optimization problem.

Furthermore, as the whole process would be automated, one may be able to find the best operational compromise between the probability of detection and the understandability (and thus usability) of detection rules.

More generally, the work described in this paper may also be applied on any topology that features a generic notion of "plan". We intend to apply it within the cybersecurity domain, i.e. the study and monitoring of actions in information systems networks. In such a use-case, the semantization of a plan resulting from an automated planning problem optimization may even bring more information to the following layers.

Fig. 1 .

 1 Fig. 1. Ontology for semantic trajectories modelling

Fig. 2 .

 2 Fig. 2. Example of a semantized trajectory

  takes place around the island of Salamine in the Saronic Gulf. The set of targets for the attackers, depicted in red on the figure, is situated in the inner part of the Eleusis Bay, along the coast. Possible departure points, depicted in yellow, are situated in the Saronic Gulf open sea, on the other side of the island.

Fig. 3 .

 3 Fig. 3. Salamine Island Attack scenario

Fig. 4 .

 4 Fig. 4. Graph pattern with support of 50%

Fig. 5 .

 5 Fig. 5. Graph pattern with support of 25%


Anne Preller
email: preller@lirmm.fr

Polynomial Pregroup Grammars parse Context Sensitive Languages

Keywords: type logical grammar, pregroup grammar, proof graph, complement control, cross-serial dependency, mildly context sensitive language, Dutch subordinate clause, Swiss-

Pregroup grammars with a possibly infinite number of lexical entries are polynomial if the length of type assignments for sentences is a polynomial in the number of words. Polynomial pregroup grammars are shown to generate the standard mildly context sensitive formal languages as well as some context sensitive natural language fragments of Dutch, Swiss-German or Old Georgian. A polynomial recognition and parsing algorithm handles the various grammars uniformly. It also computes a planar graph for the semantic cross-serial dependencies in the case of natural languages.

Introduction

The Pregroup Calculus was introduced in (Lambek 199) [START_REF] Lambek | Type Grammar revisited[END_REF] as a simplification of the earlier Syntactic Calculus in [START_REF] Lambek | The mathematics of sentence structure[END_REF] [START_REF] Lambek | The mathematics of sentence structure[END_REF]. According to [START_REF] Buszkowski | Lambek Grammars based on pregroups[END_REF] [START_REF] Buszkowski | Lambek Grammars based on pregroups[END_REF], a pregroup grammar consists of a finite set of basic types and a dictionary (or lexicon) containing a finite number of words, each listed with a finite number of types from the Pregroup Calculus. These finite grammars are proved in [ibidem] to be weakly equivalent to context free grammars.

Both [START_REF] Nissim | Commutation Augmented Pregroup Grammars and Mildly Context Sensitive Languages[END_REF]) [START_REF] Nissim | Commutation Augmented Pregroup Grammars and Mildly Context Sensitive Languages[END_REF] and (Stabler 2008) [START_REF] Edward | Tupled Pregroup Grammars[END_REF] extend pregroup grammars to mildly context-sensitive formal languages by adding new rules and/or constraints to the Pregroup Calculus. (Lambek 2008-1) [START_REF] Lambek | From word to sentence[END_REF] discusses the Dutch subordinate clause and remarks that a law of commutativity would solve the problem, but dismisses it as 'not allowed'.

The approach taken here is based on the belief that the computational efficiency and the semantic expressivity of pregroup grammars is based on the planar graphs representing derivations of the Pregroup Calculus. To keep them intact, the definition of a lexicon is relaxed allowing an infinite number of types per word. The only restriction is that some polynomial in l bounds the length of the concatenated type T 1 . . . T l associated to w 1 . . . w l for every type assignment w i : T i , 1 ≤ i ≤ l with a reduction to the sentence type. In the case of context free languages or the standard formal mildly context sensitive languages it is of degree 1, for Dutch or Swiss-German subordinate clauses it is of degree 2. The pregroup grammar generating (Michaelis, Kracht) [START_REF] Jens | Semilinearity as a syntactic invariant[END_REF]'s version of Old Georgian noun phrases is polynomial of degree 2. The description of the same noun phrases in (Bhatt and Joshi) [START_REF] Bhatt Rajesh | Semilinearity is a syntactic invariant: A reply to Michaelis and Kracht[END_REF] can be handled by a polynomial pregroup grammar of degree 1.

The natural language dictionaries presented here have entries that are triples formed by a word, a type and a meaning expression. The meaning of a sentence is computed from the chosen meanings of the words by substitution. The dictionaries are compositional in the sense of (Kracht 2007) [START_REF] Marcus | Compositionality:"The Very Idea[END_REF]. Moreover, a linear parsing and tagging algorithm generates the (cross-serial) semantic dependencies.

Section 2 recalls the Pregroup Calculus and the geometrical structure of reductions, followed by an example how to compute the meaning of a sentence involving complement control in English. Section 3 introduces polynomial pregroup grammars for formal and natural context sensitive languages. Finally, Section 4 presents the parsing algorithm based on the geometrical structure of reductions, illustrated by an example of Dutch subordinate clauses.

2 Pregroup Calculus, Proof Graphs and Meaning

Pregroup Calculus and Reductions

The set of pregroup types P (B) generated by a partially ordered set B = B, ≤ is the free monoid generated by the set of simple types S(B) = a (z) : a ∈ B, z ∈ Z .

The notation a (z) designates the ordered pair formed by the element a of B and the integer z . Elements T ∈ P (B) are called types. In an equality T = t 1 . . . t n , it is always understood that the lower case t i 's are simple types. In the case where n = 0, the string t 1 . . . t n is empty, denoted 1 . It is the unit for the binary operation of concatenation in the free monoid. A basic type is a simple type of the form a (0) . With a convenient lack of precision, a and a (0) are identified and the elements of B are referred to as basic types. The left adjoint and the right adjoint of a simple type t = a (z) are defined as t = (a (z) ) = (a (z-1) ) left adjoint t r = (a (z) ) r = (a (z+1) ) right adjoint .

The binary derivability relation on types, denoted →, is the smallest transitive relation containing 1 → 1 satisfying (Induced step) Sa (z) T → Sb (z) T (Generalized contraction) Sa (z) b (z+1) T → ST (Generalized expansion)

ST → Sa (z+1) b (z) T [START_REF] Bhatt Rajesh | Semilinearity is a syntactic invariant: A reply to Michaelis and Kracht[END_REF] where either z is even and a ≤ b or z is odd and b ≤ a . Note that the derivability relation → coincides with the partial order ≤ on the set of basic types. It is a partial preorder on types, but not an order, because it is not antisymmetric. Indeed, a → a(a r a) by generalized expansion and (aa r )a → a by generalized contraction, see [START_REF] Buszkowski | Lambek Grammars based on pregroups[END_REF] [START_REF] Buszkowski | Cut elimination for the Lambek calculus of adjoints[END_REF].

Definition 1 (Dictionaries). Let Σ be a non-empty set. A pregroup dictionary for Σ based on B is a map D defined on Σ with values in the set of subsets of P(B). A type assignment of w 1 . . . w n is a sequence of types T 1 , . . . , T n for which

T i ∈ D(w i ), 1 ≤ i ≤ n . A lexical entry w : T of D is an ordered pair w ∈ Σ and T ∈ D(w) . A dictionary is discrete if it is based on a discrete set, i.e.

a set ordered by equality.

A pregroup grammar G = D, s for Σ based on B consists of a pregroup dictionary D based on B and a distinguished basic type s ∈ B. The language of G is the following subset of

Σ * L G = {w 1 . . . w n ∈ Σ * : T 1 . . . T n → s for some T i ∈ D(w i ), 1 ≤ i ≤ n} .
By definition, T → T if and only if there is a sequence of types T 1 , . . . , T n such that T 1 = T , T n = T and T i → T i+1 is 1 → 1 or an instance of the pairs in (1) for 1 ≤ i < n. The derivations of the Pregroup Calculus can be characterized geometrically by proof graphs that have underlinks, overlinks and vertical links, see (Preller, Lambek) [START_REF] Preller | Free compact 2-183-226, 1987 categories[END_REF]. Underlinks are edges between simple types in the upper line (the antecedent) and stand for generalized contractions. Overlinks are edges between simple types in the lower line (the conclusion) and represent generalized expansions. Vertical links are edges between a simple type in the upper line and a simple type in the lower line. They code induced steps.

4 4 4 4 4 4 4 4 4 Ö Ö Ö Ö Ö Ö Ö Ö Ö Ö Ö a a a a a a a r as c r c a a b r b s c c (2)
To check grammaticality of a string of words, only derivations without instances of Generalized Expansion are to be considered, see [START_REF] Lambek | Type Grammar revisited[END_REF]) [START_REF] Lambek | Type Grammar revisited[END_REF]. The corresponding proof graphs are called reductions. If the set of basic types is discretely ordered the lower line and the vertical links can be omitted, as both are determined by the unlinked simple types in the upper line. Moreover, for a fixed type T , a reduction is determined by the position numbers of the links. This representation of a reduction as a set of unordered pairs of position numbers assures an easy formulation of the parsing algorithm in Section 4. s a a a a a r a s 1 2 3 4 5 6 7

{1, 6} {2, 5} {3, 4} s
a a a aa r a s 1 2 3 4 5 6 7

{1, 2} {3, 6} {4, 5} (3)
Note that there may be more than one reduction between two given types. The next subsection gives an example how a reduction to the sentence type assembles the meaning of the words into a meaning of the sentence.

Definition 2 (Reduction). Let 1 ≤ i 1 < • • • < i k ≤ n, T = t 1 . . . t n and T = t i1 . . . t i k be given. A reduction R from T to T , in symbols R : T ⇒ T , is a non-directed graph R = {1, . . . , n} , R such that 1) for every i ∈ {1, . . . , n} -{i 1 , . . . , i k } there is exactly one j ∈ {1, . . . , n} such that {i, j} ∈ R 2) if {i, j} ∈ R then i = j, i ∈ {i 1 , . . . , i k } , j ∈ {i 1 , . . . , i k } 3) if {i, j} ∈ R and i < l < j then {l, m} ∈ R for some m with i < m < j 4) t i t j → 1 for i < j and {i, j} ∈ R
The vertices in {1, . . . , n} are called positions and the edges in R underlinks.

Follow a few properties that intervene repeatedly in the proofs of Section 3.

Definition 3 (Simple type occurrence

). An arbitrary type T is said to be in D if w : T is a lexical entry for some word w . A simple type t occurs in T = t 1 . . . t n if t = t i for some i ≤ n. It occurs in D, if it occurs in the type of some lexical entry of D.

For example, a and s occur in sa , but not the basic type a .

Definition 4 (Modest type).

A type is modest, if all simple types occurring in it are basic, or right or left adjoints of basic types, but no basic type occurs with both its right and left adjoint. A dictionary is modest if it is based on a discrete set and every type obtained by concatenating types in the dictionary is modest.

A type

T = t 1 . . . t n is irreducible if t i t i+1 → 1 for 1 ≤ i < n . A type T is an irreducible form of T if T is irreducible and T → T .
For example, if a and b are basic then aa b r b is modest and irreducible. Every simple type is irreducible. The type constituting the top line of (3) is not modest.

The proofs of lemmas 2 -6 below are straight forward. Lemma 1 is a special case of Lemma 4.5 in (Preller 2007-2) [START_REF] Preller | Linear Processing with Pregroup Grammars[END_REF].

Lemma 1 (Uniqueness). Every modest type has a unique irreducible form and a unique reduction to its irreducible form.

The property does not hold in general. Indeed, ba aa r a has the two irreducible forms b and ba r a, whereas (3) gives a type with two distinct reductions to the same irreducible form.

Lemma 2. Let T be the irreducible form of a modest type T = t 1 . . . t m and suppose that t i . . . t j → 1 for some

1 ≤ i < j ≤ m. Then t 1 . . . t i-1 t j+1 . . . t m → T .
Again, the property above does not hold in general. For example, ba aa r a → b, a a → 1, but ba r a → b. However, the next lemma, a sort of converse of Lemma 2, holds for arbitrary types.

Lemma 3. Let t 1 . . . t m → T , s 1 . . . s n → 1. Then t 1 . . . t i s 1 . . . s n t i+1 . . . t m → T .
The next two lemmas state sufficient conditions for a simple type to remain present in every irreducible form of the original type. We say that t i t j is a block of T = t 1 . . . t m if i < j and t i is immediately followed by t j in every irreducible form of T . Lemma 4. Let t 1 . . . t m = T be modest and i < j positions satisfying 1) t i t j → 1 and t i+1 . . . t j-1 → 1 2) for all k < i, t k is not a left adjoint of t i 3) for all l > j, t l is not a right adjoint of t j .

Then t i t j is a block of T . In particular, T does not reduce to a single simple type nor the empty type.

< k ≤ n -i. Similarly, t 1 . . . t i-1 → 1 . In addition, t i-k . . . t i-1 → 1 implies t 1 . . . t i-k-1 → 1, for all 1 < k ≤ i -1.

Semantic Pregroup Grammars

In a semantic pregroup grammar, see (Preller 2007-1) [START_REF] Preller | Toward Discourse Representation Via Pregroup Grammars[END_REF], each lexical entry w : T is enriched by a (string of) logical expression(s) E, yielding a triple w : T :: E, in analogy with the triples word : Type :: Term of CCG's by (Steedman 1996) [START_REF] Mark | Surface Structure and Interpretation[END_REF]. The interpretation of a sentence is a variable-free expression, computed from the chosen interpretation of the words. The result of the computation depends on the chosen reduction to the sentence type. Semantic pregroup grammars are compositional in the sense of (Kracht 2007) [START_REF] Marcus | Compositionality:"The Very Idea[END_REF]. This is best explained by replacing the (string of) logical expression(s) associated to an entry by the corresponding 2-cell of compact 2 -categories, a proof that is beyond the scope of this paper. Consider instead the following example sentences Eva promised Jan to come (Subject Control) Eva asked Jan to come

(Object Control) . ( 4
)
The implicit agent of the infinitive is either the subject of promised or the object of asked. In the first sentence it is Eva who is supposed to come, in the second it is Jan. Consider the following semantical dictionary Eva : NP :: eva promised : NP r sδ ī NP :: promise(x 1 , x 2 , x 3 ) id(x 1 ) asked : NP r sδ ī NP :: ask(x 1 , x 2 , x 3 ) id(x 3 ) Jan : NP :: jan to : īi :: to(y) come : iδ r :: come(z)

The basic types NP , i and ī stand for noun phrase, infinitive and infinitival phrase. Finally, δ is a basic type that plays the role of a marker similar to an index in HPS Grammars of (Pollard, Sag) [START_REF] Carl | Head-driven phrase structure grammar[END_REF]. Models interpret all logical expressions as functions, including 0-ary functions like eva and jan . Some functions take their values in a 'set of truth values Ω' like promise, ask, come. Classical models interpret Ω as the two-element Boolean algebra and distributed models as a subset of real numbers.

Functional symbols correspond to basic types in the order in which they occur. Variables correspond to occurrences of non-basic types, indexed in the order of the occurrences of the types. For example,

NP r s δ ī NP x 1 ask id x 2 x 3 .
The variables on which a logical expression depends render the intuitive meaning of semantical dependency. The translations of promised : NP r sδ ī NP and asked : NP r sδ ī NP differ by the variable on which the translation id of the basic type δ depends, namely on x 1 in the case of promise and on x 3 in the case of ask .

The links of a reduction to the sentence type indicate how the variables are to be replaced. For computing the logical expression corresponding to Eva promised Jan to come

(NP ) (NP r s δ ī NP ) (NP )( ī i )(i δ r )
do the following -write the corresponding logical symbols above the simple types

1 eva x 1 promise id x 2 x 3 jan to y come z NP (NP r s δ ī NP ) NP ( ī i ) (i δ r )
-omit the types and put the links under the corresponding logical symbols eva x 1 promise id x 2 x 3 jan to y come z -define the substitutions according to the links

x 1 → eva x 2 → to(y) x 3 → jan y → come(z) z → id(x 1 ) (5)
Substituting in promise(x 1 , x 2 , x 3 ), one obtains the logical expression that translates the sentence promise(eva, to(come(id(eva))), jan)

The meaning of id is determined by the logic, i.e. it is interpreted in every model as the identity function. This is guaranteed by the axiom

id(x) = x
Finally, the translation is equivalent to the variable-free expression promise(eva, to(come(eva)), jan)

Note that eva is the agent of come.

The procedure applied to the second sentence Eva asked Jan to come

(NP ) (NP r s δ ī NP ) (NP )( ī i )(i δ r ) ,
yields the same substitutions as in (5) except for the last which is replaced by

z → id(x 3 ) .
The resulting interpretation of the sentence is now equivalent to ask(eva, to(come(jan)), jan)

Now, jan is the agent of come in opposition to [START_REF] Hans | From Discourse to Logic, Introduction to Modeltheoretic Semantics of Natural Language[END_REF]. The semantical dependency, expressed above as embedding of subexpressions corresponds to the embedding of boxes in the DR-structures in (Kamp, Reyle 1993) [?].

Polynomial Pregroup Grammars

Polynomial pregroup grammars generalize the notion of finite pregroup grammars in [START_REF] Buszkowski | Lambek Grammars based on pregroups[END_REF]) [START_REF] Bhatt Rajesh | Semilinearity is a syntactic invariant: A reply to Michaelis and Kracht[END_REF] Definition 5. A pregroup grammar is polynomial of degree n if the length of T 1 . . . T l is O(l n ) for every every type assignment w 1 : T 1 , . . . , w l : T l for which T 1 . . . T l → s .

If the length of types occurring in the dictionary does not exceed a constant α, then the corresponding grammar is linear polynomial, i.e. of degree 1. Indeed, for every string of words w 1 . . . w l the length of the assigned type T 1 . . . T l is bounded by the αl. A fortiori, finite pregroup grammars are polynomial of degree 1. Hence all context free languages are generated by polynomial pregroup grammars of degree 1 . The grammars for the semilinear mildly context sensitive formal languages below are also linear polynomial. The context sensitive natural language fragments considered in subsection 3.2 are generated by a square polynomial. In fact, the latter is the polynomial used in [START_REF] Jens | Semilinearity as a syntactic invariant[END_REF] for proving non semilinearity of languages.

Mildly Context Sensitive Formal Languages

Consider the three standard mildly context sensitive formal languages, namely

L 1 = {vv : v ∈ Σ + } L 2 = {a n b n c n : n ≥ 1, a, b, c ∈ Σ, a = b, b = c} L 3 = {a m b n c m d n : m ≥ 1, n ≥ 1, a, b, c, d ∈ Σ, a = b, b = c, c = d} .

Duplication

L 1 = vv : v ∈ Σ +
The set of basic types is constructed from Σ by adding a new symbol s called sentence type and a 'copy' ā for every a ∈ Σ . The elements of {s} ∪ {ā : a ∈ Σ} are pairwise distinct symbols not in Σ. The set of basic types B 1 = B 1 , = is ordered by equality, where

B 1 = {s} ∪ Σ ∪ {ā : a ∈ Σ} .
The dictionary D 1 maps an element a ∈ Σ to the following infinite subset of P(B 1 )

D 1 (a) = {a} ∪ {ā r } ∪ b r 1 . . . b r i a r s b1 . . . bi : b 1 . . . b i ∈ Σ * .
This dictionary is modest (recall Definition 4).

Lemma 7. The language L G 1 of the pregroup grammar

G 1 = D 1 , s contains L 1 . Proof. Assume that X = a 1 . . . a m ∈ L 1 . Hence m = 2n and a n+i = a i , 1 ≤ i ≤ n, for some n ≥ 1. Case n = 1: Choose T 1 = a 1 and T 2 = a r 1 s. From the assumption follows that T 1 , T 2 is a type assignment for a 1 a 2 . Clearly, T 1 T 2 → s.
Case n ≥ 2: Define

T j =      a j for 1 ≤ j ≤ n a r n . . . a r 2 a r j s ān . . . ā2 for j = n + 1 ār j for n + 1 < j ≤ 2n.
The assumption implies āj = ān+j and thus āj ār n+j → 1, for 1 ≤ j ≤ n. Hence T 1 . . . T m → s. Thus the language L 1 is included in the language defined by G 1 .

The type assignment T 1 , . . . , T m defined above is called the canonical type assignment and the concatenated type T 1 . . . T m the canonical type. The unique index k such that the sentence type occurs in T k is called the key-index.

Lemma 8. Suppose T j ∈ D 1 (a j ), 1 ≤ j ≤ m, is a type assignment for X = a 1 . . . a m ∈ Σ * such that T 1 . . . T m → s. Then X ∈ L 1 and T 1 . . . T m is the canonical type assignment for X.
Proof. Two things are to be proved: t m = 2n for some n ≥ 1 and that a n+i = a i for 1 ≤ i ≤ n. The assumption T = T 1 . . . T m → s implies that s has a unique occurrence in T , by Lemma 6. Therefore there is a unique k such that 1 ≤ k ≤ m and s occurs in T k . Hence

T k = b r 1 . . . b r i a k r s b1 . . . bi for some i ∈ N and some string b 1 . . . b i ∈ Σ * . Moreover, if j = k then T j = a j or T j = ār j . From Lemma 6 follows b1 . . . bi T k+1 . . . T m → 1 and T 1 . . . T k-1 b r 1 . . . b r i a k r → 1. Under the assumption that b1 . . . bi T k+1 . . . T m → 1, use induction on i to show that T k+j = ār k+j for 1 ≤ j ≤ i a k+j = b i-j+1 for 1 ≤ j ≤ i i = m -k ≥ 0 . ( 8
)
Case i = 0: Then T k = a r k s and T k+1 . . . T m → 1, by Lemma 6. Clearly, the empty string is the only string of simple types in {a, ār : a ∈ Σ} that reduces to 1. Thus k = m. Case i ≥ 1 : Note that T k+1 = ār k+1 , because the other possible choice for T k+1 would be a k+1 . In this case bi a k+1 would be in every irreducible form of T 1 . . . T m by Lemma 4, contradicting the assumption. For the same reason, bi ār k+1 → 1, i.e. bi = āk+1 . The latter implies a k+1 = b i . Let T = b1 . . . bi-1 T k+2 . . . T m . Then T → 1 by Lemma 2. The induction hypothesis applies to T . Hence

T k+1+j = ār k+1+j , a k+1+j = b i-1-j+1 for 1 ≤ j ≤ i -1 and i -1 = m -(k + 1) . Similarly, under the assumption T 1 . . . T k-1 b r 1 . . . b r i a k r → 1 show that T k-l = a k-l for 1 ≤ l ≤ i + 1 a k-l = b l for 1 ≤ l ≤ i a k-i-1 = a k 1 = k -i -1 (9)
by induction on i . In the case

i = 0, note that k > 1, because if k = 1 then a r k → 1 , which is impossible. It follows that T k-1 = a k-1 and a k-1 = a k . Hence T 1 . . . T k-2 → 1 and therefore k -1 = 1.
The induction step is similar to that given above.

From equations ( 9) and [START_REF] Marco | Midly Non-Projective Dependency Structure[END_REF] follows that i = k -2 and m = k +i = k +k -2 = 2n, where n = k -1. Moreover, if j varies between 1 and i in increasing order then l = i -j + 1 varies between i and 1 in decreasing order. Hence

a j+1 = a 2+j-1 = a k-i+j-1 = b i-j+1 = a k+j = a n+j+1 , for 1 ≤ j ≤ i = n -1. Finally, a 1 = a n+1 follows from a k-i-1 = a k .
The proof above shows that an arbitrary type assignment with a reduction to the sentence type is equal to the canonical one and also constructs the unique reduction to the sentence type, namely

a 1 a 2 . . . a k-1 a k a k+1 . . . a m a 1 a 2 . . . a k-1 (b r 1 . . . b r i a r k s b1 . . . bi ) ār k+1 . . . ār m .

Multiple Agreement

L 2 = {a n b n c n : n ≥ 1, a, b, c ∈ Σ, a = b, b = c}
In a formal language, it is customary to denote a n ∈ Σ + the string consisting of n repetitions of the symbol a. This might lead to confusion because of the notation a (m) for simple types. Therefore the n-fold repetition of t is denoted [n]t below.

The set of basic types B 2 is ordered by equality, where

B 2 = {s} ∪ Σ ∪ {ā : a ∈ Σ}
The dictionary D 2 maps an element c ∈ Σ to the following infinite subset of P(B 2 )

D 2 (c) = {c} ∪ {c r } ∪ [n]a r [n]b r s c [n]c : 1 ≤ n, a, b ∈ Σ, a = b, b = c . Note that D 2 is modest. Moreover, G 2 = D 2 , s generates L 2 . Lemma 9. A string X = a 1 . . . a m ∈ Σ * has a type assignment a i : T i ∈ D 2 , 1 ≤ i ≤ m, such that T 1 . . . T m → s if and only if X ∈ L 2 .
Proof. -Assume X = a 1 . . . a m ∈ L 2 . Then m = 3n for some integer n ≥ 1. Define

T i =      a i for 1 ≤ i ≤ 2n [n]a r n+1 [n]a r 1 s ā i [n]ā i for i = 2n + 1 ār i for 2n + 2 ≤ i ≤ m .
Clearly, this type assignment has a reduction to the sentence type. Call it the canonical type assignment and m -n + 1 the key-index.

-Assume that

T i ∈ D 2 (a i ), 1 ≤ i ≤ m, satisfies T 1 . . . T m → s.
The argument is similar to that of Lemma 8. Now the unique type with an occurrence of the sentence type has the form

T k = [n]b r [n]a r s ā k [n]ā k , for some k ≤ m, n ≥ 1, a ∈ Σ, b ∈ Σ . Recalling that ā k [n]ā k = ā k āk [n-1]ā k → [n -1]ā k show that T i = ār i and a i = a k , for k + 1 ≤ i ≤ m, and n -1 = m -k T i = a i = a, for k -n ≤ i ≤ k -1, T i = a i = b, for 1 ≤ i ≤ k -n -1 and k = 2n + 1.
From this conclude that m = k + n -1 = 3n . Hence k = 2n + 1 and X = a n b n a n 2n+1 .

Crossing Dependencies

L 3 = {a m b n c m d n : m ≥ 1, n ≥ 1, a, b, c, d ∈ Σ, a = b, b = c, c = d}
The set of basic types remains unchanged, i.e.

B 3 = {s} ∪ Σ ∪ {ā : a ∈ Σ} .
The dictionary D 3 maps an element d ∈ Σ to the following infinite subset of P(B 3 )

D 3 (d) = {d} ∪ dr ∪ [m]c r [n]b r [m]a r s d [n] d : n, m ≥ 1 a, b, c ∈ Σ, a = b, b = c, c = d Again, D 3 is modest and G 3 = D 3 , s generates L 3 . Lemma 10. X = a 1 . . . a l ∈ Σ * has a type assignment T i ∈ D 3 (a i ), 1 ≤ i ≤ l, such that T 1 . . . T l → s if and only if X ∈ L 3 . Proof. Assume X = a 1 . . . a l = a m b n c m d n . This implies a 1 = • • • = a m = a, a m+1 = • • • = a m+n = b, a m+n+1 = • • • = a 2m+n = c, a 2m+n+1 = • • • = a l = d and l = 2m + 2n .
The key-index is k = 2m + n + 1 and the canonical type assignment satisfies

T i = a i for 1 ≤ i ≤ 2m + n ār i for 2m + n + 2 ≤ i ≤ l T k = [m]a r m+n+1 [n]a r m+1 [m]a r 1 s ā k [n]ā k .
The converse is left to the reader.

Note the common features shared by the three grammars G 1 -G 3 . Sentences w 1 . . . w l have a canonical type assignment T 1 , . . . , T l with a key-index k. Moreover, the length of the type T k is proportional to l whereas the length of the other types T i , i = k, is bounded by a constant. Therefore, the length q of the canonical type t 1 . . .

t q = T 1 . . . T l is O(l).

Natural Languages

Among the context sensitive natural language fragments are the Dutch and Swiss-German subordinate clauses and the compound noun phrases of Old Georgian.

Dutch Subordinate Clause

(Pullum, Gazdar) [START_REF] Pullum | Natural Languages and Context Free Languages, in: The Formal Complexity of Natural Language[END_REF] presents a context free grammar that weakly generates the Dutch subordinate clauses. According to Salvitch et al.) [?]sa, the context free grammar generates the clauses as strings of symbols but produces parse trees that violate the intuition of speakers about the phrase structure and the semantical dependencies. On the other hand, (Bresnan et al.) [START_REF] Bresnan Joan | Cross-Serial Dependencies in Dutch[END_REF] argues that no context free grammar strongly generates the clauses.

The polynomial pregroup grammar below strongly generates the Dutch subordinate clauses. This means that the reductions to the sentence type give rise to a semantic interpretation expressing the distant cross-dependencies. For example, in the subordinate clause2 below Marie is the agent of zag and Jan the agent of zwemmen. The dependency is represented by an arrow from the verb to the agent. dat Marie Jan zag zwemmen dat marie jan ( x 1 x 2 zien z id) ( x zwemmen) s s (NP ) (NP ) (NP r NP r s ī δ) (δ r ī) [START_REF] Lambek | Type Grammar revisited[END_REF] and compute its logical interpretation according to Section 2.2 dat(zien(marie, zwemmen(id(jan))) .

Applying the identity axiom id(jan) = jan , we see that the interpretation of the clause is equivalent to dat(zien(marie, zwemmen(jan))) .

(

) 12
By convention, the first argument of a relation corresponds to the agent. Hence, the subexpression relation in [START_REF] Lambek | From word to sentence[END_REF] expresses the semantical dependencies of sentence [START_REF] Lambek | The mathematics of sentence structure[END_REF].

The dependency arrows of ( 10

In ( 13), the path starting at x and ending at jan and the path from x 2 to marie constitute the dependency links of [START_REF] Lambek | The mathematics of sentence structure[END_REF]. The dependence of zien on x 2 and z is indicated by dotted overlinks. 3The number of noun phrases and causal verbs is not limited, for example v v v v u u (dat) Eva Piet Jan zag leren zwemmen ((that) Eva saw Pete teach Jan to swim) [START_REF] Joakim | Algorithms for deterministic incremental dependency parsing[END_REF] Consider the entries Eva : NP :: eva, Piet : NP :: piet, Jan : NP :: jan and zag (saw) : NP r NP r NP r si δδ :: zien(x 3 , z) id(x 2 ) id(x 1 ) leren (teach) : δ r δ r ii δ :: leren(x 2 , z ) id(x 1 ) zwemmen (swim) : δ r i :: zwemmen(x)

Compute the reduction of the assigned type to s . . . Eva P iet Jan zag leren zwemmen . . . (eva)(piet)(jan)( x 1 x 2 x 3 zien z id id) (x 1 x 2 leren z id)(x zwemmen) . . . (NP ) (NP ) (NP ) (NP r NP r NP r s i δ δ ) ( δ r δ r i i δ) (δ r i)

Replace the simple types by the corresponding logical symbols and represent dependencies by curved overlinks (eva)(piet)(jan)( x 1 x 2 x 3 zien z id id) (x 1 x 2 ler en z id) (x zwem men) [START_REF] Mati | Lambek calculus is NP-complete[END_REF] The oriented paths starting at x 3 , x 2 and x and terminating at eva, piet and jan respectively constitute the dependency arrows of [START_REF] Joakim | Algorithms for deterministic incremental dependency parsing[END_REF]. The logical expression is zien(eva, leren(piet, zwemmen(jan))) .

The graph [START_REF] Mati | Lambek calculus is NP-complete[END_REF] induces the labelled planar graph ( 16) belonging to a family of graphs relevant for dependency parsing, see (Kuhlmann, Nivre) [START_REF] Marco | Midly Non-Projective Dependency Structure[END_REF]. The labels of the edges in ( 16) are defined by the overlinks 'hidden' inside of (the type of) the words. Every path formed by the edges with a given label corresponds to a dependency arrow of ( 14).

1 2 3 3 2 3
Eva Piet Jan z a g leren zwemmen [START_REF] Carl | Head-driven phrase structure grammar[END_REF] The last verb in the clause may be intransitive, transitive, ditransitive etc. The arity of a verb w is the number of the argument places of the interpreting relation. Hence intransitive verbs are of arity 1, transitive verbs are of arity 2 and so on. Note that the arity of a non-causal verb coincides with the number of occurrences of non-basic types, for example zwemmen (swim) : δ r i :: zwemmen(x) (intransitive) schrijven (write) : δ r δ r i :: schrijven(x 2 , x 1 ) (transitive) geven (give) : δ r δ r δ r i ::

geven(x 3 , x 2 , x 1 ) (ditransitive)
The arity of the causal verbs below also is 2. The surplus number of non-basic types in an associated type T p , p ≥ 2, provides the argument places for the 'remembering' functions id. For example,

zag (saw) : [p]NP r si [p -1]δ :: zien(x p , z) id(x p-1 ) . . . id(x 1 ), p ≥ 2 leren (teach): [p]δ r ii [p -1]δ :: leren(x p , z) id(x p-1 ) . . . id(x 1 ), p ≥ 2 (17)
where x 1 corresponds to the first occurrence of NP r , x 2 to the second occurrence of NP r and so on up to x p , whereas z corresponds to i .

A string of words w 1 . . . w l is a k-fold subordinate clause if its first word w 1 is dat, the words w 2 up to and including w 1+k are proper names, the next word w 1+k+1 is a causal verb in finite form, the so-called key-word, and after the key-word the w i 's are infinitives, of which all are causal except the last one, which is non-causal of arity m = 2k + 2 -l .

A k-fold subordinate clause w 1 . . . w l has a canonical type assignment T i , 1 ≤ i ≤ l, namely

T i =                s s if i = 1 NP if 2 ≤ i ≤ k + 1 [k]NP r s i [k -1]δ if i = k + 2 [2k -i + 2]δ r i i [2k -i + 1]δ if k + 2 < i < l [2k -l + 2]δ r i if i = l .
The proof that the canonical type assignment reduces to the clause type s uses induction on k and follows from the next two lemmas.

A type T is said to be p-infinitival if either T = [p]δ r i and p ≥ 1 or T = [p]δ r ii [p -1]δ and p ≥ 2. It is said to be causal if the latter holds and non-causal in the former case.

Lemma 11. Let T j be infinitival or equal to NP for 1 ≤ j ≤ n. Then T 1 . . . T n → 1

Proof. Assume on the contrary that T 1 . . . T n → 1. As δ and NP do not occur in T 1 . . . T n the latter does not end with δ nor with NP . Hence T n = [p n ]δ r i. Therefore the number of occurrences of i in T 1 . . . T n exceeds that of i , because the latter always occurs together with the former. As i can only be linked to i , this contradicts T 1 . . . T n → 1.

Lemma 12. Let k ≥ 1, n ≥ 1, Z = i [k]δ and T j be p j -infinitival of length q j , 1 ≤ j ≤ n such that ZT 1 . . . T n → 1 holds. Then i) T n is non-causal ii) T j is causal, 1 ≤ j ≤ n -1. Moreover, p j = k -j + 1, 1 ≤ j ≤ n iii) n = k -p n + 1 iv) q j = 3 + 2(k -j), 1 ≤ j < n, q n = k -n + 2 .
Proof. From ZT 1 . . . T n → 1 follows that T n = [p n ]δ r i by the same argument as above. Hence i) holds. Next show ii), iii) and iv) by induction on n.

Case

n = 1. From i [k]δ [p 1 ]δ r i → 1 follows that k = p 1 Case n ≥ 2. Recall that ZT 1 . . . T n = i [k]δ [p 1 ]δ r iXY → 1 where Y = T 2 . . . T n and either X = 1 or X = i [p 1 -1]δ .
The latter alternative holds if T 1 is causal, the former if it is non-causal. Note that i r does not occur in the string XY and therefore the leftmost occurrence of i in ZT 1 . . . T n → 1 is linked to the unique i on its left. It follows that Lemma 11 and the assumption n ≥ 2. Hence X = i [p 1 -1]δ with p 1 ≥ 2. Now apply the induction hypothesis to X, T 2 , . . . , T n . Finally, iii) and iv) are immediate consequences of ii) and i).

[k]δ [p 1 ]δ r → 1 and XY → 1, hence k = p 1 . If X = 1 then T 2 . . . T n = Y → 1, contradicting
Theorem 1. 1) For every subordinate clause there is a unique type assignment with a reduction to the clause type s. 2) Every string of words from the dictionary that has a type assignment with a reduction to s is a subordinate clause.

Proof. 1) The first assertion follows from the definitions by Lemmas 1 -6.

2) To see the converse, let T j ∈ D(w j ) for 1 ≤ j ≤ l and T 1 . . . T l → s . By Lemma 5, s occurs in exactly one type T i and therefore T i = ss and w i = dat. Then s also has exactly one occurrence in the string. Indeed, each of its occurrences is linked to some occurrence of s and the latter occurs only together with s . Let p be the unique index such that s occurs in T p . Therefore T j is either infinitival or the basic type NP for all j other than i and p . Note that p > i, because s and s are linked. Moreover,

T p = [k]NP r s i [k -1]δ for some k ≥ 2 .
First note that i = 1, because T 1 . . . T i-1 → 1 by choice of i. This is only possible if the string is empty by Lemma 11.

Next,

T 2 . . . T p-1 [k]NP r → 1, because s is linked to s . From this follows that T 2 = • • • = T p-1 = NP and p = 1 + k + 1 by Lemma 4.
Finally, from the preceding follows that i [k -1]δ T p+1 . . . T l → 1 . Note that NP cannot occur in this string and conclude by Lemma 12.

Theorem 1 above implies that for every s-sentence w 1 . . . w l there are unique types T i ∈ D(w i ), 1 ≤ i ≤ l, and a unique type T = T 1 . . . T l such that T → s . Call T the canonical type, T i ∈ D(w i ) the canonical type assignment and the unique reduction of T to s the canonical reduction of w 1 . . . w l .

The preceding theorem implies that the infinite grammar above is polynomial, i.e. the length of any type assignment with a derivation to s is bounded by a polynomial. The property also intervenes in the complexity estimate of the parsing algorithm in Section 4.

Corollary 2. The length of the canonical type

T 1 . . . T l of a k-fold Dutch sub- ordinate clause is bounded by k 2 + 3k + 1 . Moreover, k ≤ l/2 .
Proof. Let k be the number of noun phrases preceding the key-word w p , m the arity of the last verb w l . The number n of words after w p satisfies n = k -m by Lemma 12. The number of words before the key-word w p is k + 1. Hence l = 2k -m + 2 and therefore k ≤ l/2 .

On the other hand, the length q of the type T 1 . . . T l is

q = 2 + k + q + m + 1 ,
where q is the length of the type T p T p+1 . . . T l-1 . Starting at T l-1 and reading backward from right to left, the length of the types increases by 2 from one to the next. The length of the rightmost type T l-1 is 2 + 2m + 1 . Therefore

q = j=n j=1 (2j + 2m + 1) = n(2m + 1) + n(n + 1) = k 2 + 2k -m 2 -2m Hence, q = k 2 + 3k -m 2 -m + 3 ≤ k 2 + 3k + 1.
The canonical reduction defines the semantic dependencies as well. This follows from the next lemma, where a path in the oriented graph G represents the successive substitutions and instances of the identity axiom intervening in the interpretation.

Lemma 13. Let k > n ≥ 0 and G = V 0 ∪ V 1 , E 0 ∪ E 1 be the oriented graph defined as follows V 0 = {a ij : 0 ≤ i ≤ n, 1 ≤ j ≤ k -i} (functional symbol) V 1 = {x lp : 1 ≤ l ≤ n + 1, 1 ≤ p ≤ k -l} (variable) and E 0 = { a ij , x i+1,j : 0 ≤ i ≤ n, 1 ≤ j ≤ k -i} (substitution) E 1 = { x il , a i,l-1 : 1 ≤ i ≤ n, 2 ≤ l ≤ k -i} (identity axiom) .
Then for 1 ≤ j ≤ k there is a unique maximal path starting at a 0j . Moreover, x l,j+1-l and a i,j-i are on this path for all l such that 1 ≤ l ≤ n + 1 and j -l ≥ 0 and all i satisfying j -i ≥ 1 and 0 ≤ i ≤ n .

Proof. Straightforward by induction on k. The graph looks like this for k = 4, n = 2, where the underlinks represent the edges in E 0 and the overlinks the edges in E 1 (a 01 a 02 a 03 a 04 ) (x 14 x 13 x 12 x 11 a 11 a 12 a 13 ) (x 23 x 22 x 21 a 21 a 22 )(x 32 x 31 ) .

Pregroup Grammar with Copying Rules

(Stabler 2004) [START_REF] Edward | Varieties of crossing dependencies: Structure dependence and mild context sensitivity[END_REF] considers copying grammars when analysing crossing dependencies in human languages. Following this lead, define the following finite pregroup grammar enriched with two copying rules dictionary entries copying rules zag (saw) : NP r NP r si δ leren (teach):

δ r δ r ii δ NP r T δ → NP r NP r T δδ δ r T δ → δ r δ r T δδ . ( 18
)
The copying rules are not derivable in Pregroup Calculus. Therefore the graphical representations of derivations is lost and with them the mathematical structure of the proofs. Moreover, the semantical interpretation of the control verbs cannot be read off the type in the dictionary but must be constructed during the proof by a semantic copying rule parallel to the grammatical copying rule. It is easy to see that every clause recognized by the polynomial pregroup grammar is also recognized by the finite grammar with copying rules. Indeed, let T 1 , . . . , T n be a type assignment for w 1 , . . . , w n from the infinite dictionary with a reduction r to the clause type. The corresponding type assignment T j , 1 ≤ j ≤ n from the finite dictionary has the following derivation to the clause type. For every type T j of the form [p j ]NP r si [p j -1]δ respectivley [p j ]δ r ii [p j -1]δ apply p j -2 times the coppying rule to T j = NP r NP r si δ respectivley to T j = δ r δ r ii δ . The resulting compound type is T 1 , . . . , T n . Then apply the contraction rule as indicated by the links of r.

The converse also holds. A string derivable in the copying grammar also has a reduction in the polynomial grammar. First show that an arbitrary derivation can be replaced by one where all copying rules are applied before the contraction rule. Then use an argument similar to that establishing the second part of Theorem 1.

Swiss German Subordinate Clause

According to the analysis of (Shieber) [START_REF] Stuart | Evidence Against the Context-Freeness of Natural Language[END_REF], the Swiss-German subordinate clause has the same semantic cross-serial dependencies as Dutch, but they are also expressed in the syntax by case marking. This can be captured by distinguishing the types for noun phrases NP nom , NP dat , NP acc as well as the dummy types δ nom , δ dat , δ acc . The proofs are similar to the preceding ones. In particular, correct semantical dependencies guarantee correct syntax.

Old Georgian Noun Phrase

The pregroup grammar below generates compound noun phrases of Old Georgian according to the analysis of [START_REF] Jens | Semilinearity as a syntactic invariant[END_REF]. The dictionary lists an infinite number of distinct words. Indeed, Old Georgian uses genitive suffixes for possessive compound noun phrases. The genitive suffix is appended to noun(stem)s or names. When the construction is repeated, the previous genitive suffixes are also repeated.

govel-i igi sisxl-i saxl-isa-j m-is Saul-is-isa-j
all-Nom Art=Nom blood-Nom house-Gen-Nom Art-Gen Saul-Gen-Gen-Nom 'all the blood of the house of Saul' [START_REF] Preller | Linear Processing with Pregroup Grammars[END_REF] More generally, compound nominative noun phrases have the form

N1-Nom N2-Gen-Nom N3-Gen 2 -Nom . . . N k -Gen k-1 -Nom . ( 20
)
Square brackets highlight semantic dependencies as follows

[N 1 -Nom [N 2 -Gen-Nom [N 3 -Gen 2 -Nom . . . [N k -Gen k-1 -Nom] NP k . . . ] NP 3 ] NP 2 ] NP 1 .
Assume the basic types NP nom , N nom and G for nominative noun phrases, nominative common nouns and genitive suffixes in that order. For each p ≥ 0, the word Name-Gen p -Nom respectively Noun-Gen p -Nom has two entries in the dictionary, namely Name-Gen p -Nom :

NP nom [p]G NP nom [p]G [p + 1]G NP nom Noun-Gen p -Nom : N nom [p]G N nom [p]G [p + 1]G NP nom . ( 21
)
Common nouns are preceded4 by a determiner to form noun phrases like

Art = Nom Noun-Nom Art-Gen Noun-Gen p -Nom . ( 22
)
Adding the following entries to the dictionary

Art = Nom : NP nom N nom Art-Gen : NP nom GG N nom , ( 23
)
each of the noun phrases [START_REF] Stuart | Evidence Against the Context-Freeness of Natural Language[END_REF] has two possible types, each of which reduces to the type of a noun phrase. For p ≥ 1, the types for Art-Gen Noun-Gen p -Nom are

(NP nom GG N nom ) (N nom [p]G) → NP nom [p]G , (NP nom GG N nom ) (N nom [p]G [p + 1]G NP nom ) → NP nom [p]G [p + 1]G NP nom .
The length of the type at the left of → exceeds that of the reduced type by 4.

It follows that every string of words of the form (20) has a unique type assignment with a reduction to the noun phrase type NP and vice versa. The length of the assigned type can be expressed as a square polynomial in the length of the string.

Tagging and Parsing Algorithm

Ambiguity enters parsing by pregroup grammars in two ways. There may be different type assignments with a reduction to the sentence type or a fixed type assignment of length q may have (up to 2 q ) distinct reductions to the sentence type. Testing every type assignment for an eventual reduction to the sentence type is highly inefficient even if the dictionary is finite. The usual cubic-time polynomial recognition algorithms do not construct reductions and rely on the fact that the dictionary is finite or at least that there is a constant bounding the number of types per word in the dictionary. Some authors use 'parsing' in the weak sense that the algorithm constructs a reduction to the sentence type for a given type assignment, whereas the choice of a type assignment is called 'tagging'. 'Parsing' is used here in the following stronger sense. Definition 6. A recognition algorithm decides whether or not a string of words w 1 . . . w l ∈ Σ * has a type assignment T 1 , . . . , T l such that the concatenated type T 1 . . . T l has a reduction to the sentence type. A parsing algorithm is an algorithm that decides whether or not a string of words is a sentence and, if the answer is yes, computes a type assignment and a reduction to the sentence type.

Recognition is sufficient for formal languages, but parsing is indispensable for natural languages, because the semantic interpretation of a sentence is defined via the derivation to the sentence type.

The algorithm below is a variant of the algorithm in (Preller 2007-2) [START_REF] Preller | Linear Processing with Pregroup Grammars[END_REF]. It processes the string of words from left to right and chooses a type for each word. The choice relies on a tagging strategy motivated by properties specific to the languages L i of the preceding section. The strategy avoids 'losing' typeassignments as soon as possible. That is to say it avoids a type assignment T 1 , . . . , T i that cannot be extended to a type assignment T 1 , . . . , T i , T i+1 , . . . , T l with a reduction to the sentence type.

The Algorithm

A stack of non-negative integers is defined inductively. The empty symbol ∅ is a stack, called the empty stack. If S is a stack and i a non-negative integer then S , i is a stack. The functions top and pop send a stack S , i to its top i and to its tail S respectively. They are undefined for the empty stack.

When processing the string w 1 . . . w l ∈ Σ * , the algorithm moves through a subset of the following set of stages

S w 1 ...w l = {(i; T 1 , . . . , T i ; p) : 1 ≤ i ≤ l, 1 ≤ p ≤ q i , T j ∈ D(w j ), 1 ≤ j ≤ i} ∪ {(i; T 1 , . . . , T i-1 , 1; 0) : 1 ≤ i ≤ l + 1, T j ∈ D(w j ), 1 ≤ j ≤ i -1} ∪ {s in } ,
where q i is the length of the type T i and s in is a new symbol denoting the initial stage.

A partial order is defined on the set of stages as follows

s in ≤ s for all s (i; T 1 , . . . , T i ; p) ≤ (i ; T 1 , . . . , T i ; p ) ⇔ i < i , T j = T j for 1 ≤ j ≤ i or i = i , p = 0, T j = T j for 1 ≤ j < i or i = i , 1 ≤ p ≤ p , T j = T j , 1 ≤ j ≤ i .
This partial order induces a total order on the set of all stages less or equal to a given stage. Moreover, all stages of the form (l + 1; T 1 , . . . , T l , 1; 0) are maximal. Every non-initial stage s has a unique predecessor s -1, given by

(i; T 1 , . . . , T i ; p) -1 =          (i; T 1 , . . . , T i ; p -1), if p ≥ 2 (i; T 1 , . . . T i-1 , 1; 0) if p = 1 (i -1; T 1 , . . . , T i-1 ; q i-1 ) if p = 0 and i > 1 s in if p = 0 and i = 1 .
A non-initial stage is tagging if its last integer p = 0 and testing otherwise. Every testing stage s has a unique successor s + 1, namely (i; T 1 , . . . , T i ; p) + 1 = (i; T 1 , . . . , T i ; p + 1) if p < q i (i + 1; T 1 , . . . , T i , 1; 0) if p = q i and i ≤ l .

The algorithm executes two subroutines, tagging and testing, for each word w i . When at tagging stage (i; T 1 , . . . , T i-1 , 1; 0), i ≤ l, the algorithm has finished processing the type T 1 . . . T i-1 . The tagging routine tag D either chooses a type Tag ∈ D(w i ) or decides to stop and updates the constant output. The computation of Tag involves a constant key that depends on the language whose sentences are to be parsed. The routine tag D is defined in the next subsection. At a maximal stage (l + 1; T 1 , . . . , T l ; 0), the output is updated to the result computed so far.

Recall that the types T j at stage s = (i; T 1 , . . . , T i ; p) are strings of simple types T j = t j1 . . . t jqj . Each testing stage s = (i; T 1 , . . . , T i ; p) defines a working position p(s) = q 1 + • • • + q i + p, the simple type read t p(s) = t ip and the type processed T (s) = t 1 . . . t p(s) = t 11 . . . t 1q 1 . . . t i1 . . . t ip . To keep notation uniform, define p(s in ) = 0 and t 0 = 1. Note that for every testing stage s and positive integer i ≤ p(s), there is a unique testing stage s ≤ s such that i = p(s ). When fed the string of words Marie Jan zag zwemmen the parser goes through the following stages and values. The constant key remains undefined until a causal verb in finite form w i is encountered. There the value is updated to i and remains unchanged afterwards. The values of the other constants are listed in Table 1 below. At the maximal stage s fin = (5; T 1 , . . . , T 4 , 1; 0) , the output is updated to R(s fin ) = {{2, 3} , {1, 4} , {7, 8} , {6, 9}} T (s fin ) = NP NP NP r NP r si δδ r i I(s fin ) = s

Tag

S R s in undefined ∅, 0 ∅ (1; 1; 0) T 1 = NP ∅, 0 ∅ (1; T 1 ; 1) NP ∅, 0 , 1 ∅ (2; T 1 , 1; 0) T 2 = NP ∅, 0 , 1 ∅ (2; T 1 , T 2 ; 1) NP ∅, 0 , 1 , 2 ∅ (3; T 1 , T 2 , 1; 0) T 3 = NP r NP r si δ ∅, 0 , 1 , 2 ∅ (3; T 1 , T 2 , T 3 ; 1) NP r NP r si δ ∅, 0 , 1 {2, 3} (3; T 1 , T 2 , T 3 ; 2) NP r NP r si δ ∅, 0 {{2, 3} , {1, 4}} (3; T 1 , T 2 , T 3 ; 3) NP r NP r si δ ∅, 0 , 5 {{2, 3} , {1, 4}} (3; T 1 , T 2 , T 3 ; 4) NP r NP r si δ ∅, 0 , 5 , 6 {{2, 3} , {1, 4}} (3; T 1 , T 2 , T 3 ; 5) NP r NP r si δ ∅, 0 , 5 , 6 , 7 {{2, 3} , {1, 4}} (4; T 1 , T 2 , T 3 , 1; 0) T 4 = δ r i ∅, 0 , 5 , 6 , 7 {{2, 3} , {1, 4}} (4
One could argue following (Lambek 2008-2) [13] that simple types represent bits of information to be stored in the short-term memory (limited to 7 ± 2 bits) when processing a string of words. The present algorithm seems to confirm this claim. Theoretically, a Dutch speaker can form subordinate clauses of arbitrary length. In practice, three to four noun phrases between dat and the causal verb in finite form are rarely exceeded. For two noun phrases, the stack contains at most four bits. With three noun phrases, it goes up to five, with four to six. Accepting that the types represent the patterns in which a word can appear, one also accepts that they are learned in childhood and 'hard-wired'. This includes the pattern of causal verbs represented by [p]NP r si [p -1]δ, where p is 2 or more. They are downloaded to the 'working' memory where the subconscious processing goes on and only the result ends up in the short-term memory.

Theorem 3. The string of words w 1 . . . w l is a sentence if and only if the tagging-parsing algorithm reaches a maximal stage such that output = R, T, s . If this is the case, R is a reduction of T to s . Moreover, the algorithm is linear for the formal languages and square polynomial for the natural languages.

Proof. The first assertion follows from Lemma 14 and Lemma 1. Moreover, the number of basic steps executed at a testing stage is bounded by a constant. It is proportional to the length of the chosen type at a non-maximal tagging stage. Finally, updating the output at a maximal stage s fin is proportional to the length of T (s fin ).

Conclusion

It may be worth-while to investigate whether the degree of the polynomial of a pregroup grammar can serve as a classification for (natural) languages. Indeed, proof-search in the Pregroup Calculus is bounded by a cubic polynomial in the length of types. Therefore in general, the search for a derivation is cubic polynomial in the length of the type even after type assignment. This is in opposition to categorial grammars based on Syntactic Calculus where proofsearch is NP-complete, (Pentus 2003) [START_REF] Mati | Lambek calculus is NP-complete[END_REF]. Hence, the ratio of the length of the concatenated type over the number of words is essential when designing a pregroup grammar with an efficient algorithm.

The parsing complexity for the languages considered here is lower than the general cubic polynomial limit because proof-search is linear for the sets of types occurring in the dictionaries and because the algorithm constructs a single derivation while processing from left to right. Proof-search remains linear for larger classes of types than those mentioned here. This gives rise to grammars for language fragments involving relative pronouns and coordination, subject and object control, agreement of features among others. In fact, these grammars have been designed for a complete linear deterministic parsing algorithm with occasional backtracks producing a planar dependency graph. Empirical studies based on large scale treebanks in (Nivre) [START_REF] Joakim | Algorithms for deterministic incremental dependency parsing[END_REF] show that such algorithms are highly accurate for other formalisms in general where no proof of completeness exists.

  y y y y dat Marie Jan zag zwemmen (that Mary saw Jan swim) (10) Using the entries dat (that) : ss :: dat(y) Marie (mary) : NP :: marie zag (saw) : NP r NP r si δ :: zien(x 2 , z) id(x 1 ) Jan (jan) : NP :: jan zwemmen (swim) : δ r i :: zwemmen(x) , parse this clause

ma rie jan x 1 x 2

 2 ) can also be obtained geometrically. It suffices to represent the dependencies by curved overlinks. The vertical arrows indicate the functional symbols, connected to their arguments by the dotted overlinks. m m m m m m m m m m m m m m m m m m r r r r r r r r r r r r r r ( zien z id x zwem men .

  Lemma 5. Suppose T → T and t occurs at k distinct positions in T but neither the right nor the left adjoint of t occurs in T . Then t has k occurrences in T . Assume that T = t 1 . . . t n is modest and that T → t. Then there is a unique position i such that t = t i . Moreover, t i+1 . . . t n → 1. In addition, t i+1 . . . t i+k → 1 implies t i+k+1 . . . t n → 1, for all 1

	Lemma 6.

Table 1 :

 1 Processing Marie Jan zag zwemmen.

		δ r i	∅, 0 , 5 , 6	{{2, 3} , {1, 4}} ∪ {{7, 8}}
	(4; T 1 , . . . , T 4 ; 2)	δ r i	∅, 0 , 5	{{2, 3} , {1, 4}} ∪ {{7, 8} , {6, 9}}

; T 1 , . . . , T 4 ; 1)

if w i is a causal verb in finite form and i > 1 let key = i, k = i -1 and Tag = [k]NP r s i [k -1]δ else let output=fail if i > key if w i is

an infinitive of a causal verb let p = k -(i -key) and Tag = [p]δ r i i [p -1]δ of a non-causal verb let Tag ∈ D(w i ) else output=fail

Recall: a basic type b is identified with the simple type b(0)

adapted from examples in (Bresnan et al.)[START_REF] Bresnan Joan | Cross-Serial Dependencies in Dutch[END_REF]

This vindicates Claudia Casadio's idea that overlinks intervene in grammatical dependencies. The graph above the logical symbols in[START_REF] Lambek | Reflections on English Pronouns[END_REF] represents the concatenation of the meanings of the words. It 'lives' in symmetric compact 2 -categories, like the category of real vector spaces. The overlinks correspond to expansions in the symmetric 2-category, but not in the non-symmetric 2-category of derivations of the Pregroup Calculus. The meaning of the sentence is obtained by composing the concatenated meanings with the reduction.

The determiner may also follow its noun. This is ignored here.

Acknowledegement

The author is grateful to an anonymous reader for many helpful remarks.

* I am thankful for financial support provided by TALN/LIRMM/CNRS.

When in testing stage s, the algorithm checks if t p(s) contracts with the last not yet contracted simple type and updates the stack of positions S(s) and the reduction R(s). The latter contains the links computed so far. The former contains the unlinked positions in increasing order such that the top of the stack is the position of the last unlinked simple type.

Finally, the irreducible substring I(s) of T (s) consisting of the unlinked simple types in the order given by the stack S(s) is defined by

Definition 7. Tagger-Parser

At the initial stage s = s in , key, output, S and R are initialized to

Then the process goes to the first tagging stage s = (1; 1; 0) At tagging stage s = (i; T 1 , . . . , T i-1 , 1; 0), the stack and reduction remain unchanged

.

and the process goes to the next stage unless tag D (i) updates output to fail

At testing stage s = (i; T 1 , . . . , T i ; p), p ≥ 1,

Then the process goes to the next stage

The proof of the next lemma is given in (Preller 2007-2) [START_REF] Preller | Linear Processing with Pregroup Grammars[END_REF].

Lemma 14. For every stage s = (i; T 1 , . . . , T i ; p) , the string of simple types I(s) associated to the stack S(s) is an irreducible substring of T (s) and R(s) is a reduction from T (s) to I(s).

Tagging Strategy

The strategy is based on the fact that a sentence has a unique derivation to the sentence type. The strategy chooses the type a word must have if the whole string is a sentence. Testing validates or invalidates that choice.

In the case of the formal language L 1 , the key index for w 1 . . . w l is l/2 + 1. If the latter is not an integer, the string is not a sentence. At the first tagging stage (1; 1; 0), processing is stopped if the length l of the string is odd.

In the case of L 3 , the routine tag D 3 tests whether the length is even. If this not the case the string w 1 . . . w l is not a sentence. Otherwise, it computes the number m of repetitions of the first word w 1 . If w 1 . . . w l is a sentence the number n of repetitions of w m+1 satisfies n = l/2 -m and the key satisfies

The case of L 2 is similar with the appropriate adaptations . Finally, in the case of the Dutch dictionary D 4 , the types are chosen according to the following properties of a subordinate clause -the key-index key must be the first p for which w p is a causal verb in finite form -the non-causal words have a unique type in the dictionary -every word after the key-word except the last is a causal infinitive. The last is a non-causal infinitive.

tag D 4 (i) if key = undefined if w i is an infinitive let output=fail else if w i is not a causal verb in finite from let Tag ∈ D(w i )