Bisimilarity Distances for Approximate Differential Privacy
Dmitry Chistikov Andrzej S. Murawski David Purser



























programthplop
programProgram

proof*[1]
  
   
  
































=90pt













	language=python,
	mathescape=true,
	keywordstyle=,
        deletekeywords=val,fun,
	columns=flexible,
	identifierstyle=,
	tabsize=2,
	fontadjust=true,
    numbers=left,
    stepnumber=1,
    numberstyle=

factFact















D. Chistikov et al.



Centre for Discrete Mathematics and its Applications (DIMAP) & 
Department of Computer Science, University of Warwick, UK 

Department of Computer Science, University of Oxford, UK 



Bisimilarity Distances for Approximate Differential Privacy
    Dmitry Chistikov1
Andrzej S. Murawski2
David Purser1

    December 30, 2023
===========================================================




Differential privacy is a widely studied notion of privacy for various models of computation.
Technically, it is based on measuring differences between probability distributions.
We study ϵ,δ-differential privacy in the setting of labelled Markov chains.
While the exact differences relevant to ϵ,δ-differential privacy are not computable
in this framework, we propose a computable bisimilarity distance that yields a sound technique for measuring δ,
the parameter that quantifies deviation from pure differential privacy.
We show this bisimilarity distance is always rational, the associated threshold problem is in ,
and the distance can be computed exactly with polynomially many calls to an  oracle.








§ INTRODUCTION

 
  


Bisimilarity distances were introduced by <cit.>, as a metric analogue of classic probabilistic bisimulation <cit.>,
to overcome the problem that bisimilarity is too sensitive to minor changes in probabilities. 
Such robustness is highly desirable, because probabilistic automata arising in practice may often be based on approximate probability values, extracted or learnt from  real world data.

In this paper, we study the computation of bisimilarity distances related to differential privacy.



Differential privacy <cit.> is a security property that ensures that a small perturbation of the input leads to only a small perturbation in the output, so that observing the output makes it difficult to determine whether
a particular piece of information was present in the input.
A variant, ϵ-differential privacy, considers the ratio difference (rather than the absolute difference) between probabilities.

We will be concerned with the more general concept of  ϵ,δ-differential privacy, also referred to as approximate differential privacy.
The δ parameter allows one to assess to what degree ϵ-differential privacy (“pure differential privacy”) was achieved. 
We will design a version of bisimilarity distance which will constitute a sound upper bound on δ, thus providing a reliable measure of security.

From a verification perspective, a natural question is how to analyse systems with respect to ϵ, δ-differential privacy.
We carry out our investigations in the setting where the systems are labelled Markov chains (LMC),
abstractions of autonomous systems with probabilistic behaviour and under partial observability.
States of an LMC  can be thought of as generating probability distributions on sets of traces, and these sets are taken to correspond to observable events.
Let  be a system, and suppose s and s' are two states (configurations) of . Then we will say that s and s' satisfy ϵ, δ-differential privacy if the distributions on traces from these states are sufficiently close.
We consider the following problem: given an LMC , states s and s', and a value of ϵ, determine δ such that s and s' satisfy ϵ, δ-differential privacy.
Unfortunately,  the smallest of such δ is not computable <cit.>, which motivates our search for upper bounds.

In the spirit of generalised bisimilarity pseudometrics <cit.>, our distance, denoted α, is based on the Kantorovich-style lifting of distance between states to distance between distributions. 
However, because the underpinning distances in our case turn out not to be metrics, the setting does not quite fit into the standard picture, which presents a technical challenge.
We discuss how the proposed distance may be computed, using techniques from linear programming, linear real arithmetic, and computational logic. 
Our first result is that the distance always takes on rational values of polynomial size with respect to the size of the LMC and the bit size of the probability values associated with transitions (Theorem <ref>).

This is then used to show that the associated threshold problem (“is α upper-bounded by a given threshold value for two given states?”) is in  (Theorem <ref>).
Note that the distance can be approximated to arbitrary precision by solving polynomially many instances of the threshold problem. Finally, we show that the distance can be computed exactly in polynomial time, given an  oracle (Theorem <ref>).
This places it in (the search version of) , leaving the possibility of polynomial-time computation open.




  
Related Work Chatzikokolakis et al. <cit.> have advocated the development of Kantorovich pseudometrics,
instantiated with any metric distance function (rather than absolute value) in the context of differential privacy.
They did not discuss the complexity of calculating such pseudometrics, but asked whether it was possible  to extend their techniques to ϵ,δ-differential privacy.
Our paper shows the extent to which this can be achieved; the technical obstacle that we face is that our distances are not metrics. To the best of our knowledge, no complexity results on differential privacy for Markov chains have previously appeared in the literature, and we are the first to address this gap.

The computation of the standard bisimilarity distances has been the topic of a long running line of research <cit.>, starting with approximation <cit.>.
The distance was eventually determined to be computable in polynomial time using the ellipsoid method to solve an implicit linear program of exponential size <cit.>. This technique turns out slow in practice and further techniques have been developed which are faster but do not have such strong complexity guarantees <cit.>.
Because of the two-sided nature of our distances, the main system of constraints that we introduce in our work involves a maximum of two quantities. This nonlinearity at the core of the problem prevents us from relying on the ellipsoid method and explains the gap between our  upper bound and the polynomial-time algorithms of <cit.>.


Tschantz et al. <cit.> first studied differential privacy using a notion similar to bisimulation, which was extended to a more general class of bisimulation relations by Xu et al. <cit.>.
Both consider only ϵ-differential privacy, i.e. ratio differences, but do not examine how these could be computed.

An alternative line of research by Barthe et al. <cit.> concerns formal mechanised proofs of differential privacy.
Recently, that direction has been related to coupling proofs <cit.> – this still requires substantial effort to choose the coupling, although recent techniques 
have improved this <cit.>. We complement this line of research by taking an algorithmic verification-centred approach.

The remainder of the paper is arranged as follows. Section <ref> introduces the basic setting of labelled Markov chains.
In section <ref>, we discuss ϵ,δ-differential privacy and in section <ref> we define our distance.
Section <ref> develops technical results on our extended case of Kantorovich lifting.
These are subsequently used in section <ref> to underpin techniques for computing the relevant distances.

 




§ LABELLED MARKOV CHAINS


Given a finite set S, let S be the set of probability distributions on S.

A labelled Markov chain (LMC)  is a tuple S,,μ,,
where 
S is a finite set of states, 
 is a finite alphabet, 
μ: S→S is the transition function 
and :S→ is the labelling function.

Like in <cit.>, our definition features labelled states. Variations, such as transition labels, can be easily accommodated within the setting.
We also assume that all transition probabilities are rational, represented as a pair of binary integers. The bit sizes of these integers form part of the bit size of the representation |M|. We will often write μ_s for μ(s).

In what follows, we  study probabilities associated with   infinite sequences of labels 
generated by LMC's.
We specify the relevant probability spaces next using standard measure theory <cit.>.
Let us start with the definition of cylinder sets.

A subset ⊆^ω is a cylinder set if there exists u ∈^∗ such that
 consists of all infinite sequences from ^ω whose prefix is u. We then write _u
