Thomas Seiller

Interaction Graphs: Full Linear Logic *

Keywords: Full Linear Logic Interaction Graphs, Linear Logic, Geometry of Interaction, Quantitative Semantics, Measurable Dynamics

de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

This work deals with so-called dynamical models of proof theory, such as game semantics and geometry of interaction, as well as with quantitative models of computation. It extends previous work providing a uniform construction of quantitative dynamical models of (fragments of) linear logic to full linear logic with second-order quantification.

Geometry of Interaction.

A Geometry of Interaction (GoI) construction, i.e. a construction that fulfills the GoI research program [START_REF] Girard | Towards a geometry of interaction[END_REF], is in a first approximation a representation of linear logic proofs that accounts for the dynamics of cut-elimination. Contrarily to denotational semantics, a proof π and its normalized form π are not represented by the same object, but they remain related through a semantic interpretation of the cut-elimination called the execution Ex: Ex(π) = π . A GoI construction hence represents both the proofs and their normalization; it is in some ways an untyped variant of game semantics [START_REF] Martin | On full abstraction for PCF: I, II, and III[END_REF][START_REF] Abramsky | Games and full completeness for multiplicative linear logic[END_REF]. The further aim of geometry of interaction is to reconstruct logical operations from such a dynamical representation of proofs. The objects of study in a GoI construction are actually a generalization of the notion of proof -sometimes called paraproofs. This point of view allows a reconstruction of logic as a description of how paraproofs interact, in the same spirit as classical realizability [START_REF] Krivine | Typed lambda-calculus in classical zermelo-fraenkel set theory[END_REF][START_REF] Krivine | Realizability in classical logic[END_REF]: a program is of type nat → nat because it produces a natural number when given a natural number as an argument. As in game semantics and classical reliazability, one can however describe a necessary condition for being the interpretation of a proof, and defines winning paraproofs as those objects satisfying it.

In spite of their seemingly deep abstraction, the GoI constructions offer a mathematical model which is very close to actual computing. As an illustration of this fact, let us mention the Geometry of Synthesis program initiated by Ghica [START_REF] Ghica | Geometry of synthesis: a structured approach to vlsi design[END_REF][START_REF] Ghica | Geometry of synthesis II: From games to delay-insensitive circuits[END_REF][START_REF] Ghica | Geometry of synthesis III: resource management through type inference[END_REF][START_REF] Ghica | Geometry of synthesis IV: compiling affine recursion into static hardware[END_REF]. This research program, inspired by geometry of interaction, aims at obtaining logical synthesis methods for VLSI (Very Large Systems Integration) designs.

Quantitative Semantics. Quantitative semantics find its origins in Girard's work on functors's models for lambda-calculus [START_REF] Girard | Normal functors, power series and λ-calculus[END_REF]. This work, which predates its seminal work on linear logic [START_REF] Girard | Linear logic[END_REF] and actually inspired it, exhibits for the first time a decomposition of the semantic interpretation of lambda-terms as Taylor series. These series capture a number of informations about the time, space, resource consumption of the programs it represents. Quantitative semantics are therefore more involved than so-called qualitative semantics, since they mirror more informations about the programs that are interpreted. Recently, quantitative semantics has been used to give denotational semantics for various algebraic extensions of lambda calculus such as probabilistic [START_REF] Danos | Probabilistic coherence spaces as a model of higherorder probabilistic computation[END_REF] or differential lambda calculi [START_REF] Ehrhard | Finiteness spaces[END_REF]. Work by Laird, Manzonetto, McCusker and Pagani [START_REF] Laird | Weighted relational models of typed lambda-calculi[END_REF] provides a uniform account of several denotational models accouting for quantitative notions, using a refinement of the relational model. Interaction Graphs. Interaction graphs were first introduced by the author [START_REF] Seiller | Interaction graphs: Multiplicatives[END_REF] as a combinatorial approach to Girard's hyperfinite Geometry of Interaction [START_REF] Girard | Geometry of interaction V: Logic in the hyperfinite factor[END_REF], restricted to the multiplicative fragment of linear logic. An extension capable to deal with additives connectives was then defined [START_REF] Seiller | Interaction graphs: Additives[END_REF] and shown to abstract not only the (additive fragment of the) hyperfinite GoI model but all previously introduced GoI constructions as well. Both papers proposed a model construction in the spirit of Girard's GoI construction where proofs were interpreted by graphs instead of infinite operators. Dealing with exponentials however needs one to consider infinite objects. This is why a third paper [START_REF] Seiller | Interaction graphs: Graphings[END_REF] showed how the construction on graphs can be applied when working with a generalisation of graphs named graphings. Graphings are in some sense geometric realisations of graphs on a measured space X. This allows not only to consider infinite graphs (which can be used to define exponentials in the same way as the original GoI constructions), but also graphs acting on continuous, thus infinite, finite-measure spaces. This general construction on graphings was shown [START_REF] Seiller | Interaction graphs: Graphings[END_REF] to improve on Girard's hyperfinite GoI [START_REF] Girard | Geometry of interaction V: Logic in the hyperfinite factor[END_REF] since it allows a satisfactory treatment of secondorder quantification. Lastly, a fourth paper [START_REF] Seiller | Interaction graphs: Exponentials[END_REF] showed how the consideration of graphings can be used to define "quantitative" exponential connectives for Elementary Linear Logic [START_REF] Girard | Light linear logic[END_REF], a fragment of linear logic that captures elementary time computation [START_REF] Danos | Linear logic & elementary time[END_REF].

Unbounded Exponentials and Quantitative Aspects. The author's work on Interaction Graphs should be understood as a dynamic counterpart of weighed relational models, i.e. its relation to standard dynamical models (geometry of interaction, game semantics) is comparable to weighted relational models' relations with standar relational models. Indeed, it provides a uniform construction of models which not only captures all of Girard's GoI models, but also extends them: while Girard's constructions can be understood as interpreting proofs as graphs 1 , we here interpret proofs as weighted graphs, i.e. graphs with weighted edges2 . Furthermore, interaction graphs models can reflect these quantitative informations at the level of types since the latter are built from an orthogonality relation which can take into account those weights. Indeed, the orthogonality relation is defined through a measurement of cycles [START_REF] Seiller | Interaction graphs: Graphings[END_REF] by means of an integral over a finite-measured space -the support of the cycle. In the simplest cases one measures a cycle π of suppport supp(π) and weight ω(π) ∈ Ω, along a measurable map m : Ω → R+ , by the following integral:

supp(π) m(ω(π)) (1)
Since Interaction Graphs provide a generalization of Girard's constructions, one could easily adapt the interpretation of exponential connectives from Girard's first constructions [START_REF] Girard | Geometry of interaction I: Interpretation of system F[END_REF][START_REF] Girard | Geometry of interaction III: Accommodating the additives[END_REF] to obtain a model of full linear logic. This adaptation would extend to Danos' interpretation of pure lambda-calculus in GoI [START_REF] Danos | La Logique Linéaire Appliquée à l'Étude de Divers Processus de Normalisation (principalement du λ-calcul)[END_REF]. However, this interpretation of exponential connectives corresponds to defining !a as a (countable) infinite family of copies of a. Thus, even if a is represented by a graphing acting on a space of finite measure, its exponentiated version !a acts on a space of infinite measure. This fact hinders the quantitative aspects of our model since it creates cycles π whose support supp(π) are spaces of infinite measure. As a consequence, the integral defining the orthogonality relation (Equation 1) diverges as soon as the weight is not mapped to 0, i.e. as soon as m(ω(π)) = 0. The resulting model is therefore no longer capable of depicting quantitative informations.

Contributions and Related Work. We define, in the framework of interaction graphs, exponential connectives for full linear logic in a way that preserves the quantitative aspects of the construction. We define exponential connectives along the same lines as in our work on (bounded) exponentials [START_REF] Seiller | Interaction graphs: Exponentials[END_REF], avoiding the involvement of infinite-measure sets. With this definition of exponential connectives, one would however expect only a restriction of linear logic, such as ELL. To bypass this restriction, we relax the notion of states. Indeed, the interpretation of proofs in interaction graphs makes use of so-called thick graphs -or thick graphings in the general framework -, which can be understood as graphs with states. While previous work considered only finite sets of states, we loosen this definition to allow for infinite yet finite-measure (actually continuous) sets of states. This modification impacts slightly on the basic notions notions and constructions considered in previous work [START_REF] Seiller | Interaction graphs: Graphings[END_REF], for which we consider adequate generalisations. These changes, however, do not raise any technical difficulties. The resulting model is then shown to model digging and dereliction in addition to the principles of Elementary Linear Logic, thus interpreting full linear logic. This paper is the second GoI-style construction for full linear logic (including additives) and second order quantification. Indeed, Girard's so-called GoI3 construction [START_REF] Girard | Geometry of interaction III: Accommodating the additives[END_REF] already provided such a model. However, as explained above, Girard's treatment of exponential connectives prevents from any generalization accounting for quantitative informations. The main contribution of this paper therefore lies in its quantitative aspects. Moreover, we are able to pinpoint the computational principles (represented as measurable maps) that are essential to interpret digging and dereliction, i.e. we exhibit a single map -the exchange xch -which turns a model of ELL into a model of LL. Lastly, we provide a full soundness result and discuss the issue of the representation of cut-elimination in the model.

