Towards a definition of positivity

Peter Hancock

started: 1999-08-08 15:34:36 updated: 1999-08-09 10:11:54

This (rough, inconclusive,…) note concerns a setup which seems to be useful in modelling interactions such as 2−player games in a constructive framework such as Martin−Löf’s type theory.

A : Set,
B : A → Set,
C : ( ∏ a : A) B(a) → Set,
d : ( ∏ a : A, b : B(a) ) C(a, b) → A

The same structure can be formulated as an element of the type

( ∑ A : Set ) A →
( ∑ B : Set ) B →
( ∑ C : Set ) C → A

which has typical element

(A, λa. (B(a), λb. (C(a, b), λc. d(a, b, c))))

If one defines

F am  : Type → Type
F am(A) =^{Δ} ( ∑ I : Set ) I → A

then one can give a compact ‘coalgebraic’ formulation

( ∑ A : Set ) A → F am(F am(A))

The various components here can be given a game−theoretic interpretation, as follows. We consider 2−player games in which there is a player ‘White’ who makes the first move, and the other player ‘Black’ responds to those moves.

A  the set of positions a, a′, …
B(a)  the set of moves b, b′, … available to White in position a

C(a, b) the set of countermoves c, c′, … available to Black when

White has made move b in postion a

d(a, b, c) the next position when White has made move b from position a, and Black has responded with countermove c.

I shall often use the ‘pseudo−substitution’ notation a[b/c] instead of d(a, b, c). Other notational conveniences are to use 0 for the empty set, 1 for the singleton set with sole element 0, 2 for the booleans with 0 as false and 1 as true – thus overloading the symbols 0, 1, 2 à la ‘von Neumann’. I shall use (unary, prefix) ‘−’ for negation:

−A =^{Δ} A → 0

We suppose that White has the ‘gladiatorial’ goal of driving the game into a position a in which there is a move b : B(a) such that C(a, b) is empty. In such a position, we say that White ‘beats’ black. On the other hand, we suppose that Black’s goal is merely to make moves so as to (forever) evade any such position, so that whatever moves are made by White, there is always some countermove available to Black. If there is a strategy for Black to follow from state a so as to avoid being beaten, the state a is called positive. Positivity is a coinductive notion. It is the aim of this note to grope towards a satisfactory formulation of positivity in the framework of (ordinary, well−founded) type theory.

I do not understand where the terminology ‘positivity’ comes from. There may be some motivation for it in the context of formal topology. Or modal logic? ‘Possibility’?

1 White’s strategies

The positions a : A in which White has a strategy to beat Black satisfy the following predicate S_{W}, which has an inductive definition.

S_{W} (a) = ( ∑ b : B(a) ) ( ∏ c : C(a, b) ) S_{W} (a[b/c])

The predicate S_{W} : A → Set is to be understood as the least solution of the equation, in the sense of predicate inclusion.

The predicate S_{W} can also be defined in terms of the inductive closure of the game structure (B, C, d) on the set A, defined as follows:

B^{∗}(a)  = 1 + ( ∑ b : B(a) ) ( ∏ c : C(a, b) ) B^{∗}(a[b/c])
C^{∗}(a, bt) = case bt of \begin{matrix}0  → & 1 \\ (b, f) → & ( ∑ c : C(a, b) ) C^{∗}(a[b/c], f(c)) \end{matrix}
a[bt/cs]^{∗} = case bt of \begin{matrix}0  → & a \\ (b, f) → & case cs of (c, cs′) → a[b/c][f(c)/cs′]^{∗} \end{matrix}

These components have the interpretation

B^{∗}(a) the set of partial strategies bt available to White in position a. A partial strategy may at some point ‘run out’, which is represented here by the summand 1 + …. C^{∗}(a, b) the set of sequences cs of countermoves available to Black

to avoid being beaten when White is playing bt. I shall refer to such a sequence of countermoves as an escape.

a[bt/cs]^{∗} the position arrived at when White has played strategy bt from position a, and Black has responded with countermoves cs.

Then we define

S_{W} (a) =^{Δ} ( ∑ bt : B^{∗}(a) ) − C^{∗}(a, bt)

In other words, a strategy for black (starting from position a) is a partial strategy bt : B^{∗}(a) from which there happens to be no ‘escape’ cs : C^{∗}(a, bt).

More generally, we could define a predicate transformer:

P_{W} (X, a) =^{Δ} ( ∑ bt : B^{∗}(a) ) ( ∏ cs : C^{∗}(a, bt) ) X(a[bt/cs]^{∗})

Then in fact we have S_{W} = P_{W} (F alse).

2 Black’s strategies: growing at the end

By analogy with the definition of White’s strategies in terms of partial strategies, we arrive (after a long time!) at the following definitions for the set of Black’s (partial) strategies to avoid being beaten.

B_{∗}(a) = 1 + ( ∑ s : B_{∗}(a) ) ( ∏ e : C_{∗}(a, b), b : B(a[s/e]_{∗}) ) C(a[s/e]_{∗}, b)
C_{∗}(a, s) = case s of \begin{matrix}0  → & 1 \\ (s_{0}, f) → & ( ∑ e : C_{∗}(a, s_{0}) ) B(a[s_{0}/e]_{∗}) \end{matrix}
a[s/e]_{∗} = case s of \begin{matrix}0  → & a \\ (s_{0}, f) → & case cs of (e, b) → a[s_{0}/e]_{∗}[b/f(e, b)] \end{matrix}

The interdependencies of the definitions of the components are more intricate than in the case of White’s strategies. Moreover, one has (quite naturally) an ordinary sum−of−products in the clause for B_{∗}. There is no need to apply a choice principle (which introduces a functional type).

