Pierre Lescanne
email: pierre.lescanne@ens-lyon.fr

Boltzmann samplers for random generation of lambda terms

Keywords: lambda calculus, combinatorics, functional programming, test, random generator, Boltzmann sampler

Randomly generating structured objects is important in testing and optimizing functional programs, whereas generating random λ-terms is more specifically needed for testing and optimizing compilers. For that a tool called QuickCheck has been proposed, but in this tool the control of the random generation is left to the programmer. Ten years ago, a method called Boltzmann samplers has been proposed to generate combinatorial structures. In this paper, we show how Boltzmann samplers can be developed to generate random λ-terms, but also other random data structures like trees. These samplers rely on a critical value which parameters the main random selector and which is exhibited here with explanations on how it is computed. Haskell programs are proposed to show how samplers are actually implemented.

Introduction

Claessen and Hughes [5] ask a fundamental question:

[H]ow would one choose a random closed λ-term with a uniform distribution?

Actually generating random lambda terms and more specifically generating random typable λ-terms are fundamental for debugging functional programming compilers [START_REF] Pa Lka | Testing an optimising compiler by generating random lambda terms[END_REF], but also for answering many questions concerning λ-calculus and functional programming. We will see that this is possible using an apparatus called Boltzmann samplers (Duchon et al. [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF]) and based on the ideas of 1 statistical physics initiated by the Austrian physicist Ludwig Boltzmann . The key issue is the ability to generate random combinatorial structures with some flexibility on the size. In this paper the combinatorial structures are λ-terms, but also since we are interested in functional programming they are other data structures, like binary trees (the data type Tree in [5]) or 1-2-trees. These latter structures will allow us to introduce the concept of Boltzmann samplers. Assume a program generating random λ-terms is built. Somewhere the program chooses whether it generates a variable, an abstraction or an application. This is done according to a probability distribution. Why the chosen probability distribution is respectively variable abstraction application 0.3703026 0.25939476 0.3703026 will be explained further. For now let us say that there is a critical value ρ ≈ 0.509308127, which plays a main role in counting λ-terms and that the above values are respectively (1 -ρ 2 )/2 and ρ 2 . Once we know how to generate large plain λ-terms, we are able to address the random generation of large typable λ-terms. This paper is based on four milestone papers.

i [START_REF] De Bruijn | Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem[END_REF] Nicolaas Govert de Bruijn (1972). Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes mathematicae, 34 (5), 381-392.

ii [5] Koen Claessen and John Hughes. QuickCheck: a lightweight tool for random testing of Haskell programs. In Martin Odersky and Philip Wadler, editors, ICFP, pages 268-279. ACM, 2000. This paper received the Most Influential ICFP Paper Award for the year 2000.

iii [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF] Philippe Duchon, Philippe Flajolet, Guy Louchard, and Gilles Schaeffer. Boltzmann samplers for the random generation of combinatorial structures. Combinatorics, Probability & Computing, 13(4-5):577-625, 2004.

iv [START_REF] Tromp | Binary lambda calculus and combinatory logic[END_REF] The first paper established what is now called de Bruijn indices which play an important role here in counting λ-terms up to α-conversion. But Nicolaas de Bruijn is better known outside the Functional Programming community as one of the pioneer of modern combinatorics [START_REF] De Bruijn | Asymptotic Methods in Analysis[END_REF] (see [START_REF] Knuth | Selected Papers on Analysis of Algorithms[END_REF] fourth cover pages). We will use indirectly his combinatorics results here.

The above quotation of Claessen and Hughes is extracted from the introduction of the second paper [5] and is completed by 1We have chosen to put distribution under the human tester's control.

However unlike Claessen and Hughes, the philosophy of our paper is that we have chosen to put the distribution under a strict mathematical control, based on Boltzmann samplers and probability theory as introduced in the third paper [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF]. For that we use a counting method introduced by John Tromp in [START_REF] Tromp | Binary lambda calculus and combinatory logic[END_REF]. This amazing paper deals with algorithmic complexity theory [START_REF] Li | An introduction to Kolmogorov complexity and its applications[END_REF] and proposes to replace Turing machines by λ-calculus in this theory. Therefore it provides a very simple and elegant concrete definition of descriptional complexity (Kolmogorov complexity). For this Tromp proposes to represent λ-terms by binary chains and in this framework he defines a very small self interpreter of size 210. His coding of λ-terms in {0, 1} * is as follows2 :

n = 1 n 0 λM = 00 M M N = 01 M N
Representing λ-terms by binary chains confers to them a natural notion of size. This counting is realistic3 as it gives variables a weight depending on the distance from their binder. In other words a variable which is deep in the stack is heavier (larger) than a shallow one .

Moreover our paper relies on the book of Flajolet and Sedgewick [START_REF] Flajolet | Analytic Combinatorics[END_REF] which is the reference on generating functions. Our paper is also the application of a recent article containing results on counting binary λ-terms [START_REF] Grygiel | Counting terms in the binary lambda calculus[END_REF].

In this paper we speak about random generation of λ-terms. This applies in testing and optimizing functional programming compilers [START_REF] Pa Lka | Testing an optimising compiler by generating random lambda terms[END_REF][START_REF] Pa Lka | Testing an optimising compiler by generating random lambda terms[END_REF], but it is clear that this applies to other combinatorial objects having bound variables, like imperative programs with a block structure [START_REF] Yang | Finding and understanding bugs in C compilers[END_REF].

A survey of Boltzmann approach

Recall that a Boltzmann sampler generates uniformly random objects with a tolerance in the size of the generated objects. In other words, the sampler generates the objects in a cloud around a given size.

An orographic cloud 4

Before a Boltzmann sampler for combinatorial structures is defined, the generating function associated with these structures is first expressed. Its coefficients count the structures by size. In our case, i.e., trees and λ-terms, the expressions of the generating functions contain a square root of a polynomial, whose smallest root in module is a real which we call the critical value. This is the radius of convergence of the associated series. A Boltzmann sampler is derived from this series and based on a value x which allows generating random structures with a mean and a standard deviation which depend on x. Actually if the user has a specific size in mind, she provides the desired mean and a calculation returns the x that yields this mean. But in our case we assume that we attempt to generate large structures of size, say at least 100, perhaps 1000 or 1000000 or more. In our domain, trees and λ-terms, the choice of x is not any choice, but x shall be set to the critical value, for mathematical reasons that are explained in [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF]. This way we get a uniform random sampler for all big trees or λ-terms. Now let us focus on trees and λ-terms and assume that the structures are distributed in kinds. For instance, for λ-terms, these kinds are variables, abstractions and applications. A random selector among these kinds is built using probabilities computed using the critical value. Then the selector is embedded in a sampler which calls itself recursively. But if any freedom is left to the sampler, it may generate huge structures as well as small ones. To avoid the pitfall of generating huge objects, the sampler has an upper limit of structures it can generate. Furthermore after the generation a sieve retains only the structures that are large enough, yielding the tolerance threshold (the cloud) we mentioned previously.

Structure of the paper

The paper is structured as follows. Since the problem of counting λ-terms and presenting their Boltzmann samplers is not straightforward, we present first in Section 2 the generating functions for trees: binary trees and 1-2 trees. Then we present the generating function for counting λterms in Section 3. In Section 4 we present a less efficient method for generating λ-terms not based on Boltzmann samplers. In the following sections we address Boltzmann samplers. First in Section 5 we present the general perspective of Boltzmann samplers. Then in Section 6 we specialize on trees: binary trees and 1-2 trees. Section 7 is devoted to Boltzmann samplers for λ-terms. Until that point the paper addresses only the problem of counting and generating plain λ-terms. In Section 8 we survey the harder problem of counting and generating closed terms for which we cannot propose a Boltzmann sampler, since the generating function is not defined by a unique equation.

Counting trees

Before presenting how to count λ-terms, we will show in this section how to count trees. We will first show how to count binary trees, then how to count 1-2 trees aka Motzkin trees.

Binary trees

A binary tree (the data type Tree in [5]) is either a leaf or a compound tree made of a node and two subtrees. It can be described as follows:

B = + B × • × B.
We assume that leaves and nodes have size 1. General techniques of generating functions ( [START_REF] Flajolet | Analytic Combinatorics[END_REF] page 738) leads to the following equation for the generating function

B(z) = n≥0 B n z n
whose coefficients count binary trees of size n:

B(z) = z + zB(z) 2
or zB(z) 2 -B(z) + z = 0 which yields:

B(z) = 1 - √ 1 -4z 2 2z .
B(z) is not defined for z ∈ R larger that 1 2 . We say that B(z) has a singularity ρ B which is equal to 1 2 . We are going to use this fact in our sampler of random binary trees.

Motzkin Trees

We are going to consider another family of trees which have analogies with lambda terms, namely 1-2 trees ( [START_REF] Flajolet | Analytic Combinatorics[END_REF] pages 81). They are also called Motzkin trees. They have two kinds of internal nodes, unary nodes and binary nodes. The class of Motzkin trees is described as

M = + • × M + M × • × M .
unrankT oo :: which means that a Motzkin tree is either a leaf of size 1 or a tree of size n + 1 rooted on another tree of size n or a tree of size n 1 + n 2 + 1 rooted on two trees of size n 1 and n 2 . The generating function

Int → Integer → T erm unrankToo n k | k == (trompoo n) = Index $ fromIntegral (n -1) | k <= (trompoo (n -2)) = Abs (unrankToo (n -2) k ) | otherwise = unrankApp (n -2) 0 (k -trompoo (n -2)) where unrankApp n j r | r <= tjnj = let (dv , rm) = (r -1) ′ divMod ′ tnj in App (unrankToo j (dv + 1)) (unrankToo (n -j ) (rm + 1)) | otherwise = unrankApp n (j + 1) (r -tjnj ) where tnj = trompoo (n -j ) tjnj = (trompoo j ) * tnj
M (z) = ∞ n=0 M n z n
where M n counts the number of Motzkin trees of size n, is a solution of the equation:

M (z) = z + zM (z) + zM (z) 2 or zM (z) 2 -(1 -z)M (z) + z = 0.
Hence

M (z) = 1 -z - √ 1 -2z -3z 2 2z .
It is given by the smallest root in module of the polynomial 1 -2z -3z 2 , namely ρ M = 1/3 (the other root -1 is larger in module).

Counting lambda terms

We now consider λ-terms up to α-conversion. To count equivalence classes modulo α-conversion it is convenient to count canonical representatives of classes modulo α. For that the best way is to count terms with de Bruijn indices, since those terms are unique representatives of classes modulo α.

We work with de Bruijn indices starting at 1. Sometimes we call those indices improperly "variables". For instance λ1 is the representative of the αconversion equivalence class of the term λx.x and λλ1 2 is the representative of the α-conversion equivalence class of the term λx.λy.y x. We assume that the size of the index i is i + 1 and the size of an abstraction is 2 and the size of an application is 2 as well. Therefore we get the equation for the numbers5 of terms of size n:

S ∞,0 = S ∞,1 = 0, S ∞,n+2 = 1 + S ∞,n + n k=0 S ∞,k S ∞,n-k .
This means that there is no term of size 0 or 1 and for terms of size n+2, there is one term which is an index namely n + 1, plus S ∞,n terms that are abstractions plus n k=0 S ∞,k S ∞,n-k terms that are applications of terms of size k on terms of size n -k, for k from 0 to n. Sequence (S ∞,n ) n∈N can be found in the On-line Encyclopedia of Integer Sequences with the entry number A114851. Its first 20 values are: 0, 0, 1, 1, 2, 2, 4, 5, 10, 14, 27, 41, 78, 126, 237, 399, 745, 1292, 2404, 4259.

Recall some results of Grygiel-Lescanne [START_REF] Grygiel | Counting terms in the binary lambda calculus[END_REF]. Let S ∞ (z) denote the generating function for the sequence (S ∞,n ) n∈N , that is

S ∞ (z) = ∞ n=0 S ∞,n z n = ∞ n=0 z n+2 + ∞ n=0 S ∞,n z n+2 + ∞ n=0 n k=0 S ∞,k S ∞,n-k z n+2 S ∞ (z) fulfills the equation S ∞ (z) = z 2 1 -z + z 2 S ∞ (z) + z 2 S ∞ (z) 2 .
which yields

S ∞ (z) = z 3 -z 2 -z + 1 - √ z 6 + 2 z 5 -5 z 4 + 4 z 3 -z 2 -2 z + 1 2z 2 (1 -z) .
The radius of convergence of this series i.e., the smallest singularity of the associated analytic function, given as the smallest real root of the polynomial

z 6 + 2 z 5 -5 z 4 + 4 z 3 -z 2 -2 z + 1 = (z -1)(z 5 + 3z 4 -2z 3 + 2z 2 + z -1).
A computation using the mathematical software Sage [START_REF] Stein | Sage Mathematics Software (Version 5.8)[END_REF] tells us that this smallest root is approximately ρ S∞ = 0.509308127. Knowledge of the singularity ρ S∞ (which we will write just ρ in what follows) is crucial for computing quantities related to the sequence (S ∞,n ) n∈N . Especially it plays a key role in computing parameters of the Boltzmann sampler. The following theorem is in [START_REF] Grygiel | Counting terms in the binary lambda calculus[END_REF].

Theorem 1 (Asymptotic evaluation of S ∞,n )
The number of all binary λ-terms of size n satisfies

S ∞,n ∼ (1/ρ) n • C n 3/2 ,

Unranking lambda terms

We know how to count the λ-terms, which means basically that we know how to order the terms, assigning a number to each term (ranking). We may use this fact the other way around and build a λ term from its rank. This function is called unranking and is implemented in Haskell as unrankToo (see Figure 1).

]. If S ∞,n-2 < k < S ∞,n ,
then k corresponds to an application of two terms which are then computed. Unranking has at least three applications:

• counting typable λ-terms,

• generating random λ-terms and

• generating random typable λ-terms.

Counting typable λ-terms

We know very little about the combinatorial properties of simply typable λterms. For instance, we do not know any formula for counting them, we have no idea of their distribution among plain λ-terms and we have no information on their ratio among plain λ-terms. We propose to count how many terms of size n are typable. We proceed as follows, we generate all the plain terms of size n and we filter those that are typable and we count them. This process is relatively tedious and is limited by the number of plain terms. Here are the numbers T ∞,n of typable terms of size n we computed: In words this means that there are more than seven billions of terms of size 42 and about 14 billions of terms of size 43 which we have to traverse to know how many are simply typable. We conjecture [START_REF] Lescanne | An exercise on streams: convergence acceleration[END_REF] that like the S ∞,n 's, the T ∞,n 's increase like 1.963447954 n and the ratio T ∞,n /S ∞,n is polynomial.

n T ∞,n 0

Generating random λ-terms (plain and typable)

Thanks to unranking we have a very natural method for generating random λ-terms [START_REF] Nijenhuis | Combinatorial algorithms for computers and calculators[END_REF] (called by Duchon et al. [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF] the recursive method ). It works as follows: to generate a random λ-terms of size n one generates first a random number say k in the interval [1..S ∞,n ] and then by unranking k one creates the associated λ-term. The size of the term we can generate this way is limited by the size of the number S ∞,n we can manipulate.

To generate a random typable λ-term of size n, one repeats the process of generating plain terms until one gets a typable λ-term. The process is inefficient for two reasons: one has to repeat the generation of plain terms with a lot of waste and one has to handle huge numbers. But unlike Boltzmann samplers, unranking generates random λ-terms of a precise size. However in applications like compiler testing, we seldom need to generate terms of a very precise size. An approximation on the size is enough.

Boltzmann samplers

In this section we present the notion of Boltzmann samplers. For more detail the reader is invited to look at [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF].

A Boltzmann sampler returns a random object in a given class C according to a given index x. By convention a Boltzmann sampler for C depending on the index x is written ΓC(x). In Haskell we will write it gammaC gen x , because we need a generator of random numbers to be passed as parameter.

Before specializing the notion of Boltzmann sampler to count specifically lambda terms of size n assume we consider a generic class C of combinatorial structures, where objects of size n are counted by numbers C n . Assume in addition that the class C admits the generating function C, which means that

C(x) = ∞ n=0 C n x n .
Uniform probability distribution assigns to each γ ∈ C n the probability:

P Cn (γ) = 1 C n
We want to generate random objects with some flexibility on the size. In other words we want the objects to be generated in some cloud around a given size n, that is so that the size N of the objects lies in some interval (1-ε)n ≤ N ≤ (1+ε) for some factor ε > 0 which we call "tolerance". Such a method is called the approximate-size uniform random generation. The Boltzmann models assign to any object γ ∈ C the following probability:

P Cn,x (γ) = 1 C(x) • x |γ| .
The size of an object in a Boltzmann model is a random variable N . The probability of drawing an object of size n under the model of index x is

P Cn (N = n) = C n x n C(x) .
This is a probability since

n≥0 P Cn (N = n) = 1 C(x) n≥0 C n x n = 1
The random variable N has a first moment and a second moment [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF]:

E x (N ) = x C ′ (x) C(x) E x (N 2 ) = x 2 C ′′ (x) + xC ′ (x) C(x) .
and a standard deviation:

σ Cn (x) = E x (N 2 ) -E x (N ) 2 = x 2 C ′′ (x) + xC ′ (x) C(x) -x 2 C ′ (x) 2 C(x) 2
One builds a Boltzmann generator for a class C according to the recursive construction of the class C .

Disjoint union

If the class is built as

C = A + B, then C n = A n + B n and C(z) = A(z) + B(z).
The probability of the occurrence of some object is

P C ,x (γ ∈ A ) = A(x) C(x) , P C ,x (γ ∈ B) = B(x) C(x)
Assume we have defined a Haskell data type

data KindC = IsA | IsB
A generator for a Bernoulli variable is given by the Haskell function: where TypeA and TypeB are two types. 7 Assume two functions gammaA and gammaB . Then

gammaC :: StdGen → Double → (C , StdGen) gammaC gen x = let (class, g) = bern x gen in case class of IsA → let (a, g1) = gammaA g x in (A a, g1) IsB → let (b, g1) = gammaB g x in (B b, g1)
In what follows we will also consider not only a disjoint union of two classes C = A + B, but a disjoint union of three classes like C = A + B + D. We call randSel the function which replaces bern in this case.

Cartesian product

If the class is built as C = A × B, then the generating function satisfies

C(z) = A(z) • B(z), since C(z) = α,β ∈A ×B z |α|+|β| .
γ = α, β ∈ C has the probability:

P C ,x (γ) = x |γ| C(x) = x |α| A(x) • x |β| B(x) .
C(z) = 1 1 -A(z) .
This means that Nil is selected with probability 1/C(x) = 1 -A(x) and a non empty sequence is selected with probability A(x). A Boltzmann sampler for sequences is

gammaC :: Double → StdGen → (TypeC ′ , StdGen) gammaC x gen = let (p, g) = randomR (0, 1) gen in if p < A(x ) then let (a, g1) = gammaA x g (c, g2) = gammaC x g1 in (Times a c, g2) else (Nil , g)
The case x = ρ C Assume that the generating function we consider is of the form:

C(x) = P C (x) -Q C (x) R C (x)
where P C (x), Q C (x) and R C (x) are three polynomials and where ρ C is such that Q C (ρ C ) = 0 and where Q C (x) = 0 and R C (x) = 0 for 0 ≤ x ≤ ρ C . Those properties are fulfilled for the three generating functions B(x), M (x) and S ∞ (x) we have seen. Notice that

C(ρ C ) = P C (ρ C ) R C (ρ C )
is finite. On another hand