Apart from geometry of interaction constructions, related work include quantitative realizability [START_REF] Dal | Realizability models and implicit complexity[END_REF][START_REF] Brunel | Quantitative classical realizability[END_REF] -which provides characterizations of computational complexity classesand quantitative game semantics for linear logic [START_REF] Dal | Quantitative game semantics for linear logic[END_REF], although the latter does not deal with additives and quantifiers and seems more limited in its possible quantitative features. In particular, we believe our construction to be a generalization of quantitative realizability, allowing for characterisations of a larger family computational complexity classes [START_REF] Seiller | Towards a Complexity-through-Realizability theory[END_REF].

C S L ' 1 5 2 Interaction Graphs

We start by a discussion meant to give intuitions about the basic principles at work in the interaction graphs models. We illustrate those principles by explaining the notion of thick and sliced graphs [START_REF] Seiller | Interaction graphs: Exponentials[END_REF]. This discussion is quite informal in that we do not provide explicit and complete definitions of the objects and operations considered, to avoid overloading the reader with non-essential definitions. Indeed, the actual model uses thick and sliced graphings, a generalisation needed to accomodate both exponentials and quantifiers. Before providing the formal definition of those at the end of the section, we discuss the generalisation to continuous sets of states.

Thick and Sliced Graphs

The term "graph" will stand for "directed weighted graphs", i.e. directed graphs with a weight function from the set of edges to a monoid3 of weights Ω. Given a graph (or later, a graphing) G, we will always denote E G its set of edges, S G and D G its support and dialect, t G and s G its target and source maps, and ω G its weight map. The notion of thick graphs corresponds to considering graphs with a set of states -called a dialect. A graph G with dialect D G is nothing more than a graph whose set of vertices is of the form

V G = S G × D G -the set S G is called its support.
The set D G then acts as a set of states when considering two graphs in interaction through the notion of execution. In interaction graphs the execution of programs -or equivalently the cut-elimination procedure in logic -is represented as the computation of a graph of (alternating) paths. If G and H are two graphs with dialects D G and D H respectively, an alternating path between G and H is a finite sequence of edges e 0 e 1 . . . e k and a sequence of triples (s i , g i , h i ) k+1 i=0 such that:

(Alternation) e i ∈ E G if and only if e i+1 ∈ E H ; (States) if e i ∈ E G then s G (e i ) = (s i , g i ), t G (e i ) = (s i+1 , g i+1
) and h i = h i+1 ; For two thick graphs G, H, the shared vertices represent a cut; the result of the elimination of this cut is called the execution of G and H. It is defined as the thick graph G :: H, of dialect D G × D H , whose edges are exactly the alternating paths between G and H whose source and target lie outside of the cut. This is reminiscent of game semantics' composition and hiding: composition corresponds here to the computation of all alternating paths, while hiding corresponds to the restriction to those paths starting and ending outside the cut. Now, thick and sliced graphs are simply finite formal weighted sums of graphs i∈I G α G i G i where the coefficients α G i are real numbers and the graphs G i all share the same sets of vertices. This notion is crucial for treating additive connectives [START_REF] Seiller | Interaction graphs: Additives[END_REF]. The notion of execution is then extended "by linearity" (although the sums are not linear combinations), letting:

i∈I G α G i G i :: i∈I H α H i H i = (i,j)∈I G ×I H α G i α H j G i :: H j 2.

Continuous Dialects

Graphings are in some sense geometric realisations of graphs on a measured space X. Specifically, a graphing G is defined as a graph such that for each edge e ∈ E G , s G (e) and t G (e) are measurable subsets of X, and there is a measurable map φ G e : s G (e) → t G (e) which realises e. As for graphs, one can define thick and sliced graphings by first defining graphings with a dialect -thick graphings, then consider formal weighted sums of those. It is natural, while working with graphings, to consider (finite) discrete probability spaces as dialects; a thick graphing of dialect D is then simply a graphing over the measured space X × D.

The purpose of the work is to extend this definition to allow for continuous dialects, i.e. continuous dialects, instead of discrete ones. We will show how to define in this setting the interpretation of second order linear logic without hindering the "quantitative" features of the interaction graphs construction. This however comes with a small drawback in the form of a small complexification of the framework, which we now explain.

We did not dwell on this point earlier, but thick graphs (graphs with dialects) are considered up to renaming of their dialect; a thick graph G which is a dialect-renaming of a thick graph F is called a variant of F . To define correctly this notion of variant one needs to consider bijections between the dialects. However, when considering graphings and replacing the dialects with possibly continuous probability spaces, we face a problem when considering the two probability spaces k = {1, . . . , k} with discrete measure and [0, 1] with Lebesgue measure. Indeed, any thick graphing G with dialect k has a variant H with dialect [0, 1]: each element i ∈ k is represented by the interval I i = [i/(k + 1), (i + 1)/(k + 1)], and an edge of source (v, i) and target (v , j) realised by a map φ : (v, i) → (v , j) in G is realised in H by φ 1 × T i,j where T i,j is the translation x → x + (j -i)/(k + 1) and φ 1 is the map v → v underlying4 φ. This cannot be formalised through a notion of bijection (here it would amount to consider Borel automorphisms) between k and [0, 1]. To avoid these troubles, we will therefore consider all our dialects to be isomorphic to [0, 1] with its Lebesgue measure; as explained above, we do not lose any graphings in the process since a graphing with discrete dialect always has a variant with [0, 1] as dialect.

The second change from earlier work [START_REF] Seiller | Interaction graphs: Graphings[END_REF] is that we need to consider an extension of the notion of microcosm. A microcosm m is a monoid of measurable maps X → X used to consider "restrictions" of the model to m-graphings: graphings whose realizers can be extended to an element of m. The original notion of microcosm did not need to incorporate the dialect since the latter was discrete, and therefore the measurable maps realizing an edge in a thick graphing were nothing more than measurable maps from X to X. Now that we allow for continuous dialects, one can consider realisers of edges that do not simply arise from5 a map X → X. The following definition therefore adapts (in fact extends) the previously considered notion of microcosm to incorporate this change.

Definition 1 (Microcosm). Let X be a measured space. A microcosm is a monoid (for the composition of functions) of measurable maps6 X × [0, 1] → X × [0, 1].

Graphings and Exponential-Free Linear Logic

This section is meant to recall the main results of previous work [START_REF] Seiller | Interaction graphs: Graphings[END_REF], to which we refer the reader for a complete picture. We first define weighted (thick) graphings, a generalization of the homonymous notion considered by Adams [START_REF] Adams | Trees and amenable equivalence relations[END_REF] and later by Gaboriau [START_REF] Gaboriau | Coût des relations d'équivalence et des groupes[END_REF].

Definition 2 (Graphing). Let m be a microcosm, Ω a monoid of weights, V G a measurable subset of X and D G a probability space isomorphic to [0, 1]. A thick Ω-weighted m-graphing G of carrier V G and dialect D G is given by: a set of edges E G ; for each edge e ∈ E G , source s G (e) and target t G (e) measurable subsets of

V G × D G ; for each edge e ∈ E G , a realiser φ G e ∈ m such that φ G e (s G (e)) = t G (e); for each edge e ∈ E G , a weight ω G (e).
A graphing G is dialect-free if it does not make use of its dialect, i.e. if for all edge e, φ G e = φG e × Id D G , with φG e : X → X. Morally, graphings are sort of graphs which offer richer combinatorics since two vertices might have a non-trivial intersection without being equal. In particular, when considering paths, one should be careful about the domains: a path in a graphing G is a sequence of edges π = e 1 , e 2 , . . . , e k in E G such that s G (e i+1 ) ∩ t G (e i ) is of strictly positive measure 7 . This path is then naturally realised as the composite

Notations

φ G π = φ G e k • • • • • φ G e1
, and is considered with its maximal domain s G (π), i.e. the set of all

x such that φ G ei • • • • • φ G e1 (x) ∈ s G (e i+1 ), and its codomain t G (π) = φ G π (s G (π)). The weight of π is obviously defined as ω G (π) = ω G (e k )ω G (e k-1
) . . . ω G (e 1 ) using the composition law of Ω.

