# Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant

Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel

► To cite this version:

Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel. Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. 2023. [hal-03782650v2](https://hal-03782650v2)

HAL Id: hal-03782650

https://ut3-toulouseinp.hal.science/hal-03782650v2

Preprint submitted on 27 Feb 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Bel-Games:

## A Formal Theory of Games
of Incomplete Information
Based on Belief Functions
in the Coq Proof Assistant*

Pierre Pomeret-Coquot

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>

IRIT, Université de Toulouse III – Paul Sabatier, France

Hélène Fargier

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /></figure>

IRIT, CNRS, Toulouse, France

Érik Martin-Dorel

<figure><img src="image_6.png" /></figure>

<figure><img src="image_7.png" /></figure>

IRIT, Université de Toulouse III – Paul Sabatier, France

## Abstract

Decision theory and game theory are both interdisciplinary domains that focus on modelling and analyzing decision-making processes. On the one hand, decision theory aims to account for the possible behaviors of an agent with respect to an uncertain situation. It thus provides several frameworks to describe the decision-making processes in this context, including that of belief functions. On the other hand, game theory focuses on multi-agent decisions, typically with probabilistic uncertainty (if any), hence the so-called class of Bayesian games. In this paper, we use the Coq/SSReflect proof assistant to formally prove the results we obtained in [29]. First, we formalize a general theory of belief functions with finite support, and structures and solutions concepts from game theory. On top of that, we extend Bayesian games to the theory of belief functions, so that we obtain a more expressive class of games we refer to as Bel games; it makes it possible to better capture human behaviors with respect to lack of information. Next, we provide three different proofs of an extended version of the so-called Howson-Rosenthal's theorem, showing that Bel games can be turned into games of complete information, i.e., without any uncertainty. Doing so, we embed this class of games into classical game theory and thus enable the use of existing algorithms.

**2012 ACM Subject Classification** Theory of computation → Logic and verification; Theory of computation → Type theory; Theory of computation → Higher order logic; Theory of computation → Algorithmic game theory; Theory of computation → Solution concepts in game theory; Theory of computation → Representations of games and their complexity

**Keywords and phrases** Game of Incomplete Information, Belief Function Theory, Coq Proof Assistant, SSReflect Proof Language, MathComp Library

**Related Version** Paper-and-pencil proof article: doi:10.1016/j.ijar.2022.09.010 [29]

Formal proofs repository: https://github.com/pPomCo/belgames

**Funding** Pierre Pomeret-Coquot: ANITI, funded by the French "Investing for the Future – PIA3" program under the Grant agreement n°ANR-19-PI3A-0004.

<footnote>*Copyright © Pierre Pomeret-Coquot and Hélène Fargier and Érik Martin-Dorel; Licensed under Creative Commons License CC-BY 4.0</footnote>
# 1 Introduction

38

39

40

41

42

43

44

45

46

47

From a mathematical perspective, measure theory is a fundamental domain to learn and use, notably given its direct application to integration and probability theory. Several works thus focused on formalizing measure theory in type theory, e.g., relying on reference textbooks [14]. Next, probability play a key role in the context of game theory, gathering several multi-agent frameworks that can model situations in many application areas such as economics, politics, logics, artificial intelligence, biology, and so on. In particular, the framework of Bayesian games (a class of games of incomplete information), has been well-studied by the decision theory community [13, 25]. However, using probability and additive measures appears to be unsatisfactory to model subtle decision-making situations with uncertainty.

48

49

50

51

52

53

54

55

56

57

58

In this work, we aim to show that the belief function theory also is amenable to formal proof, and makes it possible to formally verify the correctness of three state-of-the-art algorithms. In [11, 29], we introduced the notion of *Bel games*, which faithfully models games of incomplete information where the uncertainty is expressed within the *Dempster-Shafer theory of belief functions*. This framework naturally encompass Bayesian games, as belief functions generalize probability measures. Also, we generalized the *Howson-Rosenthal theorem* to the framework of Bel games and proposed three transforms which make it possible to cast any Bel game into an equivalent game of complete information (without any uncertainty). Furthermore, these transforms preserve the space complexity of the original Bel game (they produce a game with a succinct representation, corresponding to the class of so-called hypergraphical games).

59

60

61

62

63

64

65

66

67

68

69

**Contributions.** In the present paper, we consolidate the mathematical results previously published in [29], presenting a formal verification of our algorithms using the Coq proof assistant [6]. First, we formalize a general theory of belief functions. Then, we formalize structures and solution concepts for “standard” games, Bayesian games, and Bel games, and we formally prove the correctness of the three transform algorithms, in order to provide strong confidence on these results. The software artifact obtained was released under the MIT license and is available within the official Coq projects OPAM archive. Our formalization effort also resulted in more background lemmas, integrated in the MathComp library. To the best of our knowledge, it is the first time the theory of belief functions is mechanized in a formal proof assistant, and applied to the domain of (formal) game theory of incomplete information.

70

71

72

73

74

75

76

77

78

79

80

81

82

83

**Related works.** Several formalization efforts have been carried out in game theory since 2006, each focusing on a somewhat different fragment: Vestergaard [34] then Le Roux [30], formalizing Kuhn’s existence of a Nash equilibrium in finite games in extensive form, using Coq; Lescanne et al. [21], studying rationality of infinite games in extensive form, using Coq; Martin-Dorel et al. [23], studying the probability of existence of winning strategies in Boolean finite games, using Coq; Bagnall et al. [4], formalizing well-known results of algorithmic game theory, using Coq; Dittmann [8], proving the positional determinacy of parity games, using Isabelle/HOL; Le Roux et al. [19], proving that a determinacy assumption implies the existence of Nash equilibrium in 2-player games, using Coq and Isabelle/HOL; this result being combined with that of Dittmann, using Isabelle/HOL [20]. Game theory aside, numerous works have been carried out in proof assistants to formalize probability and/or measure theory. Regarding the Coq proof assistant, we can mention the recent works by Affeldt et al. (on information theory based on discrete probability theory [2]; and measure theory based on MathComp [1]) and Boldo et al. [5], focusing on Lebesgue’s integral theory.

84

**Paper outline.** We start by introducing a motivating example, for which the Bayesian
approach fails but the Dempster-Shafer approach succeeds. Then, we incrementally present the Coq formalization of Bel games, giving successively the main mathematical definitions and lemmas and their formal Coq counterpart, throughout the paper: Section 3 presents the Dempster-Shafer theory of belief functions; then Section 4 focuses on complete-information games (including hypergraphical games) while Section 5 deals with Bel games; then Section 6 is devoted to our formalization of Howson-Rosenthal's generalized theorem in the scope of *n*-player Bel games. Finally, Section 7 gives concluding remarks and perspectives.

## 2 Motivating Example: the Murder of Mr. Jones

**► Example 1 (Inspired by the Murder of Mr. Jones, [33]).** Two players, named Player 1 and Player 2, are independently looking for an association, with either Peter (*P*), Quentin (*Q*), or Rose (*R*). The point is that a crime has been committed, for which these three people only are suspected. Furthermore, a poor-quality surveillance video allows to estimate that there is a 50% chance that the culprit is a man (*P* or *Q*), and a 50% chance that it is a woman (*R*). As to the interest of the associations, making the deal with an innocent people leads to a payoff of $6k, to be shared between the people making the deal (that is, $2k or $3k depending on if the players choose the same partner or not); associating with the culprit produces no payoff ($0k). Moreover, Player 1 is investigating about *P* and will know whether he is guilty before making the decision. Similarly, Player 2 will know whether *R* is guilty.

The Bayesian approach (claiming any knowledge shall be described by a single subjective probability) is not well-suited here. Assume Player 1 learns that *P* is innocent. It should not impact the evidence of 50% chance per sex, so the probability of guilt should become 1/2 for *Q* and 1/2 for *R*. However, in a purely Bayesian view, a prior probability must be made explicit (e.g. by equiprobability assumption: 1/4 for *P*, 1/4 for *Q* and 1/2 for *R*), so after conditioning the posterior probability would not give 50% chance per sex anymore: equiprobability and conditioning “given $\neg P$” yields 1/3 for *Q* and 2/3 for *R*: learning that *P* is innocent would increase the odds against *R*! In the sequel, we will reuse this example to highlight how the framework of belief functions better captures uncertain knowledge.

## 3 Formalization of Belief Functions for Mono-Agent Decision Making

Modelling mono-agent decision making under uncertainty involves three main tasks. First, knowledge has to be expressed in a well-suited representation, encoding what is known without making extra assumptions. Then, if the agent may learn or observe some event before the decision, one shall identify the relevant conditioning rule. Finally, the agent's preferences must be captured by a compatible decision rule. In this work, we focus on real-valued utility-based decision rules, which evaluate uncertain outcomes so that the agent prefers outcomes with a bigger score. For example, modelling well-known variable phenomena can perfectly be captured in a probabilistic setting: a probability represents the variability; conditional probability updates knowledge; and preferences over uncertain outcomes may be captured by expected utility. Still, this approach may be unsuccessful to model other kinds of uncertainty.

In the sequel, we rely on belief function theory, which generalizes probability theory and enables capturing both variability and ignorance. In this section, we focus on a single decision maker, while the material from Section 4 will deal with multi-agent decision making.
127

## 3.1 Belief functions

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

The theory of belief functions is a powerful toolset from decision theory and statistics. It encompasses two distinct approaches for reasoning under uncertainty: the Dempster-Shafer theory of evidence (DS) [7, 31] and the upper-lower probability theory (ULP) [7, 35]. Both approaches consider a finite set of possible “states of the world” $\Omega = \{\omega_1, \dots, \omega_n\}$, one of which being the actual state of the world $\omega^*$, and three functions $m$, Bel and Pl: $2^\Omega \to [0, 1]$ which all map subsets of $\Omega$ to real numbers. Those functions are deducible one from another. In the DS theory, the mass function $m$ is the basic knowledge about the world ($m(A)$ is the part of belief supporting the evidence $\omega^* \in A$: it asserts that $A$ holds but cannot be refined into smaller claims). The non-additive continuous measures Bel and Pl indicate how much a proposition is implied by (resp. is compatible with) the knowledge. By contrast, the ULP theory suppose that there is an unknown probability $\text{Pr}^*$ which is bounded by Bel and Pl: $\forall A, \text{Bel}(A) \le \text{Pr}^*(A) \le \text{Pl}(A)$; then $m$ is just a concise representation of the family of compatible probabilities.

Example 1 can be understood in both theories. In the DS theory, $m(\{P, Q\}) = m(\{R\}) = 1/2$ directly encodes the given evidences. In the ULP theory, one rather considers the family of probabilities which satisfy $\text{Pr}(\{P, Q\}) = \text{Pr}(\{R\}) = 1/2$ (see Table 1).

<table><caption>Table 1 Prior knowledge from Example 1 — in the DS theory, $m$ directly describes the knowledge, in the ULP theory, $m$ describes a family of probability measures $(\text{Pr}_x)_{x \in [0, 0.5]}$.</caption><thead><tr><th>A &sub; &Omega;</th><th>&empty;</th><th>{P}</th><th>{Q}</th><th>{R}</th><th>{P, Q}</th><th>{P, R}</th><th>{Q, R}</th><th>{P, Q, R}</th></tr></thead><tbody><tr><th>m(A)</th><td>0</td><td>0</td><td>0</td><td>0.5</td><td>0.5</td><td>0</td><td>0</td><td>0</td></tr><tr><th>Bel(A)</th><td>0</td><td>0</td><td>0</td><td>0.5</td><td>0.5</td><td>0.5</td><td>0.5</td><td>1</td></tr><tr><th>Pl(A)</th><td>0</td><td>0.5</td><td>0.5</td><td>0.5</td><td>0.5</td><td>1</td><td>1</td><td>1</td></tr><tr><th>Pr<sub>x</sub>(A)</th><td>0</td><td>x</td><td>0.5 &minus; x</td><td>0.5</td><td>0.5</td><td>0.5 + x</td><td>1 &minus; x</td><td>1</td></tr></tbody></table>

144

145

146

147

In this work, we follow the DS approach and we base our formalization on the mass function $m$. To do so, we use the Coq proof assistant, relying on the MathComp library [22] that provides a comprehensive formalization of finite sets, functions with finite support (endowed with decidable equality) as well as big operators.<fnref n="1" />

148

149

► **Definition 1 (Frame of discernment).** A frame of discernment is a finite set $\Omega$, representing the possible states of the world. One of them is the actual state of the world $\omega^*$.

150

151

► **Definition 2 (Events).** A set $A \subseteq \Omega$ is an event which represents the proposition "$\omega^* \in A$". All set functions we consider ($m$, Bel, Pl) map events to real numbers within $[0, 1]$.

152

153

154

The set $\Omega$ and the carrier of $m$, Bel and Pl are formalized in MathComp by asserting:

Variable (W : finType) (R : realFieldType).

155

156

► **Definition 3 (Basic probability assignment).** A basic probability assignment (bpa), a.k.a. mass function, is a set-function $m: 2^\Omega \to [0, 1]$ such that

158

$$m(\emptyset) = 0 \quad \text{and} \quad \sum_{A \subseteq \Omega} m(A) = 1 \quad \text{and} \quad \forall A \subseteq \Omega, m(A) \ge 0. \quad \text{Formally:} \quad (1)$$

159

<footnote n="1">¹ MathComp notations: `{set X}` denotes finite sets over `(X : finType)`, `A:&:B = A ∩ B`, `A:|:B = A ∪ B`, `~:A = A<sup>c</sup>`, `set0 = ∅`; `{ffun X -> Y}` denotes the type of finite support functions from `(X : finType)` to `(Y : Type)`; and for any `(T : X -> Type)`, `{ffun <sub>forall</sub> x : X, T x}` denotes the type of finite support functions with a dependently-typed codomain, mapping any `(x : X)` to an element of `(T x)`.</footnote>
Definition bpa_ axiom (m : {ffun {set W} -> R}) :=
[&& m set0 == 0, \sum_A m A == 1 & [∀A, m A >= 0]].
Structure bpa := { bpa_val :> {ffun {set W} -> R} ; bpa ax : bpa_ axiom bpa_val }.

► **Definition 4 (Belief function, plausibility measure).** Given a bpa m over Ω, the associated belief function Bel : 2^Ω -> [0, 1] and plausibility measure Pl : 2^Ω -> [0, 1] are defined by:

$$
\text{Bel}(A) = \sum_{B \subseteq A} m(B) \quad \text{and} \quad \text{Pl}(A) = \sum_{B \cap A \neq \emptyset} m(B). \quad \text{Formally:}
$$

Definition Bel (m : bpa) : {set W} -> R := fun A => \sum_(B | B \subset A) m B.
Definition Pl (m : bpa) : {set W} -> R := fun A => \sum_(B | B :&: A != set0) m B.

► **Proposition 1 (Duality).** For any $A \subseteq \Omega$, $\text{Pl}(A) = 1 - \text{Bel}(A^c)$ and $\text{Bel}(A) = 1 - \text{Pl}(A^c)$.

► **Proposition 2 (Super- and sub-additivity).** Bel is super-additive while Pl is sub-additive:
for disjoint sets A, B ⊆ Ω, Bel(A ∪ B) ≥ Bel(A) + Bel(B) and Pl(A ∪ B) ≤ Pl(A) + Pl(B).

► **Proposition 3 (Bounds).** $0 = \text{Bel}(\emptyset) = \text{Pl}(\emptyset) \le \text{Bel}(A) \le \text{Pl}(A) \le \text{Bel}(\Omega) = \text{Pl}(\Omega) = 1$, for any $A \subseteq \Omega$. These propositions have been formally proved, with the following statements:

Lemma BelE (m : bpa) (A : {set W}) : Bel m A = 1 - Pl m (~:A).
Lemma Bel_super m A B : [disjoint A & B] -> Bel m (A :|: B) >= Bel m A + Bel m B.
Lemma Bel0 (m : bpa) : Bel m set0 = 0. (* and likewise for Pl *)

► **Definition 5 (Focal elements, focal set).** Given a bpa m over Ω, any subset $A \subseteq \Omega$ with a non-zero mass $m(A)$ is called focal element, and the set of focal elements of m is called the focal set of m and denoted by $S_m$. Formally:

Definition focal_element (m : bpa) : pred {set W} := fun A => m A > 0.
Definition focalset (m : bpa) : {set {set W}} := [set A | focalElement m A].

► **Proposition 4 (Focal elements, focal set).** Given a bpa m over Ω, Definition 4 can straightforwardly be rephrased by rewriting the sums over the focal set:

$$
\text{Bel}(A) = \sum_{B \subseteq A} m(B) \quad \text{and} \quad \text{Pl}(A) = \sum_{B \cap A \neq \emptyset} m(B). \quad \text{Formally:}
$$

Lemma Bel_focalsetE m A : Bel m A = \sum_(B in focalset m | B \subset A) m B.
Lemma Pl_focalsetE m A : Pl m A = \sum_(B in focalset m | B :&: A != set0) m B.

Next, we recall a standard “complexity definition” about belief functions, that will prove useful to characterize probability measures:

► **Definition 6 (k-additivity).** Given a bpa m over Ω and $k \in \mathbb{N}^*$, we say that the bpa m is k-additive iff the cardinality of its focal elements is at most k. Formally:

Definition k_additivity m := \max_(B in focalset m) #|B|.

► **Proposition 5 (Probability measure).** Given a bpa m over Ω, if m is 1-additive, i.e. if all focal elements are singletons, then Bel = Pl is a discrete probability measure, associated with the distribution $x \in \Omega \mapsto m(\{\omega\})$. Formally:

Structure proba := { proba_val :> bpa ; proba ax : k_additivity proba_val == 1 }.
Lemma PrE (m : proba) (A : {set W}) : Bel m A = Pl m A.
Definition dist (m : proba) := fun w ⇒ m [set w]. (*[set w] corresponds to {w} *)
Lemma Pr_distE (m : proba) A : Bel m A = \sum_(w in A) dist m w.
214

## 3.2 Conditioning in the Belief Function Theory

215

216

217

218

219

220

Conditioning is the operation that captures knowledge revision (fact learning) as well as focusing (hypothesis) [10, 9, 12]. By turning a prior bpa into a posterior “given an event C”, one updates the knowledge so it now asserts that C is certain. Several conditioning rules for belief functions have been proposed, depending on the DS or ULP interpretation (cf. Section 3.1) and on the kind of update it involves. Starting from the same prior bpa, they yield distinct posteriors—they indeed capture distinct operations.

221

222

223

224

225

Before dealing with conditional events (·|C)—read “given C”—a precondition happens to be necessary: on the technical side, it avoids division-by-zero, and on the semantics side, it means one cannot learn that an impossible event holds. Since the definition of this precondition is specific to each conditioning rule, we abstract it away in the form of a *revisable* predicate, which indicates whether an event can be assumed.

226

227

228

**► Definition 7 (Conditioning).** Given a bpa m, a predicate revisable<sub>m</sub>: Ω → {1, 0} and an event C ⊆ Ω such that revisable<sub>m</sub>(C) holds, a conditioning turns m into the bpa m(·|<sub>cond</sub> C) such that Bel(C<sup>c</sup>|<sub>cond</sub> C) = 0. Formally:

229

230

231

232

Definition conditioning_ axiom (revisable : bpa -> pred {set W})
(Cond : ∀m C, revisable m C -> bpa) :=
∀m C (Hrev : revisable m C), Bel (Cond m C Hrev) (¬:C) = 0.

233

234

235

236

237

In other words, assuming the event *C* is revisable implies that if one learns that *C* holds, then one also learns that no evidence for the complement can hold. Next, we formalize a *conditioning* structure that encapsulates the revisable predicate, the conditioning algorithm itself—which turns a revisable prior in its posterior “given *C*”—and a proof of the *conditioning_ axiom*:

238

239

240

241

Structure conditioning := { revisable : bpa -> pred {set W} ;
                      cond_val -> ∀m C, revisable m C -> bpa ;
                      cond ax : conditioning_ axiom cond_val }.

242

243

244

245

246

247

248

249

The most common conditioning is the so-called Dempster's conditioning [7], which captures knowledge revision (i.e., fact learning). In the DS framework, it is understood as a transfer of parts of beliefs: learning that *C* holds, *m*(*B*) is transferred to *B* ∩ *C* if it is not empty, or discarded otherwise (then the posterior has to be renormalized due to Equation (1)). That is, the evidence now concerns *B* ∩ *C*, the only possible states of the world “given that *C* holds”. In the ULP framework, it is understood as a max-likelihood conditioning: the posterior probability family delimited by Bel(·|*C*) and Pl(·|*C*) is the conditioning of those prior probabilities which assign the maximal probability to event *C*, that we now know for sure.

250

251

**► Definition 8 (Dempster's conditioning).** For any bpa m and any event C such that Pl(C) ≠ 0, Dempster's conditioning defines the bpa: m(A|D C) = Σ<sub>B∩C=A≠0</sub> m(B)/Pl(C).

252

253

254

255

256

257

258

259

Definition Dempster_revisable m C := Pl m C != 0.
Definition Dempster Fun (m : bpa) (C : {set W}) := [ffun A : {set W} =>
  if A == set0 then 0
  else \sum_(B : {set W} | (B \in focalset m) && (B :&: C == A)) m B / Pl m C].
Program Definition Dempster_cond m C (Hrev : Dempster_revisable m C) : bpa :=
  {| bpa_val := Dempster Fun m C ; bpa ax := _ |}.
Program Definition Dempster_conditioning : conditioning :=
  {| cond_val := Dempster_cond ; cond ax := _ |}.

260

261

262

**► Example 2 (Knowledge revision, follow-up of Example 1/Table 1).** Dempster's conditioning is the conditioning approach fitting our example (see [9] for details). Suppose e.g. the murderer
is $\mathcal{Q}$; Player 1 learns $\omega^* \notin \{P\}$, i.e., $\omega^* \in \{Q, R\}$. From this viewpoint, the evidence concerning men now only concerns $\mathcal{Q}$: the knowledge becomes $m(\{\mathcal{Q}\}) = m(\{R\}) = 0.5$ (Fig. 1, center). Player 2 learns $\omega^* \notin \{R\}$, i.e., $\omega^* \in \{P, \mathcal{Q}\}$. From this viewpoint, the evidence about women is discarded: the knowledge becomes $m(\{P, \mathcal{Q}\}) = 1$ (Fig. 1, right).

<figure><img src="image_8.png" /><figcaption>Figure 1 Prior (left) and posteriors given $\{Q, R\}$ (center) and given $\{P, Q\}$ (right). White and gray areas denote possible and impossible events – circles denote focal elements.</figcaption></figure>

**Proposition 6 (Dempster's conditioning, Pl).** For any bpa $m$ and any event $C$ such that $Pl(C) \neq 0$, we have $Pl(A|_D C) = Pl(A \cap C)/Pl(C)$. Formally:

Lemma Demspter_condE m C (Hrev : revisable m C) :
$\forall A, Pl (Dempster_conditioning m C Hrev) A = Pl m (A :&: C) / Pl m C.$

Two other rules have been proposed and called strong (resp. weak) conditioning [28]; the former, also known as geometrical conditioning [32], is another rule capturing knowledge revision; the latter is seldom used since it yields non-intuitive results (e.g., it may happen that $Bel(C|C) < 1$). We also formalize these two rules below.

**Definition 9 (Strong conditioning).** For any bpa $m$ and any event $C$ such that $Bel(C) \neq 0$, the weak conditioning is defined by the bpa $m(A|_S C) = m(A)/Bel(C)$ if $A \subseteq C$, 0 otherwise.

Definition Strong_revisable m C := Bel m C !:= 0.
Definition Strong Fun (m : bpa) (C : {set W}) := [ffun A : {set W} ⇒
if (A != set0) && (A \subset C) then m A / Bel m C else 0].
Program Definition Strong_cond m C (Hrev : Strong_revisable m C) : bpa :=
{| bpa_val := Strong Fun m C ; bpa ax := _ |}.
Program Definition Strong_conditioning : conditioning :=
{| cond_val := Strong_cond ; cond ax := _ |}.

**Proposition 7 (Strong conditioning, Bel).** For any bpa $m$ and any event $C$ such that $Bel(C) \neq 0$, we have $Bel(A|_S C) = Bel(A \cap C)/Bel(C)$. Formally:

Lemma Strong_condE m C (Hrev : revisable m C) :
$\forall A, Bel (Strong_conditioning m C Hrev) A = Bel m (A :&: C) / Bel m C.$

**Definition 10 (Weak conditioning).** For any bpa $m$ and any event $C$ such that $Pl(C) \neq 0$, the weak conditioning is defined by the bpa: $m(A|_W C) = m(A)/Pl(B)$ if $A \cap B \neq \emptyset$, 0 otherwise. Formally:

Definition Weak_revisable m C := Pl m C !:= 0.
Definition Weak Fun (m : bpa) (C : {set W}) := [ffun A : {set W} ⇒
if A :&: C != set0 then m A / Pl m C else 0].
Program Definition Weak_cond m C (Hrev : Weak_revisable m C) : bpa :=
{| bpa_val := Weak Fun m C ; bpa ax := _ |}.
Program Definition Weak_conditioning : conditioning :=
{| cond_val := Weak_cond ; cond ax := _ |}.

**Proposition 8 (Weak conditioning, Bel).** For any bpa $m$ and any event $C$ such that $Pl(C) \neq 0$, we have $Bel(A|_W C) = (Bel(A) - Bel(A \setminus C))/Pl(C)$. Formally:

Lemma Weak_condE m C (Hrev : revisable m C) :
$\forall A, Bel (Weak_conditioning m C Hrev) A = (Bel m A - Bel m (A :\: C)) / Pl m C.$
315

## 3.3 Decision Making with Belief Functions

316

317

318

319

320

321

322

323

324

325

326

327

328

329

330

331

332

333

334

335

336

337

338

Consider a single agent decision involving several actions; let $A$ denote the set of all these actions. Also, assume that the outcome of choosing any $a \in A$ is not certain: it may lead to several outcomes depending on the actual state of the world $\omega^*$. The agent's preferences on outcomes (which are left implicit here) are expressed by a real-valued utility function $u: A \times \Omega \to \mathbb{R}$: $u(a, \omega) > u(a', \omega')$ would mean the agent prefers the outcome of $a$ when $\omega^* = \omega$ to the outcome of $a'$ when $\omega^* = \omega'$. For any action $a$, let $u_a: \Omega \to \mathbb{R}$ denote the partial application of $u$: $u_a$ provides the utility of $a$ depending on the state of the world $\omega$.

Preferences under uncertainty are then defined on $u_a$'s: a relation $u_a \succ u_{a'}$ would encode the fact the agent prefers $a$ to $a'$. In a probabilistic setting, it is meaningful to consider $u_a$'s expectation w.r.t. the probability (hence the name *expected utility*). Using bpa's, several approaches were defined, each modelling various preferences when facing ignorance. In [29], we analyzed three standard functions that generalize expected utility. They provide real values, and thus lead to completely ordered preferences over actions (since every two actions are directly comparable from their score). We denoted them CEU, JEU, and TBEU, respectively, for Choquet-, Jaffray-, and Transferable Belief-Expected Utility. We have shown they are all expressible as the integration of a particular $\varphi_{u_a}^{\text{XEU}}$ function (resp. $\varphi_{u_a}^{\text{CEU}}$, $\varphi_{u_a}^{\text{JEU}}$, and $\varphi_{u_a}^{\text{TBEU}}$) over the powerset $2^\Omega$. Those $\varphi_{u_a}^{\text{XEU}}$ functionals are themselves parametrized by $u_a = \omega \mapsto u(a, \omega)$, that is, by the utility function when $a$ is chosen. As a result, these three scoring functions can be captured by instances of a single higher-order function, which we named XEU.

339

**Definition 11 (Generalized expected utility).** For any bpa $m$, any utility function $u: A \times \Omega \to \mathbb{R}$, and any $a \in A$, let us pose $u_a = \omega \mapsto u(a, \omega)$. Let $\varphi: (\Omega \to \mathbb{R}) \to (2^\Omega \to \mathbb{R})$ be a parameter function. We then consider the following generalized expected utility of $a$:

$$ \text{XEU}(m)(\varphi(u_a)) = \sum_{B \in \mathcal{S}_m} m(B) \times \varphi(u_a)(B). \quad \text{Formally:} $$

341

342

343

**Definition** XEU ($m$: bpa) ($\text{phi}_{u_a}$: {$\text{ffun}\{\text{set } W\} \to \mathbb{R}\}$): $R := \sum_{(B \text{ in focalset } m)} m(B) * \text{phi}_{u_a} B$.

344

345

346

347

348

349

Let us review these $\varphi^{\text{XEU}}$ functions, their underlying intuition and formal definition in Coq.

A very common scoring function for belief functions is the Choquet discrete integral (CEU). It models a somehow pessimistic agent. In the ULP interpretation, Bel and Pl delimit a family of probabilities; the CEU computes the minimal expected utility that the family allows. In the DS interpretation, each mass is an evidence supporting an event, for which the CEU only consider its worst-case utility if the considered choice is made.

351

352

**Definition 12 (Choquet expected utility).** For any bpa $m$, any utility function $u: A \times \Omega \to \mathbb{R}$ and any action $a \in A$, the Choquet expected utility of $u_a: \Omega \to \mathbb{R}$ is:

353

354

$$ \text{CEU}(m)(u_a) = \sum_{B \in \mathcal{S}_m} m(B) \times \min_{\omega \in B} u_a(\omega) = \text{XEU}(m)(\varphi^{\text{CEU}}(u_a)), \\ \text{with } \varphi^{\text{CEU}}(u_a)(B) = \min_{\omega \in B} u_a(\omega). $$

355

356

357

358

359

This expression is a weighted sum indexed by the set of focal elements, which is nonempty: using the min operator is legit. Formally, the functions $\varphi^{\text{CEU}}$ and CEU are defined as follows:

**Definition** fCEU ($u_a$: $W \to \mathbb{R}$): {$\text{set } W\} \to \mathbb{R} := \text{fun } B \Rightarrow \text{match } \min_S u_a B \text{ with } \text{Some } r \Rightarrow r \mid \text{None} \Rightarrow 0 \text{ end.}$$
**Definition** CEU ($m$: bpa) ($u_a$: $W \to \mathbb{R}$): $\text{XEU } m(f\text{CEU } u_a)$.

360

361

362

363

Another rule, axiomatized by Jaffray [16, 17], is a kind of Hurwicz criterion (i.e., a linear combination over the min. and max. utility reached for each focal element). The parameter coefficients make it possible to locally modulate the pessimism of the modelled agent.
**► Definition 13 (Jaffray expected utility).** For any bpa m, any utility function u : A × Ω → ℝ and any action a ∈ A, the Jaffray expected utility of u_a : Ω → ℝ is parameterized by a family of coefficients α_{(x*,x*)} ∈ [0, 1] for each possible utility values x_* ≤ x*. For any B ≠ ∅, let us pose B_* = min_{ω∈B} u_a(ω) and B* = max_{ω∈B} u_a(ω). The Jaffray expected utility of u_a is:

$$
\begin{align*}
\text{JEU}^{\alpha}(m)(u_a) &= \sum_{B \in S_m} m(B) \times (\alpha_{(B_*, B^*)} \times B_* + (1 - \alpha_{(B_*, B^*)}) \times B^*) = \text{XEU}(m)(\varphi^{\text{JEU}^{\alpha}}(u_a)), \\
\text{with } \varphi^{\text{JEU}^{\alpha}}(u_a)(B) &= \alpha_{(B_*, B^*)} \times B_* + (1 - \alpha_{(B_*, B^*)}) \times B^*. \text{ Formally:}
\end{align*}
$$

Definition fJEU (α : R → R → R) (u_a : W → R) : {set W} → R :=
fun B ⇒ match minS u_a B, maxS u_a B with
| Some rmin, Some rmax ⇒ let alp := α rmin rmax in alp * rmin + (1-alp) * rmax
|_, _ ⇒ 0 end.

Definition JEU α (m : bpa) (u_a : W → R) := XEU m (fJEU α u_a).

Last, in the Transferable Belief Model [33], the decision rule is made by recovering a “pignistic” probability distribution<fnref n="2" /> BetP (namely, a probability that serves only for the choice) at the very moment where the decision is made (so, the equiprobability assumption is made, but after conditionings, if any). The score of an action is then the expected utility w.r.t. BetP : ω ↦→ ∑ B∈S<sub>m</sub> m(B)/|B|, that we show to be equivalent to the following definition.

**► Definition 14 (Transferable Belief Model expected utility).** For any bpa m, any utility function u : A × Ω → ℝ and any action a ∈ A, the TBEU of u_a : Ω → ℝ is defined by:

$$
\begin{align*}
\text{TBEU}(m)(u_a) &= \sum_{B \in S_m} m(B) \times \sum_{\omega \in B} u_a(\omega) / |B| = \text{XEU}(m)(\varphi^{\text{TBEU}}(u_a)) \\
\text{with } \varphi^{\text{TBEU}}(u_a)(B) &= \sum_{\omega \in B} u_a(\omega) / |B|. \quad \text{Formally:}
\end{align*}
$$

Definition fTBEU (u_a : W -> R) := fun B => \sum_(w in B) u_a w / #|B|%;R.
Definition TBEU (m : bpa) (u_a : W -> R) := XEU m (fTBEU u_a).

**► Proposition 9.** CEU, JEU, and TBEU all generalize the expected utility criterion: if the bpa m is 1-additive (i.e., it is a discrete probability measure), all these instances of XEU yield the same value as that of the expected utility:

Lemma CEU_EU (p : proba) u_a : CEU p u_a = \sum_w dist p w * u w.
Lemma JEU_EU alpha (p : proba) u_a : JEU alpha p u_a = \sum_w dist p w * u w.
Lemma TBEU_EU (p : proba) u_a : TBEU p u_a = \sum_w dist p w * u w.

In these formal proofs, the key ingredient is the fact that the criteria satisfy the natural property that $\forall u, \forall \omega \in \Omega$, $\varphi(u)(\{\omega\}) = u(\omega)$.

4 Formalization of Several Classes of Games of Complete Information

Game theory is a subdomain of multi-agent decision making [24, 25]. In this paper, we focus on simultaneous games, in which players make their choice (called action or pure strategy) without knowing others’ choices in advance; the outcome of an action depends on the choices of other agents. A typical problem amounts to identifying which actions are relevant from the viewpoint of a player, assuming others don’t cooperate but strive to increase their own utility. In this section, we consider situations where there is no uncertainty.

<footnote n="2">² The names “pignistic” and BetP are references to classical Bayesian justification in decision theory, where both utilities and beliefs are elicited by considering limits of agent’s agreement to a panel of bets.</footnote>
408

## 4.1 Games of Complete Information

409

410

411

412

413

**Definition 15 (Game of complete information).** A CGame is a tuple $G = (I, (A_i, u_i)_{i \in I})$ where I is a finite set of players; for each Player i, $A_i$ is the set of their actions; $u_i : A \to \mathbb{R}$ is an utility function, assigning an utility value to each "action profile", i.e., a vector of actions, also called "pure strategy profile" $a = (a_1, ..., a_n) \in A = A_1 \times \dots \times A_n$. Player i prefers the outcome of profile a to that of $a'$ iff $u_i(a) > u_i(a')$.

414

415

416

417

We formalize such "profiles-for-CGames" ($a \in \prod_{i \in I} A_i$) using MathComp's dependently-typed finite support functions, hence:

Definition cprofile (I : finType) (A : I -> eqType) := {ffun $\forall i : I, A i$}.

Definition cgame (I : finType) (A : I -> eqType) := cprofile A -> I -> R.

418

420

One of the most prominent solution concept in game theory is that of Nash equilibrium [26]:

421

422

423

424

425

**Definition 16 (Nash equilibrium).** A pure Nash equilibrium is a profile such that no player has any incentive to "deviate". For any pure strategy profile a and any Player i, let $a_{-i}$ be the restriction of a to the actions of Players $j \neq i$, $a'_i$ an action of Player i, then $a'_i \cdot a_{-i}$ denotes the profile a where the strategy of Player i has been switched to $a'_i$ (called change_strategy a a'_i in Coq). A profile a is a pure Nash equilibrium iff $\forall i, \forall a'_i, u_i(a) \not\le u_i(a_i \cdot a_{-i})$:

426

427

428

Definition change_strategy (p : cprofile A) (i : I) (a'_i : A i) : cprofile A

Definition Nash_equilibrium (G : cgame) (a : cprofile A) : bool := [ $\forall i : I, [\forall a'_i : A i, \sim (G \ a \ i < G (change_strategy a a'_i) i)]$ ].

429

431

432

**Example 3.** Consider Example 1 anew; suppose one knows P is the murderer. The situation is captured by the CGame $G = (I, (A_i, u_i)_{i \in I})$ where $I = \{1, 2\}$ is the set of players, $A_i = \{P_i, Q_i, R_i\}$ the set of actions of Player i (choosing P, Q or R) and the $u_i$'s of Table 2.

<table><caption>**Table 2** Utility functions of Example 3 (it is known that P is the murderer). The pair $(u_1(a_1 \cdot a_2), u_2(a_1 \cdot a_2))$ is read at the intersection of line $a_1$ and column $a_2$.</caption><thead><tr><th></th><th>P<sub>2</sub></th><th>Q<sub>2</sub></th><th>R<sub>2</sub></th></tr></thead><tbody><tr><th>P<sub>1</sub></th><td>(0, 0)</td><td>(0, 3)</td><td>(0, 3)</td></tr><tr><th>Q<sub>1</sub></th><td>(3, 0)</td><td>(2, 2)</td><td>(3, 3)</td></tr><tr><th>R<sub>1</sub></th><td>(3, 0)</td><td>(3, 3)</td><td>(2, 2)</td></tr></tbody></table>

