Gilles Barthe

Thomas Espitau

Benjamin Grégoire

Justin Hsu

Pierre-Yves Strub

P.-Y Strub

Uniformity and independence by couplings

Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and for verifying differential privacy. In this paper, we demonstrate that probabilistic couplings can be used for verifying non-relational probabilistic properties. Specifically, we show that the program logic pRHLwhose proofs are formal versions of proofs by coupling-can be used for formalizing uniformity and probabilistic independence. We formally verify our main examples using the EasyCrypt proof assistant.

Proving uniformity and independence by self-composition and coupling 1 Introduction

Uniformity and probabilistic independence are two of the most useful and commonly encountered properties when analyzing randomized computations. Uniform distributions are a central building block of randomized algorithms. Arguably the simplest non-trivial distribution-the coin flip-is a uniform distribution over two values. Given access to uniform samples, there are known transformations for converting the samples to simulate more complex distributions, like Gaussian or Laplacian distributions. Conversely, turning samples from various non-uniform distributions into uniform samples is an active area of research. Probabilistic independence is no less useful. The probability of a conjunction of independent events can be decomposed as a product of probabilities of individual events, each which can then be analyzed in isolation. Independent random variables are also needed to apply more sophisticated mathematical tools, like concentration inequalities.

Given these and other applications, it is not surprising that researchers have investigated different methods of reasoning about uniformity and independence. For instance, Pearl and Paz [18 18] develop an axiomatic theory based on graphoids for modeling conditional independence in probability theory. However, proving uniformity and independence by program verification remains a challenging task. Most verification techniques for probabilistic programs do not treat these properties as first-class assertions, and rely on reasoning principles that are cumbersome to use. Often, the only way to prove uniformity or independence is to prove exact values for the probability of specific events.

For example, consider a formal system for proving properties of the form Pr s m [E] = p, which capture the fact that the event E has probability p in the distribution obtained by executing the randomized program s on some initial memory m (many existing systems use this idea, e.g. [9 9, 13 13, 15 15, 17 17, 19 19, 20 20]). Suppose that we want to prove that a program variable x of some finite type A is uniformly distributed in the output distribution s m . The only way to show this property is to analyze the probability of each output: for every a ∈ A, prove that Pr s m [x = a] = 1 |A| .

For independence, the situation is similar. Assume that we want to prove that the two program variables x and y of respective types A and B are (probabilistically) independent in the output distribution s m . This can be done by exhibiting functions f, g, h such that for every a ∈ A and b ∈ B, we have: Pr While these approaches work in theory, they can be laborious in practice. It may be awkward to express the probability of x = a, and the functions f , g and h may be difficult to produce. The main contribution of this paper is an alternative method based on probabilistic couplings for proving uniformity and independence. Probabilistic couplings are a classical method for proving sophisticated probabilistic properties (e.g., stochastic dominance, rapid mixing of Markov chains, and more [16 16, 21 21, 22 22]). More recently, couplings have been used to reason about relational properties of probabilistic programs, notably differential privacy [5 5, 6 6].

Here we show that uniformity and independence properties can also be verified using coupling, despite being non-relational properties. As a consequence, our verification method inherits the many advantages of reasoning by couplings: compositional reasoning, and no need to reason directly about probabilistic events. Concretely, we show how uniformity and independence can be captured in the relational program logic pRHL [1 1].

In summary, our main contributions are novel methods to prove uniformity and independence properties of probabilistic programs. We prove the soundness of the methods and demonstrate their usefulness on a class of case studies.

Detailed Contributions

Uniformity. Suppose we have a program s with a program variable x ranging over a finite set A, and we want to show that x is distributed uniformly over A after executing s. Rather than computing the probability of Pr s m [x = a] for each a ∈ A, it suffices to show that the probabilities of any two outputs are equal:

∀a 1 , a 2 ∈ A. Pr s m [x = a 1 ] = Pr s m [x = a 2 ] .
Now, we can view uniformity as a relational property: if we consider two runs of s, then the probability of x being a 1 in the first run should be equal to the probability of x being a 2 in the second run. In pRHL, this property is described by the following judgment:

∀a 1 , a 2 ∈ A. s ∼ s : φ =⇒ x 1 = a 1 ⇐⇒ x 2 = a 2
where the assertion φ asserts that the initial states are equal.

Independence. Proving probabilistic independence is more involved. We show how to prove independence in two different ways. Assume that we want to prove that the program variables x and y of respective finite types A and B are independent. First, if the distribution of x, y is uniformly distributed over A × B, then x and y are independent (and are themselves uniformly distributed). Indeed, assume that for all a ∈ A and b ∈ B we have

Pr s m [x = a ∧ y = b] = 1 |A|•|B| . Then we have Pr s m [x = a] = b∈B Pr s m [x = a ∧ y = b] = 1
|A| . A similar argument applies to the probability that y = b, from which independence follows. Thus, our first method of proving independence is by reduction to proving uniformity.

This approach is simple to use, but it only applies to proving independence of uniform random variables. A more expressive, but also slightly more complicated approach is to express probabilistic independence as a property of a modified version of the program, without any requirement on uniformity. More specifically, independence of x and y can be derived from the equality between the probabilities of x = a ∧ y = b and x 1 = a ∧ y 2 = b, where in the first case the probability is taken over the output of the original program s, and in the second case the probability is taken over the output of the program s 1 ; s 2 , where s 1 and s 2 are renamings of s (we call s 1 ; s 2 a self-composition of s [2 2, 12 12]). The reason is not hard to see. Since the composed programs operate on disjoint memory, the final combined output distribution models two independent runs of the original program s. So, the probability Our encoding casts independence as a relational property between a program s and its self-composition s 1 ; s 2 , a property which can be directly expressed in pRHL:

Pr s1;s2 m 1 m 2 [x 1 = a ∧ y 2 = b]- where m 1 m 2 is the disjoint union of two copies of m-is equal to the product of Pr s1 m 1 [x 1 = a]
∀a ∈ A, b ∈ B. s ∼ s 1 ; s 2 : φ =⇒ (x 1 = a ∧ y 1 = b) ⇐⇒ (x 1 2 = a ∧ y 2 2 = b)
where the precondition φ captures the initial conditions. We show that our approach extends to independence and conditional independence of sets of program variables.

Outline Section 2 2 and Section 3 3 provide the relevant mathematical background and introduce the setting of our work. Section 4 4, Section 5 5 and Section 6 6 respectively address the case of uniformity, independence, and conditional independence. In each case we demonstrate our method using classic examples of randomized algorithms. We conclude the paper with a discussion of alternative techniques for verifying these properties.

Mathematical Background

For the sake of simplicity, we restrict ourselves to discrete (countable) sub-distributions.

Definition 1. A sub-distribution over a set A is defined by a mass function µ : A → R + , which gives the probability of the unitary events a ∈ A. This mass function must be s.t. a∈A µ(a) is well-defined and its weight satisfies |µ| = a∈A µ(a) ≤ 1. In particular, the support of the sub-distribution supp(µ) = {a ∈ A | µ(a) = 0} is discrete. When |µ| is equal to 1, we call µ a distribution. We let D(A) denote the set of sub-distributions over A. An event over A is a predicate over A. The probability of an event E in a sub-distribution µ, written Pr x∼µ [E], is defined as {x∈A|E(x)} µ(x).

When working with sub-distributions over tuples, the probabilistic versions of the usual projections on tuples are called marginals. For distributions over pairs, we define the first and second marginals π 1 (µ) and π 2 (µ) of a distribution µ over A × B by π 1 (µ)(a) = b∈B µ(a, b) and π 2 (µ)(b) = a∈A µ(a, b). We are now ready to formally define coupling. Definition 2. Let A 1 and A 2 be two sets, and let Ψ ⊆ A 1 × A 2 . A Ψ-coupling for two sub-distributions µ 1 , µ 2 resp. over A 1 and A 2 is a sub-distribution µ ∈ D(A 1 × A 2 ) such that π 1 (µ) = µ 1 and π 2 (µ) = µ 2 and supp(µ) ⊆ Ψ. We write Ψ µ 1 & µ 2 to denote the existence of a Ψ-coupling.

In addition to the general definition, we shall also consider a special case of coupling: specifically, we say that

(µ 1 , µ 2 ) are f -coupled if f : A 1 → A 2 is a bijection such that µ 1 (x) = µ 2 (f (x)) for every x ∈ A 1 . In this case, we write f µ 1 & µ 2 .
Previous works establish a number of basic facts about couplings, see e.g. Barthe et al. [1 1, 5 5], In particular, one useful consequence of couplings is that they can show that one event has smaller probability than another.

Lemma 3 (Fundamental lemma of coupling). Let E 1 and E 2 be predicates over A 1 and A 2 , and let

Ψ = {(x 1 , x 2 ) | (x 1 ∈ E 1 ) ⇒ (x 2 ∈ E 2 )}. If Ψ µ 1 & µ 2 , then Pr x1∼µ1 [E 1 ] ≤ Pr x2∼µ2 [E 2 ].
One can immediately derive a variant of the lemma where ⇐⇒ and = are used in place of ⇒ and ≤ respectively. The following lemma provides a converse to the fundamental lemma of coupling in the special case where we are interested in proving the equality of two distributions. Lemma 4. For every µ 1 , µ 2 ∈ D(A), the following are equivalent:

• µ 1 = µ 2 ; • for every a ∈ A, Pr x∼µ1 [x = a] = Pr x∼µ2 [x = a]; • for every a ∈ A, Ψa µ 1 & µ 2 where Ψ a = {(x 1 , x 2 ) | x 1 = a ⇐⇒ x 2 = a}; • Ψ A µ 1 & µ 2 where Ψ A = {(x 1 , x 2 ) | x 1 = x 2 }.
We note that the third item (existence of liftings for pointwise equality) is often easier to establish than the last item (existence of lifting for equality), since one can choose the coupling for each possible value of a, rather than showing a single coupling for all values of a.

Setting

We will work with a simple probabilistic imperative language. Probabilistic assignments are of the form x $ ← g, which assigns a value sampled according to the distribution g to the program variable x. The syntax of statements is defined by the grammar:

s ::= skip | abort | x ← e | x $ ← g | s; s | if e then s else s | while e do s
where x, e and g respectively range over (typed) variables in X , expressions in E and distributions in D. To ensure that the set of states is countable, we require that there are finitely many variables X . As usual E is defined inductively from X and a set F of simply typed function symbols. In this paper, distributions used for sampling are either uniform distributions over a finite type A, or the Bernoulli distribution with parameter p, which we denote by Bern(p). We assume that expressions and statements are typed in the usual way. We assume we are given a set-theoretical interpretation for every type and operator of the language. We define a state as a type-preserving mapping from variables to values, and we let State denote the set of states. The set of states is equipped with the usual functions for reading and writing a value; we use m(x) to denote the value of x in m, and m[x := v] to denote state update, in this case the state obtained from m by updating the value of x with v.

One can equip D(State) with a monadic structure, using the Dirac distributions δ x for the unit and distribution expectation E x∼µ [M (x)] for the bind, where

E x∼µ [M (x)] : x → a µ(a) • M (a)(x).
The semantics of expressions and distribution expressions is parametrized by a state m, and is defined in the usual way where we require all distribution expressions to be interpreted as proper distributions (sub-distributions with weight 1).

skip m = δ m abort m = 0 x ← e m = δ m[x:= e m ] x $ ← g m = E v∼ g m [δ m[x:=v] ] s 1 ; s 2 m = E ξ∼ s1 m [ s 2 ξ ] if e then s 1 else s 2 m = if e m then s 1 m else s 2 m while b do s m = lim n→∞ (if b then s) [n] ; if b then abort m
where s [n] n times s; . . . ; s. • The semantics s m of a statement s w.r.t. to some initial state m is a sub-distribution over states, and is defined by the clauses of Fig. 1 1.

• The (lifted) semantics s µ of a statement s w.r.t. to some initial sub-distribution µ over states is a sub-distribution over states, and is defined as