We can then define alternating path between thick graphings graphings as in the case of graphs. From this, one defines the execution between thick graphings, the semantic counterpart to the cut-elimination procedure. We here define execution only in the specific case when the support of one graphing is included in the support of the other: this represents an application, i.e. a modus ponens; the general case of the cut can be consulted in our earlier paper [START_REF] Seiller | Interaction graphs: Graphings[END_REF] or deduced from this specific case 8 . Definition 4 (Execution). Let F and G be graphings with V G = V F V . Their execution F :: G is the graphing of all alternating paths between F and G whose domain and codomain are restricted to V . Example 5. We consider two one-edge graphings (without dialects or weights to be concise) G and H illustrated on the left-hand side of Figure 1. The edge of G has source the segment [0, 2], target the segment [START_REF] Dal | Realizability models and implicit complexity[END_REF][START_REF] Danos | La Logique Linéaire Appliquée à l'Étude de Divers Processus de Normalisation (principalement du λ-calcul)[END_REF] and is realised by the map x → 6 -x. The edge of H has source the segment [START_REF] Dal | Quantitative game semantics for linear logic[END_REF][START_REF] Danos | La Logique Linéaire Appliquée à l'Étude de Divers Processus de Normalisation (principalement du λ-calcul)[END_REF], target the segment [START_REF] Danos | Linear logic & elementary time[END_REF][START_REF] Ehrhard | Finiteness spaces[END_REF] and is realised by the map x → x + 3. The cut is represented by the segment [START_REF] Dal | Quantitative game semantics for linear logic[END_REF][START_REF] Danos | La Logique Linéaire Appliquée à l'Étude de Divers Processus de Normalisation (principalement du λ-calcul)[END_REF]. The execution of G and H, illustrated on the right-hand side of Figure 1, is composed of two paths: the restriction of the edge of G to the segment [START_REF] Abramsky | Games and full completeness for multiplicative linear logic[END_REF][START_REF] Adams | Trees and amenable equivalence relations[END_REF], and the composition of the two edges. 7 This is a crude approximation, since a path of length 3 might satisfy these conditions but such that s G (e3) ∩ φe 2 • φe 1 (s G (e1)) is of null measure. The right conditions are defined in our earlier work introducing the general framework of interaction graphs and graphings [START_REF] Seiller | Interaction graphs: Graphings[END_REF]. 8 Noticing that (A

B) ⊗ (B C) (B B) (A C) (using the semi-distributivity law twice), one can rewrite a cut between f ∈ A B and g ∈ B C as an application of f ⊗ g ∈ (B B) (A C) with the axiom a ∈ B B. [0, 2] [4, 6] x → 6 -x [5, 6] [8, 9] x → x + 3 [0, 1][1, 2] [4, 5] x → 6 -x x → 9 -x [8, 9]
Figure 1 Example of an execution between two graphings.

Based on the notion of alternating cycle -defined easily from the notion of alternating paths, one defines a measurement •, • m of couples of graphings and taking values in R+ . This measurement is parametrized 9 by the choice of a measurable map m : Ω → R+ . It is a quite involved work to define and study, so we refer the interested reader to our previous paper [START_REF] Seiller | Interaction graphs: Graphings[END_REF]. In the specific case of graphs -which are graphings over a discrete space -this measurement is simply equals the sum, over the set of alternating cycles π, of m(ω(π)) where m is any map Ω → R+ . This notion of measurement is extended to couples (a, A) where a is a real number (potentially infinite) and A a graphing; the consideration of this additional real number -the wager -finds its reasons in technical details that are explained in previous papers [START_REF] Seiller | Interaction graphs: Multiplicatives[END_REF][START_REF] Seiller | Interaction graphs: Additives[END_REF]. The resulting couples, called projects, are used to interpret proofs.

Definition 6 (Project).

A project is a couple a = (a, A) where a ∈ R+ and A is a formal weighted sum of graphings

A = i∈I A α A i A i .
From the measurement, one defines a notion of orthogonality that accounts for linear negation. This orthogonality relation is used to define conducts, specific sets of projects which will interpret formulas. Finally, one can define a category whose objects are conducts and morphisms are projects and which is shown to interpret multiplicative-additive linear logic. We do not detail this construction since it is quite involved. However, let us point out that the resulting model is completely non-degenerate (none of the connectives or constants are identified) and do not satisfy the mix and weakening rules [START_REF] Seiller | Interaction graphs: Additives[END_REF].

Theorem 8 (Seiller [32]). Let X be a measured space, m a microcosm, Ω a monoid of weights. For all measurable map m : Ω → R+ , conducts and projects built from Ω-weighted m-graphings, with the orthogonality defined from the measurement defined from m, form a model of Multiplicative-Additive Linear Logic. 9 We won't dwell on this choice of parameter in this paper, in order to avoid unnecessary complications.

Although we here mention it for the sake of exactness, it will not play any specific role here. A fine analysis of the models would imply a consideration of specific values of m, but none of the results obtained in this paper depend on the choice of m.

The model

To describe the model, we will pick a measured space X together with a microcosm ll ρ which are defined below. The construction we describe will not depend on the choice of Ω and m : Ω → R 0 , and therefore describes a family of quantitative models of second order linear logic.

Although the underlying space used here differs from our earlier work on exponentials [START_REF] Seiller | Interaction graphs: Exponentials[END_REF], both are equivalent up to a Borel automorphism. The presentation was chose to work with here has the advantage of showing more explicitely the dynamics at work, while gaining intuitions from standard work on exponentials. Indeed, we chose to work explicitely with the Hilbert cube [0, 1] N , underlying an intuitive correspondence between boxes used to treat exponentials in proof nets and the copies of [0, 1].

Definition 9 (The space). We define the measured space X = R × [0, 1] N , product of the real line with the Hilbert cube, endowed with its usual Borel algebra and Lebesgue measure.

Notations. We will write elements of X as couples (a, s), where a ∈ R and s is a sequence of elements in [0, 1]. We will sometimes write sequences as s • s , i.e. as the concatenation of a finite sequence s = (x 1 , . . . , x k ) and a sequence s ; when s contains only one element x we will identify x and (x). When considering elements of the space X × [0, 1], we will use a natural extension of this notation, and write them (a, s, e), with (a, s) ∈ X and e ∈ [0, 1].

We now define the microcosm, denoted ll ρ , that will be used to interpret proofs. We could very well have worked with the biggest microcosm possible (the so-called macrocosm) or any microcosm containing ll ρ . It is however more interesting to point out exactly the principles that are necessary to interpret second-order linear logic.

Definition 10 (The microcosm). Let ρ be a measure-preserving bijection [0, 1]

2 → [0, 1].

We define the microcosm ll ρ as the monoid of measurable 10 maps X → X generated by: affine transformations over the real line: A α λ : (x, s) → (αx + λ, s); (finitely supported) permutations over the Hilbert cube: P σ : (x, s) → (x, σ(s)); the maps D ρ : (a, (x, y) • s) → (a, ρ(x, y) • s) and its inverse D -1 ρ . the exchange xch : X × [0, 1] → X × [0, 1] defined as (a, x • s, e) → (a, e • s, x) Notice that the exchange xch is an example of map that could not arise from a microcosm of maps from X to itself. This added principle is crucial for the definition of both dereliction and digging. Intuititvely, the microcosm of Definition 10 without the exchange map allows for Elementary Linear Logic 11 , in the same spirit as our previous work on exponentials [START_REF] Seiller | Interaction graphs: Exponentials[END_REF]; the added principle -the exchange -adds both dereliction and digging simultaneously.

Remark. One actually consider thick and sliced graphings up to a larger equivalence than that of variants. Indeed, we consider that the sliced and thick graphing 10 We notice that those are all Borel automorphisms, thus in particular Borel-preserving and non-singular. 11 To be more exact, the microcosm allowing for a model of ELL is the microcosm llρ without the exchange but with the maps Dσ which permute the family of intervals {[(i-1)/k, i/k]} k i=1 in the dialect along a permutation σ of {1, . . . , k}. Without these maps, one cannot define contraction as one cannot represent slice-changing edges [START_REF] Seiller | Interaction graphs: Exponentials[END_REF]; it is not necessary to have all of them, though, as for instance all such Dσ for permutations σ over sets {1, . . . , 2 p } are enough. Notice that these maps -in the case k = 2 p -are elements of llρ, defined as

k i=1 1 k A i
Dσ = xch•ρ (p) •Pσ •ρ -1 (p)
•xch, where ρ (p) is recursively defined by:

ρ (0) = ρ ρ (p) = ρ (p-1) • ( 2 p-1 i=1 ρ)
is equivalent to the universal 12 graphing H whose restriction to the part of the dialect

[(i -1)/k, i/k] is equal to A i , modulo the affine transformation [(i -1)/k, i/k] → [0, 1], x → (x × k) -i + 1.
By Theorem 8, we know that for any choices of Ω and m, the induced model interprets MALL. We will thus concentrate on exponential connectives here and refer the interested reader to earlier papers for the definition of MALL connectives.

4

The Exponentials

We now define the perennisation; it is not defined on all projects, but on the subset of socalled balanced projects. These are in particular projects whose dialect is equal to [0, 1] or, by extension, whose graphings are "balanced" sums:

k i=1 α i A i such that α i = 1
/k for all i. This is not a problem since projects interpreting proofs will will all satisfy these conditions. Exponentials are then quite easy to define on balanced projects: from A we construct !A by "pushing" the dialect at the first position in the sequence [0, 1] N . For technical reasons, we also need to create a fresh new copy of [0, 1] for promotion.

Definition 11. A project a = (a, A) is balanced if a = 0 and the dialect of A is [0, 1]
. If E is a set of projects, we write bal(E) the subset of balanced projects in E.

In order to define exponentials, we will need the following map:

B : X × [0, 1] → X (a, s, d) → (a, d • s)
This map B will be used to encode the dialect of A in the support of the banged project !A. This way, the resulting project !A will contain the exact same information as A, but will be dialect-free. Though it might seem a transparent and useless operation, the fact that the dialect is now part of the support makes the projects !A and A behave quite differently when put into interaction with other projects. Intuitively, while the dialect is something private -e.g. states -the support is not, and some projects might interact with !A non-uniformly w.r.t. the former dialect of A.