434

435

436

437

438

Here, both $(Q_1, R_2)$ and $(R_1, Q_2)$ are Nash equilibria.

When there is some variability regarding action choices (e.g., for repeated games), it is meaningful to look for mixed strategies. A mixed strategy $\rho_i$ of Player i is a probability over $A_i$, and a mixed strategy profile $\rho = (\rho_1, ..., \rho_n)$ is a vector of mixed strategies:

Definition mixed_cprofile := cprofile (fun i => [eqType of proba R (A i)]).

441

442

443

444

445

A mixed strategy profile $\rho$ defines a probability over the set of pure strategy profiles, namely $p_{\rho}(a) = \prod_{i \in I} \rho_i(a_i)$. We package this data in a proba structure:

Definition mkProductProba (p : $\forall i : X, \text{proba R (A i)}$) : {ffun cprofile A -> R} := [ffun a : cprofile A => \prod_i dist (p i) (a i)].

Definition prodProba (p : $\forall i : I, \text{proba R (A i)}$) (i0 : I) : proba R (cprofile A).

446

448

449

450

451

452

453

Last, the utility of a mixed strategy profile is the expected utility w.r.t. the probability over pure strategy profiles, and the notion of Nash equilibrium extends straightforwardly:

Definition ms_util (G : cgame R A) (mp : mixed_cprofile) (i : I) : R :=