s µ E m∼µ [ s m ] µ ∈ D(State).
A basic and highly important property of probabilistic programs is termination. We say that a program s is lossless if for every initial memory m, | s m | = 1. By now, there are many sophisticated techniques for proving losslessness even for languages that allow both probabilistic sampling and non-determinism (including recent advances by Chatterjee et al. [10 10, 11 11], Ferrer Fioriti and Hermanns [14 14]). These techniques are capable of showing losslessness for all of our examples (in some cases with a high degree of automation), so throughout the paper, we assume that all programs are lossless. This assumption is used in the rules of pRHL and the characterizations of uniformity and independence.

Self-Composition of Programs

For every program s and n ∈ N, we let s n denote the n-fold self-composition of s, i.e. s n = s 1 ; . . . , s n , where each s ı is a copy of s where all variables are tagged with a superscript ı. In order to state the main property of self-composition, we define the self-composition of a state; given a state m, we define its n-fold self-composition m n as the state from X n to values, where X n = {x ı | x ∈ X , 1 ≤ ı ≤ n} such that for every x and ı, m n (x ı ) = m(x). Given a state m from X n , we denote by m ı the ı-th projection of m. Proposition 6. For every program s and state m, we have

Pr s n m n [∧ 1≤ı≤n E ı ı ] = 1≤ı≤n Pr s m [E ı ]
where the event E ı is defined by E ı (m n ) = E(π ı (m )) for every ı and π ı is the projection from a self-composed state to its ı-th component.

Probabilistic Relational Hoare Logic

Probabilistic Relational Hoare Logic (pRHL) is a program logic for reasoning about relational properties of probabilistic programs. Its judgments are of the form

s 1 ∼ s 2 : φ =⇒ ψ,
where s 1 and s 2 are commands and the pre-condition φ and the post-condition ψ are relational assertions, i.e. first-order formulae built over generalized expressions. The latter are similar to expressions, except that each variable is tagged with 1 or 2 to indicate the execution that it belongs to; we call the two executions left and right. Generalized expressions are interpreted w.r.t. a pair (m 1 , m 2 ) of states, where the interpretation of the tagged variables x 1 and x 2 are m 1 (x) and m 2 (x) respectively. We write (m 1 , m 2 ) φ to denote that the interpretation of the assertion φ w.r.t. (m 1 , m 2 ) is valid. The [Conseq] rule is the rule of consequence, and reflects that validity is preserved by weakening the post-condition and strengthening the pre-condition. The [Case] rule allows proving a judgment by case analysis; specifically, the validity of a judgment with pre-condition Φ can be established from the validity of two judgments, one where the pre-condition is strengthened with Ξ and the other where the pre-condition is strengthened with ¬Ξ.

Definition 7. A judgment s 1 ∼ s 2 : φ =⇒ ψ is valid iff for every states m 1 and m 2 , (m 1 , m 2 ) φ implies {(m 1 ,m 2 )|(m 1 ,m 2 ) ψ} s 1 m1 & s 2 m2 .
The [Struct] rule allows replacing programs by provably equivalent programs. The rules for proving program equivalence are given in Fig. 3 3, and manipulate judgments of the form Φ c ≡ c , where Φ is a relational assertion. The first rule ([While-Split]) splits a single loop into two loops (the first running while e is true, and the second running for the remaining iterations); this transformation is useful for selecting different couplings in different program iterations. The second rule ([Swap]) reorders two instructions, as long as they modify disjoint variables. This allows us to couple sampling instructions that may come from two different parts of the two programs.

Moving on to the two-sided rules, the [Seq] rule for sequential composition simply reflects the compositional property of couplings. The [Assg] rule is standard. The [Rand] rule informally takes a coupling between the two distributions used for sampling in the left and right programs, and requires that every element in the support of the coupling validates the post-condition. The rule is parametrized by a bijective function f from the domain of the first distribution to the domain of the second distribution. This bijection gives us the freedom to specify the relation between the two samples when we couple them. The [Cond] rule states that two synchronized if statements can related if their respective branches are also related. The [While] rule is the standard while rule adapted to pRHL. Note that we require the guard of the two commands to be equal-so in particular the two loops must make the same number of iterations-and Φ plays the role of the while loop invariant as usual.

The one-sided rules Assg-L, Rand-L, Cond-L and While-L are similar two their two-sided variant, but only operate on the left program. The full system includes mirrored versions of each one-sided rule, for reasoning about the right program.

Throughout the paper, we often assert that the left and the right copies of a state are equal. This is captured by the relational assertion EqMem = x∈X x 1 = x 2 . We also often assert cross-equality on n-fold composition of states EqMem p , q = x∈X ,1≤ı≤p,1≤≤q x ı 1 = x  2 .

Uniformity

Reasoning about probabilistic programs often requires establishing that a set of program variables (each ranging over a finite type) is uniformly distributed:

Conseq s 1 ∼ s 2 : Φ =⇒ Ψ Φ =⇒ Φ Ψ =⇒ Ψ s 1 ∼ s 2 : Φ =⇒ Ψ Struct s 1 ∼ s 2 : Φ =⇒ Ψ Φ s 1 ≡ s 1 Φ s 2 ≡ s 2 s 1 ∼ s 2 : Φ =⇒ Ψ Case s 1 ∼ s 2 : Φ ∧ Ξ =⇒ Ψ s 1 ∼ s 2 : Φ ∧ ¬Ξ =⇒ Ψ s 1 ∼ s 2 : Φ =⇒ Ψ Seq s 1 ∼ s 2 : Φ =⇒ Ξ s 1 ∼ s 2 : Ξ =⇒ Ψ s 1 ; s 1 ∼ s 2 ; s 2 : Φ =⇒ Ψ Assg Φ = Ψ[e 1 1 /x 1 1 , e 2 2 /x 2 2 ] x 1 ← e 1 ∼ x 2 ← e 2 : Φ =⇒ Ψ Rand f g 1 & g 2 Φ = ∀v. Ψ[v/x 1 1 , f (v)/x 2 2 ] x 1 $ ← g 1 ∼ x 2 $ ← g 2 : Φ =⇒ Ψ Cond Φ =⇒ e 1 = e 2 s 1 ∼ s 2 : Φ ∧ e 1 =⇒ Ψs s 1 ∼ s 2 : Φ ∧ ¬e 1 =⇒ Ψs if e 1 then s 1 else s 1 ∼ if e 2 then s 2 else s 2 : Φ =⇒ Ψ While s 1 ∼ s 2 : Ψ ∧ e 1 1 ∧ e 2 2 =⇒ Ψ ∧ e 1 1 = e 2 2 while e 1 do s 1 ∼ while e 2 do s 2 : Ψ ∧ e 1 1 = e 2 2 =⇒ Ψ ∧ ¬e 1 1 ∧ ¬e 2 2 Assg-L Φ = Ψ[e 1 1 /x 1 1 ] x 1 ← e 1 ∼ skip : Φ =⇒ Ψ Rand-L Φ = ∀v 1 ∈ supp(g 1 ), Ψ[v 1 /x 1 1 ] x 1 $ ← g 1 ∼ skip : Φ =⇒ Ψ Cond-L s 1 ∼ s 2 : Φ ∧ e 1 1 =⇒ Ψ s 1 ∼ s 2 : Φ ∧ ¬e 1 1 =⇒ Ψ if e 1 then s 1 else s 1 ∼ s 2 : Φ =⇒ Ψ While-L s 1 ∼ skip : Ψ ∧ e 1 1 =⇒ Ψ while e 1 do s 1 ∼ skip : Ψ =⇒ Ψ ∧ ¬e 1 1
Pr µ   1≤i≤n x i = a i   = 1≤i≤n 1 |A i |
Note that the definition of uniformity (and as we will see in later sections, the definition of independence) naturally extends to sets of expressions, and so do our characterizations.

Characterization

The following proposition characterizes uniformity in terms of couplings.

Proposition 9 (Uniformity by coupling). Let X = {x 1 , . . . , x n } be a set of variables of respective finite types A 1 , . . . , A n . For every program s, the following are equivalent:

1. for every state m, X is uniformly distributed in s m ; 2. for every two tuples (a 1 , . . . , a n ), (a 1 , . . . ,

a n ) ∈ A 1 × • • • × A n , we have s ∼ s : EqMem =⇒   1≤i≤n x i 1 = a i   ⇐⇒   1≤i≤n x i 2 = a i   . Proof. [1. ⇒ 2.] Let m be a memory and assume that X is uniformly distributed in s m . Let (a 1 , . . . , a n ), (a 1 , . . . , a n ) ∈ A 1 × • • • × A n . We denote by f : State → State the bijection defined by      f (m) = m[x i ← a i ] 1≤i≤n if ∀i. m[x i ] = a i f (m) = m[x i ← a i ] 1≤i≤n if ∀i. m[x i ] = a i f (m) = m otherwise. Let η ∈ D(State × State) be the distribution defined by η(m 1 , m 2 ) = s m (m 1 ) if m 2 = f (m 1 )
, and η(m 1 , m 2 ) = 0 otherwise. We prove that η is a Ψ-coupling for s m , where

ψ = 1≤i≤n x i 1 = a i ⇐⇒ 1≤i≤n x i 2 = a i .
Regarding the marginals, we have:

π 1 (η)(m 1 ) = m2 η(m 1 , m 2 ) = η(m 1 , f (m 1 )) = s m (m 1 ) π 2 (η)(m 2 ) = m1 η(m 1 , m 2 ) = η(f -1 (m 2 ), m 2 ) = s m (f -1 (m 2 )) = s m (f (m 2 )) = s m (m 2 ),
the last equality being a consequence of X being uniformly distributed in s m . Moreover, for (m 1 , m 2 ) ∈ supp(η), we have

m 2 = f (m 1 ). Thus, m 1 [x i ] = a i iff m 2 [x i ] = a i , and m 1 , m 2 |= Ψ. [2. ⇒ 1.] Let (a 1 , . . . , a n ), (a 1 , . . . , a n ) ∈ A 1 ו • •×A n and assume that s ∼ s : EqMem =⇒ Ψ,
where Ψ is defined as in the previous case. Since m, m |= EqMem, by Lemma 3 3 we have:

Pr s m 1≤i≤n x i = a i = Pr s m 1≤i≤n x i = a i ,
showing that X is uniform in s m .

By expressing uniformity as a coupling property, we can use pRHL to prove uniformity. To demonstrate the technique, we consider classical examples from the theory of randomized algorithms.

Simulating a Fair Coin

x ← 0; y ← 0; while x = y do

x $ ← Bern(p); y $ ← Bern(p); This example considers a process for simulating a fair coin using a biased coin. The idea is simple: 1) toss the coin twice; 2) if the two outcomes differ, return the value of the first coin; 3) if the two outcomes match, repeat from step 1. The algorithm does not require the bias of the coin to be known, as long as it is some constant bias and there is positive probability of returning 0 and 1. This process can be modelled by the program s from Fig. 4 4, where 0 < p < 1 is a real parameter modeling the probability of the biased coin to return 0 (tail). Our goal is to establish the trivial judgment { } s { } and the following pRHL judgment:

s ∼ s : =⇒ x 1 ⇐⇒ ¬x 2
By the fundamental lemma of coupling, this implies that Pr s m [x = 1] = Pr s m [x = 0], and hence that x is uniformly distributed upon termination. The proof proceeds by establishing the following invariant:

x 2 = if x 1 = y 1 then y 2 else ¬x 1
Validity of the invariant entails that the desired postcondition holds when the program exits, as the invariant and the negation of the loop guard both hold. The invariant holds when entering the loop, so we only need to prove that it is preserved by the loop body. The proof proceeds as follows: first, we swap the two random assignments on the right, leading to the judgment:

(x $ ← Bern(p); y $ ← Bern(p)) ∼ (y $ ← Bern(p); x $ ← Bern(p)) : φ =⇒ φ
where φ denotes the loop invariant and φ denotes its strengthening by the loop guard-we do not need the precondition, since the values are freshly sampled in the body. Next, we apply the [Rand] rule twice, with the identity bijection. The required pre-condition

