Skip to content

Games.TypeTrees

Martin Escardo, Paulo Oliva, 2-27 July 2021

We represent the moves of a history-dependent sequential game by a
dependent-type tree, collected in a type 𝑻.  This is either an empty
tree [] or else has a type X of initial moves at the root, and,
inductively, a family Xf of subtrees indexed by elements of X, which
is written X ∷ Xf. We refer to the family Xf as a forest. We let Xt
range over such trees.

 * Xt ranges over dependent-type trees.
 * Xf ranges over dependent-type forests.


{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan

module Games.TypeTrees
        {𝓀 : Universe}
       where

open import MonadOnTypes.Definition hiding (map)
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

data 𝑻 : 𝓀 ⁺ Μ‡ where
  []  : 𝑻
  _∷_ : (X : 𝓀 Μ‡ ) (Xf : X β†’ 𝑻) β†’ 𝑻


The type of full paths in a tree Xt, from the root to a leaf, is
inductively defined as follows:


Path : 𝑻 β†’ 𝓀 Μ‡
Path []       = πŸ™
Path (X ∷ Xf) = Ξ£ x κž‰ X , Path (Xf x)


As discussed above, a play in a game is defined to be such a path.

The idea is that we choose a move x, and then, inductively, a path in
the subtree Xf x.

The variable xs ranges over paths, that is, elements of the type
Path Xt for a dependent-type-tree Xt.


pattern ⟨⟩        = ⋆
pattern _::_ x xs = (x , xs)

path-head : {X : 𝓀 Μ‡ } {Xf : X β†’ 𝑻} β†’ Path (X ∷ Xf) β†’ X
path-head (x :: xs) = x

path-tail : {X : 𝓀 Μ‡ } {Xf : X β†’ 𝑻} ((x :: xs) : Path (X ∷ Xf)) β†’ Path (Xf x)
path-tail (x :: xs) = xs

plength : {Xt : 𝑻} β†’ Path Xt β†’ β„•
plength {[]}     ⟨⟩        = 0
plength {X ∷ Xf} (x :: xs) = succ (plength {Xf x} xs)

subpred : {X : 𝓀 Μ‡ } {R : 𝓣 Μ‡ } {Xf : X β†’ 𝑻} β†’ ((Ξ£ x κž‰ X , Path (Xf x)) β†’ R) β†’ (x : X) β†’ Path (Xf x) β†’ R
subpred q x xs = q (x :: xs)


NB. An alternative inductive definition of Path is the following,
where, unfortunately, we get a higher type level, and so we won't use
it:


data Path₁ : 𝑻 β†’ 𝓀 ⁺ Μ‡ where
 []  : Path₁ []
 _∷_ : {X : 𝓀 Μ‡ } {Xf : X β†’ 𝑻} (x : X) (xs : Path₁ (Xf x)) β†’ Path₁ (X ∷ Xf)


Equip the internal nodes of a type tree with structure:


structure : (𝓀 Μ‡ β†’ π“₯ Μ‡ ) β†’ 𝑻 β†’ 𝓀 βŠ” π“₯ Μ‡
structure S []       = πŸ™
structure S (X ∷ Xf) = S X Γ— ((x : X) β†’ structure S (Xf x))


NB. An alternative inductive definition of structure is the following,
where, unfortunately, we get a higher type level, and so we won't use
it:


data structure₁ (S : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) : 𝑻 β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡ where
 []  : structure₁ S []
 _∷_ : {X : 𝓀 Μ‡ } {Xf : X β†’ 𝑻} β†’ S X β†’ ((x : X) β†’ structure₁ S (Xf x)) β†’ structure₁ S (X ∷ Xf)

structure-up : (S : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) (Xt : 𝑻) β†’ structure S Xt β†’ structure₁ S Xt
structure-up S []      ⟨⟩         = []
structure-up S (X ∷ Xf) (s :: sf) = s ∷ (Ξ» x β†’ structure-up S (Xf x) (sf x))

structure-down : (S : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) (Xt : 𝑻) β†’ structure₁ S Xt β†’ structure S Xt
structure-down S []      []        = ⟨⟩
structure-down S (X ∷ Xf) (s ∷ sf) = s :: (Ξ» x β†’ structure-down S (Xf x) (sf x))


Xt is hereditarily P if all its internal nodes satisfy P:


_is-hereditarily_ : 𝑻 β†’ (𝓀 Μ‡ β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
[]       is-hereditarily P = πŸ™
(X ∷ Xf) is-hereditarily P = P X Γ— ((x : X) β†’ Xf x is-hereditarily P)

being-hereditary-is-prop : Fun-Ext
                         β†’ (P : 𝓀 Μ‡ β†’ π“₯ Μ‡ )
                         β†’ ((X : 𝓀 Μ‡ ) β†’ is-prop (P X))
                         β†’ (Xt : 𝑻) β†’ is-prop (Xt is-hereditarily P)
being-hereditary-is-prop fe P P-is-prop-valued [] = πŸ™-is-prop
being-hereditary-is-prop fe P P-is-prop-valued (X ∷ Xf) =
 Γ—-is-prop
  (P-is-prop-valued X)
  (Ξ -is-prop fe Ξ» x β†’ being-hereditary-is-prop fe P P-is-prop-valued (Xf x))


The sequence operator for monads is defined on lists, but here we
consider a version on paths of a tree instead:


path-sequence : {β„“ : Universe β†’ Universe} (𝓣 : Monad {β„“})
                {Xt : 𝑻}
              β†’ structure (functor 𝓣) Xt
              β†’ functor 𝓣 (Path Xt)
path-sequence 𝓣 {[]}     ⟨⟩        = Ξ· 𝓣 ⟨⟩
path-sequence 𝓣 {X ∷ Xf} (t :: tf) = t βŠ—[ 𝓣 ] (Ξ» x β†’ path-sequence 𝓣 {Xf x} (tf x))


The induction principle for 𝑻 is included for the sake of
completeness, but won't be used directly:


𝑻-induction : (P : 𝑻 β†’ π“₯ Μ‡ )
            β†’ P []
            β†’ ((X : 𝓀 Μ‡ ) (Xf : X β†’ 𝑻) β†’ ((x : X) β†’ P (Xf x)) β†’ P (X ∷ Xf))
            β†’ (Xt : 𝑻) β†’ P Xt
𝑻-induction P b f = h
 where
  h : (Xt : 𝑻) β†’ P Xt
  h []       = b
  h (X ∷ Xf) = f X Xf (Ξ» x β†’ h (Xf x))

𝑻-recursion : (A : π“₯ Μ‡ )
            β†’ A
            β†’ ((X : 𝓀 Μ‡ ) β†’ (X β†’ 𝑻) β†’ (X β†’ A) β†’ A)
            β†’ 𝑻 β†’ A
𝑻-recursion A = 𝑻-induction (Ξ» _ β†’ A)

𝑻-iteration : (A : π“₯ Μ‡ )
            β†’ A
            β†’ ((X : 𝓀 Μ‡ ) β†’ (X β†’ A) β†’ A)
            β†’ 𝑻 β†’ A
𝑻-iteration A a g = 𝑻-induction (Ξ» _ β†’ A) a (Ξ» X Xf β†’ g X)


Here are some examples for the sake of illustration:


private

 Path' : 𝑻 β†’ 𝓀 Μ‡
 Path' = 𝑻-iteration (_ Μ‡ )  πŸ™ (Ξ» X F β†’ Ξ£ x κž‰ X , F x)

 Path'-[] : Path' [] ＝ πŸ™
 Path'-[] = refl

 Path'-∷ : (X : 𝓀 Μ‡ ) (Xf : X β†’ 𝑻)
         β†’ Path' (X ∷ Xf) ＝ (Ξ£ x κž‰ X , Path' (Xf x))
 Path'-∷ X Xf = refl

 structure' : (S : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) β†’ 𝑻 β†’ 𝓀 βŠ” π“₯ Μ‡
 structure' {π“₯} S = 𝑻-iteration (𝓀 βŠ” π“₯ Μ‡ ) πŸ™ (Ξ» X F β†’ S X Γ— ((x : X) β†’ F x))

 structure'-[] : (S : 𝓀 Μ‡ β†’ π“₯ Μ‡ )
               β†’ structure' S [] ＝ πŸ™
 structure'-[] S = refl

 structure'-∷ : (S : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) (X : 𝓀 Μ‡ ) (Xf : X β†’ 𝑻)
              β†’ structure' S (X ∷ Xf) ＝ S X Γ— ((x : X) β†’ structure' S (Xf x))
 structure'-∷ S X Xf = refl


