Skip to content

Games.Examples

Martin Escardo, Paulo Oliva, 2-27 July 2021

Examples of type trees.


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

module Games.Examples where

open import MLTT.Spartan hiding (J)
open import MLTT.Fin
open import Games.TypeTrees
open import MonadOnTypes.J
open import MonadOnTypes.K

module permutations where


 no-repetitions : β„• β†’ 𝓀 Μ‡ β†’ 𝑻 {𝓀}
 no-repetitions 0        X = []
 no-repetitions (succ n) X = X ∷ Ξ» (x : X) β†’ no-repetitions n (Ξ£ y κž‰ X , y β‰  x)

 Permutations : β„• β†’ 𝓀₀ Μ‡
 Permutations n = Path (no-repetitions n (Fin n))

 example-permutation2 : Permutations 2
 example-permutation2 = 𝟎 :: ((𝟏 , (λ ())) :: ⟨⟩)

 example-permutation3 : Permutations 3
 example-permutation3 = 𝟐 :: ((𝟏 :: (λ ())) :: (((𝟎 , (λ ())) , (λ ())) :: ⟨⟩))



open import UF.FunExt

module search (fe : Fun-Ext) where

 open import MLTT.Athenian
 open import Games.FiniteHistoryDependent {𝓀₀} {𝓀₀} Bool

 open J-definitions Bool

 Ξ΅β‚‚ : J Bool
 Ξ΅β‚‚ p = p true

 h : β„• β†’ 𝑻
 h 0        = []
 h (succ n) = Bool ∷ Ξ» _ β†’ h n

 Ξ΅s : (n : β„•) β†’ 𝓙 (h n)
 Ρs 0        = ⟨⟩
 Ξ΅s (succ n) = Ξ΅β‚‚ :: Ξ» _ β†’ Ξ΅s n

 Ξ΅ : (n : β„•) β†’ J (Path (h n))
 Ξ΅ n = sequenceα΄Ά (Ξ΅s n)

 qq : (n : β„•) β†’ Path (h n) β†’ Bool
 qq 0        ⟨⟩        = true
 qq (succ n) (x :: xs) = not x && qq n xs

 test : (n : β„•) β†’ Path (h n)
 test n = Ξ΅ n (qq n)



module another-game-representation {𝓀 𝓦₀ : Universe} (R : 𝓦₀ Μ‡ ) where

 open K-definitions R

 data GameK {𝓀 : Universe} : 𝓀 ⁺ βŠ” 𝓦₀ Μ‡ where
  leaf   : R β†’ GameK {𝓀}
  branch : (X : 𝓀 Μ‡ ) (Xf : X β†’ GameK {𝓀}) (Ο• : K X) β†’ GameK


TODO. GameK ≃ Game and we have a map GameJ β†’ GameK.

TODO. Define game isomorphism (and possibly homomorphism more generally).


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

 record Game⁻ {𝓀 : Universe} : 𝓀 ⁺ βŠ” 𝓦₀ Μ‡ where
  constructor game⁻
  field
   Xt  : 𝑻 {𝓀}
   q   : Path Xt β†’ R


TODO. Game⁻ ≃ (Ξ£ R : ? Μ‡ , 𝑻' R). In Game⁻, we know how to play the
game, but we don't know what the objective of the game is.