to refer to C.


Cylinder sets play a prominent role in measure theory in that their finite unions can be used as  a generating family (an algebra) 
for the set F of  measurable subsets of ^ω (the cylindric σ-algebra).
What will be important for us is that any measure ν on F is uniquely determined by its values on cylinder sets.
Next we show how to assign a measure ν_s on F to an arbitrary state of an LMC.
We start with several auxiliary definitions.

Given =S,,μ,, let μ^+:S^+→[0,1] and ^+:S^+→^+ be the natural 
extensions of μ and  to S^+, i.e.
μ^+(s_0⋯ s_k) = ∏_i=0^k-1μ(s_i)(s_i+1) and ^+(s_0⋯ s_k) = (s_0)⋯(s_k), 
where k≥ 0 and s_i∈ S (0≤ i≤ k).
Note that, for any s∈ S, we have μ^+(s)=1.
Given s∈ S, let s be the subset of S^+ consisting of all sequences that start with s.



Let =S,,μ, and s∈ S. We define ν_s: F→ [0,1] to be the unique measure on F
such that for any cylinder _u we have

    ν_s(_u) = ∑{ μ^+(p)  |   p∈s, ^+(p) = u }.


Our aim will be to compare states of labelled Markov chains from the point of view of differential privacy.
Note that two states s,s' can be viewed as  indistinguishable if ν_s=ν_s'.
If they are not indistinguishable then the difference between them can be quantified using the total variation distance, defined by
(ν,ν') = sup_E∈F  |ν(E)-ν'(E)|. 
Given =S,,μ, and s,s'∈ S, we shall write (s,s') to refer to (ν_s,ν_s'). 

(s,s') turns out  surprisingly difficult to compute: it is undecidable whether the distance is strictly greater than a given threshold,
and the non-strict  variant of the problem (“greater or equal”) is not known to be decidable <cit.>.

To measure probabilities relevant to differential privacy, we will need to study a more general variant α of the above distance, which we introduce next.




§ DIFFERENTIAL PRIVACY

Differential privacy is a mathematical guarantee of privacy due to Dwork et al <cit.>. 
It is a property similar to non-interference: the aim is to ensure that inputs which are related in some sense lead to very similar outputs. 
The notion requires that for two related states there only ever be a small change in output probabilities, and therefore discerning the two is difficult, which maintains the privacy of the states. 
Below we cast the definition in the setting of labelled Markov chains.

Let =S,,μ, be a labelled Markov chain and let R⊆ S× S be a symmetric relation.
Given ϵ≥ 0 and δ∈ [0,1], we say that
 is ϵ, δ-differentially private (wrt R) if, for any s,s'∈ S such that (s,s')∈ R, we have

    ν_s(E) ≤ e^ϵ·ν_s'(E) + δ

for any measurable set E∈F.


Note that each state s∈ S can be viewed as defining a random variable X_s with outcomes from ^ω such that P(X_s∈ E) = ν_s(E). Then the above can be rewritten as P(X_s ∈ E) ≤ e^ϵ  P(X_s'∈ E) + δ, 
which matches the definition from <cit.>, where one would consider X_s, X_s' neighbouring in some natural sense. 

The above formulation is often called approximate differential privacy. For δ=0, one talks about (pure) ϵ-differential privacy.
Note that then the above definition boils down to measuring the ratio between the probabilities of possible outcomes.
δ is thus an indicator of the extent to which ϵ-differential privacy holds for the given states.
Intuitively, one could interpret ϵ,δ-differential privacy as “ϵ-differential privacy with probability at least 1-δ" <cit.>.
Our work is geared towards obtaining sound upper bounds on the value of δ for a given ϵ.


What it means for two states to be related (as specified by R) is to a large extent domain-specific. In general, R makes it possible to spell out which
states should not appear too different and, consequently, should enjoy a quantitative amount of privacy.
In the typical database scenario, one would relate database states that differ by just one person.

In our case, we refer to states of a machine, 
for which we would like it to be indiscernible as to which was the start state (we assume the states are hidden and the traces are observable).

To rephrase the inequality underpinning differential privacy in a more succinct form, it will be convenient to work with the skewed distance Δ_α,
first introduced by Barthe et al <cit.> in the context of Hoare logics and ϵ,δ-differential privacy.


For α≥ 1, let Δ_α: ×→ be defined by 
Δ_α(x,y) = max{x - α y,  y - α x,   0}.


It is easy to see that Δ_α is anti-monotone with respect to α. In particular, because α≥ 1, we have Δ_α(x,y) ≤Δ_1(x,y)= |x-y|.
Observe that Δ_2(9,3)=9-2× 3 = 3, Δ_2(9,6) = 0 and Δ_2(6,3)=0.
Note that Δ_2(x,y)=0 need not imply x=y, i.e. Δ_2 is not a metric.
Note also that the triangle inequality may fail: Δ_2(9,3) > Δ_2(9,6)+Δ_2(6,3), i.e. Δ_2 is not a pseudometric[A pseudometric must satisfy m(x,x)=0, m(x,y)=m(y,x) and m(x,z)≤ m(x,y)+m(y,z). 
For metrics, one additionally requires that m(x,y)=0 should imply x=y.].
This will complicate our technical development, because we will not be able to use the framework of <cit.> directly.

The significance of the skewed distance will be seen shortly in Fact <ref>. We first introduce the skewed analogue of the total variation distance called α, for which  is a special case (α=1).


Let α≥ 1. Given two measures ν,ν' on (^ω, F), let

    α(ν,ν') = sup_E ∈FΔ_α(ν(E),ν'(E)).


Following the convention for , α(s,s') will stand for α(ν_s,ν_s').
Fact <ref> is an immediate corollary of Definitions <ref>, <ref>, and <ref>.


M is ϵ,δ-differentially private wrt R if and only if, for all s,s'∈ S such that (s,s')∈ R, we have α(s,s') ≤δ, where α = e^ϵ.

Some values of α are readily known. For instance, the distance between any bisimilar states turns out to be zero.

A probabilistic bisimulation on an LMC =S,,μ,  is 
an equivalence relation R⊆ S× S such that  if (s,s') ∈ R then (s)=(s') and for all X ∈ S/R, ∑_u∈ Xμ(s)(u) =∑_u∈ Xμ(s')(u),
i.e. related states have the same label and probability of transitioning into any given  equivalence class.

It is known that probabilistic bisimulations are closed under union and hence there exists a largest one, written ∼ and called probabilistic bisimilarity.
Two states are called bisimilar, written s∼ s', if (s,s')∈∼. Equivalently, this means that the pair (s,s') belongs to a probabilistic bisimulation.
It follows from <cit.>, that for bisimilar s,s', we have 1(s,s')=0. As (s,s')≤1(s,s') we obtain the following.

If s∼ s' then (s,s') =0.

In contrast to <cit.>, the converse will not hold.

In the LMC shown in Figure <ref>, states s_0 and s_1 are not bisimilar.
To see this, observe first that  s_2 must be the only state in its equivalence class with respect ∼, because other states have different labels.
Now note that the probabilities of reaching s_2 from s_0 and s_1 respectively are different (0.4 vs 0.6).

However,  for α=1.5,  we have α(s_0,s_1)=0, because Δ_α(0.6,0.4)= max(0.6-1.5· 0.4, 0.4-1.5· 0.6, 0)=0.


In an “acyclic” system, α can be calculated by exhaustive search: the natural algorithm 
is doubly exponential, as one needs to consider all possible events over all possible traces.
However, in general, α is not computable (Remark <ref>).
Thus, in the remainder of the paper, we shall introduce and study another distance .
It will turn out possible to compute it and it will provide a sound method
for bounding δ for ln(α),δ-differential privacy.  
Our main result will be Theorem <ref>: the new distance can be calculated in polynomial time, assuming an  oracle. Pragmatically, this means that this new distance can be computed efficiently, assuming access to an appropriate satisfiability or theory solver.





§ SKEWED BISIMILARITY DISTANCE


Our distance will be defined in the spirit of bisimilarity distances <cit.> through a fixed point definition
based on a variation of the Kantorovich lifting.
To motivate its shape, let us discuss how one would go about calculating α recursively.
If (s)≠(s') then ν_s(C_(s)) = 1, ν_s'(C_(s)) = 0, therefore (s,s')=1.
So, let us assume (s)=(s'). Given E⊆^ω and a∈, 
let E_a = { w ∈^ω |  a w ∈ E}.  Then we have:

    α(ν_s,ν_s')    = sup_E ∈FΔ_α(ν_s(E),ν_s'(E))
    
       = sup_E_(s)∈FΔ_α(∑_u∈ S μ_s(u) ν_u(E_(s)),∑_u∈ Sμ_s'(u) ν_u(E_(s))).

If we define f: S→ [0,1] by f(u) = ν_u(E_(s)), this can be rewritten as

    sup_E_(s)∈FΔ_α(∑_u∈ S μ_s(u)  f(u),∑_u∈ Sμ_s'(u) f(u)).

We have little knowledge of f, otherwise we could compute α, but  from the definition of α, we do know that Δ_α(f(v),f(v')) ≤α(v,v') for any v,v'∈ S.
Consequently, the following inequality holds.

    (s,s') ≤sup_f: S → [0,1] 
    ∀ v,v' ∈ S Δ_α(f(v), f(v')) ≤α(v,v')-18muΔ_α(∑_u∈ Sμ_s(u) f(u),∑_u∈ Sμ_s'(u)f(u))


The expression on the right is an instance of the Kantorovich lifting <cit.>, which uses (“lifts”) the distance α between states s,s' to
define a distance between the distributions μ_s,μ_s' associated with the states. We recall the definition of the Kantorovich distance between distributions 
in the discrete case, noting that then, for μ∈S,  we have ∫ f d μ = ∑_u∈ S f(u)  μ(u).
 
Given μ,μ' ∈S and  a pseudometric m:S× S→[0,1], the Kantorovich distance between μ and μ' is defined to be

    K(m)(μ,μ') = sup_f:S → [0,1] 
    ∀ v,v' ∈ S |f(v) - f(v')| ≤ m(v,v') -18mu|∫ f dμ - ∫ f dμ'|.



The Kantorovich distance is
 also known under other names (e.g. Hutchinson, Wasserstein distance), having been rediscovered several times in history <cit.>.
Chatzikokolakis et al. <cit.> studied the Kantorovich distance and related bisimulation distances when the absolute value distance above is replaced with another metric.

For our purposes, instead of |...|, we need to consider Δ_α, even though Δ_α is not a metric and m may not be a pseudometric.

Given μ,μ' ∈S and a symmetric distance d:S× S→[0,1], the skewed Kantorovich distance between μ and μ' is defined to be

    (d)(μ,μ') = sup_f:S → [0,1] 
    ∀ v,v' ∈ S  Δ_α(f(v), f(v')) ≤ d(v,v') -18muΔ_α(∫ f dμ,∫ f dμ')



Note that setting α = 1 gives the standard Kantorovich distance (Definition <ref>). Below we define a function operator, which will be used to define our distance.

Let : [0,1]^S× S→ [0,1]^S× S be defined as follows.

    Γ_α(d)(s,s') =  
    K_α(d)(μ_s, μ_s')    (s) = (t) 
     
    1    (s) (t)


Note that [0,1]^S× S equipped  with the pointwise order, written ⊑, 
is a complete lattice and that Γ_α is monotone with respect that order (larger d permit more functions, thus larger supremum).
Consequently,  has a least fixed point <cit.>. 
We take our distance to be exactly that point.

Let α: S× S→ [0,1] be the least fixed point  of .


Recall that the least fixed point is equal 
to the least pre-fixed point (min{ d | (d)⊑ d}).

Recall our initial remarks about the Kantorovich distance ()(μ_s,μ_s') overapproximating (s,s').
They can be summarised by ⊑(), i.e.  is a post-fixed point of .
Since we want to bound α as closely as possible, we can show that the least fixed point α also bounds  from above.

⊑α.


The lemma is an analogue of Theorem 2 <cit.>.
Its proof in <cit.> relied on the fact that the counterpart of Δ_α 
was a metric, which is not true in our case (unless α=1). 


Just like Δ_α is anti-monotone with respect to α, so is α.
This means that α⊑1.
The definition of 1 coincides with the definition of the classic 
bisimilarity pseudometric 𝖽_1 (see e.g. <cit.>), which satisfies 𝖽_1(s,s')=0 if and only if s and s' are bisimilar.
Consequently, we obtain the following corollary.

For any α≥ 1,  if s∼ s' then α(s,s')=0.

As in the case of α, we do not have the converse in our setting. Example <ref> shows that s_0≁s_1 but we observe that 1.5(s_0,s_1)=0. Observe:

    1.5(s_0,s_1)   ≤
    max_f ( ∑_s ∈ S f(s)(μ_s_0(s)- 1.5·μ_s_1(s)),∑_s ∈ S f(s)(μ_s_1(s)- 1.5·μ_s_0(s))) 
    
    
    = max_f (f(s_2)(0.6 - 1.5· 0.4) + f(s_3)(0.4-1.5· 0.6), 
    
                  f(s_2)(0.4-1.5· 0.6) + f(s_3)(0.6 - 1.5· 0.4) ).

Notice the coefficients of f(s) are all non-positive. Consequently, regardless of the restrictions on f, the maximising allocation will be f(s) = 0
and, thus,  1.5(s_0,s_1) = 0.







 §.§ Example: Dining Cryptographers


In the dining cryptographer model <cit.>, a ring of diners want to determine whether one of the diners paid or an outside body.
If a  diner paid, we do not want to reveal which of them it was. The protocol proceeds with each adjacent pair privately flipping a coin, each diner then reports the XOR of the two coin flips they observe, however if the diner paid he would report the negation of this. We can determine if one of them paid by taking the XOR of the announcements. With perfectly fair coins, the protocol guarantees privacy of the paying diner, but it is still differentially private if the coins are biased. If an outside body paid, 
there is no privacy to maintain so we only simulate the scenarios in which one of the diners did pay. The scenario where Cryptographer 0 paid must have similar output distribution to Cryptographer 1 paying, so that it can be determined that one of them did pay, but not which. The internal configuration of the machine is always assumed to be hidden, but the announcements are made public whilst maintaining the privacy of the participating Cryptographer (and the internal states). 

The LMC in Figure <ref> shows the 2-person dining cryptographers protocol (Figure <ref>) starting from Cryptographers 0 and 1 using weighted coins with p = 49/100. The states of the machine encode the 5 variables that need to be tracked. To achieve ϵ,δ-differential privacy with α = e^ϵ = 1.0002 the minimal (true) value of δ is 0.00030004. Our methods generate a correct upper bound α(s_0,s_1) = 0.0004, showing ln(1.0002),0.0004-differential privacy. The protocol could be played with n players, requiring O(n^2) states, for all possible assignments 
of paying cryptographer  and current cryptographer. In a two-person scenario, the diners would know which of them had paid but an external observer of the output would only learn that one of them paid, not which.







 





§ SKEWED KANTOROVICH DISTANCES


Here we discuss how to calculate our variant of the Kantorovich distance. This will inform the next section, in which we look into computing α.

Recall the definition of (d)(μ,μ') from Definition <ref>.
In the general case of Δ_α (a,b), both a-α b and b-α a could be negative, so the maximum with 0 is taken. 
However, within the Kantorovich function, the constant function f(i) = 0 is a valid assignment, which achieves 0 in either case (0 - α× 0 =0). 
Consequently, we can simplify the definition of Δ_α to omit the 0 case inside K_α. 

If α=1 then Δ_α is the absolute value function and it is known that the distance corresponds to a single instance of a linear programming problem <cit.>.
However, this is no longer true in our case due to the shape of Δ_α (x,y)=max(x-α y, y-α x). 
Still, one can present the calculation as taking the maximum of a pair of linear programs.
We shall refer to this formulation as the “primal form” of (d). We give the first program below,
the other is its symmetric variant with  μ, μ' reversed. Below we write f_i for f(i) and let i,j range over S, and assume that d is symmetric.

    max_f ∈ [0,1]^S (∑_i f_i μ(i) -α∑_i f_i μ'(i))     subject to    ∀ i,j   f_i - α f_j ≤ d_i,j




The standard Kantorovich distance (α=1) is often presented in the following dual form when m is a pseudometric, based on the minimum coupling between
the two distributions μ and μ', weighted by the distance function. 

    K(m)(μ,μ') = min_ω∈ [0,1]^S× S∑_i,jω_i,j m_i,j    subject to    [  ∀ i  ∑_j ω_i,j = μ(i); ∀ j  ∑_i ω_i,j = μ'(j) ]



The dual form can be viewed as an optimal transportation problem in which an arbitrarily divisible cargo must be transferred from one set of locations (represented by a copy S^L of S) to another (represented by a different copy S^R of S).
Each state  s^R∈ S^R must receive μ(s), while each state s^L∈ S^L must send μ'(s). If ω_i,j is taken to represent the amount that gets sent from j^L to i^R then the above conditions restrict ω in accordance with the sending and receiving budgets.
If d_i,j represents the cost of sending from j^L to i^R then the objective function  ∑_i,jω_i,j· d_i,j corresponds to the overall cost of transport. Consequently, the problem is referred to as 
a mass transportation problem <cit.>.

To achieve a similar “dual form” in our case,  we take the dual form of each of our linear programs.
Then we can calculate the distance by taking the maximum of the two minima.
The shape of the dual is given below on the right.


    [                 max_f ∈ [0,1]^S(∑_i f_i μ(i) -α∑_i f_i μ'(i))                                                             = min_ω∈ [0,1]^S× S, τ,γ, η∈ [0,1]^S∑_i,jω_i,j· d_i,j  + ∑_iη_i;                                                                                                                                                                                          ;                                    ∀ i,j  f_i - α f_j ≤ d_i,j                                                                                      ∀ i: ∑_jω_i,j  + τ_i  -γ_i + η_i= μ(i);                                                                                                                                                         ∀ j: ∑_i ω_i,j + τ_j -γ_j/α≤μ'(j) ]


The dual form presented above is a simplified (but equivalent) form of the immediate dual obtained via the standard LP recipe.
Note that the polytope we are optimising over is independent of d, which appears only in the objective function.
The dual of the other linear program is obtained by swapping μ,μ'.

In the skewed case,  we optimise over the following polytope

    Ω_μ,μ' = { (ω , η )∈ [0,1]^S× S×[0,1]^S    |   [                        ∃γ,τ∈ [0,1]^S; ∀ i: ∑_jω_i,j + τ_i -γ_i +η_i = μ(i);    ∀ j: ∑_i ω_i,j + τ_j -γ_j/α≤μ'(j) ]}
 
One can also view it as a kind of transportation problem. As before, cargo can be transferred through the standard routes with ω at a cost d or new resource η can be obtained from an extra location at a cost of 1. There are also additional, cost-free routes between corresponding pairs s^L and s^R (represented by τ_s) and back (represented by γ_s). 
These extra routes are quite peculiar.  En route from s^L to  s^R the cargo `grows': when τ_s/α is sent from s^L, a larger amount of τ_s is received at s^R.
Overall, the total amount of cargo sent may be less than that received, so the sending constraints are now inequalities. 
From s^R to s^L the cargo `shrinks': when γ_s is sent from s^R, only γ_s/α is received by s^L. 

It is immediate that τ routes can be useful.
The γ routes may be useful for optimisation under two conditions. Firstly 
the shrinkage of the cargo must be made up elsewhere, i.e.,
through `growing' τ routes. Additionally the cost α× d(s_1^L, s^R) + d(s^L, s_2^R) is lower than d(s_1^L, s_2^R), which may well be the case due to the lack of triangle inequality.


We arrive at the following formulation, which we call the “dual form”:

    K_α(d)(μ, μ') = max{min_ω, η∈Ω_μ,μ'∑_i,jω_i,j· d_i,j + ∑_i η_i
     ,  min_ω,η∈Ω_μ',μ∑_i,jω_i,j· d_i,j  + ∑_i η_i  }.

Note that K_α(d)(μ,μ') can  be computed in polynomial time as a pair of linear programs in either primal or dual form, 
and taking the maximum (in either case).
In our calculations related to α, the distributions μ,μ' will always be taken to be μ_s,μ_s' respectively, for some s,s'∈ S.
The ability to switch between primal and dual form will play a useful role in our complexity-theoretic arguments.




§ COMPUTING Α


We start off by observing that all distances α(s,s') are rational and can be expressed in polynomial size with respect to M.
To that end, we exploit a result by Sontag <cit.>, which states that, without affecting satisfiability, 
quantification in the first-order fragment of linear real arithmetic (LRA) 
can be restricted to rationals of polynomial size  with respect to formula length (as long as all coefficients present in the formula are rational). 
Consequently, if we can express “there exists a least fixed point d of " in this fragment (with a polynomial increase in size), we can draw the intended conclusion.

 We give the relevant formula in Figure <ref>.
The formula asserts the existence of a distance d,
which is a pre-fixed point of Γ_α  (∀ f. ϕ(d,f)) such that any other pre-fixed point d' of Γ_α is greater.
Note that ∀ f.ϕ(f,d) exploits the fact that max_f A(f) ≤ d(s,s') is equivalent to ∀ f (A(f)≤ d(s,s')). Sontag's result
then implies the following.


Values of α are rational.  There exists a polynomial p such that for any LMC M and 
s,s'∈ S, the size of α (in binary) can be bounded from above by a polynomial in |M|. 





Sontag <cit.> uses the fact mentioned above to relate the alternation hierarchy within LRA to the polynomial hierarchy :
formulae of the form ∃ x_1 ∀ x_2 … Q x_k F(x_1 … x_k) (with quantifier-free F) 
correspond to Σ_k^ (and formulae starting with ∀ to Π_k^). Recall that Σ_1^=.


Next we focus on the following decision problem for α.



: given s,s'∈ S and θ∈, is it the case that α(s,s') ≤θ?


Recall that  the analogous problem for  is undecidable (Remark <ref>).
In our case, the problem turns out to be decidable and the argument does not depend on whether  < or ≤ is used.
To establish decidability we can observe that α(s,s') ≤θ can be expressed in LRA simply by adding d(s,s')≤θ to the formula from Figure <ref>.


We can simplify the formula, though,  using  α=min {d | Γ_α(d)⊑ d}.
Then α(s,s')≤θ  can be specified as  the existence of a pre-fixed point d such that d(s,s') ≤θ.
This can be done as follows, using ϕ(d,f) from Figure <ref>.

    ∃ d ∈ [0,1]^S× S  ( ∀ f ∈ [0,1]^Sϕ(d,f) ∧ d(s,s')≤θ )

By Sontag's results, this not only yields decidability but also membership in Σ_2^. Recall that ⊆Σ_2^⊆⊆.

Note that the universal quantification over f remains, i.e. we can still only conclude that the problem is in Σ_2^.
To overcome this, we shall use the dual form instead (Lemma <ref>). This will enable us to eliminate the universal quantification and replace it
with existential quantifiers using the fact that
min_ω A(ω)≤ B is equivalent to ∃ω (A(ω)≤ B). The resultant formula is shown in Figure <ref>.



Note the formula is not linear due to ω_i,j· d_i,j. However, because we know (Theorem <ref>) 
that α corresponds to an assignment of poly-sized rationals,
 we can consider the formula with d fixed at α. Then it does become an LRA formula (of polynomially bounded length with respect to |M|) and
we can again conclude that  the assignments of ω, γ, τ  must also involve rationals whose size is polynomially bounded. 
 Consequently, the formula implies membership of our problem in Σ_1^=: it suffices to guess  the satisfying assignment, guaranteed to be rational and of polynomial size.

 is in .



The decidability of  makes it possible to approximate α(s,s') to arbitrary (rational) precision ϵ by binary search.
This will involve O(|ϵ|) calls to the oracle for  (where |ϵ| is the number of bits required to represent ϵ in binary).

What's more, assuming the oracle, one can actually find the exact value of α(s,s') in polynomial time (wrt M). This exploits the fact that the value of α is rational and its size is polynomially bounded, so one can find it by approximation
to a carefully chosen level of precision and then finding the relevant rational with the continued fraction algorithm <cit.>. 




α can be calculated in polynomial time with an  oracle.


As a consequence, the problem of computing 
reduces to propositional satisfiability, i.e., can be encoded in SAT.
This justifies, for instance, the following approach: treat every variable
as a ratio of two integers from an exponential range, and give the system
of resulting constraints to an Integer Arithmetic or SAT solver. While
this might look like resorting to a general-purpose “hammer”, Theorem <ref>
is necessary for this method to work: it is not, in fact, possible to solve general polynomial constraint systems
relying just on SAT.
[
More precisely, the existence of such a procedure would be a breakthrough
in the computational complexity theory,
showing that 𝐍𝐏 = ∃ℝ. This would imply that
a multitude of problems in computational geometry could be solved using
SAT solvers <cit.>. Unlike for , variable assignments in these problems may need to be
irrational, even if all numbers in the input data are integer or rational.
]

We expect, however, this direct approach to be inferior to the following
observation. Theorem <ref> reveals that the variables in our constraint
system need not assume irrational values or have large bit
representations. Thus, one can give the system to a more
powerful theory solver, or an optimisation tool, but to expect that the
existence of simple and small models (solutions) will help the SMT
heuristics (resp. optimization engines) to find them quickly.

 



§ CONCLUSION AND FURTHER WORK


We have demonstrated that bisimilarity distances can be used to determine differential privacy parameters, despite their non-metric properties. 
We have established that the complexity of finding these values is polynomial, relative to an  oracle. Yet, 
it may still be possible to obtain a polynomial algorithm—although much like in the case of the classical bisimilarity distances and linear programming, it may not necessarily outperform theoretically slower procedures.

We conjecture that α, which we defined as the least fixed point of the operator Γ_α, may in fact be characterized as the unique fixed point of a similar operator. By the results of Etessami and Yannakakis <cit.>, it would then follow that α can be computed in , a smaller complexity class, improving upon our  upper bound and matching the complexity of a closely related setting (see below). The reason is the continuity of Γ_α, which follows from the properties of the polytope over which f ranges (in the definition of K_α(d)). Whether α can in fact be computed in polynomial time or is -hard seems to be a challenging open question.

Our existing work is limited to labelled Markov chains, or fully probabilistic automata. However, the standard bisimulation distances can also be defined on deterministic systems, where 
their computational complexity is  <cit.>. In our scenario, the privacy can only be analysed between two start states, but it is also reasonable to allow an input in the form of a trace or sequence of actions; the output would also be a trace. Here the choice of labels (at a specific state) would correspond to decisions taken by the user, and the availability of only one label would mean that this is the output. This setting would support a broader range of scenarios that could be modelled and verified as differentially private.
 


  §.§.§ Acknowledgement

David Purser gratefully acknowledges funding by the UK Engineering and Physical Sciences Research Council (EP/L016400/1), the EPSRC Centre for Doctoral Training in Urban Science. Andrzej Murawski is supported by a Royal Society Leverhulme Trust Senior Research Fellowship and the International Exchanges Scheme (IE161701).


splncs04






§ PROVING LEMMA <REF>. Α⊑


We will first introduce the skewed Kantorovich distance K_α() over traces that we will place in between the two. We will show that for all s,s' ∈ S: α(s,s') = K_α()(ν_s,ν_s') ≤(s,s;). We consider each of these (in)equalities:

α(s,s') = K_α()(ν_s,ν_s')



K_α()(ν_s,ν_s') ≤




 §.§ Definition and Properties of K_α()(ν_s,ν_s')

We introduce a generic version of the skewed Kantorovich distance, defined for any object X rather than states (X = S) as defined in the main body.

Given μ,μ' ∈ Dist(X) and d:X→[0,1] a distance function 

    K_α(d)(μ, μ') = sup_f: X → [0,1] 
    ∀ x,x' ∈ X Δ_α(f(x),f(x')) ≤ d(x,x')  Δ_α(∫ f dμ,∫ f dμ')


We can instantiate this on distributions for traces with X = ^ω so can measure difference between trace distributions for states e.g. ν_s,ν_s'. 

We assume whenever we write f that we restrict only to those which are measurable in our space (^ω, F).



Let us define
(t,t') : ^ω×^ω→{0,1} as the indicator function which is one if the arguments are not the same and zero if they are. We also define ^h a restriction considering only the prefix of length h, (t^h is the prefix of length h of trace t).


    (t, t' )=  1    if  t  t' 
     0    otherwise   and   ^h(t, t' )=  1    if  t^h  t'^h 
     0    otherwise
 




 
The use of  is so that Δ_α(f(t),f(t')) ≤(t,t) is rather no restriction at all, since either a trace is the same, thus Δ_α(f(t),f(t')) = 0 or the traces are different and (t,t') = 1. So K_α() takes supremum over all measurable f.



In the following sections we will use the notation f̂(μ) = ∫ f dμ.




 §.§ Proof of Lemma <ref>: α(s,s') = K_α()(ν_s,ν_s')

Whilst we only really require α(s,s') ≤ K_α()(ν_s,ν_s') for our main proof we will show equality, this will give us an alternative representation of α that will prove useful along the way.


α(s,s') ≤ K_α()(ν_s,ν_s')


Consider E ∈F then E is a measurable function in the argument of the supremum of K_α() with ∫E dν_s = ν_s(E) thus Δ_α(ν_s(E), ν_s'(E)) = Δ_α(∫E dν_s,∫E dν_s').



 α(s,s') ≥ K_α()(ν_s,ν_s')
 


We have shown a 1-1 correspondence between indicator functions and events. We further show any function that is not an indicator function does not contribute to the supremum. We proceed first by considering simple functions and extend this to other functions with the Monotone convergence theorem. Our proof follows the technique of <cit.>, however we define our new function explicitly.



    K_α()(μ, μ')= maxsup_f: A^ω→ [0,1]{f̂(μ) - αf̂(μ') },  sup_f: A^ω→ [0,1]{f̂(μ') - αf̂(μ) }


This is symmetric, so without loss of generality we consider only f̂(μ) - αf̂(μ') as our distance.

A simple function f can be described by a finite sum ∑_i a_i A_i, where A_i is the characteristic function on A_i ∈F. This means f takes on finitely many values in its range.

We want to show that if f(a) ∈ (0,1) then we can only increase the value of f̂(μ) - αf̂(μ') by changing to f: A^ω→{0,1}. Note this will maintain that f valid in the restriction of the sup, since we only require to stay measurable.

Since we have f simple then img(f) is finite. Let n = |img(f) ∖{0,1}|

Consider v ∈ img(f_i) ∖{0,1}. Let A_i = {x : f(x) = v}

Then we can define f_i+1 = f_i + g_i with g_i = t ×1_A_i where t is defined as follows:

if μ(A_i) - αμ'(A_i) ≥ 0 we set t = 1-v, this gives us f_i+1(x) = 1 for all x ∈ A_i. Otherwise t = -v so f_i+1(x) = 0 for all x ∈ A_i.

We show f_i+1 gives no smaller value in the supremum.

    f̂_i+1(μ) - αf̂_i+1(μ')    = ∫ f_i+1d(μ) - α∫  f_i+1 d(μ')
       = ∫ f_i + g_i d(μ) - α∫  f_i+1 + g_i d(μ') 
       = ∫ f_i  d(μ) - α∫ f_id(μ') +  ∫ g_i d(μ) - α∫  g_i d(μ') 
       = f̂_i(μ) - αf̂_i (μ') +  t μ(A_i) - α t μ'(A_i)  
       ≥f̂_i(μ) - αf̂_i (μ') Either t>0 and μ(A_i) - αμ'(A_i) ≥ 0 or t<0 and μ(A_i) - αμ'(A_i) < 0

In particular the indicator f_n  is not worse than the simple function f, that is  

    f̂_n(μ) - αf̂_n(μ') ≥f̂(μ) - αf̂(μ').



Consider for f not simple, which can be approximated by h_1, h_2, … simple, converging point-wise to f. Then by monotone convergence principle, with d(a,b) = a - α b continuous.


    lim_n →∞ĥ_n(μ) - αĥ_n(μ') = f̂(μ) - αf̂(μ').


For every simple h_i, we are not smaller than an indicator function. Since it holds for each n we are no larger than an indicator function, the limit is also no larger than the supremum of indicator functions. Therefore indicator functions, which have 1-1 correspondence with events are sufficient in the supremum.



When using  over trace distributions we need only consider the supremum over indicator functions with no restrictions.

    K_α()(μ, μ') = sup_f: X →{0,1}Δ_α(∫ f dμ,∫ f dμ')





 §.§ Proving Lemma <ref>: K_α()(ν_s,ν_s') ≤


Our proof strategy generally follows the strategy of <cit.>. We will show for all prefixes of a trace h restricting  to the prefix will provide the required bound for all h. The main change in this argument is different in the base case, where an additional result (Lemma <ref>) 
is needed to compensate for the fact that Δ_α is not a metric. The induction step is similar, changing only our distance function Δ_α.

We will then extend ^h to the supremum over h, i.e. K_α(). To do this, we will approximate the events in K_α() by cylinders and show that for some h, K_α(^h) is ϵ close to K_α(). An additional lemma to support this is provided in Lemma <ref> and the extension is shown in Lemma <ref>.

This extension from K_α(^h) to K() differs from the strategy of <cit.> who argue it is enough to show continuity of K_V(m) with respect to m. Continuity does hold in our case, but it is unclear to us that this actually shows the result. Since ^h are discrete the ϵ, δ formulation of continuity says at  there exists m such that max_a,b |(a,b)  - m(a,b)| ≤δ, however no such m = ^h satisfies this unless it is exactly  as if it differs in any point, the difference is 1.






  §.§.§ Additional Lemmas


Note that in our case, given Δ_α(f(x),f(x'))=0 we cannot conclude f(x)=f(x'), because Δ_α is not a metric. 
To compensate for this, we show a weaker result that still holds.


Consider f:X→ [0,1] such that ∀ x,x': Δ_α(f(x),f(x')) = 0.
Then ∀μ, μ': Δ_α(f̂(μ),f̂(μ')) = 0.




We consider the range of values f could take, first consider a = inf_x {f(x)}



We know that for all x, Δ_α(f(x),a) ≤ 0. So f(x)-α a ≤ 0 and a-α f(x) ≤ 0. 



f(x) ≤α a and we known f(x)≥ a by definition so f(x) ∈ [a, α a] for all x.




Now consider ∫_X f dμ where f(x) ∈ [a, α a] and ∫_X dμ = 1. 

    f̂(μ)    = ∫_X f dμ≥∫_X a dμ = a ∫_X dμ
    = a
    f̂(μ)    = ∫_X f dμ≤∫_Xα a dμ 
    =  α a ∫_X  dμ
    = α  a


So for all x and μ then f̂(μ) = ∫_X f dμ∈ [a, α a], telling us the expectation must also lie in this range. Next we notice that any two numbers in this range give distance zero, in particualr the expections.


Consider x,y ∈ [a, α a] 

    Δ_α(x,y)    ≤max(x - α y, y - α x, 0) 
       ≤max(α a -  α a, α a - α a, 0) 
       = max(0,0,0) = 0


Therefore Δ_α(f̂(μ),f̂(μ_s)) = 0.




The following lemma generalises the classic result that measure on any measurable event can be approximated by events from the generating set. In our case, the generating set (algebra) corresponds to finite unions of cylinders, which are themselves determined by sequences from Σ^∗.
We show that simultaneous approximation to the same degree of accuracy is  possible for two different measures too.

 

Let (B, B, μ) and (B, B, μ') be measure spaces over the σ-algebra (B, B).  Let A⊂B be an algebra generating B.
S = { X ∈ℬ   |   ∀ϵ ∃ A ∈𝒜 such that μ(A  X)<ϵ and μ'(A  X)< ϵ} also forms a σ-algebra.


We adapt the proof from <https://math.stackexchange.com/questions/228998/approximating-a-sigma-algebra-by-a-generating-algebra> to the case where there are two measures.

To show that a set S is a σ-algebra we require the inclusion of the empty set, closure under complement, and closure under countable unions. We show the full set rather than the empty set in Case 1, which shows the empty set by complement in Case 2. We show finite unions in Case 3 and extend to countable union in Case 4. 


Since B ∈A, B∈S.

 Complement:
If X ∈S and ϵ > 0 then there ∃ A ∈𝒜 such that μ(A  X)<ϵ and μ'(A  X)< ϵ

Then A^c ∈A and μ(A^c  X^c) = μ(A  X) <ϵ, so X^c ∈ S


Finite Union:
Let X_1, X_2 ∈ S then  ∃ A_i ∈𝒜 such that μ(A_i  X_i)<ϵ/2 and μ'(A_i  X_i)< ϵ/2.

μ(X_1 ∪ X_2  A_1 ∪ A_2) ≤μ(X_1 ∪ A_1  X_2 ∪ A_2) ≤ϵ/2 + ϵ/2  = ϵ, similarly for μ' and A_1 ∪ A_2 ∈A so X_1 ∪ X_2 ∈ S.


 Countable Union.
Let {X_k}⊂ S, pairwise disjoint and ϵ > 0. For each k, let A_k ∈A such that μ(A_k  X_k) ≤ϵ/2^k and μ'(A_k  X_k) ≤ϵ/2^k

Take N such that μ(⋃_j > NX_j) ≤ϵ/2 and μ'(⋃_j > NX_j) ≤ϵ/2. (Make μ(⋃_j > NX_j) ≤∑_j > Nμ(X_j) arbitrarily small due to finite  measure, take N big enough so both are μ and μ' sufficiently small).

Let A = ⋃_j=1^N A_j ∈A.

Then (⋃_k X_k) A ⊂⋃_j=1^N(X_j A_j) ∪⋃_j > N X_j

Then μ(⋃_k X_k) A ) ≤μ(⋃_j=1^N(X_j A_j) ∪⋃_j > N X_j) ≤∑_j=1^Nϵ/2^j + ϵ/2≤ϵ and also for μ'.

Then ⋃_k X_k ∈ S








Our stratergy will be to prove the result by induction, we show this is sufficient to extend to K_α() in the following lemma, using Lemma <ref>.



We show if K_α(^h) ≤ for all h then K_α() ≤α.




We now extend to the result from all h to K_α() by showing that ∀ϵ ∃ h such that K_α() - K_α(^h) ≤ϵ (notice K_α() is always larger).

Either 

    K_α()(ν_s, ν_s') = sup_f:^ω→{0,1}∫ fdν_s - α∫ f dν_s' = V

or

    K_α()(ν_s, ν_s') = sup_f:^ω→{0,1}∫ f dν_s' - α∫ f dν_s = V


Assume wlog that we are in the first case and remember by Corollary <ref>, f:^ω→{0,1} are indicator functions. Consider such an f with |V - (∫ fdν_s - α∫ f dν_s')| ≤ϵ/2 (made possible by supremum).

If we show that ∀ϵ ∃ h such that ∫ fdν_s - α∫ f dν_s' - K(^h)(ν_s,ν_s') ≤ϵ /2 then V - K(^h)(ν_s,ν_s') ≤ϵ and we are done.

Let A = {x ∈ A^ω |  f(x) = 1}. Since f measurable then A ∈ then:


    ∫ fdν_s - α∫ f dν_s' = ν_s(A) - αν_s'(A)


By Lemma <ref>, we know ν_s(A) and ν_s'(A) can be approximated by cylinder sets since F⊆ S as F is the smallest σ-algebra generated by combinations of cylinders, so contained in S approximable by cylinders. Let C be a cylinder set such that 

    ν_s(A) -∑_c ∈ Cν_s(c) ≤ϵ/4α and ν_s'(A) -∑_c ∈ Cν_s'(c) ≤ϵ/4α


We assume without loss of generality that all prefixes in C are of length h. If not generalise all prefix's shorter than the maximum length h by adding all possible suffixes to make length h.



    ∑_c ∈ Cν_s(c) - α∑_c ∈ Cν_s'(c) 
    
       ≤∑_c ∈ C g(c) (ν_s(c) - αν_s'(c)) 
    
       ≤ K_α(^h)(ν_s, ν_s')


    g(c) =  1    ν_s(c) - αν_s'(c) > 0 
     0     otherwise


If K_α(^h)(ν_s, ν_s') > ν_s(A) - αν_s'(A) then as K_α()(ν_s, ν_s') ≥ K_α(^h)(ν_s, ν_s') so K_α()(ν_s, ν_s') - K_α(^h)(ν_s, ν_s') ≤ϵ/2≤ϵ already.

Otherwise

    ν_s(A) - αν_s'(A) - K_α(^h)(ν_s, ν_s')
    
       ≤ν_s(A) - αν_s'(A) - (∑_c ∈ Cν_s(c) - α∑_c ∈ Cν_s'(c))
    
       ≤ |ν_s(A)- ∑_c ∈ Cν_s(c)| + α|ν_s'(A) -∑_c ∈ Cν_s'(c)| 
    
       ≤ϵ/4α + αϵ/4α≤ϵ/2





  §.§.§ Proof of Lemma <ref>


To show K_α()(ν_s,ν_s') ≤ we show by induction on h:


    K(^h)(ν_s,ν_s') ≤ bd_α(s,s)
 
for all h and the result follows from Lemma <ref>.




  
Base Case: h=0
In the base case, we show that K_α(^0) =0. Thus it is necessarily smaller than any value of bd_α.


    K_α(^h)(ν_s,ν_s')  =  sup_f: A^ω→ [0,1]
    Δ_α(f(t),f(t')) ≤^h(t,t)  ∀ t,t' ∈ A^ωΔ_α(f̂(ν_s), f̂(ν_s'))

But since ^h = 0, then 

    K_α(^h)(ν_s,ν_s')  =  sup_f: A^ω→ [0,1]
    Δ_α(f(t),f(t')) ≤ 0  ∀ t,t' ∈ A^ωΔ_α(f̂(ν_s), f̂(ν_s'))

Then we know by Lemma <ref> that Δ_α(f(t),f(t')) ≤ 0 for all t,t' ∈ A^ω then Δ_α(f̂(ν_s), f̂(ν_s')) = 0 and we obtain:

    K_α(^h)(ν_s,ν_s')  =  sup_f: A^ω→ [0,1] | Δ_α(f(t),f(t')) ≤ 0{0 } = 0


Therefore K_α(^h)(ν_s,ν_s') =0 ≤ bd_α(s,s')



  
Induction Case:


We assume K_α(^h)(ν_s,ν_s') ≤ bd_α(s,s') and show K_α(^h + 1)(ν_s,ν_s') ≤ bd_α(s,s')






Case 1:
(s) (s') then bd_α(s,s') = 1 ≥ K_α(^h+1)(ν_s,ν_s') 


Case 2: (s) = (s') = a ∈

The strategy is to consider a function f: ^ω→ [0,1] valid under K_α(^h+1). We will construct a function g:S→ [0,1] valid under the expansion of  with the same difference of expectations. This will allow us to conclude the sumpremum in K_α(^h+1) ≤
	


We show a function that is valid under ^h+1 to first find a function valid under ^h.

Consider an f such that Δ_α(f(t),f(t')) ≤^h+1(t,t') for all t,t' ∈ A^ω and let f_a(t) = f(at).


 Δ_α(f_a(t), f_a(t')) ≤^h(t,t').


    Δ_α(f_a(t), f_a(t'))    = Δ_α(f(at), f(at')) by defn of f_a
       ≤^h+1(at,at')    =  0     at^h = at'^h
     1    otherwiseby assumption on f
       = ^h(t,t')    =   0     t^h = t'^h
     1    otherwise


Given this function we find a function g which is valid in the restrictions in K_α() = thus the difference of expectations of g is below .

Let 
    g(s) = f̂_a(ν_s) =∫_A^ω f_a dν_s



For all s,s': Δ_α(g(s), g(s'))≤ bd_α(s,s')


    Δ_α(g(s), g(s'))    = Δ_α(f̂_a(ν_s),f̂_a(ν_s') by definition of g
       ≤ K_α(^h)(ν_s,ν_s') 
    
       = sup_f: A^ω→ [0,1]
    Δ_α(f(t),f(t')) ≤^h(t,t') ∀ t,t' ∈ A^ω{Δ_α( f̂(ν_s),  f̂(ν_s') ) }f_a is one such f, Property <ref>
       ≤ bd_α(s,s') induction assumption
 

We show the difference of expectation of g is equal to the difference of expectation of f:

















f̂(ν_s)= ĝ(μ_s)


    f̂(ν_s)    = ∫_A^ω f dν_s 
       = ∫_A^ω starting a f dν_s s can only yield a
       = ∫_A^ω f_a Σ_s_i ∈ Sμ_s(s_i) dν_s_isμ_s
       = Σ_s_i ∈ Sμ_s(s_i)  ∫_A^ω f_a  dν_s_i
       = Σ_s_i ∈ Sμ_s(s_i)  g(s_i) definition of g
       = ĝ(μ_s) expectation of g










This allows us to plant the difference of expectation of g (and thus f) below the supremum defining the fixed point and thus below the fixed point.


Δ_α(f̂(ν_s), f̂(ν_s')) ≤ bd_α(s,s')


    Δ_α(f̂(ν_s), f̂(ν_s'))    = Δ_α(ĝ(μ_s), ĝ(μ_s')) Property <ref>
       ≤ K_α(bd_α)(μ_s, μ_s') = sup_f: S → [0,1]
    Δ_α(f(s),f(s')) ≤ bd_α(s,s') ∀ s,s' ∈ S{Δ_α( f̂(μ_s),  f̂(μ_s') ) }g is such an f, by Property <ref>
       ≤ bd_α(s,s') Γ_α(bd_α) ≤ bd_α by definition


Since by Property <ref> we have Δ_α(f̂(ν_s), f̂(ν_s')) ≤ bd_α(s,s') for all f satisfying ^h+1 then we also have it in the supremum.

Thus:


    K_α(^h + 1)(ν_s,ν_s')    = sup_f: A^ω→ [0,1] 
    Δ_α(f(t),f(t')) ≤^h+1(t,t') ∀ t,t' ∈ A^ωΔ_α( f̂(ν_s),  f̂(ν_s') )
    
       ≤ bd_α(s,s')




















§ DUAL FORM OF SKEWED KANTOROVICH (PROOF OF LEMMA <REF>)


The primal form can be expressed as the following LP:

    [ max_f⃗∈ [0,1]^nf⃗·c⃗;           Subject to;              A f⃗≤m⃗;  ]

Where:

    [ c⃗_i = μ_i -αυ_i;   A_(i,j), i = 1;  A_(i,j), j = -α; A_(i,i), i = 1-α ]










We consider an equivalent LP in standard form, to achieve this we separate f⃗∈ [0,1]^n into two vectors a⃗,b⃗∈ [0,1]^n, with a⃗ = b⃗ (intended to be equal to f⃗). We obtain the following linear program in standard form:
 

    max_a⃗,b⃗∈ R_+^n(μ, -αν)[ a⃗; b⃗ ]

  Subject to:
  
    [  A A';  I -I; -I  I;  I  0 ][ a⃗; b⃗ ]≤[ m⃗; 0⃗; 0⃗; 1⃗ ]

Where 


    [                     A_(i,j), i = 1;                   A'_(i,j), j = -α; I  is the standard identity matrix;              0  is the zero matrix ]



(A,A') [ a⃗; b⃗ ]≤m⃗ specify the skewed distance must be less than m. (I, - I)[ a⃗; b⃗ ]≤0⃗ and (-I, I)[ a⃗; b⃗ ]≤0⃗ work to specify a⃗ = b⃗. (I, 0)[ a⃗; b⃗ ]≤1⃗ specifies a⃗≤1 (the condition f⃗∈ [0,1]). 

This results in the following dual form following standard techniques.

    min_ω∈ [0,1]^n× n, γ,τ,η∈[0,1]^n∑_i,jω_i,j m(i,j) + ∑_i η_i
       Subject to:
       ∀ i: ∑_jω_i,j -γ_i + τ_i  + η_i ≥μ_i 
       ∀ j: ∑_iαω_i,j -γ_j + τ_j ≤αν_j


It would be possible to merge τ_i, γ_i ∈ [0,1] into a single variable in [-1,1], but for consistency with the standard requirement of linear programs and the transportation problem intuition we keep them separate.

We can set the first equation to equality, since there is no sense over-satisfying it (reduce ω_i,j, τ_i, η_i or increase γ_i with no violation of other constraints). For parity with standard couplings we would like to remove γ, τ, η and ≤. 












 