C ′ (x) = P ′ C (x) R C (x) - Q ′ C (x) 2 Q C (x)R C (x) - (P C (x) -Q C (x))R ′ C (x) R C (x) 2
shows that lim

x→ρ C C ′ (x) = ∞. Hence lim x→ρ C E x (N ) = lim x→ρ C xC ′ (x) C(x) = ∞.
Therefore if we choose x to be ρ C , the size of the generated structures will be distributed all over the natural numbers.

6 Boltzmann samplers for trees

Boltzmann samplers for Motzkin trees

Given a number x, the mean value formula (or first moment) E x,M (N ) = xM ′ (x)/M (x) allows us by solving the equation xM ′ (x)/M (x) = n to tell which value of x provides a sampler with n as mean value for the size. For instance, xM ′ (x)/M (x) = 100 returns x 100 = 0.33330833286456574 it says that the sampler gammaM gen x 100 (see below) will generate a random term with a mean value 100. Similarly since x 600 = 0.3333326388880542, gammaM gen x 600 will generate a random term with mean value 600. For a small value, say 10 we get x 1 = 0.3308286281723805. The standard deviation σ Mn (x) can be instantiated to x 10 or x 100 or to x 600 . Actually σ Mn (x 10 ) ≈ 25 σ Mn (x 100 ) ≈ 816 σ Mn (x 600 ) ≈ 1200.

Added to the fact that x 100 and x 600 are very close to the ρ M = 1/3 (which is called the critical value) it appears that a Boltzmann sampler for large values of n is obtained by parameterizing gammaM with ρ M , namely 1/3. See [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF] Section 7.2 for a mathematical justification of this choice. Since there are three components in the addition, we generalize the Bernoulli generator and then we specialize it to the case of Motzkin trees, producing a function we call randSelM . Let us call

M 0 (z) M (z) = z M (z) the first component of (z + zM (z) + zM (z) 2 )/M (z), M 1 (z) M (z) = z
the second component of (z + zM (z) + zM (z) 2 )/M (z) and

M 2 (z) M (z) = zM (z)
the third component of (z + zM (z) + zM (z) 2 )/M (z). We define the following Haskell functions:

m z = (1 -z -sqrt(1 -2 * z -3 * z * z ))/(2 * z ) p1 x = x / m x p2 x = p1 x + x
One may notice that p2 x + x * m x == 1 for every value of x, which means that when one adds all the probabilities of the events one gets 1.

data KindMotzkin = IsLeaf | IsUnary | IsBinary randSelM :: StdGen → Double → (KindMotzkin, StdGen) randSelM gen x = let (p, g) = randomR (0, 1) gen in if p < p1 x then (IsLeaf , g) else if p < p2 x then (IsUnary, g) else (IsBinary, g)
Then we define the data type

data MTree = MNil | MU MTree | MB MTree MTree
for Motzkin trees and we get the Boltzmann sampler for Motzkin trees: An interesting feature should be noticed in this program. Indeed the function gammaM gen x calls gammaM g x and should not terminate since we can prove in no way that the first arguments namely gen versus g decrease. Thus the termination is only probabilistic and depends on the choice of x. The implementation of randSelM makes gammaM gen x to terminate with probability 1, thanks to the whole theory of Boltzmann samplers. For instance if the generator is buggy and takes its values only in the interval ( 13 , 1] the program will not terminate.

gammaM :: StdGen → Double → (MTree, StdGen) gammaM gen x = let (kind , g) = randSelM gen x in case kind of IsLeaf → (MNil , g) IsUnary → let (t1, g1) = gammaM g x in (MU t1, g1) IsBinary → let (t1, g1) = gammaM g x (t2, g2) = gammaM g1 x in (MB t1 t2, g2) ceiledGammaM :: StdGen → (EMTree, Int, StdGen) ceiledGammaM gen = let (kind , g0) = selOneThird gen in case kind of IsLeaf → (OK MNil , 1, g0) IsUnary → let (et1, n1, g1) = ceiledGammaM g0 in case et1 of OK t1 → if n1 <= upLimit then (OK (MU t1), n1 + 1, g1) else (Error , upLimit, g1) Error → (Error , upLimit, g1) IsBinary → let (et1, n1, g1) = ceiledGammaM g0 (et2, n2, g2) = ceiledGammaM g1 in case et1 of OK t1 → case et2 of OK t2 → if n1 + n2 + 1 <= upLimit then (OK (MB t1 t2), n1 + n2 + 2, g2) else (Error , upLimit, g2) Error → (Error , upLimit, g2) Error → (Error , upLimit, g2)

Samplers for large Motzkin trees

Note that M (ρ M ) = 1. For large Motzkin trees the right choice is to take x = ρ M = 1/3. This gives the probability

• for drawing a leaf ρ M M (ρ M ) = 1 3 ,
• for drawing a tree rooted by a unary node ρ M = 1 3 , • for drawing a tree rooted by a binary node ρ M M (ρ M ) = 1 3 . Actually since choosing ρ M generates large trees, it is advisable to limit the size of the tree to be generated during the process. Therefore, we consider what Duchon et al. call ceiled random generation. We define a constant upLimit which sets a size upper limit that the sampler should respect during the generation. We then define a data type: data EMTree = OK MTree | Error and a selection function selOneThird which selects a kind among IsLeaf , IsUnary and IsBinary with probability 1/3, 1/3, 1/3. The function ceiledGammaM is defined in Figure 2.

If we want to generate a term between say a and b we generate terms with an upLimit set to b until we get a term larger than a. Duchon et al. have shown that the complexity of this method is linear. In other words, the generation of a tree with a size between a and b takes a time 0(b).

Boltzmann samplers for binary trees

The binary trees are implemented in Haskell by data BTree = BNil | BNode BTree BTree If we compute for B(z) the means associated to some values of n, a we did above for M (z), we get: There are two kinds of binary trees:

• leafs (represented by BNil ) which correspond to

B 0 (z) B(z) = z B(z)
which is the first component of (z + zB(z) 2 )/B(z), and

• nodes (represented by BNode t1 t2) which correspond to

B 1 (z) B(z) = zB(z)
which is the second component of (z + zB(z) 2 )/B(z).

Let us define

b z = (1 -sqrt(1 -4 * z * z ))/ (2 * z ) p1 x = x * x / (1 -x ) / soo x p2 x = p1 x + x 2
Using Sage we computed the values:

x 100 = 0.5092252666102192 x 500 = 0.5093048407797965

x 600 = 0.5093058457062517

x 1000 = 0.5093073063214039 which are the choices of x yielding mean values 100, 500, 600 and 1000 respectively.

General samplers of λ-terms

The values of the probabilities for a given x are

• p v (x) = x 2
(1-x)S∞(x) for variables,

• p abs (x) = x 2 for abstractions,

• p app (x) = x 2 S ∞ (x) for applications. whose square is rhosquare = rho * rho which yields ρ 2 = 0.25939476825293667. Notice that since ρ is a root of the polynomial below the square root, S ∞ (ρ) = 1-ρ 2 2ρ 2 . The values of the probabilities for selecting among variables, abstractions and applications are:

• p v (ρ) = 2ρ 4
(1-ρ)(1-ρ 2 ) for variables,

• p abs (ρ) = ρ 2 for abstractions,

• p app (ρ) = 1-ρ 2 2
for applications.

Let us simplify

2ρ 4 (1-ρ)(1-ρ 2 ) into 1-ρ 2 2
by computing the difference:

2ρ 4 (1 -ρ)(1 -ρ 2 ) - 1 -ρ 2 2 = 4ρ 4 -(1 -ρ 2 ) 2 (1 -ρ) 2(1 -ρ)(1 -ρ 2 ) = ρ 5 + 3ρ 4 -2ρ 3 + 2ρ 2 + ρ -1 2(1 -ρ)(1 -ρ 2 ) = 0.
Therefore we get the result announced in the introduction namely that

• p v (ρ) = 1-ρ 2 2
≈ 0.3703026 for variables,

• p abs (ρ) = ρ 2 ≈ 0.25939476 for abstractions,

• p app (ρ) = 1-ρ 2 2 ≈ 0.3703026 for applications.

We build the random selector: pvrho = (1rhosquare) p2rho = pvrho + rhosquare randSelRho :: StdGen → (KindTerm, StdGen) randSelRho gen = let (p, g) = randomR (0, 1) gen in if p < pvrho then (IsVariable, g) else if p < p2rho then (IsAbstraction, g) else (IsApplication, g)

We generate a Boltzmann sampler for indices (or variables). A de Bruijn index is a natural number i.e., a sequence of 1's. Hence we take the Boltzmann sampler for sequences with A(z) = z and A(ρ) = ρ.

gammaV :: StdGen → (Integer , StdGen) gammaV gen = let (a, g) = randomR (0, 1) gen in if a < rho then let (n, g1) = gammaV g in (n + 1, g1) else (1, g)
We want to generate terms that are below a certain upLimit. Thus when the limit is passed we generate an error. For that we create a type with error.

data ETerm = OK Term | Error This method recalls the sized generation of [5]. A Boltzmann sampler for large λ-terms which is given: To generate a large plain λ-term, terms are filtered until a term that is large enough is generated. Recall that the method is linear in time complexity. Thus the generation of a term of size 100, 000 takes a few seconds, the generation of a term of size one million takes three minutes and the generation of a term of size five millions takes five minutes on a laptop.