∀v 1 , v 2 , v 2 = (if v 1 = v 2 then v 1 else ¬v 1 )
is clearly true.

Cyclic Random Walk

Consider a random walk over a cyclic path composed of n nodes labeled 0, 1, . . . , n -1: starting from position 0, at each step, we flip a fair coin over {-1, 1} and update the position accordingly to the result of the coin flip. To take into account that we are on a cyclic structure, all arithmetical operations are in the cyclic ring Z/ nZ -i.e. are performed modulo n. At each iteration, when moving between two contiguous positions over the circle, we consider that the random walk visited the arc between the two nodes. We want to show that the last visited arc is uniformly distributed. Fig. 5 5 (left) gives a graphical representation of the random walk, where c is the random walk position and the dashed arc is the last visited arc when c moved from 0 to 1. This process can be seen as a simple version of an algorithm that samples a uniformly random spanning tree on a graph-when the graph is a cycle, a spanning tree visits all but one of the edges. While Broder [8 8] analyzes the general problem, we can verify uniformity for the cyclic random walk with couplings.

0 n-1 f 1 2 l c d ← 0; c ← 0; f ← 0; l ← 0; while l + 1 ≤ f do d $ ← U {-1,1} ; if c = l ∧ d = 1 then l ← l + 1; if c = f ∧ d = -1 then f ← f -1; c ← c + d; ret ← (l, l + 1)
The proof proceeds as follows. We imagine executing two random walks, from the same initial position. The goal is to couple the walks so that (a, a + 1) is the last arc in the first walk if and only if (b, b + 1) is the last arc in the second walk. If we can show this property for all a, b, then this coupling argument shows that any two arcs have the same probability of being the last arc, hence the last arc must be uniformly distributed. To describe the coupling informally, we first execute asynchronously the two random walks until they eventually synchronize respectively on the arcs (a, a + 1) and (b, b + 1). At that point, we are in one of the following cases: either the random walks synchronize on the same side of the arcs (a, a + 1) and (b, b + 1), or they synchronize on opposite sides. (These cases are depicted on the left diagrams above, where the arc we want to synchronize on is dashed.) From that point, we execute the two processes resp. in lock-step (if they synchronized on the same side) or anti-lock-step (if they did not).

At some point, both processes will visit the other side of the arcs (a, a+1) and (b, b+1), and since they execute in (anti)-lock-step, these events will occur synchronously. At that point, either the processes finished their walk and they resp. return the arcs (a, a + 1) and (b, b + 1) as their result (case (i) of the right diagram above), or they have other nodes to visit and so they will not resp. return the arcs (a, a + 1) and (b, b + 1) (case (ii) of the same diagram).

We now detail the formal proof. Consider the program of Fig. 5 5, where all arithmetical operations are done modulo n. This algorithm instruments the random walk with two points f and l representing the range [f, l] (using clockwise ordering) of all the points that have been visited by the walk. When all nodes of the cycle have been visited (i.e. when l + 1 = f ), the arc between l and l + 1 is the only arc that has not been visited by the walk. Let s be the program of Fig. 5 5 and s the loop body of the single loop of s. We want to show that the final arc ret-the only arc that has not been marked-is uniformly distributed among all arcs. This follows by the judgment:

∀a, b ∈ Z/ nZ , s ∼ s : =⇒ ret 1 = (a, a + 1) ⇐⇒ ret 2 = (b, b + 1).
First, we make use of the loop splitting equivalence rule ([While-Split]) to transform the main loop into three pieces. In the left program:

while (|v| < n ∧ a, a + 1 / ∈ [f, l]) do s ; while (|v| < n ∧ ¬(a, a + 1 ∈ [f, l])) do s ; while (|v| < n) do s
where [f, l] represent the range f, f + 1, . . . , l. We use a similar transformation on the right program, with b in place of a. To carry out the proof, we first use the one-sided loop rules ([While-L] and the corresponding version [While-R]) on the first loops of the left and right programs. This part of the proof correspond to the walks synchronization as described above. By a straightforward loop invariant, we can show that

Φ ∧ P (a) 1 ∧ P (b) 2
holds after the first loops, where

P (x) = (x ∈ [f, l] ⊕ (x + 1) ∈ [f, l]) and Φ = ∀i ∈ {1, 2}. (c ∈ [f, l]) i indicates that the current positions (c 1 , c 2
) are contained in the range of visited arcs. Next, we show that after the two second loops the following relational invariant is satisfied:

(a, a + 1 ∈ [f, l]) 1 ∧ (b, b + 1 ∈ [f, l]) 2 ∧ (l 1 = a ⇐⇒ l 2 = b)
After the second loop, there are two cases for the third loop. If l 1 = a, we have l 2 = b, f 1 = a + 1 (since a + 1 is visited in 1 ) and f 2 = b + 1. In this case, which corresponds to the case (i) of the last diagram, the third loops both exit immediately and the random walks resp. return the arcs (a, a + 1) and (b, b + 1). Otherwise, we have l 1 = a and l 2 = b, and we can show, using the rules [While-L] and [While-R], that l 1 (resp. l 2 ) will never be set to a (resp. b). In this case, which corresponds to the case (ii) of the last diagram, we can show that the walks resp. return arcs distinct from (a, a + 1) and (b, b + 1).

We now focus on the second loops, relating them with the two-sided variant of the [While] rule. The particular coupling we choose will depend on the current positions in the two sides at the start of the second loops. If a ∈ [f, l] 1 and b ∈ [f, l] 2 then we have l 1 = a and l 2 = b (since a + 1 / ∈ [f, l] 1 ) and we couple the walks to make identical moves. In that case, the key part of the loop invariant is:

     Φ ∧ (a ∈ [f, l]) 1 ∧ (b ∈ [f, l]) 2 c 1 -a = c 2 -b l 1 = a ⇐⇒ l 2 = b     
The first line enforces some structural invariant and the second line enforces that both walks make identical moves relative to a and b. The main difficulty is to show that both loops are synchronized. Note that there are two reasons the loop may exit. If l has been incremented, then the increment will be done on both side. Otherwise, if f has been decremented to a + 1, then we have

c 1 = f 1 = a + 2, so c 1 -a = c
∈ [f, l] 2 or a ∈ [f, l] 1 and b + 1 ∈ [f, l]
2 is similar except that we force the walks to be execute in anti-lock-step. Using the rule [Case], we put together these four cases and we conclude by application of the rule for sequence.

Ballot Theorem

So far, we have shown how couplings can be used to prove that a set of program variables is uniformly distributed. Couplings can also be used for showing that two events have the same probability, such as in the following example.

Example 10 (Ballot Theorem). Assume that voters must choose between two candidates A and B. The outcome of the vote is n A votes for A and n B votes for B, with n A > n B . Assuming that the order in which the votes are cast is uniformly random, the probability that A is always strictly ahead in partial counts is

(n A -n B ) /(n A +n B ).
The process can be formalized by the program from Fig. 6 6. Here we use the list l to store intermediate results. Using l i to denote the i-th element of the list l, the Ballot Theorem is captured by the statement:

∀n A , n B .n A > n B =⇒ Pr s m   1≤i≤n l i = 0 x A = n A ∧ x B = n B   = n A -n B n A + n B . r ← 0; x A ← 0; x B ← 0; l ← ; while |l| ≤ n do r $ ← {A, B}; if r = A then ; x A ← x A + 1; else x B ← x B + 1; l ← l :: (x A -x B )

Figure 6: Ballot theorem

There exist many proofs of the Ballot Theorem; we formalize a proof that is sometimes called Andre's reflection principle. The crux of the method is a coupling proof of the following fact: "bad" sequences starting with a vote to the loser are equi-probable with "bad" sequences starting with a vote to the winner, where a sequence of votes is "bad" if there is a tie at some point in the partial counts. Let φ = ( 1≤i≤n l i = 0) and ψ = x A = n A ∧ x B = n B . The above facts are captured by the pRHL judgment (universally quantified over n A and n B such that n A > n B ):

s ∼ s :

=⇒ ξ where

ξ = (l 1 • l n > 0 ∧ φ ∧ ψ) 1 ⇐⇒ (l 1 • l n < 0 ∧ φ ∧ ψ) 2 .
It follows from the properties of coupling that for every n A and n B such that

n A > n B , Pr s m [l 1 • l n > 0 ∧ φ ∧ l n = k] = Pr s m [l 1 • l n < 0 ∧ φ ∧ l n = k].
In terms of conditional probabilities, we have Pr

s m [l 1 • l n > 0 ∧ φ | ψ] = Pr s m [l 1 • l n < 0 ∧ φ | ψ]
. Now observe that any sequence that starts with a vote to B (i.e. the loser) is necessarily bad. Therefore,

Pr s m [l 1 • l n < 0 ∧ φ | ψ] = Pr s m [l 1 • l n < 0 | ψ].
By the above and elementary properties of conditional independence:

Pr s m [φ | ψ] = Pr s m [l 1 • l n > 0 ∧ φ | ψ] + Pr s m [l 1 • l n < 0 ∧ φ | ψ] = 2 • Pr s m [l 1 • l n < 0 | ψ] .
Note that the probability in the right-hand side of the last equation represents the probability that the first vote goes to the loser, conditional on ψ. This turns out to be exactly n B n A +n B , so we conclude that Pr s

m [φ | ψ] = 2 • n B n A +n B or equivalently Pr s m [¬φ | ψ] = n A -n B
n A +n B as desired. We now turn to the proof of the pRHL judgments. By symmetry it suffices to consider the first judgment. Using the rule of consequence and the elimination rule for universal quantification, it suffices to prove for every i:

s ∼ s : =⇒ l 1 1 • l n 1 > 0 ∧ l i 1 = 0 ∧ ψ 1 ⇒ l 1 2 • l n 2 < 0 ∧ l i 2 = 0 ∧ ψ 2
We couple the samplings of x using the negation function until |l| = i, and then with the identity bijection. This establishes the following loop invariant, from which we can conclude:

(∀j ≤ i. l j 1 = -l j 2 ) ∧ l i 1 = l i 2 = 0 ∧ (∀j > i. l j 1 = l j 2 ).

Independence

We now turn to characterizing probabilistic independence using couplings. We focus on probabilistic independence of program variables, a common task when reasoning about randomized computations. In our setting, the textbook definition of probabilistic independence can be cast as follows:

Pr µ   1≤i≤n x i = a i   = 1≤i≤n Pr µ [x i = a i ] .

Characterization

Our first characterization of independence is based on the observation that uniformity entails independence.

Fact 12 (Independence from uniformity). From every state m, if X is uniformly distributed in s m then X is independent in s m .

This observation enables proving independence by coupling, in the special case where variables are uniform and independent. For the general case, we will use an alternative characterization based on self-composition.

Proposition 13 (Independence by coupling). The following are equivalent:

1. for every state m, X is independent in s m ; 2. the following judgment, between a single copy of the program on the one hand and a n-fold copy on the other hand, is derivable for every (a 1 , . . . , a n ) ∈ A 1 × . . . × A n :

s ∼ s n : EqMem 1 , n =⇒ 1≤i≤n x i 1 = a i ⇐⇒ 1≤i≤n x i i 2 = a i .
Proof. The validity of the universally quantified pRHL judgment is equivalent to the following statement: for every a 1 , . . . , a n and n-fold copy m n of some initial state m,

Pr s m   1≤i≤n x i = a i   = Pr s n m n   1≤i≤n x i i = a i   = 1≤i≤n Pr s m [x i = a i ] .
The last equality comes from the property of n-fold self-composition (Proposition 6 6).

Pairwise Independence of Bits

Our first example is a well-known algorithm for generating 2 n pairwise independent bits. The algorithm first samples n independent bits b 1 . . . b n , and then defines for every subset X ⊆ {1, . . . , n} the bit z X = i∈X b i .