$\sum_{p : cprofile A} (\text{dist}(\text{prod\_proba mp witnessI mp}) p) * (G p i)$.

Definition ms_Nash_equilibrium (G : cgame R A) (mp : mixed_cprofile) : Prop :=

$\forall i (\text{si} : \text{proba R (A i)}), \sim \text{ms\_util G mp i} < \text{ms\_util G (change\_strategy mp si)} i$.
A standard reduction [18, Def. 4.6.1] amounts to viewing a mixed equilibrium of a game $(N, (A_i, u_i)_{i \in N})$ as a pure equilibrium in the mixed extension $(N, (A_i, u_i)_{i \in N})$, where $A_i$ is the set of mixed strategies over $A_i$. Formally:

Definition mixed_cgame (G:cgame R A) : cgame R (fun i ⇒ [eqType of proba R (A i)]) := fun mp i ⇒ ms_util G mp i.
Lemma mixed_cgameE G mp i : ms_utility G mp i = (mixed_cgame G) mp i.
Lemma ms_NashE (G : cgame R A) (mp : mixed_cprofile) : ms_Nash_equilibrium G mp <=> Nash_equilibrium (mixed_cgame G) mp.

## 4.2 Hypergraphical Games

Some games of complete information can be expressed succinctly as hypergraphical games [27, 36], where the utility is not defined globally but locally (namely, split in several “local games”). This yields an hypergraph, where vertices denotes players and hyperedges denote local games. Formally, a hypergraphical game is a tuple $G = (I, E, (A_i)_{i \in I}, (u_i^e)_{e \in E, i \in e})$, where $I$ is the set of players, $E \subseteq 2^I$ is the set of local games (in any local game $e = \{a, b, c, \dots\}$, Players $a, b, c, \dots$ are playing), $A_i$ is the set of actions of Player $i$ and $u_i^e : A_e \to \mathbb{R}$ is the utility function of Player $i$ in the local game $e$ ($A_e = \prod_{i \in e} A_i$ is the set of local profiles related to $e$'s players). A hypergraphical game with 2-player local games is called a polymatrix.

In our formalization, local games are indexed by the finite type (`localgame`: `finType`); players playing a local game (`lg`: `localgame`) are those who verify the Boolean predicate (`plays_in lg`); `plays_in` thus formalizes $E$ as a family of sets of players:

Variables (localgame : finType) (plays_in : localgame → pred I).

For any local game `lg`, local profiles are profiles that involve only players which `plays_in lg`:

Definition localprof (lg : localgame) := {ffun ∀s : {i : I | plays_in lg i}, A (val s)}.

In hypergraphical games, every player chooses one action, and plays it in every local game they are involved in. The global utility of a player is the sum of the locally obtained utilities: $u_i(a) = \sum_{e \in E} u_i^e(a_e)$, where $a_e \in A_e$ is the restriction of $a$ to indices of $e$. Thus, an hypergraphical game is a CGame that is specified by its local utility functions:

Definition hg game (u : ∀lg, localprof lg → {i : I & plays_in lg i} → R) : cgame := fun a i ⇒ \sum_(s : {lg : localgame | plays_in lg i}) u (tag s) [ffun i ⇒ a (val i)] (exist _ i (tagged s)).

## 5 Bel Games

Harsanyi has proposed [13] a model for decision-making situations where players may have some uncertainty about other players, their actions, their utility functions, or more generally about any parameter of the game. To model such situations, the partially known parameters are expressed by so-called types:<fnref n="3" /> each Player $i$ has a set of possible types $\Theta_i$. Each type $\theta_i \in \Theta_i$ represents a possible parameter describing Player $i$'s characteristics and knowledge. Every Player $i$ knows (or learns) their own type $\theta_i \in \Theta_i$ at the time of choosing an action. It may or may not be correlated with other players' types, so it is possible to model players that are not aware of other players' type as well as players with some knowledge about them.

<footnote n="3">³ Thus, type can refer to a type-theory concept or a game-theory one. Context will allow to disambiguate.</footnote>
Harsanyi defined the model of games of incomplete information where players' knowledge is given by a subjective probability and preferences agree with the expected utility: the so-called class of Bayesian games. In this setting, a probability measure expresses the knowledge on type configurations (the frame of discernment being the cartesian product of all players' types, that is, $\Omega = \prod_{i \in N} \Theta_i = \Theta$). Games of incomplete information already were extended to a possibilistic setting by Ben Amor et al. [3], and we extend it further to Belief functions (so generalizing both Bayesian games and possibilistic games) [11, 29].