ceiledGammaSoo :: StdGen → (ETerm,
To generate large typable λ-terms we generate λ-terms and check their typability. Currently we are able to generate random typable λ-terms of size 500.

Ranking and unranking closed lambda terms

Boltzmann samplers work only when one knows the generating function explicitly. Thus if one wants to generate typable closed terms, one has two solutions. First one generates a random typable term using the Boltzmann sampler described above and if the produced term is not closed, one closes it by adding the adequate number of abstractions. Second one uses an unranking method similar to this described in Section 4.2. For that let us recall how one counts terms with at most m free indices [START_REF] Grygiel | Counting terms in the binary lambda calculus[END_REF]. The specific case of the closed terms is the case when the number of free indices is at most 0.

S m,0 = S m,1 = 0, S m,n+2 = [m ≥ n + 1] + S m+1,n + n k=0 S m,k S m,n-k .
Given a predicate P , [P ( x)] denotes the Iverson symbol, i.e., [P ( x)] = 1 if P ( x) and [P ( x)] = 0 if ¬P ( x). S 0,n counts closed terms and is computed by tromp 0 n.

Related works

In the introduction we cited papers that are clearly connected to this work. In a recent work, Bacher et al. [START_REF] Bacher | Efficient random sampling of binary and unary-binary trees via holonomic equations[END_REF] propose an improved random generation of binary trees and Motzkin trees, based on Rémy algorithm [START_REF] Rémy | Un procédé itératif de dénombrement d'arbres binaires et son application à leur génération aléatoire[END_REF] (or algorithm R as Knuth calls it [START_REF] Knuth | Fascicle 4: Generating All Trees, History of Combinatorial Generation[END_REF]). Instead of growing the trees from the root, they propose like Rémy to grow the trees from inside by an operation called grafting. It is not clear how this can be generalized to λ-terms as this requires "to find a combinatorial interpretation for the holonomic equations [which] is not [...] always possible, and even for simple combinatorial objects this is not elementary" (Conclusion of [START_REF] Bacher | Efficient random sampling of binary and unary-binary trees via holonomic equations[END_REF] page 16). We would like also to mention papers on counting λ-terms [START_REF] Lescanne | On counting untyped lambda terms[END_REF][START_REF] Grygiel | Counting and generating lambda terms[END_REF] and evaluating their combinatorial proprieties namely [START_REF] Bodini | Lambda-terms of bounded unary height[END_REF][START_REF] David | Asymptotically almost all λ-terms are strongly normalizing[END_REF][START_REF] Bodini | Enumeration of generalized BCI lambda-terms[END_REF][START_REF] Bodini | Asymptotics and random sampling for BCI and BCK lambda terms[END_REF]. Another related paper is [START_REF] Duregård | Feat: functional enumeration of algebraic types[END_REF] which proposes Haskell programs for enumerating structures.

Acknowledgments

We would like to thank Katarzyna Grygiel, Bruno Salvy and John Tromp, for fruitful discussions. We are also indebted to Neil Sloane and the developers of the On-line Encyclopedia of Integer Sequences which allowed us to know about sequence A114851 which was the starting point of this research.

Conclusion

Boltzmann samplers are central tools for the uniform generation of random structures, like trees or λ-terms. Two directions are now open for applications: first to integrate the programs proposed here in actual testers and optimizers and second to extend Boltzmann samplers to other kinds of programs, for instance programs with block structures. From the theoretical point of view, more should be known about generating functions for closed λ-terms or λ-terms with fixed bound on the number of variables. Boltzmann samplers should be designed for such terms which requires to extend the theory. Concerning combinatorial properties of simply typable λ-terms many question are left open and seem to be hard. Besides since we are interested in generating typable terms, it could be worth to build random uniform samplers delivering directly typable terms, for instance based on a hashing table built offline.

Figure 1 :

 1 Figure 1: The unranking function of λ-terms in Haskell

bern : :

 : Double → StdGen → (KindC , StdGen) bern x gen = let (p, g) = randomR (0, 1) gen in if p < A(x )/C (x ) then (IsA, g) else (IsB , g) The class C is represented by the type TypeC : data TypeC = A TypeA | B TypeB

Assume we have defined a

  Haskell data type data TypeC = Times TypeA TypeB In this case the Boltzmann sampler is gammaC :: Double → StdGen → (TypeC , StdGen) gammaC x gen = let (a, g1) = gammaA gen x (b, g2) = gammaB g1 x in (g2, Times a b) Sequences C can be the class of all finite sequences of elements of a class A . Its associated type is: data TypeC = Nil + Times TypeA TypeC This means that C is the solution of the equation C = 1 + A × C where 1 denotes the empty sequence. The associated generating function is solution of C(z) = 1 + A(z) • C(z) which yields:

Figure 2 :

 2 Figure 2: The function ceiledGammaM

x

  10 = 0.4960783708241233 x 100 = 0.4999739685017913 x 600 = 0.49999930090217926 for which we obtain the standard deviations: σ Bn (x 10 ) ≈ 22 σ Bn (x 100 ) ≈ 970 σ Bn (x 600 ) ≈ 14623.

For

  selecting among IsVariable, IsAbstraction and IsApplication we use the following selector written in Haskell randSel :: StdGen → Double → (KindTerm, StdGen) randSel gen x = let (p, g) = randomR (0, 1) gen in if p < pv x then (IsVariable, g) else if p < pv x + pabs x then (IsAbstraction, g) else (IsApplication, g) Samplers for large λ-terms Like for trees, the best choice of x for generating large λ-terms is ρ which we call rho in Haskell: rho :: Double rho = 0.5093081270242373.

Figure 3

 3 gives a program for unranking terms with at most m indices, where tromp m n is the Haskell function representing S m,n .unrankT ::Int → Int → Integer → Term unrankT m n k | m >= n -1 && k == (tromp m n) = Index $ fromIntegral (n -1) -terms 1 n-1 0 | k <= (tromp (m + 1) (n -2)) = Abs (unrankT (m + 1) (n -2) k ) -terms 00M | otherwise = unrankApp (n -2) 0 (ktromp (m + 1) (n -2)) -terms 01M N where unrankApp n j h | h <= tmjtmnj = let(dv , rm) = (h -1) ′ divMod ′ tmnj in App (unrankT m j (dv + 1)) (unrankT m (nj ) (rm + 1)) | otherwise = unrankApp n (j + 1) (htmjtmnj )where tmnj = tromp m (nj ) tmjtmnj = (tromp m j ) * tmnj

Figure 3 :

 3 Figure 3: unrankT function in Haskell.

  John Tromp. Binary lambda calculus and combinatory logic. In Marcus Hutter, Wolfgang Merkle, and Paul M. B. Vitányi, editors, Kolmogorov Complexity and Applications, volume 06051 of Dagstuhl Seminar Proceedings. Internationales Begegnungs-und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2006.

See appendix for the whole quotation.

Not exactly since Tromp starts indices at 0 like[START_REF] Lescanne | From λσ to λυ, a journey through calculi of explicit substitutions[END_REF] and we starts indices at 1 like de Bruijn[START_REF] De Bruijn | Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem[END_REF].

In a previous submission[START_REF] Grygiel | Counting and generating lambda terms[END_REF] where we chose to give de Bruijn indices size 0, a referee said: "If the authors want to use the de Bruijn representation, another interesting experiment could be done: rather than to count variables as size 0, they should be counted using their unary representation. This would penalize deep lexical scoping, which is not a bad idea since 'local' terms are much easier to understand and analyze than deep terms".

Public Domain Picture, origin: Wikimedia, source: U.S. National Oceanic and Atmospheric Administration

The index ∞ is justified by the fact that S∞,n is the limit of Sm,n when m goes to ∞. See Section 8.

The notation oo mimics ∞.

It can be the case that TypeA and TypeB are TypeC itself or are defined recursively using TypeC .

We can then introduce the sampler:

Once again we see that the best value for x to generate random large binary trees is ρ B = 1 2 . Thus gammaB gen 0.5 generates large binary trees. For a similar approach of the same problem with in particular a discussion of ceiled random generation see [START_REF] Yorgey | Random binary trees with a size-limited critical Boltzmann sampler[END_REF]. For other methods for generating random binary trees, see [START_REF] Knuth | Fascicle 4: Generating All Trees, History of Combinatorial Generation[END_REF], pages 18-19 and [START_REF] Rémy | Un procédé itératif de dénombrement d'arbres binaires et son application à leur génération aléatoire[END_REF].

Boltzmann samplers for lambda terms

Like for Motzkin trees we consider the equation of the generating function:

with three components: the first corresponds to de Bruijn indices, the second to abstractions, the third to applications. Like for Motzkin trees we have to build a random selector among three probabilities. First we describe a data type:

where sq = sqrt(z 6 + 2 * (z 5 ) -5 * (z 4 ) + 4 * (z 3 )z 2 -2 * z + 1)

and two functions:


Olga Mínguez Moreno
email: olga.minguez@dege.uhu.es

ENVIRONMENTAL INDICATORS AS CONTEXTUAL INFORMATION FOR TERRITORIAL ACTORS

Keywords: Sustainable Development, Environmental Indicators, Territory, Policy

In the last few decades, a great variety of indicators of sustainable development have been elaborated to feed models or assess strategies in form of macro-indexes or systems of indicators. But, Are the measures found in literature good references to be applied to lower territorial levels? This paper presents the results of CAENTI work in terms of the environmental dimension of sustainable development, since there are many other teams working in the social, institutional and economic dimensions. Therefore, it is just one of the pieces of the puzzle, which needs to be connected to other pieces.

ENVIRONMENTAL INDICATORS AS CONTEXTUAL INFORMATION FOR TERRITORIAL ACTORS 1. SUSTAINABLE DEVELOPMENT AND RELATED CONCEPTS

Important progresses have been accomplished regarding to Sustainable Development (SD) in both, theory and praxis, but there is still a gap between theoretical modelling of SD and measurement initiatives implemented at the territorial level, that is, sustainable development indicators. Despite the fact that different perspectives of SD lead to different models, there are some agreements in its key factors: natural capital maintenance and equity with future and present generations. Both aim at ensuring human welfare through time. Economic literature has generally focused on how to include natural capital preservation within economic models to be passed on to future generations rather than studying intragenerational equity. In this sense, weak and strong sustainability models have been developed and they have been accompanied by measurements of sustainable development.

Thus, depending on the chosen model, sustainable development measures may vary. Measurements from the weak sustainability perspective are generally based on income models resulting in concepts as sustainable income, Green Net National Product (GNNP) or wealth-equivalent income [START_REF] Pezzey | Progress and Problems in the Economics of Sustainability[END_REF]. Measures developed from the strong sustainability position take into account tighter constrains, rules and principles to guarantee species preservation, minimum standards for impacts on environmental quality and sustainable use of renewable resources, including in their analysis physical measures. None of these measures consider intergenerational equity, which has a spatial dimension. It could be due to the fact that preservation of natural capital is easier to be accepted, modelled and measured than aspects related to equity, particularly intragenerational solidarity. Theoretical foundations have been based at this respect from the development process perspective.

Therefore, conceptualisation of sustainable development results on a specific model and moving to action means materialising it into a particular territory through sustainable policy. At this respect, it is very important to delimit a sustainability policy (as a unique policy or as the coordination of every policy implemented in a territory) rather than an environmental policy, establishing the requirements to fulfil not only environmental sustainability but also social sustainability and to be able to detect global constrains to be implemented at local levels. Good governance, both at the international and the territorial levels, could contribute to raise solutions in order to respect those global restrictions and develop actions to be implemented at local levels since institutional framework, principles and rules regulating relationship among territorial actors and their organisation play a critical role in implementing sustainability values within the territorial development path. In this context, we conceive "territory" as a complex, socially build and evolving concept [START_REF] Leloup | La gouvernance territoriale comme nouveau mode de coordination territoriale ?[END_REF].

Besides the complexity of variables comprising the concept of sustainable development and its manifold interpretations, theoretical foundations have not always been accompanied by applied developments.

Measurement not only entails to determine implications of the concept, but also establishes boundaries related to how it is going to be addressed in praxis. Evaluation has traditionally been the framework for measurements produced at territorial levels. Policies, plans, programs and projects -among others-are constantly assessed including sectoral, thematic, partnership or even global analysis. Those initiatives implemented at different territorial levels involving different actors are not always based on a common understanding of sustainable development and may not even seek common objectives. The field to which sustainable evaluations are performed is quite broad and experiences are not usually exchanged from different fields. In addition to this, interdisciplinarity is faced as a competition of approaches and methods rather than add value to the process [START_REF] Martinuzzi | Understanding Sustainable Development and Fields of Application[END_REF].

MEASURES OF SUSTAINABLE DEVELOPMENT

In the last few decades, a great variety of indicators of sustainable development have been elaborated to feed models or assess strategies. They could be classified as macro-indexes and indicator systems. Complex or aggregated indicators are usually elaborated to give information about variables of a model or feed decision making in terms of policies or strategies while indicator systems also respond to a model of sustainability, but are usually designed to monitor the performance of territorial policies at different scales [START_REF] Moreno | La medición del desarrollo sostenible. Una reflexión sobre su aplicación en el ámbito local[END_REF].

On the one hand, Green GDP, Genuine Savings or ISEW (Index of Sustainable Economic Welfare or GPI, Genuine Progress Indicator as an updated version) are examples of macroeconomic measures adjusted by environmental and social information. Based on National Accounting, there are also some attempts to measure wellbeing. The most well-known composite quality of life indicator is the Human Development Index and its associated ones, the Human Poverty Index and the Gender Related Development Index. There are also attempts of sustainable indicators more focused on the environmental sphere than the economic or the social ones, for instance, Ecological Footprint; Environmental Sustainability Index (or its two associates

THE CONTRIBUTION OF CAENTI TO THE ENVIRONMENTAL DIMENSION OF SUSTAINABLE DEVELOPMENT.

But, Are these examples good references to be applied to lower territorial levels? How are the processes of modelling and measuring SD at the local level? What elements need to be considered to guarantee sustainability in a territory? What kind of information do different territorial actors need? Where could they find it?

These questions should be answered from different viewpoints: theory and praxis.

From a theoretical perspective and focusing on a specific territory, we should study ecosystems, not only those located in the municipal territory, but also the ones located in surrounding areas in order to find out what is the natural capital to be preserved at the local level. Besides this, policies with impact on territory should be studied and the model guiding local development determined. Reality becomes complex when numerous administrations have different competences managing sustainability principles. Moreover, actors (enterprises, associations, scientific community, etc.) not always operating in the same territory are also involved in their implementation.

Institutional dimension plays a key role in territorial management. Equity application as second sustainability key factor is a twofold dimension. Intergenerational equity is raised by preserving natural capital, among others, as a bequest to future generations. Intragenerational equity is suggested from universalism, focusing on people's ability to generate opportunities to "live worthy lives". At a global scale, consumption decisions and development aid influence global consequences of local decisions, from the social sustainability point of view. At a local scale, attention must be put on satisfactors. Culture by values, environmental and sustainability education and transparency in information; induce responsibleness in consumption and production patterns; which could be fostered by administration.

In summary and based on a theoretical perspective, policy coordination and introducing sustainability as a transversal factor in every policy implemented in the territory are the key elements to connect natural capital and equity in the local area. At this respect, a territorial information system should be the common framework to include information regarding to the progress made by a territory in terms of sustainability (for more information, please see the contribution of WP3 and WP6 of CAENTI).

But, what about applications of all that? What has been the contribution of CAENTI to praxis? The questions related to processes of modelling and measuring SD at the local level or the elements to assure sustainability in a territory could be answered better from a theoretical perspective. But questions related to the information needed by territorial actors or where could they find it should be faced from praxis. In order to answer these questions according to the work done by other teams and workpackages inside CAENTI, we have centred on European territories where CAENTI partners operate.

This paper presents the results of CAENTI work in terms of the environmental dimension of sustainable development, since there are many other teams working in the social, institutional and economic dimensions. Therefore, it is just one of the pieces of the puzzle, which needs to be connected to other pieces.

First of all, we have focused on finding out what should be studied or measured according to the theory of sustainable development. At this respect, theory focuses on natural capital and equity; that is, one of the basic things to do is to study ecosystems sustaining those particular human settlements or communities to focus on. But unfortunately, CAENTI's objective is not to study ecosystems of the territories where its partners are located, for the time being. As one of CAENTI products has been to define territory, one of the future steps will be to include the natural delimitation of the territories in which CAENTI partners are operating in order to see the natural boundaries that should be respected in each particular territory.

The next step theory has shown as important is to consider policies implemented in each territory and analyze their connections. As sustainable development embraces a great variety of aspects and links, which usually differ in each territory; and this is a first attempt to include the environmental dimension into CAENTI work; we have decided to focus on the policy boosted at an European level: the European Strategy of Sustainable Development (ESSD).

The ESSD has focused on ten main themes to measure its progress to sustainability. Those are: i) socioeconomic development, ii) climate change and energy; iii) sustainable transport; iv) sustainable consumption and production; v) natural resources; vi) public health; vii) social inclusion; viii) demographic changes; ix) global partnership; and x) good governance.