Example 12. We consider two graphings, say G and H, both though of 13 as graphings with dialects {1, 2}. Now, suppose that G and H are of type A and A B respectively. Their execution F :: G is then of type B, and its dialect should be thought of as {1, 2} × {1, 2}. We can also consider !G and !H, which are of respective types !A and !(A B), and their execution !G :: !H. Let us explain why the latter cannot be of type !B. Figure 2 illustrates this situation with examples of graphings G, !G, H, !H, as well as lists of the edges (alternating paths) of G :: H and !G :: !H.

The execution of !G and !H actually produces the graphing defined as follows: compute the execution of G and H as if they did not have any dialect, and then take the perennisation of the result. In other words, the only alternating paths computed between G and H are those where the states of G and H are equal: this creates new paths (pictured in red path in Figure 2), this deletes paths (the blue paths), and leaves some of them "unchanged". As a consequence, we cannot prove that !G :: !H is of type !B since the only graphing we know for sure to belong to this type is !(G :: H). Definition 13 (Perennisation). Let a = (0, A) be a balanced project. We define its perennisation !a = (0, !A) by considering the dialect-free graphing !A = B 2 (A × Id [0,1] ).

A1 A2 B1 B2 g 1 g 2 g 3 g 4 (a) Graphing G B1 B2 C1 C2 h 1 h 2 h 3 h 4 h 5 (b) Graphing H g 1 h 2 g 1 h 4 h 1 g 4 h 2 g 3 h 1 g 2 h 3 g 4 h 4 h 3 g 2 (c) Edges of F :: G A1 A2 B1 B2 !g 1 !g 2 !g 3 !g 4 (d) Graphing !G B1 B2 C1 C2 !h 1 !h 2 !h 3 !h 4 !h 5 (e) Graphing !H !h 1 !g 4 !h 2 !g 1 !h 4 !g 1 !h 5 !g 4 !h 2 !g 3 !h 3 !g 2 (f) Edges of !F :: !G

Definition 14 (Exponentials).

Let A be a conduct. We define the perennial conduct !A as the bi-orthogonal closure of the set

A = {!a | a ∈ bal(A)}

A Model of Full Linear Logic

To ensure that we have a sound interpretation of exponential connectives, we need to show that the following principles can be implemented:

functorial promotion (!A ⊗ !(A B)) !B; dereliction !A A; digging !A !!A.

The principle of contraction !A

!A ⊗ !A does not appear in this list as it holds for every possible definition of perennisation 14 . Let us notice moreover that the principle of functorial promotion was already obtained in our earlier work on exponentials [START_REF] Seiller | Interaction graphs: Exponentials[END_REF]. We will however use here a less involved method for defining exponentials and implementing functorial promotion. The principles at work are the same as in our earlier work, but this new implementation -inspired from recent work on complexity [START_REF] Seiller | Towards a Complexity-through-Realizability theory[END_REF] -offers a clearer picture.

The change of perspective illustrated in Example 12 is at the heart of the question of implementing functorial promotion. We want to "simulate" the disjointness of dialects. This is done in two steps: first make the encodings (in !G and !H) of the dialects of G and H disjoint, by linking !G and !H through the permutation exchanging the two first copies of [0, 1]. This corresponds to encoding the dialect of one of the two graphings on the second copy of [0, 1] instead of the first. Then we compute the result of this execution, obtaining a graphing which is almost !(G :: H) except for the fact that his dialect is encoded on the two first copies of [0, 1] and not only on the first. We then use a specific graphing that will use ρ : [0, 1] 2 → [0, 1] to encode this dialect on the first copy only.

Theorem 15. Functorial Promotion holds.

Proof (Sketch). The proof is much simpler in this setting than in our previous work on exponentials [START_REF] Seiller | Interaction graphs: Exponentials[END_REF]. The principle is however quite the same: we use a first map to ensure the disjointness of the two "public dialects", and then we use a second map that will merge both copies. I.e. we define the maps:

twist : (λ, (x, ρ(y, z)) • s) → (λ, (y, ρ(x, z)) • s) merge : (λ, (x, ρ(y, z)) • s) → (λ, (ρ(x, y), z) • s)
To prove the result, we exhibit a project prom and show that prom ∈ !A ⊗ !(A B) !B. For this, we show that for all !a = (0, !A) ∈ !A and !f = (0, !F ) ∈ !(A B), we have prom :: !a :: !f = (0, merge(!A :: twist(!F ))

Finally, one easily checks that merge(!A :: twist(!F )) is equal to !(F :: A).

Both digging and dereliction will work based on the simple idea that a continuous dialect [0, 1] can be exchanged with a copy of [0, 1] appearing in the Hilbert cube. This is exactly the computational principle encapsulated in the exchange map xch. This implies that the potential infinite of (finite) dialects -i.e. the fact that a dialect can be any finite set, without bounds on its cardinality -can be managed within the projects themselves, something that could not be done in earlier constructions.

Theorem 16. Digging holds.

Proof (Sketch). As for the proof of Theorem 15, we exhibit an element dig ∈ !A !!A. We show that, for all !a = (0, !A) in !A, one can compute dig :: !a = (0, push(!A)), where: push : (λ, (x, ρ(y, ρ(z, w))) • s, e) → (λ; (e, z, x, y) • s, w)

It is clear that push(!A) is equal to !!A, since the dialect of !A (although !A is dialect-free, not all elements of !A are, and therefore this is important) is encoded in the first copy of [0, 1], while the second copy remains unused (this is because the second copy of [0, 1] in !A is unused 15 ). The dereliction consists in "reconstructing" a dialect from a banged project. This can be performed using the same kind of tricks, i.e. using a continuous dialect.

Theorem 17. Dereliction holds.

Proof (Sketch). Again, we exhibit an element der ∈ !A A. For this, we show that for all !a ∈ !A, one can compute der :: !a = (0, raise(!A)) where raise : (λ, (x, y) • s, e) → (λ, s, ρ(x, ρ(y, e)))

Again, one easily checks that raise(!A) is equal to A. Notice that the maps used to interpret dereliction and digging are not the only ones that satisfy the right properties, e.g. if one replaces raise by the map raise (2) (λ, (x, y) • s, e) → (λ, s, ρ(ρ(x, y), e)), we still have raise (2) . The exact expressions are however important when to ensure that the execution soundly represents cut-elimination.

Interpretation of proofs

We first recall the notion of winning projects [START_REF] Seiller | Interaction graphs: Exponentials[END_REF]. Winning projects are the equivalent of game semantics' winning strategies or classical realizability's proof-like terms. In particular, all interpretations of proofs will be winning projects.

Definition 18.

A project a = (a, A) is winning if it is balanced and if A is a disjoint union of transpositions, i.e. each edge e in A has a reverse edge e * with φ A e * = (φ A e ) -1 and the sources of edges are pairwise disjoint.

We now recall the basics of the proof system for which we define the interpretation of proofs. We are working with three different kinds of formulas, positive, negative and neutral. The technical reasons behind this are explained in our work on ELL [START_REF] Seiller | Interaction graphs: Exponentials[END_REF]. Intuitively, neutral formulas correspond to the fragment of linear logic which does not allow for structural rules, negative formulas are those created from a perennisation while positive formulas are duals of negative formulas. They are defined inductively through the following grammar (neutral formulas are denoted by B which stands for behavior [START_REF] Seiller | Interaction graphs: Exponentials[END_REF]): Definition 20 (The System LL pol ). A proof in the system LL pol is a derivation tree constructed from the derivation rules of ELL pol [START_REF] Seiller | Interaction graphs: Exponentials[END_REF], which are nothing more than polarised variants of elementary linear logic sequent calculus rules -presented with functorial promotion, extended with the rules in Figure 3.

B := X | X ‹ | 0 | T | B ⊗ B | B `B | B ⊕ B | B & B | ∀X B | ∃X B | B ⊗ N | B `P N := 1 | !B | !N | N ⊗ N | N & N | N ⊕ N |
One can then extend the inductive interpretation of proofs defined for ELL pol in earlier work [START_REF] Seiller | Interaction graphs: Exponentials[END_REF] by interpreting the additional rules as follows: the interpretation π of a proof π obtained from a proof π by using a dereliction rule (resp. a digging rule) is defined as the execution of π with the project der (resp. dig).

Theorem 21. For every proof π of a sequent ∆ Γ; Θ in LL pol , the interpretation π is a winning project in ∆ Γ; Θ Proof. The proof is uninteresting and follows exactly the proof of the same result for the restricted system ELL pol . The additional cases of dereliction and digging rules are completely transparent since the projects exhibited in the proofs of Theorem 16 and 17 are clearly winning projects.

Notice that it is an open question whether the exponential isomorphism between !(A&B) and !A ⊗ !B did hold in the ELL model 16 . In the model we just described, however, this isomorphism holds; one just has to write down the usual derivation which can be interpreted soundly in the model:

A, A ‹ ; der !A A; weak !A, !B A; B, B ‹ ; der !B B; weak !A, !B B; & !A, !B ; A & B ! pol !!A, !!B ; !(A & B) dig !A, !!B ; !(A & B) dig !A, !B ; !(A & B) ; (!A ⊗ !B) !(A & B)
This implies not only that that two conducts !A ⊗ !B and !(A & B) are isomorphic, but that they are equal. Indeed, the inclusion !(A & B) ⊆ !A ⊗ !B can be proved as in our earlier paper [START_REF] Seiller | Interaction graphs: Exponentials[END_REF]. Moreover, the interpretation π of the above derivation can be shown to satisfy What about cut-elimination? It is known that GoI does not represent cut-elimination exactly, i.e. it is not always the case that if π is the normal form of π, then π = Ex( π ). It was shown that cut-elimination for MLL is soundly represented by execution [START_REF] Seiller | Interaction graphs: Multiplicatives[END_REF], but there is a mismatch even in the exponential-free fragment because of additive cuts. This issue is discussed in details in previous work [START_REF] Seiller | Interaction graphs: Additives[END_REF], where we solve this problem by considering a notion of observational equivalence ∼ =. Indeed, we showed that, even if π = Ex( π ) in presence of an additive cut, π and Ex( π ) are observationally equivalent.

Theorem 23 (Seiller [30]). If π is obtained from π by applying a step of cut-elimination (&/⊕) then π ∼ = π .

We now consider the exponential connectives. We will consider a promotion rule cut against the following rules: dereliction, digging, and contraction. We consider for this a proof π of A ‹ , B, or a proof π of A ; B as both promotion rules are treated similarly, and its interpretation π ∈ A B. Applying a promotion rule (polarised or not) to π yields a proof ρ whose interpretation is ρ = ! π :: prom. Then, given a proof π to which we apply one of the three structural rules above to obtain a proof ρ , we consider the interpretations of the proof ν obtained by a cut between π and ρ, and the interpretation of the proof ν obtained by applying a step of the cut-elimination procedure on ν. It turns out that those are equal, i.e. ν = ν . Theorem 24. If π is obtained from π by applying a step of cut-elimination among (promotion/dereliction), (promotion/digging) or (promotion/contraction), then π = π . So execution computes these elimination steps on the nose. What about the last step, namely (promotion/weakening)? In that case, we are faced a problem similar to what happens for additive cuts in MALL. As execution is a completely local procedure, it cannot erase a whole proof at once. Thus, this elimination step is not soundly represented by the execution. However, one can show the following weaker result. Theorem 25. If π is obtained from π by applying a step of cut-elimination among (promotion/weakening), then π ∼ = π .

However, these results are not enough to entail that cut-elimination is soundly represented by execution up to observational equivalence. In particular, one would need to show that perennisation and observational equivalence interact properly, i.e. one would hope for a result stating that, given two balanced projects a and b, a ∼ = b if and only if !a ∼ = !b. One can prove that a ∼ = b implies !a ∼ = !b, however the converse implication is still an open question.

Conclusion

Girard's so-called "GoI3" model [START_REF] Girard | Geometry of interaction III: Accommodating the additives[END_REF] already provided an interpretation of full linear logic. However, we managed to do so in a quantitative-flavoured framework. Beyond the results presented here, the adaptation of the interaction graphs framework to deal with continuous dialects results in a more mature and complete construction. Indeed, the possibly to manage the maps at the level of the dialect through the microcosm opens new possibilities in terms of computational complexity. Indeed, while the weight monoid and the measurement of weights seem to be related to different computational paradigms and can be used, for instance, for representing probabilistic computation [START_REF] Seiller | Towards a Complexity-through-Realizability theory[END_REF], the microcosm can be used to restrict the computational principles allowed in the model and characterise in this way various complexity classes [START_REF] Seiller | Towards a Complexity-through-Realizability theory[END_REF][START_REF] Seiller | Interaction graphs and complexity I[END_REF]. All the characterisations obtained considered variants of exponentials satisfying at least the contraction principle. In the more general construction explained here, we are now able to consider models of exponentials that do not satisfy this principle. In this line of work, it would be interesting to understand if one can adapt Mazza and Terui's work on parsimonious lambda-calculus [START_REF] Mazza | Non-uniform polytime computation in the infinitary affine lambdacalculus[END_REF][START_REF] Mazza | Parsimonious types and non-uniform computation[END_REF][START_REF] Mazza | Simple affine types and logspace[END_REF], and obtain an interaction graph model for it.

  . Let B be a Borel automorphism of X × [0, 1]. We denote B(A) the graphing whose edges are B -1 • φ • B; up to the automorphism between D A and [0, 1]. When B is a Borel automorphism of X, we abusively denote by B(A) the graphing B × Id [0,1] (A). We also denote by A × Id [0,1] the graphing of dialect D A × [0, 1] whose edges are realised as φ e × Id [0,1] . Definition 3 (Variants). Let F and G be graphings. If there exists a Borel automorphism φ : [0, 1] → [0, 1] such that F = Id X × φ(G), we say that F and G are variants.

Definition 7 (

 7 Orthogonality -Conduct). Two projects a = (a, A) and b = (b, B) of equal supports are orthogonal, denoted a ‹ b, when a, b m = 0, ∞. A conduct of support V is the orthogonal of a set T of projects of support v, i.e. V = T ‹ = {a | ∀b ∈ T, a ‹ b}.

Figure 2

 2 Figure 2 Illustration of Example 12 with graphing seens as graphs.

Figure 3

 3 Figure 3 Additional Rules for Dereliction and Digging

  N `P | ∀X N | ∃X N P := ⊥ | ?B | ?P | P `P | P & P | P ⊕ P | N ⊗ P | ∀X P | ∃X P Definition 19. A sequent ∆ Γ; Θ is such that ∆, Θ contain only negative formulas, Θ containing at most one formula and Γ containing only neutrals.

Theorem 22 .

 22 π ::(!a ⊗ !b) = !(a & b), where a & b is the usual construction of the & rule between a and b, yielding the converse inclusion. For any conducts A and B in the model, !(A & B) = !A ⊗ !B.

Girard interprets proofs as partial isometries acting on a Hilbert space H which, by considering the right basis for H correspond to graphs.

Actually, the most general models are build around the lesser known notion of weighted graphing. However, thinking about graphings as graphs should provide the reader with good intuitions.

As we consider paths in the following, the structure of monoid is essential as it allows to define the weight of a path as the product of the weights of the edges that it is composed of.

Since k is discrete, any measurable map φ : (v, i) → (v, j) is defined from a measurable map φ1 : v → v by φ(x, i) = (φ1(x), j).

As an example, one can consider the exchange map defined below (Theorem 10) and which is needed to interpret both digging and dereliction.

For technical reasons discussed in earlier work[START_REF] Seiller | Interaction graphs: Graphings[END_REF], these should be Borel-preserving and non-singular.C S L ' 1 5

C S L ' 1 5

This is the smallest such graphing, i.e. if H also satisfies this property, then H is included in H .

Recall that we are actually working with "variants" G c and H c whose dialect are [0, 1].C S L ' 1 5

As this is not the case for elements of A, this explains why digging is not a co-dereliction.C S L ' 1 5

This is discussed in our earlier paper[START_REF] Seiller | Interaction graphs: Exponentials[END_REF], but can be understood as follows: in the non-affine sequent calculus for ELL (presented with the functorial promotion rule) one cannot prove the implication (!A ⊗ !B) !(A & B).

This work was partially supported by the ANR 12 JS02 006 01 project COQUAS and the ANR-10-BLAN-0213 Logoi.


Franc ¸ois Stéphanie Jacquemont

Marc Jacquenet
email: jacquene@univ-st-etienne.fr

Sebban
email: sebbanma@univ-st-etienne.fr

Sequence Mining Without Sequences: a New Way for Privacy Preserving

During the last decade, sequential pattern mining has been the core of numerous researches. It is now possible to efficiently discover users' behavior in various domains such as purchases in supermarkets, Web site visits, etc. Nevertheless, classical algorithms do not respect individual's privacy, exploiting personal information (name, IP address, etc.). We provide an original solution to privacy preserving by using a probabilistic automaton instead of the original data. An application in car flow modeling is presented, showing the ability of our algorithm to discover frequent routes without any individual information. A comparison with SPAM is done showing that even if we sample from the automaton, our approach is more efficient.

Introduction

Sequential pattern mining aims at automatically finding subsequences (or patterns) that appear frequently (i.e. more than a support threshold) in a database of sequences. One of the algorithmic difficulties is that each pattern can be made up of non-consecutive elements in the original sequence. Many algorithms have been proposed during the last decade, such as [START_REF] Mannila | Discovery of frequent episodes in event sequences[END_REF][START_REF] Zaki | Sequence mining in categorical domains: incorporating constraints[END_REF][START_REF] Garofalakis | Mining sequential patterns with regular expression constraints[END_REF][START_REF] Pei | Mining sequential patterns with constraints in large databases[END_REF]. There have also been a lot of applications based on such techniques [START_REF] Han | Emerging scientific applications in data mining[END_REF]. One of the first concerned the discovery of customer's behavior in supermarkets [START_REF] Agrawal | Mining sequential patterns[END_REF] in the form of subsequences of purchases. That knowledge may be very valuable for marketing department of the companies. In the domain of manufacturing supervision, sequence mining can be used to discover frequent patterns of alarms, what may help supervisors while searching for defaults in the plant [START_REF] Klemettinen | Interactive exploration of interesting findings in the telecommunication network alarm sequence analyzer[END_REF]. More recently, in the domain of Web Mining [START_REF] Kosala | Web mining research: A survey[END_REF], various systems have been designed for making use of Web site logs in order to model the behavior of Web users [START_REF] Spiliopoulou | Data mining for measuring and improving the success of web sites[END_REF]. Another application, for which we implemented a prototype in this paper, is the discovery of routes frequently used by car drivers in towns.

These numerous applications prove that sequence mining algorithms are useful tools for discovering knowledge in various situations. Nevertheless, in the case we try to discover knowledge from the observation of human behavior, we claim that these algorithms do not preserve individual's privacy. For example, regarding the problem of discovering frequent sequences of Web pages visited throughout time, the input data are, at least, the IP address of the visitors and the Web pages they have browsed. This is a great breach to their privacy and users might want their private information not to be logged on the servers. In the case of frequent routes in towns, to get interesting knowledge, one could install many Web cams in the town and trace the route for each driver. This is obviously a non acceptable breach to the privacy of car drivers.

Privacy preserving data mining is a new subject of research that appeared to be essential for some years. There is a great demand from users, and more generally from the society, that data miners preserve their privacy. As stated by [START_REF] Verykios | State-of-the-art in privacy preserving data mining[END_REF], the main objective in privacy preserving data mining is to develop algorithms for modifying the original data in some way, so that the private data and private knowledge remain private even after the mining process. A huge number of papers have been published during the last five years, for example [START_REF] Agrawal | Privacy-preserving data mining[END_REF][START_REF] Sweeney | k-anonymity: a model for protecting privacy[END_REF][START_REF] Evfimievski | Privacy preserving mining of association rules[END_REF][START_REF] Bayardo | Data privacy through optimal k-anonymization[END_REF]. Considering the discovery of frequent routes traversed by car drivers, to preserve their privacy, we may think about de-identifying images from Web cams such as in [START_REF] Newton | Preserving privacy by de-identifying face images[END_REF], but this is a costly solution. Moreover, installing a Web cam in every street of a town may lead to psychological resistance from people.

In this paper, we propose a costless solution to privacy preserving for problems that may be stated as flow control problems, that is the case of frequent path discovery in Web sites and frequent route discovery in towns. We propose to model this flow of data in the form of a weighted automaton for which we provide a probabilistic solution to discover frequent patterns (potentially with gaps) under constraints, without any information about the original data.

In Web usage mining, the states of this automaton are the pages of the site and transitions the hyperlinks between pages. The weight assigned to each transition corresponds to the number of users who clicked on the corresponding hyperlink and the weight of each state is the number of times users left the web site from the corresponding page. Therefore, for the users, we do not need anymore their IP address and the Web pages they visited, but only counters on each transition and state. [START_REF] Borges | Mining association rules in hypertext databases[END_REF] exploited this idea defining the concept of composite association rule processed from a structured directed graph built from the log files of the Web site. More recently, [START_REF] Borges | Generating dynamic higher-order markov models in web usage mining[END_REF] show how to use higher-level Markov models in order to process a weighted automaton to discover frequent paths of Web site users from log files. Nevertheless, these works are more restricted than our approach in the sense that first, they need the Web log files and second, they aim at discovering sequential patterns made up of consecutive Web pages while we are able to discover non consecutive ones.

The problem of discovering frequent routes in a town can also be represented in the form of an automaton. Considering a map of a part of a town, the non-initial and nonfinal states model the crossroads. The initial and final states respectively represent the entry and exit gates in the map. The transitions model the streets. The weights are obtained by using counters on transitions and on the final states (the other states having a null counter). For each car, we do not need anymore its license and the streets it traverses. We will show that it is possible to discover frequent routes just using the automaton. It is essential to be able to discover frequent non consecutive patterns for example to set up some combined advertisements campaign, for improving traffic, etc.

The rest of this paper is organized as follows. Section 2 defines the way we replace the database of sequences by a probabilistic automaton. This idea was originally proposed in [START_REF] Hingston | Using finite state automata for sequence mining[END_REF] and exploited in [START_REF] Jacquenet | Mining decision rules from deterministic finite automata[END_REF]. We extend it, in Section 3, by using such an automaton-based structure to propose a constrained sequence mining algorithm in the context of privacy preserving. Section 4 describes a traffic simulator able to discover frequent routes in towns. Beside the description of the system, we experimentally show that our algorithm is more efficient than sampling sequences from the automaton and then using a classical sequence mining algorithm.

2 Using a PDFA instead of Sequences

Definitions and Notations

Achieving a sequence mining task without the original sequences requires the use of a suited structure able to ex-press the same knowledge as the one underlying in the sequences themselves. We propose here to use a probabilistic deterministic finite state automaton (PDFA). Definition 1 a PDFA A =< Q, Σ, q, q 0 , π, π F > is a tuple where Q is a finite set of states; Σ is the alphabet; q : Q × Σ → Q is a transition function; q 0 is the initial state; π : Fig. 1 shows a PDFA where Q = {0, 1, 2}, Σ = {a, b}, q 0 = 0, and for instance q(0, a) = 2, π(0, a) = 0.314 and π F (0) = 0.338. In this paper, we assume that we have a weighted automaton of the problem we tackle. We showed in introduction that the "real life" can provide such automata, that is the case of a road traffic. To be a PDFA, we must normalize the counters of the automaton to obtain a probability distribution as follows:

Q × Σ → [0, 1] is a transition function; π F : Q → [0, 1]
π(S, z) = n(S, z) P z ∈Σ∪{#} n(S, z ) , ∀z ∈ Σ ∪ {#}, ∀S ∈ Q (1)
where n(S, z) is the counter of the transition q(S, z), # is a termination symbol, and n(S, #) is the counter of state S (note that π(S, #) = π F (S)).

Estimation of Pattern Probabilities

If we aim at using a PDFA for sequence mining, it must first allow us to correctly estimate the true probability (i.e. in the hidden original sequences) of any pattern. Let us show now that using formulas proposed by Hingston in [START_REF] Hingston | Using finite state automata for sequence mining[END_REF], we can correctly assess the true probability of any pattern. Then, we will generalize them to build an efficient sequence mining algorithm that will allow us not only to do without the original data but also to impose constraints on the extracted patterns.

Let A =< Q, Σ, q, q 0 , π, π F > be a PDFA. To estimate (with p(x)) the unknown (or hidden) proportion p(x) of sequences that contain a letter x, Hingston defines the probability P (S, x) that a path in A starting from state S contains an x. This is ensured either if a path begins with an x (of probability π(S, x)), or with some other symbol z ∈ Σ and is followed by a path starting at the next state (given by q(S, z)) and containing an x. This can be written with the recursive formula:

P (S, x) = π(S, x) + X z =x∈Σ (π(S, z) × P (q(S, z), x)) (2)
that one can rewrite as follows:

P (S, x) = π(S, x) + X T ∈Q 0 @ X z =x,q(S,z)=T π(S, z) 1 A × P (T, x). (3)
If S = q 0 , P (S, x) represents p(x). Computing P (S, x) requires to handle a system of linear equations that can be efficiently solved with matrix products. Let ρ(x) be the matrix of components ρ S,T (x) = z =x,q(S,z)=T π(S, z) describing the probability to use a transition different from x between states S and T . Let P (x) (resp. π(x)) be the vector of values of P (S, x) (resp. π(S, x)), Eq.3 becomes:

P (x) = π(x) + ρ(x)P (x) = (I -ρ(x)) -1 π(x), (4)
where I is the identity matrix. Let us take an example with PDFA of Fig. We deduce that p(a) = P (0, a) = 0.635. Based on the same principle, one can estimate the proportion of sequences that contain a pattern w =< x 1 ...x l > composed of l symbols potentially non consecutive. Let F (S, T, x 1 ) be the probability that a random path starting at state S and ending at state T contains exactly one symbol x 1 . Hingston uses similar reasoning as in P (x) to show that:

F (S, T, x1) = P x j =x 1 (p(S, xj) × F (q(S, xj), T, x1))
+p(S, x1), if q(S, x1) = T and 0 otherwise. [START_REF] Borges | Mining association rules in hypertext databases[END_REF] One can rearrange Eq.5 using a matrix γ(x 1 ) of values γ(S, T, x1) = p(S, x1) if q(S, x 1 ) = T and 0 otherwise. Writing F (x 1 ) for the matrix of values F (S, T, x 1 ), Eq.5 becomes: F (x 1 ) = γ(x 1 ) + ρ(x 1 )F (x 1 ) and as before, we deduce F (x 1 ) = (Iρ(x 1 )) -1 γ(x 1 ).

Returning to our objective, we aim at computing P (S, < x 1 ...x l >), the probability of any pattern starting at state S. Let us focus on the case l = 2, i.e. P (S, < x 1 x 2 >). Note that a sequence containing an x 1 followed later by an x 2 can be divided into one part containing the first x 1 in the sequence, and the following part, which contains an x 2 . We can deduce that:

1 state : [a-f] 1 state : [a-f][a-f] 10 states : [a-f] 10 states : [a-f][a-f] 30 states : [a-f] 30 states : [a-f][a-f]
P (S, < x1x2 >) = X T F (S, T, x1)P (T, x2). (6)
Using a matrix form, P (< x 1 x 2 >) = F (x 1 )P (x 2 ). Generalizing, we get

P (S, < x1...x l >) = F (x1) × ... × F (x l-1 ) × P (x l ). (7)
To assess the efficiency of a PDFA to estimate the true probabilities of the hidden sequences, we implemented these formulas and carried out a series of experiments. We simulated several target distributions, from an alphabet Σ = {a, b, c, d, e, f }, in the form of automata with 1, 10 or 30 states. From each automaton, we sampled sets of sequences of different sizes (from 10 to 6,000), and for each of them, we computed p(< x 1 x 2 >) ∀x 1 , x 2 ∈ Σ ∪ {λ} (where λ is the empty symbol), and compared it with the true probability p(< x 1 x 2 >) observed in the set of sequences. Fig. 2 shows the average difference between the estimated and the true probabilities. We note that in all cases it converges rapidly toward 0. In other words, if the PDFA models a sufficiently large number of hidden sequences, we can claim that it correctly estimates the probability of any pattern, and so we can build a PDFA-based sequence mining algorithm.

In a PDFA-based sequence mining algorithm, the test deciding if a pattern w =< x 1 ...x l > is frequent will not be done using its unknown probability p(w) but its estimate P (q 0 , < x 1 ...x l >). How can we ensure that the decision taken is right or wrong? We provide here a lower bound of the number of sequences, on which the PDFA must be built, to ensure a given level of completeness and correctness. Let us design the following statistical test. Accepting a pattern w as being frequent means that the unknown probability p(w) must be at least equal to a fixed support threshold σ 0 . Since p(w) is unknown, one must formulate a null hypothesis H 0 on its value. Here, we fix H 0 : p(w) = σ 0 . Writing H 0 like that rather than H 0 : p(w) > σ 0 is necessary because the establishment of a null hypothesis requires to fix a specific value on the theoretical parameter. However, we are only interested here in rejecting H 0 (in favor of an alternative hypothesis H a ) in one direction, i.e. the case where p(w) is in fact smaller than σ 0 . So, the main feature of the test is its alternative hypothesis H a : p(w) < σ 0 .

When a statistical test is carried out, there are two kinds of possible errors: First, a true null hypothesis can be incorrectly rejected and second, a false null hypothesis can fail to be rejected. The former error is called a Type I error (usually designated by α) and the latter error is called a Type II error (usually called β). α corresponds to the risk to reject a true frequent pattern, that statistically defines the non completeness of the algorithm. More formally, α = P (p(w) < k|H 0 true). When the number of sequences is higher than 30, it is known that a proportion follows a normal law such that: p(w) ≈ N (p(w), p(w)(1-p(w)) N ) (N will be estimated by N in the following of the paper). α can be rewritten as

α = P ( p(w) -σ0 q σ 0 (1-σ 0 ) N < k -σ0 q σ 0 (1-σ 0 ) N ). (8)
We can easily deduce the bound k which corresponds to the (1α)-percentile z α of the normal law.

k = σ0 -zα r σ0(1 -σ0) N . (9)
As defined above, β corresponds to the risk to accept a false frequent pattern, that statistically defines the non correctness of the algorithm. Since H a : p(w) < σ 0 is true here, we have to fix a given value for p(w) satisfying the constraint p(w) < σ 0 . Let σ a < σ 0 be this value. More formally, β = P (p(w) > k|H a true). As previously done for α,

β = P ( p(w) -σa q σa(1-σa) N > k -σa q σa(1-σa) N
).

We can finally deduce that

k = σa -z β r σa(1 -σa) N . (11)
Theorem 1 To ensure a completeness of (100-α)% and a correctness of (100-β)% according to a given support threshold σ 0 , the lower bound on the number of sequences N LB on which the PDFA must be built is equal, ∀σ a ∈ [0, 1]|σ a < σ 0 , to

N LB = [ z β σ a (1 -σ a ) + z α σ 0 (1 -σ 0 ) σ 0 -σ a ] 2 ,
Proof 1 The proof is straightforward using Eq.9 and 11. Actually, we can deduce that

σ0 -zα r σ0(1 -σ0) N = σa -z β r σa(1 -σa) N .
Extracting N from this equation, we obtain the lower bound.

Constraint-based Sequence Mining

The use of constraints is one of the current trend in sequence mining. Length and width restrictions, minimum or maximum gap between elements, time window of occurrence, or regular expressions [START_REF] Zaki | Sequence mining in categorical domains: incorporating constraints[END_REF][START_REF] Garofalakis | Mining sequential patterns with regular expression constraints[END_REF][START_REF] Pei | Mining sequential patterns with constraints in large databases[END_REF] are used to reduce the number of frequent patterns. Since we do not have the original sequences, we propose to use the information provided by the PDFA to constrain the extracted patterns.

Relevance of the Patterns

The aim is here to use the values P (q 0 , < x 1 ...x l >) to assess the statistical relevance of a frequent pattern. Roughly speaking, we mean that a frequent pattern does not always express a significant information. Since tuning the support threshold is a tricky task, we propose to constrain, using two statistical tests, a sequence to be not only frequent but also statistically relevant.

Proportion Constraint. The first test verifies an absolute condition: a pattern w =< x 1 ...x l > must cover a significant part of the probability density of all hidden sequences. To ensure this constraint, we apply a proportion test (called PROP TEST) aiming at verifying if P (q 0 , < x 1 ...x l >) (that we will call p(w)) is high enough. To do this, we test the null hypothesis H 0 : p(w) = 0, against the alternative one H a : p(w) > 0 (where p(w) is the unknown probability). If the number of sequences N is large enough 1 , p(w) asymptotically follows the normal law. Let us determine the threshold k which defines the bound of rejection of H 0 , and which corresponds to the (1α)-percentile U α of the distribution of p(w) under H 0 . We can show that

P (p(w) > k) = α iff k = U α p(w)(1-p(w)) N
. We get the decision rule: if p(w) > k, the proportion constraint on w is satisfied.

Estimation of N.

To assess the unknown value N , we are using the PDFA and computing an estimate N . Let µ be the unknown average size of the hidden sequences. The estimate of N is N = n μ , where n is the number of letters used in the sequences and μ is the estimate of µ. In fact, n is computable with the formulae n = S∈Q z∈Σ n(S, z), using n(S, z) as defined in Section 2.1. It remains to compute μ, such that:

μ = ∞ δ=0 δ × P (q 0 , size = δ) ( 12
)
where P (q 0 , size = δ) is the probability of a hidden sequence to have δ letters. Let τ S,T = z,q(S,z)=T π(S, z) be the probability to use one transition between states S and T . We can establish that:

P (S, size = δ) = T ∈Q τ S,T × P (T, size = δ -1). ( 13
)
This is a geometric series of common ratio τ and first term P (S, size = 0) = π F (S). Using P (q 0 , size = δ) and Eq.12 we deduce that:

N = P S∈Q P z∈Σ n(S, z) P ∞ δ=0 δ × P (q0, size = δ) . ( 14
)
We carried out experiments to show that Eq.14 provides a correct estimate of N . We sampled several sets of sequences (of size N from 100 to 6,000) from the PDFA of Fig. 1. For each set, we compared N and N . Fig. 3 shows that N provides a good estimation of N , and then can be efficiently used in PROP TEST.

Dependence Constraint. We also propose here to verify a relative condition, i.e. if there exists a statistical dependence between w and the pattern w =< x 1 ...x l-1 >. Roughly speaking, the majority of the sequences that contain w must also satisfy w =< w > . < x l >, where "." is the concatenation function. This dependence can be assessed by analyzing the nature of x l occurring after w . We generate an output vector

--→ V out of dimension |Σ ∪ {#}|. Each com- ponent --→ V out (i)
is the expected number of sequences that have the symbol z i ∈ Σ ∪ {#} which follows the pattern w . It means that --→ V out (i) = P (q 0 , < x 1 ...x l-1 z i >) × N . We arrange --→ V out such that the considered symbol x l is the first component of the vector. Then we test the dependence between --→ V out and an input vector -→ V in for which the first component is the expected number of sequences that contain the pattern w (the other components are null). To do this, we run a Chi-square test (called CHI2 TEST) from -→ V in and --→ V out , building the following statistic χ 2 :

χ 2 = |Σ∪{#}| X i=1 [( -→ Vin(i) -Ψ(i)) 2 + ( --→ Vout(i) -Ψ(i)) 2 ] Ψ(i) ,
where

Ψ(i) = --→ Vin(i)+ --→ Vout(i) 2 . χ 2 follows a Chi-square distribution with 2 × |Σ ∪ {#}| -1 degrees of freedom. It is then possible to test if χ 2 is smaller than X 2×|Σ∪{#}|-1 α
, which is the (1-α)-percentile of the Chi-square law. We get the decision rule:

if χ 2 < X 2×|Σ∪{#}|-1 α
, the dependence constraint is verified. Combining the two constraints, we can define a frequent and relevant pattern. Definition 2 A pattern w =< x 1 ...x l-1 x l > is frequent and relevant iff P (q 0 , w) is higher than a support threshold σ, and the proportion constraint on P (q 0 , w) and the dependence constraint between w and w =< x 1 ...x l-1 > are satisfied.

The ACSM Algorithm

Combining all the concepts we presented so far, we propose a new constraint-based sequence mining algorithm. It aims at discovering from a PDFA all the fre-

Input: A PDFA A = (Q, Σ, q, q0, π,

Car Flow Modeling

Traffic Miner

In order to bring to the fore the interest of our approach, we design a road traffic simulator, called TRAFFICMINER (see Fig. 4). We simulated a road traffic on a map captured from mappy T M 's web site. We implemented a graphical in- one-way and two-way roads as transitions of the PDFA, entry gates, exit gates and crossroads respectively as initial, final and other states. On each street, we put a counter to get the number of cars going through it. When the map is modeled, we can simulate the traffic by generating a random flow of cars. At any moment, we can stop the flow and get a PDFA A =< Q, Σ, q, π, π I , π F > where: Q is the set of crossroads, and enter and exit gates; Σ is the set of street names; q : Q × Σ → Q defines a transition, i.e. a street between two crossroads; π : Q × Σ → [0, 1] associates a probability to each pair (S,z), i.e. the probability to leave the crossroad S taking the street z (as defined in Eq.1); π F : Q → [0, 1] associates to each final state (i.e. the exit gates) a non-null probability π F (S) to leave the map taking the gate S; π I : Q → [0, 1] associates to each initial state (i.e. to entry gates) a non-null probability π I (S). According to Def.1, a PDFA must have only one initial state to be deterministic. In our case, despite the fact that we have several initial states (entry gates), the determinism is not challenged because there does not exist two paths, starting from two initial states, that use the same transition. To simulate the road traffic, a multinomial distribution is applied on the entry gates, and others are used on each crossroad to simulate the routes.

Interest of a Car Flow Modeling

From this PDFA, we can run ACSM to extract patterns that may be very interesting in many domains. First, it may be efficiently used in road traffic regulation. By finding frequent paths taken by the same cars, one could locate places in the map which would deserve some developments (traffic circles, traffic lights, etc.) to make the traffic more fluid. For example, in Fig. 4, we can locate on the right a place where the traffic is very heavy. Second, it could be used to simulate a new traffic organization (modification of street directions, creation of new one-way streets, etc.) to avoid traffic jams. Finally, it could be useful in campaign advertising. Note again that a frequent and relevant pattern w =< x 1 x 2 >, extracted with our model, would express, without any information about the individual trail of the drivers, that the majority of cars taking the street x 1 will probably also take later the (possibly not adjacent) street x 2 . This is the case of the pattern composed of the two black streets at the bottom in Fig. 4. Our system is able to ensure that those who take the first street will also take the second one.

This kind of information could help in many domains. First, an advertising agency could use such techniques to find the best strategic position for billboards: either repeat the same hoarding to increase the effect of the advertisement or put a different one. Moreover, such information could also be useful for determining an optimal traffic regulation or simulating a new traffic organization.

Experimental Results

The main contribution of this paper is to show that one can achieve with a PDFA a constrained sequence mining task while preserving the privacy of the data. The experiments we carried out in Section 2 have proven the ability of the PDFA to succeed without constraints.

Effect of the Constraints.

Let us now evaluate the individual effect of our constraints on the number of extracted patterns. We run then our simulator. Fixing θ = 0, the two charts of Fig. 5 show the effects of the relevance constraints. We tested the influence of PROP TEST without incorporating CHI2 TEST (first chart, fixing α 2 = 100%) and reciprocally (second chart, fixing α 1 = 100%). Of course, we can note that the stronger one of these constraints is, the more the number of patterns decreases. Moreover, we can note that the more σ increases, the more the relevance constraints become obviously useless.

Experimental Comparison with SPAM. Since we do not use the original data, a comparison with other sequence mining algorithms seems more difficult. To overcome this drawback, we sampled sequences from the PDFA and tried to find back the same patterns with SPAM2 [START_REF] Ayres | Sequential pattern mining using a bitmap representation[END_REF]. The experimental setup was the following. We simulated a flow of cars in our map, and we run ACSM to extract the patterns (here, without constraints to allow us the comparison with SPAM). We measured the time complexity (called ACSM time). From the PDFA, we sampled many sets of sequences (from 100 to 35,000 sequences). From each sample, we run SPAM to extract a second set of frequent patterns. Both of the algorithms were run with σ = 10%. We computed also the time complexity of SPAM by taking into account the sampling time and the mining time (SPAM time). The chart of Fig. 6 describes the behavior of the two methods.

While ACSM has a constant time complexity, the one of SPAM increases a lot in function of the sequence set size. We added on this chart a curve (Cover) corresponding to the proportion of frequent patterns extracted by SPAM which have also been extracted by ACSM. We can observe that SPAM needs a large number of sequences to approach the results of ACSM. We can note that once the size of the set is sufficiently large, about 20,000 examples, more than 97% of all the frequent patterns extracted from the PDFA are covered by the those founded by SPAM. But in this case, the time cost of SPAM is higher than the one of ACSM.

Conclusion

In this paper we have shown that, in situations that can be modeled as flow control problems, a sequence mining task may preserve privacy thanks to an underlying probabilistic automaton. We have proposed a new constrained sequence mining algorithm based on that data structure and shown this approach is more efficient than sampling a database from the PDFA and using a classical sequence mining algorithm. Our algorithm has been implemented in a prototype we have used to visually show the frequent routes of towns without any private information from its drivers. In the future, we want to use ACSM on two flow control problems: Web usage mining by using a PDFA to model the structure of a site with the flow of visits, and social network modeling by using a PDFA to model the flow of emails between people. In order to be as efficient as possible, it will be interesting to integrate other constraints such as mingap, maxgap, etc.

Figure 1 .

 1 Figure 1. An example of PDFA.

  1 and estimate with p(a) the unknown probability p(a) of sequences that contain the letter a. Vector π(a) has the components π(0, a) = 0.314, π(1, a) = 0.532, π(2, a) = 0.54. For matrices ρ(a) and (Iρ(a)) -1 , we get

Figure 2 .

 2 Figure 2. Average difference between p(< x 1 x 2 >) and p(< x 1 x 2 >) according to regular expressions on Σ.

Figure 3 .

 3 Figure 3. Comparison between N and N . The dotted line is the situation where N would perfectly estimate N . The solid line is obtained with the series of experiments.

  quent and relevant patterns, according to a support threshold σ and two statistical risks α 1 and α 2 . The pseudo-code of our ACSM algorithm (Automata-based Constraint-based Sequence Mining) is presented in Algorithm 1. From lines 2 to 9, it initializes a set of relevant frequent patterns composed of only one symbol. Since no pattern has been extracted yet, only the support test (line 4) and PROP TEST (line 5) are run. The paths of the PDFA that do not satisfy these two tests will not be studied anymore, that allows us to prune the search space. The second part of ACSM tests additional symbols to search for larger frequent and relevant patterns. Three conditions must be satisfied: the support test (lines 17), PROP TEST (line 18) and CHI2 TEST (line 19). The boolean function MERGE(w, w ) (line 15) returns true if the n -1 last symbols of w are identical to the n -1 first ones of w . This ensures that all subsequences of the resulting pattern v =< w > . < x n > (line 16) are yet frequent and relevant.

Figure 4 .

 4 Figure 4. TrafficMiner

Figure 5 .

 5 Figure 5. (a) and (b): Effect of constraints on the number of patterns.

Figure 6 .

 6 Figure 6. Comparison SPAM vs ACSM.

Algorithm 1 :

 1 πF ), a support threshold σ, two risks Pseudo-code of ACSM

		α1 and α2
		Output: a set of relevant frequent patterns G
	1	begin
	2	G1 ← ∅ ;
	3	foreach l ∈ Σ do
	4	if P (q0, l) ≥ σ then
	5	if PROP TEST (P (q0, l), α1) is satisfied then
	6	G1 ← G1 ∪ {l} ;
	7
	8
	9	G ← G1 ;
	10	n ← 1 ;
	11	while Gn = ∅ do
	12	Gn+1 ← ∅ ;
	13	foreach w =< x1...xn >∈ Gn do
	14	foreach w =< x 1 ...x n >∈ Gn do
	15	if MERGE (w, w ) then
	16 17	v ← < w > . < x n > ; if P (q0, v) ≥ σ then
	18 19	if PROP TEST (P (q0, v), α1) then if CHI2 TEST ( --→ Vin, --→ Vout, α2) then
	20	Gn+1 ← Gn+1 ∪ {v} ;
	21
	22
	23
	24
	25
	26
	27	G ← G ∪ Gn+1 ;
	28	n ← n + 1 ;
	29	return G ;
	30	end

Since we don't use the sequences, N is unknown. We will explain how to estimate N using the PDFA.

http://himalaya-tools.sourceforge.net/Spam/