for i = 1 to n do b i $ ← {0, 1}; for j = 0 to 2 n -1 do z j ← k∈bits(j) b k ; We can prove pairwise independence of the computed bits, i.e. for every X = Y , z X and z Y are independent. Since there are 2 n subsets of {1, . . . , n}, this gives us 2 n pairwise independent bits constructed from n independent bits. The algorithm is encoded by the program s in Fig. 7 7, where bits maps {0, . . . , 2 n -1} to a subset in P({1, . . . , n}) of positions that are 1 in the binary representation, and for i = a to b do s is usual syntactic sugar for while loop with an incrementing counter i. By our characterization based on self-composition, pairwise independence of z j and z j for every j = j is equivalent to the (universally quantified) pRHL judgment

s ∼ s 1 ; s 2 : =⇒ z j 1 = a ∧ z j 1 = a ⇐⇒ z 1 j 2 = a ∧ z 2 j 2 =
a . Since j = j , the two sets bits(j) and bits(j ) must differ in at least one element. Let k 0 be the smallest element in which they differ. Without loss of generality, we can assume that k 0 / ∈ bits(j) and k 0 ∈ bits(j ). The crux of the proof is to establish the following judgment:

s l ∼ s r : =⇒ z 1 = a ∧ z 1 = a ⇐⇒ z 2 = a ∧ z 2 = a where z = k∈bits(j) b k , z = k∈bits(j ) b k and z = k∈bits(j ) b k and s l = for i ∈ [1 . . . n] \ k 0 do b i $ ← {0, 1}; b k0 $ ← {0, 1} s r = for i ∈ [1 . . . n] \ k 0 do (b i $ ← {0, 1}; b i $ ← {0, 1}); b k0 $ ← {0, 1}; b k0 $ ← {0, 1}.
This is proved by coupling the variables of the two programs in an appropriate way. We couple the random samplings as follows:

• for every k = k 0 , we couple b k 1 and b k 2 using the identity sampling;

• we use the Rnd-R rule for b k 2 for every k = k 0 ;

• we couple b k0 1 and b k0 2 with the bijection which ensures

b k0 1 ⊕   k∈bits(j )\{k0} b k 1   = b k0 2 ⊕   k∈bits(j )\{k0} b k 2   .
Putting everything together, the final proof obligation follows from the algebraic properties of ⊕.

k-wise Independence

The previous example can be generalized to achieve k-wise independence for general k. Suppose we wish to generate n random variables that are k-wise independent. We will work in Z/pZ, the field of integers modulo a prime p, such that k ≤ p. Let a 0 , . . . , a k-1 be drawn uniformly at random from Z/pZ and define the family of random variables for every m ∈ {1, . . . , n}:

x m = k-1 j=0 a j • m j ,
where we take 0 0 = 1 by convention. The corresponding code is given in Fig. 8 8. Then, we can show that any collection of k distinct variables {x i } i is independent.

for i = 1 to n do a i $ ← Z/pZ; for m = 0 to n -1 do x m ← 0; for j = 0 to k -1 do x m ← a j • m j ; Figure 8: k-wise independence
For simplicity, we will show that the first k elements x 0 , . . . , x k-1 are uniform, and hence independent. Let v 0 , . . . , v k-1 ∈ Z/ nZ be arbitrary elements of the field. Then the probability that (x 0 , . . . , x k-1 ) = (v 0 , . . . , v k-1 ) is equal to p -k . Indeed, the equations

     v 0 = a 0 . . . . . . v k-1 = k-1 j=0 a j • (k -1) j
define a system of linear equations with variables a 0 , . . . , a k-1 . By basic linear algebra the system of equations has a unique solution for the variables a 0 , . . . , a k-1 , 1 1 which we denote (v * 0 , . . . , v * k-1 ). Now consider the pRHL judgment that establishes uniformity:

s ∼ s : =⇒ x 0 1 = v 0 ∧ • • • ∧ x k-1 1 = v k-1 ⇐⇒ x 0 2 = w 0 ∧ • • • ∧ x k-1 2 = w k-1
By applying (relational) weakest precondition on the deterministic fragments of the program, the judgment is reduced to

s ∼ s : =⇒ a 0 1 = v * 0 ∧ • • • ∧ a k-1 1 = v * k-1 ⇐⇒ a 0 2 = w * 0 ∧ • • • ∧ a k-1 2 = w * k-1
We then repeatedly apply the rule for random sampling, with the permutation on Z/pZ that exchanges (v * i , w * i ).

6 Conditional Independence Definition 14. Let X = {x 1 , . . . , x n } be a set of program variables of types A 1 , . . . , A n and let E be an event. We say that X is independent conditioned on E in a distribution µ ∈ D(State) iff for every (a 1 , . . . , a n ) ∈ A 1 × . . . × A n :

Pr µ   1≤i≤n x i = a i E   = 1≤i≤n Pr µ [x i = a i | E] .
(For this definition to make sense, we are implicitly assuming that Pr µ [E] = 0.)

1 Let the Vandermonde matrix V (1, . . . , k -1) = i j-1 i,j be V (1, . . . , k -1) • (a 0 , . . . , a k-1 ) T = (v 0 , . . . , v k-1 ) T .

The system of equations has a unique solution if and only if the matrix V (1, . . . , k -1) is invertible in the space of matrices over Z/ nZ , which happens if and only if its determinant is non-zero mod n. Expanding, det(V (1, . . . , k -1)) = i =j

(i -j) = k-1 i=2 i!
Note that p does not divide the determinant by Gauss' lemma, since n can't divide any of the terms i! for any i < n. Therefore, the system of equations has a unique solution.

Formalization

EasyCrypt [3 3, 4 4] is an interactive proof assistant that supports reasoning about (relational) properties of probabilistic programs, using the pRHL logic. We have applied EasyCrypt to the main examples of this paper. For uniformity, it suffices to establish the required pRHL judgment; in contrast, independence via self-composition requires to build the self-composed program, which we have done manually. The main challenges for the verification are:

1. Restructuring the code of the program to make the rules of the logic applicable; this is done by applying the equivalent of the [Struct] rules.

2. Discovering and establishing the correct proof invariants. The current version of EasyCrypt requires that invariants are produced by the users.

3. Building an appropriate coupling, primarily applying the rule for random samplings with carefully chosen bijections.

Our examples are formalized in about 1,000 lines of proof script in EasyCrypt. 2 2 The most complex example, and the one where the three challenges are most pronounced, is the random walk over a cycle. This example is formalized in about 500 lines of EasyCrypt code, out of which the statement, including the definition of the program, takes about 50 lines. The remaining 90% of the formalization covers the notions used in the proof and the proof itself.

Conclusion

We have proposed a new method based on probabilistic couplings for formally verifying uniformity and independence properties of probabilistic programs. Our method complements the existing range of techniques for probabilistic reasoning, and has many potential applications in program verification, security, and privacy.

  s m [x = a] = f (a), Pr s m [y = b] = g(b), Pr s m [x = a ∧ y = b] = h(a, b). Then, independence between x and y holds by proving that h(a, b) = f (a) • g(b) for every a ∈ A and b ∈ B.

  and Pr s2 m 2 [y 2 = b]. Since s 1 and s 2 are just renamed versions of the original program s, these probabilities are in turn equal to Pr s m [x = a] and Pr s m [y = b] in the original program.

Figure 1 :

 1 Figure 1: Denotational semantics of programs

Fig. 2 2

 2 Fig.22 presents the main rules of the logic; see Barthe et al.[1 1, 7 7] for the full system. The logic includes two-sided rules, which operate on both programs, and one-sided rules, which operate on a single program (left or right).The[Conseq] rule is the rule of consequence, and reflects that validity is preserved by weakening the post-condition and strengthening the pre-condition. The [Case] rule allows proving a judgment by case analysis; specifically, the validity of a judgment with pre-condition Φ can be established from the validity of two judgments, one where the pre-condition is strengthened with Ξ and the other where the pre-condition is strengthened with ¬Ξ.The [Struct] rule allows replacing programs by provably equivalent programs. The rules for proving program equivalence are given in Fig.33, and manipulate judgments of the form Φ c ≡ c , where Φ is a relational assertion. The first rule ([While-Split]) splits a single loop into two loops (the first running while e is true, and the second running for the remaining iterations); this transformation is useful for selecting different couplings in different program iterations. The second rule ([Swap]) reorders two instructions, as long as they modify disjoint variables. This allows us to couple sampling instructions that may come from two different parts of the two programs.Moving on to the two-sided rules, the [Seq] rule for sequential composition simply reflects the compositional property of couplings. The [Assg] rule is standard. The[Rand] rule informally takes a coupling between the two distributions used for sampling in the left and right programs, and requires that every element in the support of the coupling validates the post-condition. The rule is parametrized by a bijective function f from the domain of the first distribution to the domain of the second distribution. This bijection gives us the freedom to specify the relation between the two samples when we couple them. The [Cond] rule states that two synchronized if statements can related if their respective branches are also related. The [While] rule is the standard while rule adapted to pRHL. Note that we require the guard of the two commands to be equal-so in particular the two loops must make the same number of iterations-and Φ plays the role of the while loop invariant as usual.The one-sided rules Assg-L, Rand-L, Cond-L and While-L are similar two their two-sided variant, but only operate on the left program. The full system includes mirrored versions of each one-sided rule, for reasoning about the right program.Throughout the paper, we often assert that the left and the right copies of a state are equal. This is captured by the relational assertion EqMem = x∈X x 1 = x 2 . We also often assert cross-equality on n-fold composition of states EqMem p , q = x∈X ,1≤ı≤p,1≤≤q x ı 1 = x  2 .

Figure 2 :

 2 Figure 2: Proof rules (selection)

Figure 3 :

 3 Figure 3: Equivalence rules (selection)

Figure 4 :

 4 Figure 4: Bernoulli uniformizer

Figure 5 :

 5 Figure 5: Cyclic random walk

2

 2 -b = 2 and c 2 = b + 2 and the right loop will also decrement f to b + 1. The case a + 1 ∈ [f, l] 1 and b + 1 ∈ [f, l] 2 is very similar, by reversing the roles of f and l. The remaining two cases, a + 1 ∈ [f, l] 1 and b

Figure 7 :

 7 Figure 7: Pairwise independence

Finally, we consider

  how to show conditional independence. Recall that the conditional probability Pr x∼µ [A | B] is defined when Pr x∼µ [B] = 0 and satisfies Pr x∼µ [A | B] = Prx∼µ[A∧B] Prx∼µ[B] .

  Definition 11. A set X = {x 1 , . . . , x n } of program variables of types A 1 , . . . , A n is probabilistically independent in a distribution µ ∈ D(State) iff for every (a 1 , . . . , a n ) ∈ A 1 × . . . × A n :

Proofs are available at the following link: https://gitlab.com/easycrypt/indep https://gitlab.com/easycrypt/indep

Acknowledgments

We thank the anonymous reviewers for their detailed comments. This work was partially supported by NSF grants TC-1065060 and TWC-1513694, by the European Union's H2020 Programme under grant agreement number ICT-644209, and a grant from the Simons Foundation (#360368 to Justin Hsu).

The following lemma unfolds the definition of conditional independence and is useful for the characterization of the next section. Lemma 15. A set of variables X is independent conditioned on an event E in µ iff for every

Characterization

The characterization of independence based on self-composition can be extended as follows.

Proposition 16 (Conditional independence by coupling). The following are equivalent:

1. for every state m, X is independent conditioned on E in s m ;

2.

Proof. The proof is similar to the case of independence (Proposition 13 13).

6.2 Example: Conditional Independence We consider a simple example often used to illustrate Bayesian networks models. Let x, y, z, w and w be random variables, where x, y and z are sampled from distributions µ, µ and µ respectively, and w and w are defined by their respective assignments. Both w and w depend on y, along with independent sources of randomness, respectively x and z. While w and w are not independent-they share dependence on y-if we condition on a particular value of y, then w and w are independent.

The code of the corresponding program s is given in Fig. 9 9. We want to show that w and w are independent conditioned on y = c for every c. Using our characterization based on self-composition, it amounts to proving the following (universally quantified) pRHL judgment:

The proof proceeds by moving the samplings of z 1 and z 2 in both programs to the front of the program, and then swapping samplings in the left program (we can use the rule [Swap] to reorder the instructions, as the sampling instructions for z 1 and z 2 operate on different variables). Then, we couple z 1 1 to be equal to z 2 2 , and z 2 1 to be equal to z 1 2 . We apply the identity coupling to all other random samplings.


Gahitte Agnès

Jean Christophe

AXIOMATICS AND CONSTRUCTION OF THE CENTRAL PLACE SYSTEM

Keywords:

The construction of the loschian landscape is a basic element in the Theory of Economic Regions. It is based on an hexagonal lattice and loschian numbers having properties used by DACEY (10,11,12,13) and MARSHALL (16,17,18,19,20). In fact, the former has not tested his model. In this paper our purpose is to prove that DACEY failed to build mathematically the Central Place System, and to propose a new method of construction of the loschian landscape.

INTRODUCTION CHRISTALLER (8 ) has created the Theory of Economic

Regions and LÖSCH (15) has developped it before the second World War, second chapter of his reference book : "The Economics of Location". TARRANT [START_REF] Tarrant | Comments on the LOSCH Central Place System[END_REF] has endeavored to show how it is possible to develop the löschian landscape on a rhombic lattice using non orthogonal reference axes.

Next to him, two different "schools" (BEAVON and MABIN (4,5,6,7), later on BEAVON (1,2,3) and MARSHALL (16,17,18,19)) began to deal with the same subject. MARSHALL (17) asserted that LÖSCH's single good model was too restrictive.

The aim of this paper is not to question the löschian Theory of Regions but to explain its construction. Of course, we could blame LÖSCH (15) for his lack of explanation concerning the structure of his landscape. A number of authors have ignored the problem in putting that part of the theory aside. MARSHALL(17,18,19,20) has constructed a landscape which is not a löschian one because its elaboration doesn't respect location and maximisation constraints enforced by LÖSCH (15). Then he denies the existence of alternating city rich and city poor sectors but his claim doesn't disturb the löschian scheme... In fact DACEY (10,11,12,13) in 1964 has been the forerunner of a strictly mathematical approach of this theory. He has worked out the first postulates which allow us to formulate the Central Place model, and has transformed a concealed structuration into an adequate mathematical language : mathematics revealed to be an effectual implement.

Farms have in this framework analysis equivalent properties to those of points in an hexagonal lattice, basis of the system. The number of farms completely supplied is characterized by a löschian number provided with properties of Number theory (10,11,16). To fix this number comes to the same thing as to resolve a Diophantine Equation, which uses integers only. In "Geometry of Central Place Theory" DACEY (12,p 120) has restated the essential elements of LÖSCH ' s argument and summarized the most important properties of the Central Place System. Our purpose is specially to examine the algorithm T5 (12, pl20). DACEY asserts that it must be able to give the primitive function point n(n+z). An attempt will be made here to prove that this method is not efficient to locate some centers of market areas. The mathematical proof will be given just as examples. These one will show that it is impossible to make a choice between several function points of the form n(n+z) in using T5.

A constructive solution allowing a logical construction of the landscape must be treated by computer.

1 2 ' ' v ' 1 ' 2
The plane is constructed as a linear lattice having translation period repeated at an interval t (with n t i i = 1 et i i t i i = 1 ).

2

In the lattice we use an angle of periodic rotation of n/3, t Ot = IT/3 (see figure 1). We get six sextants which cover the plane. If we note c p the six sextants we defined the lattice points P by : A parallelogram is formed by four points 0,X,XY,Y. The translation T = (X,Y) changes it into another one having point T' as first vertex (see figure 3). By joining the vertices X and Y of that reduced parallelogram and the two vertices corresponding of each "répliqua" we get six identical triangles whose vertices are the lattice points and have non obtus angle. If we connect the circumcenters of these six equilateral triangles we obtain a Dirichlet region : a polygon that contains a lattice point at its center and every point of the plane is closer to that lattice point than to any other lattice point.

The loschian system is developped on a six fold axis, for this axis the primitive Dirichlet region is always a regular hexagon which contains a lattice point as center.

Definition

The fundamental region of a plane is a parallelogram which has four lattice points for its vertices and no other points on its edges or faces. Such a region is defined by the points : that region has a lattice point at its center and one or more other points within its interior, on an edge or at a vertex. Each Dirichlet region is identified by degree. A region is said to have a degree q if the sum of the three following values equals q : i) the number of lattice points interior to the region ii) one half the number of lattice points on edges of the region iii) one third the number of lattice points at vertices of the region. A point that is interior to a Dirichlet region, including the center, is said to belong to that region. { u i t + v j t }, sublattice which includes the origin 0 . We can show by induction that the number of points in each region having as center (i,j) is given by :

-► -♦ -► -► -► -♦ -► -♦ 1 \ + J V (i+1) \ + J
kij = i2 + ij + j2 -► -t
kij is called the order of the regions defined by {uit + v j t } and by any Dirichlet region determined by a vector of the1 form 2 i t^ + j t is called a first degree region.

Permissible orders of Dirichlet regions of degree 1

The order of a first degree region is by kij, Location of a point which is the center of Dirichlet region of order kij and adjacent to a region of same order centered in 0(0,0) is obtained in substituing in i ^ + j t every (i,j) (ie N, j e N) satisfying i2 + ij + j2 . For each (i,j) centers of these regions are determined by rotation and translation of the vector (i,j).

124 Orders of separable first degree regions.

An interesting collection of first degree Dirichlet regions having important economic implications to LOSCH's Theory of central Place are those orders in which all the lattice points are interior to a region, that is no lattice points are located on edges or at vertices of this region. This system is called separable Dirichlet regions. A separable region cannot be located on X axis or on a secondary symmetry axis (i=j). The number of points in a separable region must, to retain symmetry, be an integer multiple of six plus an additionnal center point. All centers of theses regions of

-♦ -♦
degree 1, noted { u i t + v j t }, are given by rotation and translation of (us, vs) for which the following three conditions hold: kij = 6z + 1 z e N* j * i I j J * 0 We can also see that t = ajn (a=l the distance between two lattice points is unitary). We can say that an integer is a loschian number, if and only if, its factorization satisfies the condition such as the prime number 2 and all the prime numbers of the form (6x-l) have even power. The proof of this assertion is given by MARSHALL (16, p422) and GAHITTE (22bis). A loschian number is also an integer as 3 or every prime number of the form (6x+l) having even or odd power. In fact we have prooved that an integer n such as n = i2 + ij + j2 is loschian if its factorization in prime numbers (as 2 or every prime number of the form 6x-l) is such as these numbers have odd power, and 3 or prime numbers of the form 6x+l have even or odd power.

Then we can conclude that not only loschian numbers have this kind of factorization, but every integer having this kind of factorization is a loschian number. See table 1.

PI:

At least one lattice point in HN is the center of the Dirichlet region with degree q, q<N. P2:

if any lattice point in HN is assigned to a Dirichlet region with degree q, then every lattice point in HN is assigned to exactly one Dirichlet region with degree q. P3:

There is at least one sector of n/6 radians with locus at any lattice point (i,j) that contains at least one vertex of each Dirchlet region with center (i,j ). Al:

The origin of the lattice is the center of Dirichlet regions with degree q, q<N. This assumption is valid only if it exists a lattice point which is the center of a Dirichlet region in each tessalation occuring in HN. Tl:

There exist at least one lattice point which is the center of Dirichlet regions with degree q, q e { q },q<N.

Dl

D4: definition of order :

A point that has function n, n< n ', n, n ' e { q } have order n. if (i,j) has order n and no other order n point is closer to 0(0,0), then (i,j) is a primitive order n point.

Some properties of the Central Place system HN

LI:

The value of q is an element of the set { q } = {i2 + ij + j2} i e N, j 6 N.

L2:

If N and N+z, z e N, and no integer between N and N+z, N+z is an element of { q }, then all system Hz for which N<Zl<z are identical. (1) when there is a single solution, the center of the DIRICHLET region will be located in (i,j ). This one will have an order kij. To locate centers of DIRICHLET adjacents regions primitive function point is displaced in the lattice with vectorial translation of what we call "primitive" vector (i,j) till a fixed couple of coordinates (in our case (50,50)). The part obtained after (k-1) translations is noted A 1 = k (i,j), this point is again displaced in the lattice by rotation of n/3 angle, it means that point A" image of A' by that rotation is get as follows :

A2

0 1 0 1 A" = A' -1 1 = k (i,j) -1 1
A" is again translated by (i,j) we get point A''' such as A''1 = (-kj + i, ki + kj + j) till (50,50). Thus we obtain all the centers of adjacent Dirichlet region of function n. The points which are neither perfect squares nor multiple function points and which after this last translation have negative abscissa are rotated of -n/3 angle. In this case the matrix is 1 -1 1 0

The points obtained are then translated with the primitive vector (i,j)•

(2) when the solution is not unique the point is located prioritary where the maximum of points are already located (whatever the way they have been obtained). These points are previously the centers of function n and n+z. If there is the same number of centers we must choose the point which has the higher order.

For example n(n+z) = 9 1 , two points are possible (6,5) and (9,1). In (6,5) there is no center of DIRICHLET region and in (9,1) there is one center of function n = 7. For n(n+z) = 273 we must choose between (11.8) and (16,1). In (11,8) there are three regions of function n = 3, 13, 21 then in (16,1) there is n = 3, 7, 13 therefore we choose (11.8 ).

(ii)

the second one (case 2) chooses the primitive function point having the higher abscissa in the same situation as (i ). then according as the choice wich is made the landscape will be modified (table 2). For i < 50 (i e N) and j 1 50 (j e N), if we choose the point having the smaller abscissa (case 1) we locate 13 supplementary centers of region in the city rich sector (PI) than if we choose case 2.

Figure 1 :

 1 Figure 1 : Hexagonal lattice used in the Central Dlace Sys tem.

Figure 2 :Figure 3 :

 23 Figure 2 : Coordinates of the typical parallelogram™.

  If 0(0,0) and any other point (i,j) are centers of two adjacent multiple Dirichlet regions they define a unique set of regions, because by rotation and translation (i,j) is carried into the lattice other point is the center of that Dirichlet region. Because of the symmetry of the lattice, the hexagons have identical area and contain identical numbers of lattice points, when they belong to the same set of regions

  ij + j , a positive integer; however not all integers values occur as permissible orders for first degree regions. The set of integers { k } which are orders of first degree regions is given by { k } = { i2 + ij + j2 } i>j and i>l.

Figure 4 :Figure 5 :

 45 Figure 4 : Superposition of three Dirichlet regions of order 7, 13, 19.