**Definition 10 (Bel game).** A Bel game [29] is defined by a tuple $G = (I, (A_i, \Theta_i, u_i)_{i \in I}, m)$:

I is the finite set of players;

A$_i$ is the set of actions of Player i; $\Theta_i$ is the finite set of types of Player i;

u$_i$: $A \to \Theta \to \mathbb{R}$ is the utility function of Player i; it depends on the joint action $(a_1, \dots, a_n) \in A := \prod_{i \in I} A_i$ and on the type configuration $(\theta_1, \dots, \theta_n) \in \Theta := \prod_{i \in I} \Theta_i$;

m: $2^\Theta \to [0, 1]$ is a bpa which describes the prior knowledge.

Formally speaking, a Bel game is fully defined by two elements: the bpa (prior knowledge) and the utility functions (the players' preferences). This pair is parameterized by three types I, the players; A, the family of actions $(A_i)_{i \in I}$; and T, the family of types $(\Theta_i)_{i \in I}$:

Definition belgame (I : finType) (A : I \to eqType) (T : I \to finType) := (bpa R (cprofile T) * (cprofile A \to cprofile T \to player \to R)).

**Example 4 (Bel game).** We now are able to endow Example 1 with a Bel game $G = (I, (A_i, \Theta_i, u_i)_{i \in I}, m)$. The set of players is $= \{1, 2\}$, their action sets are $A_i = \{P_i, Q_i, R_i\}$. Player 1 will learn either that $P$ is the murderer ($\omega^* \in \{P\}$) or that he is not ($\omega^* \in \{Q, R\}$): Player 1's type set is $\Theta_1 = \{\bar{P}, \bar{P}\}$. Similarly, Player 2 will learn either that $R$ is the murderer ($\omega^* \in \{R\}$) or that she is not ($\omega^* \in \{P, Q\}$), so $\Theta_2 = \{\bar{R}, \bar{R}\}$. The knowledge is expressed over $\Theta = \Theta_1 \times \Theta_2$: since $(\bar{P}, \bar{R}) \equiv P$, $(\bar{P}, \bar{R}) \equiv Q$, $(\bar{P}, R) \equiv R$ and $(\bar{P}, R)$ is impossible, the knowledge is $m(\{\bar{P}, \bar{R}\}, (\bar{P}, \bar{R})) = m(\{\bar{P}, R\}) = 0.5$. Finally, utility functions are given in Table 3.

<table><caption>Table 3 Utility functions of Example 4 for $\theta = (\bar{P}, \bar{R})$ (left, $P$ is the murderer), $\theta = (\bar{P}, \bar{R})$ (center, $Q$ is the murderer) and $\theta = (\bar{P}, R)$ (right, $R$ is the murderer). Configuration $\theta = (\bar{P}, R)$ can't occur.</caption><thead><tr><th></th><th>P<sub>2</sub></th><th>Q<sub>2</sub></th><th>R<sub>2</sub></th><th></th><th>P<sub>2</sub></th><th>Q<sub>2</sub></th><th>R<sub>2</sub></th><th></th><th>P<sub>2</sub></th><th>Q<sub>2</sub></th><th>R<sub>2</sub></th></tr></thead><tbody><tr><th>P<sub>1</sub></th><td>(0, 0)</td><td>(0, 3)</td><td>(0, 3)</td><th>P<sub>1</sub></th><td>(2, 2)</td><td>(3, 0)</td><td>(3, 3)</td><th>P<sub>1</sub></th><td>(2, 2)</td><td>(3, 3)</td><td>(3, 0)</td></tr><tr><th>Q<sub>1</sub></th><td>(3, 0)</td><td>(2, 2)</td><td>(3, 3)</td><th>Q<sub>1</sub></th><td>(0, 3)</td><td>(0, 0)</td><td>(2, 2)</td><th>Q<sub>1</sub></th><td>(3, 3)</td><td>(2, 2)</td><td>(3, 0)</td></tr><tr><th>R<sub>1</sub></th><td>(3, 0)</td><td>(3, 3)</td><td>(2, 2)</td><th>R<sub>1</sub></th><td>(3, 3)</td><td>(3, 0)</td><td>(2, 2)</td><th>R<sub>1</sub></th><td>(0, 3)</td><td>(0, 3)</td><td>(0, 0)</td></tr></tbody></table>

Since players know their own type before choosing their action, a pure strategy of Player i becomes a function $\sigma_i : \Theta_i \to A_i$: having the type $\theta_i$, Player i will play $\sigma_i(\theta_i) \in A_i$. Next, a strategy profile $\sigma = (\sigma_1, \dots, \sigma_n)$ is a vector of such functions:

Definition iprofile I A T := cprofile (fun i \Rightarrow [eqType of {ffun T i \to A i}]).

If the actual type configuration is $\theta = (\theta_1, \dots, \theta_n)$, then for any strategy profile $\sigma$ we denote by $\sigma^\theta = (\sigma_1(\theta_1), \dots, \sigma_n(\theta_n)) \in A$ the action profile that will actually be played:

Definition proj_iprofile I A T (p : iprofile A T) : cprofile A := fun theta \Rightarrow [ffun i \Rightarrow p i (theta i)].

In the following, we denote by $u_{i,\sigma} : \Theta \to \mathbb{R}$ the function mapping states of the world $\omega$ to the corresponding utility of $\sigma$ for Player i. It is defined by $u_{i,\sigma}(\theta) = u_i(\sigma^\theta, \theta)$.

In Bayesian games, the global utility of a strategy profile $\sigma$ for Player i with type $\theta_i$ is the expected utility w.r.t. the conditioned probability distribution “given $\theta_i$”. In Bel games, both expectation and conditioning have to be made explicit, to properly model agents' preferences and knowledge updates. For example, studying a Bel game with Dempster's conditioning and
CEU expectation implies that the utility of a given strategy profile $\sigma$ for Agent $i$ with type $\theta_i$ is $\sum_{B \subseteq \Omega} m(B | D, \theta_i) \times \min_{\theta' \in B} u_i(\sigma^{\theta'}, \theta')$. Doing so, we need to ensure that conditioning is meaningful and technically possible, that is, the bpa is revisable given any type of any player. For the sake of readability, we now introduce two shorthands: Tn, representing the set $\Theta$ gathering all type configurations; and event_ti := $\theta_i \mapsto \{\theta' \in \Theta | \theta'_i = \theta_i\}$:

Notation Tn := [finType of {dffun $\forall i : I, T i$}].

Definition event_ti i (ti : T i) := [set t : Tn | t i == ti].

A proper Bel games, in which conditioning is safe, shall satisfy the predicate:

Definition proper_belgame A T (G : belgame A T) (cond : conditioning R Tn) : bool
:= [∀i : player, [∀ti : T i, revisable cond G.1 (event_ti ti)]].

**► Definition 11 (Utility in a Bel game).** For any Bel game $G = (I, (A_i, \Theta_i, u_i)_{i \in I}, m)$, any conditioning cond for which $G$ is proper and any XEU parameter $\varphi^{\text{XEU}} : (\Theta \to \mathbb{R}) \to 2^\Theta \to \mathbb{R}$, the utility of the pure strategy profile $\sigma$ for Player $i$ having type $\theta_i \in \Theta_i$, is the integration of $u_{i,\sigma} = \theta \mapsto u_i(\sigma^\theta, \theta)$, i.e., XEU $(m(\cdot |_{\text{cond } \theta_i})) (\varphi^{\text{XEU}}(u_{i,\sigma}))$.

Definition belgame_utility A T (G : belgame A T) (cond: conditioning R Tn)
fXEU (HG : proper_belgame G cond) (p : iprofile A T) (i : player) (ti : T i) : R
:= let kn := cond G.1 (event_ti ti) (is_revisable HG ti) in
XEU kn (fXEU (fun t => G.2 (proj_iprofile p t) t i)).

Also, for Bel games, the definition of Nash equilibrium applies: an iprofile is a Nash equilibrium iff no player, whatever is this player's type, has any incentive to deviate:

Definition BelG_Nash_equilibrium A T (G : belgame A T) (cond : conditioning R Tn)
fXEU (H : proper_belgame G cond) (p : iprofile A T) :=
∀i : I, ∀ti : T i, ∀ai : A i,
~ (belgame_utility u H p ti < belgame_utility u H (change_istrategy p ti ai) ti).

**► Example 5 (Utility of a strategy).** Let $\sigma = (\sigma_1, \sigma_2)$ be defined by $\sigma_1(\bar{P}) = Q_1$, $\sigma_1(\bar{P}) = P_1$, $\sigma_2(\bar{R}) = Q_2$, $\sigma_1(\bar{R}) = R_2$. $\sigma$ is a pure strategy asserting that Player 1 will choose $Q$ when learning that $P$ is the murderer, and choose $P$ otherwise, and that Player 2 will choose $Q$ when learning that $R$ is the murderer, and choose $R$ otherwise.

Considering Dempster's conditioning, the Choquet expected utility of $\sigma$ for Player 1 with type $\bar{P}$ is the integration of $\varphi^{\text{CEU}}(u_{i,\sigma})$ w.r.t. the posterior bpa $m(\cdot | \bar{P})$. Recall Example 2, the posterior bpa "given $\bar{P}$" has two focal elements: $\{Q\}$ and $\{R\}$, both with mass $1/2$. Considering type configurations, those focal elements are $\{(\bar{P}, \bar{R})\}$ and $\{(\bar{P}, R)\}$.

$$ 
\begin{aligned}
\text{XEU} (m(\cdot |_D \bar{P})) (\varphi^{\text{CEU}}(u_{1,\sigma})) &= \sum_{B \in S_{m(\cdot |_D \bar{P})}} m(B |_D \bar{P}) \times \min_{\theta \in B} u_1(\sigma^\theta, \theta) \\
&= 0.5 \times u_1((P_1, Q_2), (\bar{P}, \bar{R})) + 0.5 \times u_1((P_1, R_2), (\bar{P}, \bar{R})) = 3.
\end{aligned}
$$

One may check that for every player and type, $\sigma$'s CEU equals 3, the best possible score. Since no player, whatever is their type, has incentive to deviate, $\sigma$ is a Nash equilibrium.

# 6 Howson-Rosenthal-like transforms

Howson-Rosenthal's theorem asserts the correctness of a transform, which casts a 2-player Bayesian game into an equivalent polymatrix game (of complete information) [15]. Bayesian games thus benefit from both theoretical and algorithmic results of classical game theory.

In the following, we formally define and prove correct three Howson-Rosenthal-like transforms that we have devised in previous work [11, 29]. All these transforms cast n-player Bel games into hypergraphical games; the games so obtained all have the same utility values,
Definition HRdirect_plays_in (lg : HRdirect_localgame) (i_ti : HRplayer) : bool
:= [∃t : Tn, [&& t \in lg & t (projT1 i_ti) == projT2 i_ti]].

Then, local utility functions are given by a function which constructs from a local profile $p$ and a type configuration $\theta$, the cprofile $(p_{(1,\theta_1)}, \dots, p_{(n,\theta_n)})$. This function has type:

Definition HRdirect_mkprofile lg i_ti (Hi_ti : HRdirect_plays_in lg i_ti)
(p : HRdirect_localprof lg) (t : Tn) : profile.

Local utility in a local game $e_B$ is the part of the XEU computed from the prior focal element $B$. Note that Dempster's conditioning transfers masses from $B$ to $B \cap \{\theta' \in \Theta \mid \theta'_i = \theta_i\} = B \cap (\text{event}_ti \ \theta_i)$ so the local utility amounts to an on-the-fly Dempster's conditioning. The resulting HG game is finally built from local utility functions:

Definition HRdirect_u : ∀lg, HRdirect_localprof lg → HRdirect_localplayer lg → R
:= fun lg p x ⇒ let (i_ti, Hi_ti) := x in let (i, ti) := i_ti in
G.1 lg * fXEU [ffun t ⇒ G.2 (HRdirect_mkprofile Hi_ti p t) t i]
(lg :&: (event_ti ti)) / Pl G.1 (event_ti ti).
Definition HRdirect : cgame R HR_action := hgZYX game HRdirect_u.

**Theorem 12 (Correctness of the direct transform).** For any proper Bel game $G$, Player $i$ with type $\theta_i$, XEU function $\varphi^{\text{XEU}}$, and profile $\sigma$, we have XEU $(m(\cdot |_D \theta_i))(\varphi^{\text{XEU}}(u_{i,\sigma})) = \tilde{u}_{(i,\theta_i)}(\text{flatten}(\sigma))$. Then, Nash equilibria of $G$ and $\tilde{G}$ are in one-to-one correspondence:

Theorem HRdirect correct (i : I) (ti : T i) (p : iprofile A T) :
belgame\_utility fXEU properG p ti = HRdirect (flatten p) (existT _ i ti).

Theorem HRdirect_eqNash (p : iprofile A T) :
BelG_Nash\_equilibrium fXEU proper_G p <=> Nash\_equilibrium HRdirect (flatten p).

## 6.2 The Conditioned Transform

The conditioned transform holds for any conditioning and XEU. Starting from a Bel game $G$, all the conditioning “given $\theta_i$” are pre-computed, let $S^*$ be the union of all posterior focal sets (i.e., the set of all possible focal elements given any $\theta_i$). Each $B \in S^*$ leads to a local game. As in the direct transform, a vertex $(i, \theta_i)$ plays in $e_B$ if $\theta_i$ is possible in $B$. Its utility in $e_B$ is the part of XEU computed over the posterior focal element $B$. Note that $(i, \theta_i)$'s local utility in $B$ may be 0, if $B$ is not focal in the posterior “given $\theta_i$”. Formally speaking:

**Definition 18 (Conditioned transform).** The conditioned transform of a Bel game $G = (I, (A_i, \Theta_i, u_i)_{i \in I}, m)$ is the hypergraphical game $\tilde{G} = (\tilde{I}, \tilde{E}, (\tilde{A}_{(i,\theta_i)})_{(i,\theta_i) \in \tilde{I}}, (\tilde{u}^e_{(i,\theta_i)})_{e \in \tilde{E}, (i,\theta_i) \in e})$:

■ $\tilde{I} = \{(i, \theta_i) \mid i \in I, \theta_i \in \Theta_i\}$, $\tilde{E} = (e_B)_{B \in S^*}$, $e_B = \{(i, \theta_i) \mid \theta_i \in B, i \in I\}$, $\tilde{A}_{(i,\theta_i)} = A_i$,

■ for each $e_B \in \tilde{E}$, $(i, \theta_i) \in e_B$ and $\tilde{\sigma} \in \tilde{A}$, let us pose $\tilde{v}_i^{\tilde{\sigma}}(\theta) = u_i(\tilde{\sigma}^{\theta}, \theta)$ in:

$$ \tilde{u}^{e_B}_{(i,\theta_i)}(\tilde{\sigma}_{e_B}) = m(B | \theta_i) \times f^{\text{XEU}}_{\tilde{v}_i^{\tilde{\sigma}}}(B). $$

Formally, let fXEU be any $\varphi^{\text{XEU}}$, cond any conditioning, and G be proper w.r.t. cond:

Variables (fXEU: (Tn -> R) -> {set Tn} -> R)
(Cond : conditioning R Tn) (proper_G : proper\_belgame G cond).

After similar definitions for HRcond_localgame and HRcond_plays_in, we define:

Definition HRcond_u : ∀lg, HRcond_localprof lg → HRcond_localplayer lg → R
:= fun lg p x ⇒ let (i_ti, Hi_ti) := x in let (i, ti) := i_ti in
let kn := cond G.1 (event_ti ti) (is\_revisable proper_G ti) in
kn lg * fXEU [ffun t ⇒ G.2 (HRcond_mkprofile Hi_ti p t) t i] lg.
Definition HRcond : cgame R HR_action := hgZYX game HRcond_u.
704

705

706

707

708

709

710

711
712

**▶ Theorem 13 (Correctness of the conditioned transform).** For any proper Bel game G, Player i with type $\theta_i$, conditioning c, XEU function $\varphi^{\text{XEU}}$, profile $\sigma$: XEU $(m(\cdot|_c \theta_i))(\varphi^{\text{XEU}}(u_{i,\sigma})) = \tilde{u}_{(i,\theta_i)}(\text{flatten}(\sigma))$. Thence, Nash equilibria of G and $\tilde{G}$ are in one-to-one correspondence:

Theorem HRcond correct (i : I) (ti : T i) (p : iprofile A T):
belgame_utility fXEU proper_G p ti = HRcond (flatten p) (existT _ i ti).

Theorem HRcond_eqNash (p : iprofile A T),
BelG_Nash_equilibrium fXEU proper_G p <=> Nash_equilibrium (HRcond) (flatten p).

713

## 6.3 The TBM Transform

714

715

716

717

718

The TBM transform is designed for the Transferable Belief Model [33], in which knowledge is first revised using Dempster's conditioning, then decision is eventually made w.r.t. a probability distribution BetP which is deduced from the bpa m (Definition 14). Here we benefit from BetP's 1-additivity to produce a low-complexity hypergraph: local games correspond to single states of the world, that is, they all involve only n players.

719

720

**▶ Definition 19 (TBM transform).** Let $G = (I, (A_i, \Theta_i, u_i)_{i \in I}, m)$ be a Bel game; it is TBM-transformed into the hypergraphical game $\tilde{G} = (\tilde{I}, \tilde{E}, (\tilde{A}_{(i,\theta_i)}))_{(i,\theta_i) \in \tilde{I}}$, $(\tilde{u}_{(i,\theta_i)}^e)_{e \in \tilde{E}, (i,\theta_i) \in e}$ s.t.:
$$ \tilde{I} = \{(i, \theta_i) \mid i \in I, \theta_i \in \Theta_i\}, \quad \tilde{E} = (\text{Players}(\theta))_{\theta \in \Theta}, \quad \tilde{A}_{(i,\theta_i)} = A_i, $$

721

722

$\tilde{u}_{(i,\theta_i)}^{e_\theta}(\tilde{\sigma}_e) = \text{BetP}_{(i,\theta_i)}(\theta) \times u_i(\sigma^\theta, \theta)$.

723

Formally, let cond be a conditioning and G be a proper Bel game w.r.t. cond; $\tilde{G}$'s local games are indexed by type configurations, and $(i, \theta_i)$ plays in $e_{\theta'}$ iff $\theta_i = \theta'_i$:

724

725

726

727

728

729
730

Variables (cond : conditioning R Tn) (proper_G : proper_belgame cond).

Definition HRTBM_localgame : finType := Tn.

Definition HRTBM_plays_in : HRTBM_localgame -> pred HRplayer :=
fun lg i_ti => lg (projT1 i_ti) == projT2 i_ti.

Local utilities are computed w.r.t. the “pignistic” distribution BetP:

731

732

733

734

735

736

737

Definition HRTBM_u : ∀lg, HRTBM_localprof lg → HRTBM_localplayer lg → R ::= fun lg p x ⇒ let (i_ti, _ ) := x in let (i, ti) := i_ti in let betp := BetP (cond G.1 (event_ti ti) (is_revisable proper_G ti)) in dist betp lg * G.2 (HRTBM_mkprofile p) lg i.
Definition HRTBM : cgame R HR_action := hg game HRTBM_u.</ Definition

739

740

741

742

743

744

745

746
747

**▶ Theorem 14 (Correctness of the TBM transform).** For any proper Bel game G, Player i with type $\theta_i$, conditioning c, and profile $\sigma$, TBEU $(m(\cdot|_c \theta_i)) (\varphi^{\text{TBEU}}(u_{i,\sigma})) = \tilde{u}_{(i,\theta_i)}(\text{flatten}(\sigma))$. Thence, Nash equilibria of G and $\tilde{G}$ are in one-to-one correspondence:

Theorem HRTBM correct (i : I) (ti : T i) (p : iprofile A T) :
belgame_utility fTBEU proper_G p ti = HRTBM (flatten p) (existT _ i ti).

Theorem HRTBM_eqNash (p : iprofile A T),
BelG_Nash_equilibrium fTBEU proper_G p <=> Nash_equilibrium HRTBM (flatten p).

748

# 7 Conclusion and Perspectives

749

750

751

752

753

754

In this paper, a Coq/SSReflect formalization of Bel games has been presented. It provides a generic class of games of incomplete information, built upon the Dempster-Shafer theory of belief functions. This framework makes it possible to capture (lack of) knowledge better than usual game models based on probability. Following Howson's and Rosenthal's approach, three different algorithms transforming such incomplete games into standard complete-information games have been formalized, and the fact that these transforms preserve equilibria (as long
as we comply with Table 4) has been formally verified. Thus, Bel games can ultimately be solved using state-of-the-art, effective algorithms for complete games.

This work provides strong guarantees on the correctness of the transforms, so that game theorists may rely on them without any concern about correctness. Furthermore, the formalization allowed us to identify subtleties that were left implicit in the definitions (e.g., the conditioning precondition), as well as to help improving the proofs, both in their flow and in their prose. Last, generic lemmas that proved useful during our formalization effort have been proposed for integration in the MathComp library.