Moved here 22 Oct 2025 from code from 8th October 2025 in the file
OptimalPlays, with a simplification on 29th October.


open import MLTT.List

private
 Ξ½ : {X : 𝓀 Μ‡ }
     {Xf : X β†’ 𝑻}
   β†’ ((x : X) β†’ List (Path (Xf x)))
   β†’ (X β†’ List (Path (X ∷ Xf)))
 Ξ½ f x = map (x ::_) (f x)


Notice that the above function Ξ½ transforms a dependent function into
a non-dependent one.


list-of-all-paths : (Xt : 𝑻)
                    (lt : structure listed Xt)
                  β†’ List (Path Xt)
list-of-all-paths [] ⟨⟩ = [ ⟨⟩ ]
list-of-all-paths (X ∷ Xf) ((xs , m) , lf) = List-ext (ν f) xs
 where
  f : (x : X) β†’ List (Path (Xf x))
  f x = list-of-all-paths (Xf x) (lf x)

path-is-member-of-list-of-all-paths : (Xt : 𝑻)
                                      (lt : structure listed Xt)
                                      (xs : Path Xt)
                                    β†’ member xs (list-of-all-paths Xt lt)
path-is-member-of-list-of-all-paths [] ⟨⟩ ⟨⟩ = in-head
path-is-member-of-list-of-all-paths (X ∷ Xf) ((ys , m) , lf) (x :: xs) = III
 where
  f : (x : X) β†’ List (Path (Xf x))
  f x = list-of-all-paths (Xf x) (lf x)

  IH : member xs (f x)
  IH = path-is-member-of-list-of-all-paths (Xf x) (lf x) xs

  I : member  (x :: xs) (Ξ½ f x)
  I = member-of-map→ (x ::_) (f x) xs IH

  II : member (Ξ½ f x) (map (Ξ½ f) ys)
  II = member-of-map→ (ν f) ys x (m x)

  III : member (x :: xs) (List-ext (Ξ½ f) ys)
  III = member-of-concat→ (x :: xs) (map (ν f) ys) (ν f x) II I


We are not currently using pmap, but we keep it for the record:


pmap  : {X : 𝓀 Μ‡ }
        {Xf : X β†’ 𝑻}
      β†’ ((x : X) β†’ Path (Xf x))
      β†’ List X
      β†’ List (Path (X ∷ Xf))
pmap = dmap