For example 2692 is a loschian number because 2692 = 22

 22 Diophantine equations n = i + ij + j we only can use iterative process. The construction of the loschian landscape (the test of the model) needs some postulates and definitions (DACEY(12). We note HN the Central Place system, it contains a set of Dirichlet regions for each degree lower than N.

  : definition of the function of a point : a point which is the center of a Dirichlet region with degree n has a function n. D2: definition of a primitive point : if (i,j) has the function n and no other function n point is closer to the origin point 0, (i,j) is a primitive function n point. D3: definition of multiple function : a point that is the center of Dirichlet regions of degrees n and (n+z), z e N, have function n(n+z).

"

  : N e { q }. The sublattice PI is partitionned into two sector of n/6 radians. These two 30°sectors are identified as the upper half of PI and the lower half of PI, labeled Pu and PI. Boundaries between Pu and PI are defined by secondary axis (i = j ) of PI. If (i,j) e PI then (i) (i,j) is interior to Pu if i>j>0 (ii) (i,j) is interior to PI if j>i>0 (iii) (i,j ) is on one edge if i=0, j=0 ou i=j A3: The PI does not contain any vertex of a Dirichlet region with center n+zIN and that n e { q }, then the primitive function n(n+z) point exists. Further the primitive function (n(n+z)....n+z') point exists if and only if, n, n+z,..n+z'<N and n,n+z...n+z' are all elements of { q }. 2 Location of the multiple function point. 21 Theorical review of DACEY's algorithm During the construction of the loschian Central Place system we must locate what DACEY calls the "primitive function points" Suppose that (i, j ) is a primitive function n point which is the center of a Dirichlet region (n = i + i j + j ). We must consider three cases (i) n is a prime number (ii) n is a perfect square (iii) n is a multiple function point neither prime number nor square. This last case is treated by DACEY (12, p 120) with the algorithm T5. 211 Terns of the algorithm T5 : Assume (i,j) and (h,k) are respectively primitive function n and n+z points. The primitive function n(n+z) point is located at (r,s) where s e N, r e N given by the equations : (4) r = [ ah + £(h+k) ] = [ yi + S(i + j) ] s = [ ak -(Sh ] = VJ " Si a and \ are positive integers and @ and 5 are integers subject to the conditions : (a) p(hk + h2 + k2 ) = \(ik -hj ) + S(ik + jk + ih) 't know an efficient algorithm. Also, the solution is not necessary unique. When (4) is solved iteratively the following inequalities may be used. (c) -ah < p < ak and a By repeated appications of T5 to pairs of functions an expression is obtained that gives coordinates of primitive points with multiplicity greater than 2" DACEY (12, p 120). 212 Discussion of the algorithm. In fact to resolve this system we must change it into an homogeneous one. We must find a, p, \, 6, and not r and s. r and s are known, we can find them in solving the next equations : n + z = h2 + hk + k2 .2 , . . . .2 n = i + i j + j n(n+z) = r2 + rs + s2 If (h,k) and (i,j) are known then n + z, n and so n(n+z) are known too n(n+z) = (h2 + hk + k2 ) (i2 + ij + j2 ) = r2 + rs + s2 The new system can be written as : f ah + ( 3 (h+k) -\i -S(i+j) the first equation (by k) and of the second one (by h) and by subtraction of them we obtain : <==> pk (h+k) -Yik ~ 5k(i+j) + ph + Yhj -Sih = Q £( kh + h2 + k2 ) = y ( ik -h j ) + 5 ( ki + k j + ih)which is exactly equation (a). a is obtained by transposing (3, y , 5 in the second equation of (7). We can see that (a), (b) are redundant equations relatively to the system (6). It was not necessary to introduce them next to (4). We solve (6) by linear combination of the last two equations, a minimization criterion. The required set of values is that which minimizes (\2 + y5 + S2 ). We can demonstrate that this criterion is not able to allow a choice between more than two multiple primitive function points :

  use (\2 + \5 + 52 ) as a minimization criterion is equivalent to use n + z . Now as r and s verify n( n+z) = r2 + rs + s2 , in many cases the choice between numerous multiple primitive function points n(n+z) will be impossible because they will have the same n+z. For example : if n(n+z) = 273 two solutions exist (11,8) and (16,1) with n =3 and n+z = 91. For those points it is not possible to determine the optimal point. The same argument can be applied to a2 + ap + p2 if we choose it as a criterion of maximization or minimization. 2122 Inequality constraints Concerning inequality constraints (5) we can prove that they are always true whatever the values of r, s, i, j, k, h, n, n+z. Proof : the first inequality constraint c) become : 4), n = 21, i = 4, j = 1, n+z = 28, h = 4, k = 2, if we take DACEY's minimization criterion this solution will be preferred to the other because n+z = 28 we get a=-5, £=-1, \ =6, 6 =-2 with -10 < -1 < -1

  n = 4, i = 2, j =0, n+z = 147, h = 11, k = 2, this solution will not be taken into account because it does not minimize n+z, we obtain a = 2, p = 0, \ = 13, 5 + 5 , in any constraints are always verify. We can find cases for which the criterion is respected and the constraints always checked, the choice is then impossible. If we take n(n+z) = 868 the solutions are (18,16) and (26,that (18,16) and (26,6) are equivalent points, but it is incorrect ! The conclusion can be the following one T5 is an inefficient algorithm because . some of the equations are redundant the minimization criterion is incorrect because we can not choose between primitive function points . inequality constraints are inefficient because they are always true when r e N, s e N.

Figure G :

 G Figure G : Location of centers of Dirichlet regions in the Central Place System.

Figure 7 :

 7 Figure 7: Superposition of three market areas :(N02,N°2,N°5)

- 4

 4 In 1965 DACEY(11) has written " when the vector cij such as : t + j t and the point 0 (0,0) are located and are the centers of adjacents DIRICHLET regions of degree n, by rotation of U/3 and translation of the vector (i,j) points of the lattice cp^ { cij } are obtained and are the centers of these regions".The strict application of this rule is unable to determine the landscape constructed by LOSCH.31 Explanation of the location of the pointsThis method must allow us to locate all the solutions (i,j) of the Diophantine equation :, . .

  the number of coinciding centers is the same and when they have the same functions (for example n(n+z) = 169 located in (8,7) or in (13,0) where is already the point of function n = 13). In fact no criterion can allow us to choose because the works of LOSCH are of no help (15) : "First we lay the nets so that all of them shall at least one center in common. Here a metropolis will arise.. .Second, we turn the nets about this center so as to get six sectors with many and six sectors with only a few production sites. With this arrangement the greatest number of location coincide..." These conditions are respected for two points (8,7) and (13,0) for the function n(n+z) = 169. This is not the single one and its location will influence the one of multiple function of 169: For example n(n+z) = 7x169 = 1183, the primitive function point 1183 can be located in (26,13), (29,9) or (31,9). If we locate the center of DIRICHLET region of order 169 in (8,7) the center of order 1183 region will be located in (26,13) as will as those of order 7, 13, 91, in (29,9) there is no center except the one of order 1 located everywhere in the lattice; in (31,9) we get the point which is the center of the region of order 1321. But if we locate the center of the DIRICHLET region of order 169 in (13,0) the region of order 1183 will be centered in (26,13) as the regions of function 7,13,91,169. In (29,9) there is a point of order 1, in (31,9) is centered a region of order 1321. We can identify two cases : (i ) the first one (case 1) chooses the primitive function point having the smaller abscissa, when at least two points have the same number of coinciding centers with the same function.

When this region has the shortest possible sides we call it reduced parallelogram. Dirichlet region is a reguler hexagon whose interior consists of all points in the plane which are closer to particular lattice point than to any other lattice point. The set of Dirichlet regions (each of them surrounding a lattice point) exhausts the plane without overlapping. The fundamental or primitive Dirichlet region contains only one lattice point, which is the center of each region, and is called a region of degree 0 and order 1. The concept of Dirichlet region may be extended to polygons containing more than one lattice point, and such a region is called a multiple Dirichlet region :

	t 2; 1 \ + (J+1) t 2; (i+1) \ + (J+1) \

Table 1 : new test of T5 for n(n+z) = 399, aeR, p e R , \eR, SeR z s n( n+z) n n+z

 1

				a	P	Y	6 a+p	Y+S	-a/P Y/S a-p Y-tt
	13 10	399	3 133 1,86 -0,29 11	1	1,57 12	6,41 11	2,1 10
	13 10	399	3 133 1,98 -0,73 11	1	1,25 12	2,71 11	2,7 10
	13 10	399	7 57 3	1	8	-1 2	7	3	-8	4	9
	13 10	399 19 21 4,86 -1,29 4,6 0,2 3,57	4,89 3,76 22, 6,1 4,
	17	5 399	3 133 1,64 0,14 9 4	1,78 13	11,7 2,2 1,5 5
	17	5 399	3 133 1,86 -0,29 9	4	1,57 13	6,41 2,2 2,1 5
	17	5 399	7 57 2,79 -0,32 7	1	2,47	8	8,71 7	3,1 6
	17	5 399 19 21 4,43 -0,14 4	1	4,29	5	31,6 4	4,5 3

If we only use the minimization criterion of DACEY (13,10) on line 4 and (17,5) on line 8 are possible and if we impose criterion 1 the choice proceeds on (17,5) when the solution is (13,10). If we maximize a + p it is insatisfactory because we will choose (17,5). A lot of other examples can be given revealing the same inefficiency. In view of these results we have forsaken the algorithm. Then, it was necessary to propose a new method of construction of the loschian landscape based on concepts set up by DACEY. 3 New method of elaboration of the Central Place System To throw out the algorithm doesn't mean that all the postulates and definitions of DACEY are incorrect.

table 2 : Differences between case 1 and case 2

 2

		C£ ise 1 (8, 1 r... 7)	... 1 cas>e 2 ( 13, 0)
	max (i,j)	nb pts	nb pts		nb pts	nb pts	nb pts	nb pts
		I > J	I = J		I < J	I > J	I = J	I < J
	(50,50)	3731		412		2870	3709	418	2873
	(100,100)	16378		1011		13109	16295	1032	13129
	(150,150)	38542		1674		31414	38378	1716	31456
	(200,200)	70608		2407		58199	70304	2468	58292
	(250,250)	112610		3152	w T__	93645	112150	3236	93770
		I ca£ U i -( D	00	_____ r .... ... n	I cas i se 2 (13,( I i ))
	max (i,j ) nb pts	nb pts	casl / 2	cas 1 /2	cas 1 /2	cas 1/2
		E cas 1	E cas2	I > J	I = J	I < J	E
	(50,50)	7013		7000		22	-6	-3	13
	(100,100)	30498	30456		83	-21	-20	42
	(150,150)	71630	71550		164	-42	-42	80
	(200,200)	131214 131064		304	-61	-93	150
	(250,250)	209407 209156		460	-84	-125	251

remarques : I < J city poor sector I > J city rich sector I = J city rich and poor sectors boundary

CONCLUSION

This paper has provided a new method of construction of the loschian landscape and has proved the inefficiency of an algorithm elaborated by DACEY. Our system is based on translations and rotations. To settle the mosaic of Dirichlet regions two cases must be distinguished.

(i) if (i,j) is a primitive function point such as j =0. Then we must translate this point with a "primitive" vector (i,j) till a fixed point (50,50) for example. The point obtained is rotated with an angle of n/3, the matrix transformation is 0 1 -1 1 this point must again be translated with the primitive vector (i,j) till (50,50).


E Billot

Distribution of Power and Social Utility under Nonadditive Aggregation Rules An t o in

social decision rules (Bandyopadhyay, Deb & Pattanaik 1982, Barberà # Valenciano 1983, Heiner & Pattanaik 1983). The restrictions on coalitional power derived in all of them relate to the power of coalitions to influence social probabilities over two-element feasible sets only. As noticed by Pattanaik & Peleg 1986, all these authors adopted a formulation in terms of probabilistic social preferences and not in terms of probabilistic social choice. Basically, Barberà & Sonnenschein 1978 show that every binary and Paretian method for passing from preference profiles to lotteries over preferences is associated with a subadditive function on the set of coalitions of individuals. This function gives the power of each coalition in order to secure its preference for any pair of alternatives. McLennan 1980 proves this power function to be strictly additive, i.e. probabilistic, whenever there are six or more alternatives. Also, as indicated by both Barberà & Sonnenschein 1978 and McLennan 1980, Butters proves by another way the converse of Barberà & Sonnenschein's Theorem is valid when the set of alternatives does not exceed five. This methodology depends on the view that admitting as social preferences lotteries on preferences over the basic alternatives increases the possibility for satis factory preference aggregation. Nevertheless, they show that the dimensions of this increase are limited and they come to the conclusion that the force of Arrow's Theorem is not diminished. Originally, Arrow tries to consider the only methods which allow passing from social preference profiles to social preference relations while Barberà & Sonnenschein studies methods for passing from social preferences profiles to lotteries over social preference relations (called social welfare schemes). Thus, the latter show that allowing lotteries permits a wide variety of nondictatorial procedures. In return, their paper is a generalization of Arrow's Possibility Theorem 1963 by considering functions which map profiles on individual preference relations into lotteries on the set of preference relations. These functions translate formally the idea of method for passing from profiles to lotteries. They have to satisfy two axioms : binarity and a Paretian property. Binarity is simply a generalization of Arrow's condition of Independence of Irrelevant Alternatives and the Paretian property corresponds to that of Unanimity. In this paper, we try first to shift the problem onto the agents. We want actually to consider some methods for passing from coalitions to lotteries over coalitions. These methods are associated with a function that could correspond to a social utility function. It gives the level of satisfaction coming from the anticipated "consumption" of a subset of alternatives (goods, candidates,..) by a coalition. Second, we want to define the distributions of power regardless of those two-element feasible sets which characterize preferences in basic models on one side, and we try to exhibit a theoretical relation between the basic Barberà & Sonnenschein's model and ours thanks to the Choice Axiom of Luce 1959 on the other side. Third, McLennan's argument against the validity of subadditivity for all power functions, i.e. the number of alternatives, disappears since we can introduce nonadditive lotteries directly from a Generalized Choice Axiom that can be obtained with the introduction of Choquet capacities. These latter, which appeared in Choquet 1953, were introduced in economics by Gilboa 1987 and Schmeidler 1989. They allow to weaken the standard constraints on probabilities in putting a simple condition of monotrmjcity in place of additivity. Finally, we try to prove that it is possible to deduce a ^cial or a coalitional utility function directly from lotteries over preferences in implying a Power Scheme (i.e. a distribution of power decision) from the basic Social Welfare Scheme, this last being probabilistic or non additive. 1. N o t a t io n s a n d D é fin itio n s LetX = (*,)>,z,...} be the set of alternatives and N = { 1 , 2 , n) be the set of individuals. In order to avoid McLennan's limitation of relevance for Barberà &

Sonnenschein 's Theorem, we assume throughout X and N to be finite and we already suppose the number of elements of X as those of N (denoted #X and #N) to be at least six. Let ® = [B, B ', B ,...} be the set of individual strict preference relations (complete, asymmetric and transitive binary relations) on X, and IT, the n-fold Cartesian product of (8, be the set of social preferences profiles. A generic profile is denoted by B = (B^Bp ..,Bn).

A probabilistic lottery on 'B is a probability measure on ' B ; i.e.. a function /(.) : 2® -> [0,1] such that 1(0) = 0, /(«) = 1 and l(S u T)) = l(S)+l(T) -l( S n T ) for all S,T c 'B. Let L(B) be the set of lotteries on 'B. When a probabilistic lottery is defined on a subset T e ®, we note it lT(.). For x ,y e X, let 'B(xBy) = {B e C 8 : xDy}.

For /(.) e L(<8), let p[l(.),xBy] = l(<S(xBy)). It means, for all distinct x ,y , p[l(.),xBy]+ p[l(.),yBx] = 1. Furthermore, given B e « ' , let \f(<B,xBy) = [i e N : xB ,y).

A nonadditive lottery on <8 (resp. /V) is a normalized Choquet capacity on 'B (resp. There is a lot of ways to define these Representatives, from preferences, alternatives or even lotteries. We do not choose here a particular way in order to focus the analysis on the only power decision which comes from leadership.

We could call them natural leaders of A for x (cf. The following properties hold for any restriction of any PS.

APS A (.) is anonymous if for any A, B e 2" such that A, fi c C and for any x e X, "x(A)=x(.B)'' => "p[hc(A),x] = p[hc(B),x]".

A PS h{.) is unanimous if for any A e 2N and for any x e X, "x(A)=Xx" ^" p[h A(A),x] = r \

The first axiom means that the induced power decision of two Representatives must be the same whenever their two coalitions draw the same set of preferred alter natives for a given on e; the coalition must stay anonymous for the distribution of power. The second axiom means that the coalition concentrates all the power on its Representative whenever its collective choices are extremely dispersed; the leadership is strengthened up to an enforced unanimity when choices are totally divided. Another interpretation leads to consider the unanimity axiom in so far as a definition of dic tatorship according to collective choices since the coalition (or the society in the whole) totally deputes its power decision onto its Representative. In and only in the particular case where x (N )= X x, (N,x) is exactly the Arrovian dictator: i.e.

p[hc(A),x] = p[hc(B),.] xp[hB(A),x] i.e., hc(A ,x) = hc(B )xhe(A,x).

This axiom is called the Generalized Choice Axiom (GCA). We call class of distributions all the lotteries which are linked thanks to GCA. We must consider it as a coherence axiom which guarantees partial distributions of power to be relevant with social ones. Furthermore, it is natural to assume the power decision of a given Representative to be weakened inside a wider coalition than his. B,B' e S",a n d x ,y ,e A,y(B ,x B The following theorem and lemmas are completely independent from previous theorems. We try to prove the existence of a social or a coalitional utility (it depends on the support of lotteries) from lotteries over agents in order to pass from coalitions to lotteries over coalitions. This analysis is just the opposite side of the one we treated before, i.e. Barberà & Sonnenschein's one. Actually, we study some social rules dealing with agents but based on alternatives while they study some other rules according to agents behaviors ; their paper comes from preferences to choice prob abilities of preferences when ours comes from agents to power-decision probabilities.

From Preferences to Lotteries over Agents via power

We can notice the dominance lemma to be the dual of nonperversity one in Barberà & Sonnenschein 1978. Identically, the duality lemma is also the dual of neutrality.

/i -Theo r e m : Given an anonymous, unanimous and Lucian PS h(.) ofC(N), there exists a function uk(.) : 2* -» [0,1] such that : VA e 2'v, \/x e X,

uh(x(A)) = p[h(A),x],

(1)

furthermore we have, uh (0) = 0, (2)

ifh (.):^-^L (N ), uh(x(A))+uh(x(A)) = 1, (3) whenever x(A) z> x(B), uh(x(A))>uh(x(B)).

(4)

Remark 6 : From now on, we note PS* any PS which is anonymous and unani mous.

Remark 7 : The function uh{.) is not necessarily additive. This property does not depend on #A even though we assume #Af to be at least six. Actually, if A ciV, #A < #N ; hence #A can be lower than six and we could suppose Barberà & Son nenschein's Theorem to apply. But, uh(.) is directly generated from a lottery. If this last belongs to L(N), then uh(.) is additive. In return, if /i(.) corresponds to a lottery of C(N), then uh(.) can be nonadditive. We want here to analyze the proper influence of the designed lottery without studying that of the set of alternatives. Even if #A is greater than seven, twelve or seventy-two, uh{.) is strictly nonadditive if and only if

h(.) e NAC(N).

The proof of the theorem follows two lemmas.

We suppose here h(.) to be a Lucian PS*. i

Proof: I f x (A )= X x, the

unanimity axiom yields p[hc(A),x] = p[hc(B),y], A similar argument applies if x(A) = 0 , since the preference relations are strict Let us suppose the only proper subsets of X. When proving duality, we have to prove the following monotony: x(A)z> y(A) =* p[hc(A),x] ^ p[hc(A),y]. If x(A) = y(B) => x(A )czx(B ) and y(B) czy(A). From the dominance lemma, we can deduce: hc{A,x) < hc(B ,x) and hc(B ,y) < hc(A,y). Moreover, x(B) z> y(B). The other case (equality) is prohibited by strictness of the preference relations. Let us suppose the following proposition x(B)z>y(B)=* hc(B,x)<hc(B,y). Thus, y (A )z>x(A) => hc(A ,y)<hc(A.,x). Now, hc(A ,y) < hc(A,x) < hc(B,x) < hc(B ,y) which implies hc(A ,y) < hc(B ,y). This is a contradiction with the previous proposition hc(B ,y )< h c(A ,y). Thus, if x(A) = y(B), x(B)z>y(B) =>hc(B ,x)> h c(B ,y). In mixing monotony with anonymity, we can conclude hc(A,x) = hc(B,y).

Q.E.D.

Remark 8 : Both propositions x(B) z> y(B) and y (A) 3 x(A) are obviously true since x(A) = y(B)

and the preference relations are strict.

Because we have proved duality, it is natural to propose a basic definition of uhQ : 2* -¥ [0,1] that one can find in the theorem by uh(S) = p {h(A),x] where * is an arbitrary alternative and A any coalition such that x(A) = S. This expression of «*(.) as a function of alternatives suggests that it could be interpreted as a social utility (if hAQ = /luQ) oracoalitional utility (if hA(.) * hN(.),A * 0 ) for any subsetof alternatives.

Proof of the Theorem : From the basic definition of uh{.), it is clear that uk(.) satisfies (1) and (2). Furthermore, if h(.) e L(N), (3) trivially holds because jc(A)uì(A)=X . Lemma 1 of dominance guarantees that (4) is always satisfied.

Q.E.D.

In order to obtain lotteries over coalitions, the method consists in defining a social or coalitional utility function which allows to pass from coalitions to lotteries. It means that if such a function exists, we can explain the existence of power distributions and then their influence on methods for passing from profiles to lotteries over preferences. This particular manner for conferring utility levels coming from the weight of each Representative for each alternative means all the Representatives to be the only determinants of the utility levels. Moreover, the latter are directly measured by each Representative's power rather than that of the whole coalition. The social utility function (based on the induced PS" hN(.)) is unique for each SSWSp g(.) even though we shall specify later (point 4.) the relation between a previous SSWSp and its induced PSa u.

E q u iv a l e n c e fo r L o t t e r ie s : A Theo r e m

Barberà & Sonnenschein's Theorem is based on the existence of a binary and Paretian SS WS. In its turn, the h-Theorem is based on the existence of an anonymous and unanimous PS. Furthermore, we know the particular PS which is induced by the initial SSWS to be always Lucian since based on GCA. We can obtain an equivalence theorem between Barberà & Sonnenschein's Theorem and the /i-Theorem in using both theorems in the sense of an equivalence between two axioms, binarity and the Paretian property on one side and unanimity and anonymity on the other, and the existence of two functions, a power function on one side and a social utility function on the other ; then, we have just to apply GCA in order to link both theorems. In that case, i.e. when considered lotteries (over profiles as over coalitions) are all proba bilistic, we write /i+-Theorem.

i EQUIVALENCE (+) T h e o r e m : Barberà & Sonnenschein's Theorem is equivalent to the h+-Theorem if GCA holds for probabilistic lotteries.

The proof firstly, consists in showing that binarity and the Paretian property imply anonymity and unanimity if GCA holds and secondly that anonymity and unanimity imply binarity and the Paretian property if GCA holds. The proof is purely logical. This particular version only deals with additive lotteries. From now on, we can consider any induced PS to be anomymous and unanimous if the initial SSWS is binary and satisfies the Paretian property. As soon as GCA holds, the induced PS is Lucian ; hence, under GCA, the induced PS -if existing -is a Lucian PS".

A

  ar>d Sz>T implies c(S) > c(T) for all S, T c ® (resp. N). Let C($) (resp. C(N)) be the set of nonadditive lotteries on S (resp. N). Moreover, we note NAC(<B) (resp. NAC (N)) the subset of strict nonadditive lotteries. When a nonadditive lottery is defined onasubsetT e ®(resp.C e N), we note it c;(.) (resp. cc). Given any coalition A g 2'v, x(A) = [y e X :xBAy ). We assume "BA" to be set up from the following rule : x(A) = x[u ieA/] = u, e A x(i). "x(A)" can be also interpreted as a degree of dispersion for the A's collective choices. If #x(A) is little when #A is big, it means that the A's collective choices are very concentrated ; if x(A) =x(B) while #A > #B, it means that the A's collective choices are more concentrated than those of B. Furthermore, x(A) u x (A )= X. V5 e 2*, Vjc e S, we note Sx, the set of alternatives which belong to 5 except x. If x(A) = Xx, the collective choices of A are said totally divided. Remark 1 : L(' B) c C ( î) , It means that a lottery which belongs to C (r B) can be a probability.Actually, L((B) u NAC((B) = C(' B).A Strict Social Welfare Scheme (SSWS) is a function g(.) : IT -> C(®). If g(.) comes from & -> L(®), we note it g+(.) order to designate the SSWS(s) which lead to probabilistic lotteries. It means that g+(.) corresponds exactly to a SSWS à laBarberà 6 Sonnenschein 1978. A SSWS g(.) is binary if for any x ,y e X, and any pair of profiles BSSWS g(.) is Paretian if for any x, y e X, and any Be®", a probability measure, we note it /»+(.) in order to indicate that this PS is additive; p[h+(A),x] = lN(A,x) could be interpreted as the part of representativity in N of the agent i e A who are designated to be the A-Representative; i.e. the power-decision of (A,x) ¡where (A,x) corresponds to this A-Representative. There exists a Repre sentative for each feasible coalition of 2" and each element* e X ;i.e.VA e 2" ;A *■ 0 , Vx e X , ( A ,x ) * 0 .

  p[hN(N),x] = 1. It means also that each time x(N) * Xx, then there is no Arrovian dictatorship. Let us introduce a new axiom of choice from Luce 1959, which was generalized to nonadditive probabilities in Billot & Thisse 1991. A PS h(.)isLucianiffoTanyA,B e 2N suchthatA c # c C and for any* e X,

  Functions and GCA Basically, Barberà & Sonnenschein's Theorem consists in pointing out an additive function (since #X > 6) on the set of coalitions of individuals from probabilistic lotteries over preferences : Barbera & Sonnenschein's Theorem : Given any binary and Paretian SSWS g+{.) :®" ->L(®), there exists an additive function l^C) : 2N -> [0,1] such that: V Be 'ff,'ix ,y e X, (j.s(\ji(B,xBy)) = p[g+(B),xfi;y]. Moreover, we have, |ig(0) = 0 ; fo ra llA czN, p.s(A)+p.g(N-.A) = 1 ; whenever A z>B, p.g(A) >n.g(B). In order to prove this theorem, Barberà & Sonnenschein 1978 established the two following lemmas of neutrality and nonperversity (pp. 247 and 248) : NEUTRALITY L e m m a : Let g+(.) be a binary and Paretian SSWS. Then, for any BLet g+(.) be a binary and Paretian SSWS. Then, for any

Remark 4 :

 4 From now on, we note ssWSp anY SSWS which is binary and Paretian. Because we assume #X to be greater than six, the power function \ig coming from Barberà & Sonnenschein's Theorem is necessarily additive. Hence, we can leave out the term "subadditive" from the original Theorem. By Luce's Theorem, we know such a function, positive and defined upon a powerset, to be equivalent to the existence of a class of distributions of probabilities. We note Lg(N) the subset of L{N) which is induced by \ig9 i.e. the g -class of distributions of probabilities. It means : L u c i a n (+) L em m a : For any given SSWSp g+(.) : -» L ($), GCA is satisfied if and only if there exists a g-class of distributions of probabilities L8(N) such that, VA c N ffor any lottery /j(.) e L8(N) we have : The proof is the same as Luce's one. Hence, we can associate each power function [ig to a g -class of distributions of probabilities over agents. Thus, since g+(.) : -> L(iB), l8(.) can only be interpreted as a probabilistic lottery over the agents. It means that we can define probabilistic lotteries over coalitions from profiles of preferences whenever there exists a power function ; i.e. each time Barberà & Sonnenschein Theorem holds. This way, GCA could be the second step of a method searching for passing from preferences to lotteries over coalitions. Remark5 : If there exists an induced set of lotteries Lg(N), it means that, VA cAi, any Zf (.) e Lg(N) is Lucian since GCA holds ; i.e. each induced lottery over coalitions is Lucian. Remark 6 : We shall note Cg(N) the subset of C(N) which will be induced by \igi i.e. the g -class of distributions of Choquet capacities, when generalizing Barberà & Sonnenchein 1978 to C(N).

  3. F r o mA g e n t s t o N onaddittve L o tter ie s o v e r A g en ts v ia So c ia l U t il it y F u n c t io n s

D

  o m in a n c e L em m a :Ifx(A) 3 x(B) => p[hc(A),x] > p[hc(B),x]. Proof : If x(A) =X Z, the unanimity axiom yields p[hc(A),x] > p[hc(B),x]• We know that x {A )= x[u, 6 A i] = u, Ë A x(i). Hence, we can conclude by x(A u B ) = x(A) => Pihc(A u /?),*] = p[hc{A),x], since the anonymity axiom holds. By another way, hc(B,x) = hc(A u B, x) x /iA ufl>1(5 , x) because A (.) is a Lucian PS^. It means :hc(B,x) = hc(A v B ,x ) x h AuBiX(B,x) = hc(A ,x)xhAuBx(B,x). Now, hc(A < jB ,x)= hc(B ,x )/ thus hAuBx(B,x) < 1. Hence, hc(B,x) < hc(A,x). So, we can deduce : lity Lem m a : IfxiA ) = y(B) => p[hc(A),x] = p[hc(B),y].

  5. F r o m P r o b a b il is t ic Lo tter ie s o v er Preferences Social U t il it y F un c tio n s We have just to mix both results of Barberà & Sonnenschein's Theorem, Lucian (+) Lemma and h -Theorem in order to prove the existence of a social or a coalitional utility based on lotteries over preferences. Lucian (+) Lemma consists in restricting the basic set of lotteries L(N) into a particular subset L*(N) coming from the previous SSWSp #+(.)• Thus, in taking the induced power scheme PS" h*(.) : 2* -> [0,1] into L*(N), we satisfy both conditions of the /j-Theorem ever since hi(.) is Lucian ; i.e. as soon as A*(.) exists which is guarantied by Equivalence (+) Theorem. C o r o l l a r y (+) : Given any SSWSp £+(.): S" -> £,(«), VB e IT, Vx e X, the induced PS" h*(.) e Lg(N) is Lucian. Then, there exists a function wf (.) : 2'v -> [0,1] such that : uj;(x('y(li,xBXx))) = p[g+(B),xBXx], Proof : Because g+Q is a SSWSp, there exists a power function ng(.) such that (ig(\|r(B,x0!Xx)) = P Thanks to Equivalence (+) Theorem, we know the induced /t*(.) to be a Lucian PS". Thus, in applying Lucian (+) Lemma, we have \ig(y(B,xBXx))lft(x\f(B,xBXx)) since \ig(N) = 1 by definition and Af(.) = fê(.) e LS(N). Hence, ihe h-Theorem yields, u%(x(y(B,xBXx))) = p[/!*(y(B),xZyy,;t] which also means uZ(x(y(B,xBXx))) = p [g+{B),xBXx]. N onadditive Lotteries over Preferences to SocialU tility F unctions The proof of Barberà & Sonnenschein's Theorem is completely independent from the probabilistic nature of considered lotteries. If rewriting both axioms of binarity and that dealing with the Paretian property according to nonadditive lotteries over preferences, we can immediately obtain the two basic generalized results of neutrality and nonperversity. Hence, it is obvious to conclude by : Barbera & Sonnenschein'S Generalized Theorem : Given any SSWSp g(.) : -> C('2), there exists a function |X S(.) : 2N -> [0,1] such' that : VB e Vx, y e X, \Lg(y(K,xBy)) = p\g(B ),xB yl furthermore we have, |is(0) = 0 ; whenever A^>B, |IS(A) > Remark 9 : The only property which differs from the original theorem deals with the probabilistic constraint of mass-unity (see Billot 1991b) ; actually, since \ig is nonadditive, the sum of any coalition's power and that of its complement could be different from 1. Hence, the probabilistic constraint of mass-unity disappears. The proof is based on same arguments as Barberà & Sonnenschein 1978 ones (p. 248) even though we do not search here any subadditive function but only a nonadditive function. This last characteristic is directly issued from the definition of the SSWSp : IP -> C(®) ; i.e. the membership of the designed lottery to C(s). Since we have proved the Gen eralized Luce's Theorem in Billot & Thisse 1991, we can establish the following theorem : Lucian Generalized Lemma : For any given SSWSp ->C(<8), GCA is satisfied if and only if there exists a g-class of distributions of Choquet capacities Cg(N) such that, VA c; N ,for any nonadditive lottery cf(.)e CS{N) we have : C W ) = -¿ C ) forallB<zAc:N. The proof is exactly the same as Billot & Thisse's one. Each nonadditive lottery cj(.) e Cf{N) corresponds to the induced PS /i'(.)becauseof GCA. Thus,by definition, the induced PS h8(.) = c8(.) ™ always Lucian. Hence, we can prove the following theorem in mixing the proofs of Barberà & Sonnenschein's Generalized Theorem, h -Theorem and Lucian Generalized Lemma. G en er a lized C o r o l l a r y : Given any SSWS£ g(.) : -> C (OE ), VBe # \ \fx e X, the induced PS* h8Q e Cg(N) is Lucian. Then, there exists a function «/(.) : 2" -> [0,1] such that : m/(x(v(B,xBXJ)) = p\g(1S),xBXx]. This last result is just a generalization of Corollary (+) to C(N). The social or coalitional utility that we define according to a nonaddilive lottery over agents is nonadditive. If the induced PS" h*(.) is subadditive, if h*(.) is a possibility for example, then the social utility w/(.) is subadditive since possibilistic (see Zadeh 1978 and Billot & Thisse 1991). Actually, all the properties of «/(.) come from those of he{.) which in their turn come from those of #(iv a l e n c e G e n er a lized Theo r e m : Barberà & Sonnenschein's General ized Theorem is equivalent to the h-Theorem if GCA holds for nonadditive lotteries. Tb s last theorem guarantees the equivalence for nonadditive lotteries and thus the existence of a method for passing from nonadditive lotteries over profiles to nonadditive lotteries over coalitions as soon as GC A holds. It means also the induced PS" h(.) to be always Lucian. This way, for example, possibilistic lotteries over preferences could come from a possibilistic, hence subadditive power function (re gardless of #X) which implies possibilistic lotteries over coalitions coming from a possibilistic, hence subadditive utility function. In Billot & Thisse 1991, following Lovasz 1983, we proved any submodular (i.e. subadditive) utility function (for a basic finite set of alternatives) to imply the existence of what we called a decreasing discrete marginal utility function. Then, we proposed to analyze this property in assimilating subadditivity and discrete concavity. Hence, in order to restore the complete Barberà & Sonnenschein's result in so far as the exhibition of a subadditive power function leading to lotteries over preferences, we could restrict the previous social utility function to the only discrete concave ones. In that very case, which is particularly intuitive (since corresponding to a decreasing discrete marginal utility function), the power function should be obviously subadditive. In return, lotteries over preferences should be also subadditive. C o n c lu sio n This paper deals with the only strict relations of preference. The extension to weak orderings does not change a priori neither the methodology nor the basic sense of results. One of the most interesting comments of Barberà & Sonnenschein's paper consists in interpreting the power function as a distribution of dictatorial power. Thus, in dividing this dictatorial power by means of lotteries o''er preferences, one could dimmish the risk of dictatorship. Finally, in our paper, we try to found a method which allows to define this power distribution directly from alternatives by means of a social utility. This last exists whenever we assume a Power Scheme to be anonymous and unanimous. In other words, the social utility function can be interpreted as a distribution of utility upon the set of alternatives. Since we know Barberà & Sonnenschein to be equivalent to ours A-Theorem when GCA holds, we know also that dividing the dic tatorial power is equivalent to divide the social utility if the Power Scheme is socially consistent, i.e. Lucian. Basically, this conclusion confirms the Arrovian analysis of aggregation.

Billot 1991a) as they are exoge- neously determined. If h{.) is a nonadditive probability, i.e. a Choquet capacity, then p[h(A),x] could be interpreted as a degree of representativity of these natural leaders. If we restrict a PS h(.) into a subset CcJV,we note it hc(.). Remark 2 : Most of the time, the degree of representativity in any C of the Representative (A,x) e C will be noted directly hc(A,x). Remark 3 : p\h(A),x] can be a probability or a capacity. "p[.,.]" is just a symbol to note any probabilistic or strictly nonadditive lottery; but as soon as h (.) e L(N), we note p[h+(A ),x \