The next step has a twofold dimension. On the one hand it is necessary to detect the information needs of territorial actors in environmental aspects and to what extend are they fulfilled by the work of other teams of CAENTI. On the other hand, it is essential to examine the availability of the information gathered for measuring the progresses of the European Strategy of Sustainable Development; the methodology, protocols, and levels to which information is computed.

As a result of this, and as themes related to socio-economic development, social inclusion, demographic changes and public health, are widely covered by the socioeconomic indicators developed by WP4 and WP6, we have decided to focus on sustainable consumption and production, climate change and energy and natural resources; choosing five indicators from the wide battery provided by the European Union (EUROSTAT). Those are:

 Municipal waste generated.  Electricity consumption by households.  Greenhouse gas emissions.  Modal split of passenger transport.  Built up areas.

Those indicators are calculated for the member states of the European Union, at a NUTS 1 level and are made comparable from one to other territories. But, what happens if we try to deep on lower levels to the national one?

We usually find out that the information behind the equally called indicator in one or other territory is not gathered in the same way. For instance, the indicator "municipal waste generated" is computed by EUROSTAT through the EUROSTAT-OECD Joint Questionnaire for the NUTS 1 level, while the Spanish Statistics Institute applies a survey on collected and treated urban waste for the NUTS 1 and NUTS 2 levels; or the Statistical Office of the Republic of Slovenia, using a different methodology, gathers information related to urban waste for the NUTS 3 level. But it still becomes more difficult if one goes deep into the local level. In one country -let's choose Spain as an examplealthough every municipality should have information related to waste generated within the territory, this information is not gathered the same way and by the same institutions or organisms. For instance, in Huelva province (NUTS 3), there are two different administrations dealing with waste, both using different methodologies. For this specific case, the Local Employment Observatory has gathered all the information and it is available at http://www.ole.uhu.es/ for LAU 2 level. It is likely that those municipalities with Local Agenda 21 may have collected some information related to waste.

For the other four indicators chosen, the situation is very similar.

CONCLUSIONS

We have started from analyzing the several theories elaborated for the concept of sustainable development. After that we have deepen on the various measurements of sustainable development built on and calculated through specific literature. Having realized this wide scanning, some questions arise: Are the measures found in literature good references to be applied to lower territorial levels? How are the processes of modelling and measuring SD at the local level? What elements need to be considered to guarantee sustainability in a territory? What kind of information do different territorial actors need? Where could they find it? Some restrictions arose in our way of answering these questions. For instance, theory recommends focusing on natural capital; therefore ecosystems sustaining those particular human settlements in which CAENTI partner operates should be delimited and investigated in order to see the natural boundaries that should be respected in each particular territory to assure physical limits of sustainable development. Unfortunately, this is still not an objective for CAENTI's work.

After considering the European Strategy of Sustainable Development and the main themes in which it is focused, we approach to the environmental dimension of sustainable development from a twofold dimension: needs of territorial actors regarding to environmental aspects and the availability of environmental information from the European to the local level. At this respect, restrictions related to information availability are still really hard.