This work opens several research directions, both on the theoretical side and on the formal verification side. On the one hand, we aim at extending this result with other decision-theoretic approaches, e.g., partially-ordered utility aggregations for belief function and other non-additive-measure approaches (Choquet capacities of order 2, RDU). On the other hand, we would like to focus on complexity proofs which, albeit not safety-critical, play a key role when choosing one transform over the other. Eventually, we would like to encompass this work into a larger library of decision under uncertainty, fostering further developments on related models and proofs.

References

1 Reynald Affeldt and Cyril Cohen. Measure construction by extension in dependent type theory with application to integration, 2022. URL: https://arxiv.org/abs/2209.02345.

2 Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. A library for formalization of linear error-correcting codes. *Journal of Automated Reasoning*, 64(6):1123–1164, 2020.

3 Nahla Ben Amor, Hélène Fargier, Régis Sabbadin, and Meriem Trabelsi. Possibilistic Games with Incomplete Information. In *Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence*, pages 1544–1550. ijcai.org, 2019.

4 Alexander Bagnall, Samuel Merten, and Gordon Stewart. A Library for Algorithmic Game Theory in SSReflect/Coq. *Journal of Formalized Reasoning*, 10(1):67–95, 2017.

5 Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formalization of Lebesgue integration of nonnegative functions. *Journal of Automated Reasoning*, 66(2):175–213, 2022. URL: https://doi.org/10.1007/s10817-021-09612-0.

6 The Coq Development Team. The Coq Proof Assistant, 2022. URL: https://doi.org/10.5281/zenodo.1003420.

7 Arthur P. Dempster. Upper and Lower Probabilities Induced by a Multivalued Mapping. *The Annals of Mathematical Statistics*, 38:325–339, 1967.

8 Christoph Dittmann. Positional determinacy of parity games. Available at https://www.isa-afp.org/browser_info/devel/AFP/ParityGame/outline.pdf, 2016.

9 Didier Dubois and Thierry Denoeux. Conditioning in Dempster-Shafer Theory: Prediction vs. Revision. In *Belief Functions: Theory and Applications - Proceedings of the 2nd International Conference on Belief Functions*, pages 385–392. Springer, 2012.

10 Didier Dubois and Henri Prade. Focusing vs. belief revision: A fundamental distinction when dealing with generic knowledge. In *Qualitative and quantitative practical reasoning*, pages 96–107. Springer, 1997.

11 Hélène Fargier, Érik Martin-Dorel, and Pierre Pomeret-Coquot. Games of incomplete information: A framework based on belief functions. In *Symbolic and Quantitative Approaches to Reasoning with Uncertainty - 16th European Conference, volume 12897 of Lecture Notes in Computer Science*, pages 328–341. Springer, 2021.

12 Ruobin Gong and Xiao-Li Meng. Judicious judgment meets unsettling updating: Dilation, sure loss and simpson's paradox. *Statistical Science*, 36(2):169–190, 2021.

13 John C Harsanyi. Games with Incomplete Information Played by “Bayesian” Players, I–III. Part I. The Basic Model. *Management Science*, 14(3):159–182, 1967.
804

14 Johannes Hölzl and Armin Heller. Three chapters of measure theory in Isabelle/HOL. In *Interactive Theorem Proving*, pages 135–151, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.

805

806

807

15 Joseph T Howson Jr and Robert W Rosenthal. Bayesian Equilibria of Finite Two-Person Games with Incomplete Information. *Management Science*, 21(3):313–315, 1974.

808

809

16 Jean-Yves Jaffray. Linear Utility Theory for Belief Functions. *Operations Research Letters*, 8(2):107–112, 1989.

810

811

17 Jean-Yves Jaffray. Linear Utility Theory and Belief Functions: a Discussion. In *Progress in decision, utility and risk theory*, pages 221–229. Springer, 1991.

812

813

18 Rida Laraki, Jérôme Renault, and Sylvain Sorin. *Mathematical foundations of game theory*. Springer, 2019.

814

815

19 Stéphane Le Roux, Érik Martin-Dorel, and Jan-Georg Smaus. An Existence Theorem of Nash Equilibrium in Coq and Isabelle. In *Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification*, volume 256 of *Electronic Proceedings in Theoretical Computer Science*, pages 46–60, 2017.

816

817

818

819

20 Stéphane Le Roux, Érik Martin-Dorel, and Jan-Georg Smaus. Existence of Nash equilibria in preference priority games proven in isabelle. In *Kurt Gödel Day and Czech Gathering of Logicians*, 2021.

820

821

822

21 Pierre Lescanne and Matthieu Perrinel. "backward" coinduction, nash equilibrium and the rationality of escalation. *Acta Informatica*, 49(3):117–137, 2012.

823

824

22 Assia Mahboubi and Enrico Tassi. *Mathematical Components*. Zenodo, January 2021.

825

23 Érik Martin-Dorel and Sergei Soloviev. A Formal Study of Boolean Games with Random Formulas as Payoff Functions. In *22nd International Conference on Types for Proofs and Programs, TYPES 2016*, volume 97 of *Leibniz International Proceedings in Informatics*, pages 14:1–14:22, 2016.

826

827

828

829

24 Oskar Morgenstern and John Von Neumann. *Theory of Games and Economic Behavior*. Princeton University Press, 1953.

830

831

25 Roger B Myerson. *Game Theory*. Harvard university press, 2013.

832

26 John Nash. Non-Cooperative Games. *Annals of Mathematics*, pages 286–295, 1951.

833

27 Christos H. Papadimitriou and Tim Roughgarden. Computing Correlated Equilibria in Multi-Player Games. *Journal of the Association for Computing Machinery*, 55(3):1–29, 2008.

834

835

28 Bernard Planchet. Credibility and Conditioning. *Journal of Theoretical Probability*, 2(3):289–299, 1989.

836

837

29 Pierre Pomeret-Coquot, Hélène Fargier, and Érik Martin-Dorel. Games of incomplete information: A framework based on belief functions. *International Journal of Approximate Reasoning*, 151:182–204, 2022.

838

839

840

30 Stéphane Le Roux. Acyclic preferences and existence of sequential nash equilibria: A formal and constructive equivalence. In *Proc. Theorem Proving in Higher Order Logics, 22nd International Conference*, volume 5674 of *Lecture Notes in Computer Science*, pages 293–309. Springer, 2009.

841

842

843

31 Glenn Shafer. *A Mathematical Theory of Evidence*. Princeton University Press, 1976.

844

32 Philippe Smets. Jeffrey's Rule of Conditioning Generalized to Belief Functions. In *Uncertainty in artificial intelligence*, pages 500–505. Elsevier, 1993.

845

846

33 Philippe Smets and Robert Kennes. The Transferable Belief Model. *Artificial Intelligence*, 66(2):191–234, 1994.

847

848

34 René Vestergaard. A constructive approach to sequential nash equilibria. *Information. Processing Letters*, 97(2):46–51, 2006. doi:10.1016/j.ipl.2005.09.010.

849

850

35 Peter Walley. *Statistical Reasoning with Imprecise Probabilities*. Chapman & Hall, 1991.

851

36 Elena Yanovskaya. Equilibrium Points in Polymatrix Games. *Lithuanian Mathematical Journal*, 8:381–384, 1968.

852