There is, admittedly, something rather strange, namely the strategy 0. We would not expect a strategy for Black to have any ‘visibility’ till White has made a move. I am having second thoughts!

The trees in B_{∗} (for that is what they are: trees which grow at the leaves) have two kinds of branches – those which lead to a position in which White has no further moves (of course, Black can avoid being beaten by being gladiatorial enough to actually beat White); and those which lead to a ‘hole’. The paths in a tree which lead to holes are actually all of the same length.

The question remains of defining P os(a). Perhaps this should mean that there is a sequence (or directed family?) of partial strategies in which each successive partial strategy ‘fills in some holes’ in its predecessor. To do this requires a notion of one partial strategy being a development or extension of another. I expect that there is something here like an (inverse) limit. But what is the index?

Am I getting close? What is crucial here is not to use a notion of equality, but perhaps a (definable) comparison relation between partial strategies.

We can’t define

S_{B}(a) =^{Δ} ( ∑ s : B_{∗}(a) ) − C_{∗}(a, s)

because that’s empty.

3 Black’s strategies: growing at the start

In some ways more obvious. Maybe more sensible than in the last section.

B_{⋆}(a) = 1 + ( ∏ b : B(a) ) ( ∑ c : C(a, b) ) B_{⋆}(a[b/c])
C_{⋆}(a, s) = \begin{matrix}case s of \\ 0  → & 1 \\ λb. (c(b), s(b)) → & ( ∑ b : B(a) ) C_{⋆}(a[b/c(b)], s(b)) \end{matrix}

a[s/bs]_{⋆} = case s of

0  → a
λb. (c(b), s(b)) → \begin{matrix}case bs of \\ (bs_{0}, bs′) → & a[bs_{0}/c(bs_{0})][s(bs_{0})/bs′]_{⋆} \end{matrix}

4 The winner when two partial strategies fight

A mildly surprising thing (given the abstract nature of the datatypes) is that this is decidable. The gist of it is:

α vs. β : B^{∗}(a) + B_{⋆}(a) [a : A, α : B^{∗}(a), β : B_{⋆}(a)]
α vs. β = case α of (b, λc. α′(c)) → case β of λb. (c(b), β′(b)) → α′(c(b)) vs. β′(b) 0  → i α (0, β)  → j β

Here I have represented the outcome of a fight as an element of the disjoint union. The winner of a fight is the one who is left standing. (Note that the Black strategy 0 can be the winner, but only if the White strategy is 0.)

If you want a boolean,

β beats α : 2 [a : A, α : B^{∗}(a), β : B_{⋆}(a)]
α vs. β = case α of (b, λc. α′(c)) → case β of λb. (c(b), β′(b)) → α′(c(b)) vs. β′(b) 0  → 0 (0, β)  → 1

Several other things could be defined here by elaboration of the definition, such as the sequence of interactions, or predicates which mean that Black survives, White survives, and so on.

Exploiting such a definition, we can define a comparision relation between strategies. For example, if β and β′ are Black strategies, then β is ‘as strong as’ β′ if β beats everything that β′ beats. Write this β ⊑ β′ – thinking of β as a neighbourhood, and β as a more inclusive one. (Note this does not mean that β is an extension (development, elaboration) of β′. It is a relation ‘of magnitude’, it seems. Maybe this is a fatal flaw in what follows.)

β ⊑ β′ : Set [a : A, β : B_{⋆}(a), β′ : B_{⋆}(a)]
β ⊑ β′ = ( ∏ α : B^{∗}(a) ) β′ beats α → β beats α

This suggests that we might define a predicate of Black’s strategies (for a given state) to be total if:

1. For any two strategies β and β′ which satisfy the predicate, there is another β′′ which is at least as strong as both of them. (Directedness to left.)

2. If β satisfies the predicate, and β ⊑ β′, then β′ satisfies the predicate. (Upward closure.)

3. For any of White’s strategies α, there is a β which satisfies the predicate which beats α. (Maximality.)

Or a sequence of Black’s strategies to be convergent if first, successive strategies are as strong as preceding ones, and second, any White strategy is eventually beaten by some element of the sequence. Two such strategies are equivalent if for any element of one there is an element of the other which is as strong as it.

5 Discrimination

In this section I consider the question of defining ‘the’ simulation relation

(⪯) : A → P ow(A)

between states induced by a (B, C, d) structure on A. This should be the maximal solution of the equation

a ⪯ a′ ≡ \begin{matrix}( ∏ b : B(a) ) \\ ( ∑ t : B^{∗}(a′) ) \\ ( ∏ cs : C^{∗}(a′, t) ) \\ ( ∑ c : C(a, b) ) \\ a[b/c] ⪯ a′[t/cs]^{∗} \end{matrix}

Now we can consider an arbitrary ‘test program’ t : B^{∗}(a), and ask whether we can refute the statement a ⪯ a′ using the program t. To this end we define a subscripted version of ⪯. The meaning of a ⪯_{t} a′ is that as far as we can tell using the test program t, the state a can be simulated by the state a′. We define ⪯_{t} by recursion on t.

\begin{matrix}a ⪯_{0} a′ & =^{Δ} & T rue \\ a ⪯_{(b,f)} a′ & =^{Δ} & \begin{matrix}( ∑ t : B^{∗}(a′) ) \\ ( ∏ cs : C^{∗}(a′, t) ) \\ ( ∑ c : C(a, b) ) \\ a[b/c] ⪯_{f(c)} a′[t/cs]^{∗} \end{matrix} \end{matrix}

Now, how about defining a ⪯ a′ to mean ( ∏ t : B^{∗}(a) ) a ⪯_{t} a′ ?

That probably doesn’t work, but the idea is surely that one state refines another if it is indistinguishable from it in all well−founded environments.