Finally, as a first step in CAENTI's work related to the environmental dimension, five indicators are chosen for the national level: municipal waste generated, electricity consumption by households, greenhouse gas emissions, modal split of passenger transport, built up areas.

  On the other hand, systems of sustainable development indicators have also been generated and greatly improved since the Río Conference. Instead of aggregating separate components into a single index, one way of addressing the multiplicity of factors and dimensions of sustainable development is to generate a system. At an international level, United Nations has made an outstanding effort to reach consensus on the implementation of an indicator system to measure national progress towards sustainable development. World Bank and OECD have also developed systems and gather data related to indicators of sustainable development. The European Union, apart from its Structural Indicators, has accomplished a system of sustainable development indicators to measure progress in terms of political priorities. The work of the European Environmental Agency regarding to environmental indicators systems based on DPSIR Framework is a very rigorous reference.

	: Environmental
	Performance Index and Environmental Vulnerability Index); or energy indicators such as National Energy
	Surplus; Available Energy Surplus; Total Exosomatic Production, Endosomatic Energy Consumption; or
	dematerialisation indicators such as Factor X.


Emilie Diot
email: diot@labri.fr

Cyril Gavoille
email: gavoille@labri.fr

Path Separability of Graphs

In this paper we investigate the structural properties of kpath separable graphs, that are the graphs that can be separated by a set of k shortest paths. We identify several graph families having such path separability, and we show that this property is closed under minor taking. In particular we establish a list of forbidden minors for 1-path separable graphs.

Introduction

"Divide and Conquer" is an common technique in computer science to solve problems. The whole data is separated into different small parts to find a solution in these parts, and then to merge the solutions to obtain the result on the input graph.

A wide theory has been developed for graphs that can be decomposed into small pieces. Such graphs, a.k.a. bounded treewidth graphs, supports polynomial algorithms for many class of problems, whereas no algorithms of complexity better than exponential complexity are known for the general case. This has contributed to new insights into Fixed Parameterized Tractable theory whose consequences for practical algorithms are effective improvements on the running time [START_REF] Abu-Khzam | Kernelization algorithms for the vertex cover problem: Theory and experiments[END_REF][START_REF] Koster | Treewidth: Computational experiments[END_REF].

There are however problems that can be efficient solved even for graphs without small separators (or equivalently of large treewidth). Large separators but "well shaped" reveal very useful for approximation algorithms. For instance, if the separator has a small diameter, or a small dominating set, then distances between vertices can be computed efficiently up to some small additive errors (see [START_REF] Dourisboure | Tree-decompositions with bags of small diameter[END_REF][START_REF] Chepoi | Diameters, centers, and approximating trees of delta-hyperbolic geodesic spaces and graphs[END_REF][START_REF] Umezawa | Tree-length equals branch-length[END_REF] for works about the treelength of a graph).

An important observation due to Thorup [START_REF] Thorup | Compact oracles for reachability and approximate distances in planar digraphs[END_REF] is that separators consisting of a set of shortest paths are also very useful for the design of compact routing scheme, distance and reachability oracles. More precisely, he used the fact that every weighted planar graph with n vertices has a set of three shortest paths whose deletion split the graph into connected components of at most n/2 vertices (a decomposition into components of at most 2n/3 vertices using two shortest paths was early proved in [START_REF] Lipton | A separator theorem for planar graphs[END_REF]). Using a recursive decomposition, and sampling each such shortest path, he showed that distances between any pair of vertices can be approximated up to a factor of 1 + ε in polylogarithmic time, for every ε > 0, with an oracle of size1 O(ε -1 n log n).

This notion of "shortest path" separator has been extended in [START_REF] Abraham | Object location using path separators[END_REF]. Roughly speaking, a k-path separator is the union of k shortest paths whose removal halve the graph. The formal definition is actually slightly more complicated and is described in Section 2. The same authors have showed that k-path separable graphs have efficient solutions for several "Object Location Problems" including compact routing schemes, distance oracles, and small-world navigability. Based on the deep Robserton-Seymour's decomposition [START_REF] Robertson | Graph minors. XVI. Excluding a non-planar graph[END_REF], they show in particular that every weighted graph excluding a minor H has a (1 + ε)-approximate distance oracle of size O(ε -1 kn log n), where k = k(H) depending only of H. Actually, the oracle can be distributed into balanced labels, each of size O(ε -1 k log n) such that distance queries can be answered from given the source-destination labels only. The graphs excluding a fixed minor is a huge family of graphs including (and not restricted to) bounded treewidth graphs, planar graphs, and graphs of bounded genus.

Our Results

An approximate distance oracle for a graph G is a data-structure that quickly returns, for any source-destination pair, an approximation on cost of a shortest path connecting them. Such data-structures are obtained by preprocessing G where each edge has a weight corresponding to the cost of traversing this edge (or length). However, in practice, the number n of vertices of G is large whereas the number of interesting vertices for which we want approximate the distance is small (say t). Current solutions [START_REF] Abraham | Object location using path separators[END_REF][START_REF] Thorup | Compact oracles for reachability and approximate distances in planar digraphs[END_REF] provide oracles of size O(t log n) whereas a space independent of n would be preferable.

Such a compression can be achieved by adding weights on the vertices of the input graph. Typically, interesting vertices receive a weight 1 whereas the others receive a weight 0. A k-path separator on such vertex-and edge-weighted graph is then defined as previously, excepted that the removal of the separator must leave connected components of size at most half the total vertex-weight of the graph. The size of the oracles is improved since log t recursion levels suffice instead of log n in the initial formulation.

In this paper we extend the classical notion of k-path separability to edgeand vertex-weighted graphs. In particular, we prove that previous results (e.g., the 3-path separability of planar graphs) still hold in this new framework.

We establish a connection between separators corresponding to the border of a face and k-path separability, and we identify several families of graphs that are 1-path and 2-path separable. We note that most of our proofs are constructive, and lead to polynomial and even linear algorithms.

More interestingly, we show that the family of graphs that are k-path separable for any weight function is minor-closed. Combined with the Graph Minor Theory of Robertson and Seymour [START_REF] Robertson | Graph minors. XX. Wagner's conjecture[END_REF], it follows that the k-path separability can be theoretically tested in cubic time [START_REF] Robertson | Graph minors. XIII. The disjoint paths problem[END_REF] for each fixed k, although no algorithm is currently known. Finally, we provide a first step towards the characterization of 1-path separable graphs.

Preliminaries

A minor of a graph G is a subgraph of a graph obtained from G by edge contraction. We denote by K r the complete graph (or clique) on r vertices, and K p,q the complete bipartite graph. For convenience, the term component is a short for connected component.

A vertex-weight function (resp. edge-weight function) is a non-negative real function defined on the vertices (resp. edges) of a graph. A non-negative real function applying on both vertices and edges is simply called weight function. A weighted graph is graph G having a weight function ω, that we denote also by (G, ω). The weight of a subgraph H of G, denoted by ω(H), is the sum of the weights over the vertices of H.

A half-separator for a graph G with vertex-weight function ω is a subset of vertices S such that each component of G\S has weight at most ω(G)/2. Observe that the deletion of a half-separator does not necessarily disconnect the graph.

A k-path separator of a weighted graph G is a subgraph P 0 ∪P 1 ∪. . . where each P i is a subgraph composed of the union of k i minimum cost paths in G\ j<i P j , and where i k i k. A k-path separator is said strong if it consists of P 0 only, i.e., composed of the union of k minimum cost paths in G. A weighted graph is (strongly) k-path separable if every induced subgraph has a (strong) k-path separator.

A tree-decomposition of a graph G is a tree T whose vertices, called bags, are subsets of vertices of G such that:

1. for every vertex u of G, there exists a bag X of T such that u ∈ X; 2. for every edge {u, v} of G, there exists a bag X of T such that u, v ∈ X; and 3. for every vertex u of G, the set of bags containing u induces a subtree of T .

An important property following from the last two points is that every path between u ∈ X and v ∈ Y in G has to intersect all the bags on the path from X and Y in T . Therefore, the deletion of every bag X disconnects G provided that T \ X is composed of more than one subtree and that no bags Y ⊆ X.

The width of a tree-decomposition T is max X∈T {|X| -1}. A treewidth-t graph is a graph having a tree-decomposition of width t, and the treewidth of G is the minimum t such that G is a treewidth-t graph.

We will use several times the following basic result (the proof of this lemma, and of several others, appear in the full version).

Lemma 1. Every tree-decomposition of a vertex-weighted graph has a bag that is a half-separator of the graph. Such a bag is called center of the treedecomposition.

For the sake of presentation, we prove the following folklore results. 2. It is well-known that every planar graph has a tree-decomposition such that every bag consists of at most three shortest paths. This comes from the well-known fact that every planar graph having a depth-h rooted tree has a tree-decomposition where each bag consists of 3 paths of the tree starting from the root (see [START_REF] Flum | Parametrized Complexity Theory[END_REF][pp. 305]). By Lemma 1, the center C of the tree-decomposition is a half-separator. So, C forms a strong 3-path separator. Indeed, every k-path separator S consists of at most 2k vertices since every shortest path in a clique consists of an edge. K 4k+1 \ S is a clique on at least 2k + 1 vertices, so S is not a half-separator.

As remark in [START_REF] Abraham | Object location using path separators[END_REF], the k-path separability of minor-free graphs holds also for vertex-weighted graphs. However the formal proof of this result cannot be considered as folklore, and its self-contained proof is currently more than the page limitation of this paper.

One the of unresolved problem we left open is to know whether they are planar graphs that are not 2-path separable.

Face-Separable Graphs

As we will see later in Section 4, graphs that are k-path separable have strong structural properties. In particular, planarity plays an important role, at least for k = 1 in the light of Theorem 3. In this section we will see that, a half-separator of a special "shape" implies a low path separability of the graph. Moreover, this half-separator is defined independently of the shortest path metric of the graph, it only depends on the vertex-weight function.

A half-separator S of a weighted graph G is a face-separator if G has a plane embedding such that S is the border of a face. A graph is face-separable if every induced subgraph has a face-separator.

By definition, outerplanar graphs are face-separable, since the outerface contains all vertices of the graph. We will see that the family of face-separable graphs includes more general graphs, like the series-parallel graphs, the subdivisions of a K 4 (Proposition 2), and even includes some unbounded treewidth planar graphs (Proposition 3).

The main result of this section is:

Theorem 1. Every face-separable weighted graph is strongly 2-path separable.

The bound given by Theorem 1 is best possible because there are face-separable graphs that are not 1-path separable. This can be proved by combining Proposition 2 and the fact there are treewidth-2 graphs and subdivisions of K 4 that are not 1-path separable -see Fig. 3.

Proposition 2. Every weighted treewidth-2 graph or weighted subdivision of K 4 is face-separable.

Proof. Let (G, ω) be any weighted treewidth-2 graph. It is known that every treewidth-2 graph is a subgraph of a series-parallel graph, and in particular a planar graph. As any subgraph of G is also a treewidth-2 graph, it is sufficient to prove that G has a face-separable. We consider the graph H obtained from G by adding as many edges as possible while preserving a treewidth-2 graph. Let T be a tree-decomposition of H of width 2, and let C be the center of T . Bag C is composed of a K 3 . We embed H in the plane such that C is the border of a face of this embedding. This is possible by moving some subgraph from inside the K 3 to outside. If not, H would contain a K 4 -minor, contradicting the fact that H has treewidth 2. We can now remove the edges that have been added to H in order to obtain G, and we consider the border S of the face containing the three vertices of C. Such a face exists since deleting edges can only enlarge the existing faces of a plane embedding. We have S ⊆ C, and C is a half-separator of H (Lemma 1). Note that H has the same total weight of G (we have added only edges). It follows that S is a half-separator for G. This completes the first part of the statement of the proposition. Consider now a subdivision G of K 4 having a vertex-weight function ω, and H be an induced subgraph of G. If H is a proper subgraph of G (i.e., H = G), then H is outerplanar and thus has a face-separator. So, assume that H = G.

We assume given a plane embedding of H. We denote by v 1 , . . . , v 4 the four degree-3 vertices of H, and by P i,j the path between v i and v j , for all i, j ∈ {1, . . . , 4}. Let w i = ω(v i ), and let p i,j = ω(P i,j \ {v i , v j }) be the sum of the weights of vertices on P i,j excluding its extremities.

Let assume that H has no face-separator. There are four possible faces F 1 , . . . , F 4 , each one bordered by three paths. Faces are ordered such that whenever the border of F i is removed, the remaining component is composed of three paths sharing vertex v i . The total weight of this component is w i + j =i p i,j . As the border of F i is not a face-separator, we have w i + j =i p i,j > ω(H)/2. This holds for each i ∈ {1, . . . , 4}. Summing these four equations, it turns out (observe that each path p i,j occurs twice in this sum):

i w i + 2 i =j p i,j > 2ω(H) = 2 ⎛ ⎝ i w i + i =j p i,j ⎞ ⎠ .

It implies 0 >

i w i : a contradiction, by definition ω(v) 0 for each vertex v. Therefore, one of the face F i is a face-separator for H, that completes the proof.

Up to now, the graphs we have proved to be face-separable are all of treewidth 3. From Proposition 1 (Point 1), they are 2-path separable. It is natural to ask whether all face-separable graphs have such a low treewidth property. We answer negatively to this question. Proposition 3. For every n, there is a uniform weighted face-separable graph with at most n vertices whose treewidth is Ω(log log n).

Proof. (Sketch).

The proof is based on the construction of a graph called G p , for integral p 1. It has treewidth at least k = p -O(log log p) because we can show it contains a k × k-grid minor, and the number of vertices of G p is n < 2 2 p . In other words, the treewidth of G p is at least log log n -O(log (4) n).

Graph G p is composed of a tree T p of depth p where each vertex of depth i < p has exactly d(i) children, for some function d defined later. Furthermore, for each depth i, a path linking all depth-i vertices is added to T p to form G p . Let us denote by L(i) the number of depth-i vertices in T p . The values L(i) and d(i) obey to the following induction:

L(0) = 1 and L(i) = L(i -1) • d(i -1), where d(i) = i j=0 L(j).
The first values of L(i) and d(i) are given in the table hereafter, and G 4 is depicted on Fig. 1. To prove Proposition 3, we show that every subgraph H of G p contains a face-separator. An important property we use is that in G p , the number d(i) of children for a vertex of depth i is at least the vertex number of the graph induced by T i-1 . The key point is that H is either outerplanar, or there must exist a vertex v of depth i in T p such that all its children belongs to the border of the outerface of H. In the first case, H is trivially face-separable. In the second one, and using the property on d(i), we derive that at least half the vertices of H lie on the outerface.

The Hierarchy of Separable Graphs

For every integer k 1, we denote by PS k the family of all the graphs G that are k-path separable for every weight function ω. More formally,

PS k = {G | ∀ω, (G, ω) is k-path separable} .
We define similarly the family SPS k of all the graphs that are strongly k-path separable for every weight function.

We have seen that every weighted planar graph is strongly 3-path separable. In other words, planar graphs are in SPS 3 . In Section 3, we have seen that every subdivided outerplanar graph is face-separable, and thus strongly 2-path separable. Thus this family is in SPS 2 We will show in Proposition 6 that outerplanar graphs are in actually in PS 1 . Obviously, families PS 1 and SPS 1 coincide.

Clearly, for each k, SPS k ⊂ PS k since a strongly k-path separator is a particular k-path separator. Also, the hierarchies

PS 1 ⊂ • • • ⊂ PS k and SPS 1 ⊂ • • • ⊂ SPS k
are strict because of the complete graph. By Proposition 1 (points 3 and 4), K 4k+1 ∈ SPS k+1 and K 4k+1 / ∈ PS k . The family PS k is however much larger than SPS k as suggested by the next proposition.

Proposition 4. For each k > 4, there is a graph G k with O(k 2 ) vertices such that G k ∈ SPS k , but G k ∈ PS 4 .
Proof. Consider the graph G k composed of a 2(k + 1) × 2(k + 1)-grid in which a vertex v is connected to all the vertices of the grid. G k has 4k 2 + 5 vertices. Vertex and edge weights are unitary. As shown in [START_REF] Abraham | Object location using path separators[END_REF], G k has no strong k-path separator, the removal of any set of k shortest paths deletes at most 2k + 1 vertices, and 2(k + 1) are required to halve the graph. Therefore, G k / ∈ SPS k . However, for every weight function ω, (G k , ω) has a 4-path separator. The first path consists of the universal vertex v, and the three others are defined as in the planar case (since G k \ {v} is planar, and thus 3-path separable). Therefore,

G k ∈ PS 4 .
For the study of PS k and SPS k graphs families, the next proposition tell us that we can always assume that graphs are biconnected.

Proposition 5. A graph belongs to PS k (reps. SPS k ) if and only if all its bicomponents belong to PS k (resp. SPS k ).

Closed under Minor Taking

The remarkable property of PS k and SPS k families is they are closed under minor taking. From the Graph Minor Theorem, such families can be characterized by a finite list of forbidden minors, and membership of a given graph in one of these families can be done in time O(n 3 ) for fixed k. Proof. We give the proof for the family SPS k , the proof for PS k is similar. Let H be any minor of a graph G. We will prove that if G is k-path separable, then H is k-path separable too. To prove that H is k-path separable, we need to prove the property for every induced subgraph of H. However, since every subgraph of H is also a minor of G, we simply show that H has a k-path separator.

It is not difficult to see that if H is a minor of G, then with each vertex u of H we can associate a connected subgraph of G, called super-node of u, such that if (u, v) is an edge of H, then there exists an edge of G, called super-edge of (u, v), connecting a vertex of the super-node of u and a vertex of the super-node of v. (If there are several such edges we select only one.) The super-nodes must be pairwise disjoint (see Fig. 2).

Let ω H be any weight function on H. From ω H , we construct a weight function ω G on G as follows. For every edge (x, y) of G that is a super-edge of (u, v) (colored black on Fig. 2), we set ω G (x, y) = ω H (u, v). For every edge (x, y) of G such that x and y both belongs to the same super-node (called internal-edge and dashed on Fig. 2), we set ω G (x, y) = 0. And, for all other edges (x, y) of G (called external-edge and colored red on Fig. 2), we set ω G (x, y) = 1 + e∈E(H) ω H (e), so that the cost of a path in G using any such edge is strictly larger than the cost of any simple path in H. The weight of a vertex x that belongs to the super-node of u is ω G (x) = ω H (u)/t u , where t u is the number of vertices of the super-node of Fig. 2. A graph G and a minor H u. Note that the sum of weights of the vertices of the super-node of u is precisely ω H (u). The weight of all other vertices is 0. Observe that ω G (G) = ω H (H).

Since G ∈ SPS k , the weighted graph (G, ω G ) has a k-path separator S G consisting of k shortest paths in G. Let H 0 , H 1 , . . . be the components of H, and assume that ω H (H 0 ) is maximum. With each path P of S G that intersects a super-node of a vertex of H 0 , we associate a path Q in H 0 as follows. Let (U 0 , . . . , U t ) be the ordered sequence of all the super-nodes of vertices of H 0 traversed by P . We denote by u i the vertex of H 0 such U i is the super-node of u i . Path Q is obtained by adding an edge between u i-1 to u i , for each i ∈ {1, . . . , t}. We claim that the set composed of each path Q constructed from P as above, and denote by S H , is a half-separator of H.

First, let us show that Q is a shortest path in H 0 (and thus in H). Path P between the last vertex of U i-1 and the first vertex of U i consists of the superedge of (u i-1 , u i ), because H 0 is connected and the weight of this super-edge is less than the weight of any external-edges. Thus Q is a path in H 0 . Now, assume that there exists a path Q in H 0 , from u 0 to u t , that is shorter than Q. Then, from Q we can construct a shorter path in G (shorter than P ) from the last vertex of U 0 to the first vertex of U t . This is due to the fact that each super-node is connected and internal-edges have weight 0. This contradicts that P is a shortest path, hence Q is a shortest path in H 0 .

It remains to show that S H is a half-separator of H. Observe that for i = 0, ω H (H i ) ω H (H)/2 because ω(H 0 ) is maximum. Let X H0 be the set of vertices of any component in H 0 \ S H . Then, there must exists a component X G in G \ S G wholly containing all the super-nodes of the vertices of X H0 . Let v be a vertex of X H0 whose its super-node belongs to none component of G \ S G . Then, there exists a vertex of this super-node that is in S G . From our construction, v belongs to S H (vertices of Q and super-nodes of P correspond): contradiction. Therefore, ω H (X H0 ) ω G (X G ). Moreover, ω G (X G ) ω G (G)/2 = ω H (H)/2. Thus, S H is a half-separator of H, completing the proof.

One-Path Separable Graphs

In this part, we concentrate our attention to the graphs that belong to PS 1 . We have seen in Proposition 2, that the subdivisions of outerplanar graph or of K 4 are face-separable, and thus belong to PS 2 (and even to SPS 2 ). Actually, outerplanar graphs are in PS 1 : Proposition 6. Every weighted outerplanar graph is 1-path separable.

Unfortunately, Proposition 6 does not generalize to treewidth-2 graphs. As depicted on Fig. 3, there are simple series-parallel graphs and subdivisions of K 4 that are not in PS 1 .

The family PS 1 does not reduce to outerplanar graphs, as shown in Proposition 7. A globe graph is a subdivision of K 2,r , for some r, in which the two degree-r vertices may be adjacent. Proposition 7. Every weighted globe graph is 1-path separable. A first attempt to characterize PS 1 is given by Theorem 3. Theorem 3. Every biconnected graph of PS 1 is either isomorphic to K 3,3 , or planar and excludes the list of minors depicted on Fig. 3.

Proof. Let (G, ω) be a biconnected weighted graph with G ∈ PS 1 . First assume that G is not planar. From Kuratowski's criteria, G contains a subdivision of K 5 or K 3,3 .

The complete graph K 5 is not 1-path separable graph from Proposition 1 (cf. Point 4 with k = 2). From Theorem 2, it follows that G cannot contain a subdivision of K 5 , so it must contain a subdivision of K 3,3 .

We shall proof that a subdivision of K 3,3 in which only one edge is subdivided into two edges is not 1-path separable. Denote by M this graph, and set unitary all the weights so that the total vertex-weight is 7. The diameter of M is two. The deletion of any shortest path deletes at most three vertices. Moreover, such a deletion cannot disconnect M , and thus leaves a component with at least 4 > 7/2 vertices. M is not 1-path separable. Therefore, if G is not planar, then G can only be isomorphic to K 3,3 .

We prove now that K 3,3 is 1-path separable. Denote by {x 1 , x 2 , x 3 } and {y 1 , y 2 , y 3 } the vertex set of each part of K 3,3 . We first show that K 3,3 has a 1-path separator. Later we will prove it for all its induced subgraphs. W.l.o.g. assume that ω(x 1 ) ω(x 2 ) ω(x 3 ).

Define P 1 be a shortest path from x 1 to x 2 , and assume P 1 contains y i1 . Define P 2 be a shortest path from y i2 to y i3 (with i 1 , i 2 , i 3 pairwise different indices), and assume it contains x j1 (denote by j 2 , j 3 the two other x's indices). We show that P 1 or P 2 is a 1-path separator. By contradiction, if P 1 is not a half-separator, then (and similarly for P 2 ) ω(P 1 ) < ω(K 3,3 )/2 and ω(G \ P 1 ) > ω(K 3,3 )/2. As ω(P 1 ) is lower bounded by ω(x 1 ) + ω(x 2 ) + ω(y i1 ) and ω(G \ P 1 ) upper bounded by ω(x 3 ) + ω(y i2 ) + ω(y i3 ) (and similarly for P 2 ), it follows that:

ω(x 1 ) + ω(x 2 ) + ω(y i1 ) < ω(x 3 ) + ω(y i2 ) + ω(y i3 ) (1) ω(x j1 ) + ω(y i2 ) + ω(y i3 ) < ω(x j2 ) + ω(x j3 ) + ω(y i1 ) (2)
By summing these equations, we obtain:

ω(x 1 ) + ω(x 2 ) + ω(x j1 ) < ω(x 3 ) + ω(x j2 ) + ω(x j3 ) ⇒ ω(x 1 )+ω(x 2 )+ω(x 3 ) < ω(x 3 )+ω(x j2 )+ω(x j3 ) ω(x 3 ) + ω(x 2 ) + ω(x 1 )
since, by assumption, ω(x 3 ) ω(x j1 ) and ω(x j2 ) + ω(x j3 ) ω(x 2 ) + ω(x 1 ). This leads to a contradiction. Thus, P 1 or P 2 is a 1-path separator for K 3,3 . Now, let H be any induced subgraph of K 3,3 . We use similar notations excepted that the two vertex-sets are {x 1 , . . . , x p } and {y 1 , . . . , y q } with 1 p q 3. If p + q 4, then H is outerplanar, and thus 1-path separable by Proposition 6. We are left with the case p = 2 and q = 3, the case p = q = 3 is already done. We define similarly the two paths P 1 and P 2 , i.e., a shortest path from x 1 to x 2 containing y i1 , and the shortest path between y's vertices different from y i1 and through x j1 . If these both paths are not half-separators, then Eq. ( 1) and (2) rewrite in (vertices x 3 and x j3 do not exist anymore): ω(x 1 ) + ω(x 2 ) + ω(y i1 ) < ω(y i2 ) + ω(y i3 ) ω(x j1 ) + ω(y i2 ) + ω(y i3 ) < ω(x j2 ) + ω(y i1 ) Summing these equations, we obtain: ω(x 1 ) + ω(x 2 ) + ω(x j1 ) < ω(x j2 ), a contradiction since vertex-weights are non-negative and ω(x j2 ) ω(x 1 ). Thus, P 1 or P 2 is a 1-path separator for H.

Therefore, we have proved that the only non-planar graph of PS 1 is K 3,3 . For planar graphs, we manage to find forbidden minors represented in Fig. 3. To prove that each minor M of this list is indeed excluded, we exhibit a particular weight function ω for M . Actually, each vertex and edge has weight 1 or 2 as depicted on Fig. 3. We then exhaustively check that, for each pair u, v of vertices of M , the deletion of any shortest path from u to v leaves a component of weight > ω(M )/2.

To illustrate this, consider for instance the "wheel graph", composed of a cycle of length 5 and a degree-5 vertex, called hereafter center, connected of all vertices of the cycle. The total weight of the graph is 7, the center has weight 2. Any shortest path from the center to a non-center vertex consists of one edge. Therefore its deletion leaves a path of 4 vertices, so of weight 4. Any shortest path between two non-center vertices consists of 2 edges at most, so leaving a component with the center and two (or more) non-center vertices, thus of weight at least 4. In both cases, the weight is > 7/2. This graph has no half-separator composed of a shortest path, and thus is not in PS 1 .

Conclusion

In this paper we have investigated the family of graphs that are k-path separable. Graph Minor Theory implies that such a family can be characterized by a finite set of forbidden minors that we have started to list for k = 1.

We propose here a list of further researches.

1. Determine the full list of forbidden minors for k-path separable graphs and for k = 1. 2. Find an explicit linear time algorithm to determine if a graph is k-path separable, for fixed k. 3. Prove or disprove that planar graphs are 2-path separable. 4. Prove NP-completeness for the problem of determining whether a given weighted graph has a k-path separator. 5. Extend the study to more general isometric separators, not only shortest paths.

3 .

 3 Consider any subgraph H of a weighted graph (G, ω) with n vertices. Let W be the smallest set of vertices in H such that ω(W ) ω(H)/2. Thus, the components of H \ W have weight ω(H)/2. It is clear that W contains at most half the vertices of H, i.e., |W | |V (H)|/2 . A set of at most |W |/2 shortest paths suffices to cover W . Therefore, H has a strong k-path separator with k = |V (H)|/2 /2 n/4 , completing the proof of Point 3. 4. Let us show that the uniform weighted K 4k+1 has no k-path separator.

Fig. 1 .

 1 Fig. 1. The graph G4 with 108 vertices

Theorem 2 .

 2 For each integer k 1, the families PS k and SPS k are minorclosed.

Fig. 3 .

 3 Fig. 3. Forbidden minors for planar graphs in PS1. Black vertices and bold edges have weight 2, blue edges have weight 3, other vertices and edges have weight 1. The two non-planar forbidden minors are K5, and a K3,3 whose one edge is subdivided into two edges.

  Proposition 1 1. Every weighted treewidth-t graph is strongly (t + 1)/2 -path separable. 2. Every weighted planar graph is strongly 3-path separable. 3. Every weighted n-vertex graph is strongly n/4 -path separable 4. The uniform 2 weighted clique K 4k+1 is not k-path separable. Proof. 1. Consider any subgraph H of a weighted graph G. The treewidth of H is at most the treewidth of G. So H has a tree-decomposition of width t. By Lemma 1, the center C of the tree-decomposition is a half-separator. It can be covered by at most |C|/2 (t + 1)/2 shortest paths. Therefore, H has a strong (t + 1)/2 -path separator, and thus G is strongly (t + 1)/2 -path separable.

The size is actually the number of "distance items" stored in the oracle.

That is with a unit weight for all vertices and edges.

", and the équipe-projet commune LaBRI-INRIA