"How to Make Good Choices" notes for a talk

Choices.agda

{-# OPTIONS --postfix-projections #-}
module Choices where

open import Level using (0ℓ) renaming (suc to lsuc)
open import Data.Product using (_,_; _×_; Σ-syntax; proj₁; proj₂)
open import Data.Bool using (true; false; if_then_else_; _∧_; not)
  renaming (Bool to 𝔹)
open import Data.Nat using (ℕ; zero; suc; _≤ᵇ_)
open import Data.Unit using (⊤; tt)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)


------------------------------------------------------------------------------
--
--         HOW TO MAKE GOOD CHOICES
--
--  Robert Atkey, MSP 101, 8th November 2024
--
------------------------------------------------------------------------------


------------------------------------------------------------------------------
-- Part I : Choice Monads
------------------------------------------------------------------------------

record ChoiceMonad : Set (lsuc 0ℓ) where
  field
    Mon    : Set → Set
    unit   : ∀ {A} → A → Mon A
    bind   : ∀ {A B} → Mon A → (A → Mon B) → Mon B
    choose : Mon 𝔹
open ChoiceMonad


-- Choice trees:

data Choices (A : Set) : Set where
  success : A → Choices A
  branch  : Choices A → Choices A → Choices A

Choices-unit : ∀ {A} → A → Choices A
Choices-unit a = success a

Choices-bind : ∀ {A B} → Choices A → (A → Choices B) → Choices B
Choices-bind (success a)    k = k a
Choices-bind (branch c₁ c₂) k = branch (Choices-bind c₁ k) (Choices-bind c₂ k)

Choices-choose : Choices 𝔹
Choices-choose = branch (success true) (success false)

ChoicesChoiceMonad : ChoiceMonad
ChoicesChoiceMonad .Mon = Choices
ChoicesChoiceMonad .unit = success
ChoicesChoiceMonad .bind = Choices-bind
ChoicesChoiceMonad .choose = Choices-choose

argmin : ∀ {A} → (A → ℕ) → Choices A → A
argmin cost (success a)    = a
argmin cost (branch c₁ c₂) =
  let a₁ = argmin cost c₁
      a₂ = argmin cost c₂
   in if cost a₁ ≤ᵇ cost a₂ then a₁ else a₂


-- Selectors:

Selection : Set → Set → Set
Selection R A = (A → R) → A

Selection-unit : ∀ {R A} → A → Selection R A
Selection-unit a _cost = a

Selection-bind : ∀ {A B R} → Selection R A → (A → Selection R B) → Selection R B
Selection-bind c k = λ cost →
  let b = c (λ a → cost (k a cost)) in k b cost

Selection-choose : Selection ℕ 𝔹
Selection-choose cost =
  if cost true ≤ᵇ cost false then true else false

SelectionChoiceMonad : ChoiceMonad
SelectionChoiceMonad .Mon = Selection ℕ
SelectionChoiceMonad .unit = λ a _ → a
SelectionChoiceMonad .bind = Selection-bind
SelectionChoiceMonad .choose = Selection-choose


-- Claim:
--
--   The Choices monad and the Selection monad are the same, *if* we
--   only use the `choose` operation, and we only care about the
--   `argmin` result.

------------------------------------------------------------------------------
-- Part II: A Language of choices
------------------------------------------------------------------------------

module Language where

  data Type : Set where
    `nat `bool : Type
    _`×_ _`⇒_ : Type → Type → Type
    `choices   : Type → Type

  data Ctx : Set where
    ε    : Ctx
    _,-_ : Ctx → Type → Ctx

  variable
    S T U V : Type
    Γ Δ : Ctx

  data Var : Ctx → Type → Set where
    zero :           Var (Γ ,- T) T
    suc  : Var Γ T → Var (Γ ,- S) T

  data Term : Ctx → Type → Set where
    `var  : Var Γ T → Term Γ T

    `lam  : Term (Γ ,- S) T
          → Term Γ (S `⇒ T)
    `app  : Term Γ (S `⇒ T)
          → Term Γ S
          → Term Γ T

    `pair : Term Γ S
          → Term Γ T
          → Term Γ (S `× T)
    `fst  : Term Γ (S `× T)
          → Term Γ S
    `snd  : Term Γ (S `× T)
          → Term Γ T

    `true `false : Term Γ `bool
    `ifte : Term Γ `bool
          → Term Γ T
          → Term Γ T
          → Term Γ T
    `const : ℕ → Term Γ `nat

    `pure : Term Γ T
          → Term Γ (`choices T)
    `let  : Term Γ (`choices S)
          → Term (Γ ,- S) (`choices T)
          → Term Γ (`choices T)
    `choose : Term Γ (`choices `bool)

------------------------------------------------------------------------------
-- Part III: Interpretation
------------------------------------------------------------------------------

module Interpretation (CM : ChoiceMonad) where

  open Language

  ⟦_⟧ty : Type → Set
  ⟦ `nat ⟧ty       = ℕ
  ⟦ `bool ⟧ty      = 𝔹
  ⟦ S `× T ⟧ty     = ⟦ S ⟧ty × ⟦ T ⟧ty
  ⟦ S `⇒ T ⟧ty    = ⟦ S ⟧ty → ⟦ T ⟧ty
  ⟦ `choices T ⟧ty = CM .Mon ⟦ T ⟧ty

  ⟦_⟧ctx : Ctx → Set
  ⟦ ε ⟧ctx      = ⊤
  ⟦ Γ ,- T ⟧ctx = ⟦ Γ ⟧ctx × ⟦ T ⟧ty

  ⟦_⟧var : Var Γ T → ⟦ Γ ⟧ctx → ⟦ T ⟧ty
  ⟦ zero ⟧var  (_ , t) = t
  ⟦ suc x ⟧var (γ , _) = ⟦ x ⟧var γ

  ⟦_⟧tm : Term Γ T → ⟦ Γ ⟧ctx → ⟦ T ⟧ty
  ⟦ `var x ⟧tm      γ = ⟦ x ⟧var γ
  ⟦ `lam M ⟧tm      γ = λ s → ⟦ M ⟧tm (γ , s)
  ⟦ `app M N ⟧tm    γ = ⟦ M ⟧tm γ (⟦ N ⟧tm γ)
  ⟦ `pair M N ⟧tm   γ = ⟦ M ⟧tm γ , ⟦ N ⟧tm γ
  ⟦ `fst M ⟧tm      γ = ⟦ M ⟧tm γ .proj₁
  ⟦ `snd M ⟧tm      γ = ⟦ M ⟧tm γ .proj₂
  ⟦ `true ⟧tm       γ = true
  ⟦ `false ⟧tm      γ = false
  ⟦ `ifte L M N ⟧tm γ = if ⟦ L ⟧tm γ then ⟦ M ⟧tm γ else ⟦ N ⟧tm γ
  ⟦ `const n ⟧tm    γ = n
  ⟦ `pure M ⟧tm     γ = CM .unit (⟦ M ⟧tm γ)
  ⟦ `let M N ⟧tm    γ = CM .bind (⟦ M ⟧tm γ) (λ s → ⟦ N ⟧tm (γ , s))
  ⟦ `choose ⟧tm     γ = CM .choose

-- Interpretation using the choice trees:
module ChoiceInterp = Interpretation ChoicesChoiceMonad

-- Interpretation using the selection functions:
module SelectionInterp = Interpretation SelectionChoiceMonad

-- These two interpretations are not equal!
--
-- It is not true that
--         ∀ T → ChoiceInterp.⟦ T ⟧ty ≡ SelectionInterp.⟦ T ⟧ty
-- and we can't even state
--         ∀ M → ChoiceInterp.⟦ M ⟧tm ≡ SelectionInterp.⟦ M ⟧tm

------------------------------------------------------------------------------
-- Part IV: Relating two Interpretations
------------------------------------------------------------------------------

record ChoiceMonadR (CM1 CM2 : ChoiceMonad) : Set (lsuc 0ℓ) where
  field
    RMon  : ∀ {A₁ A₂} → (A₁ → A₂ → Set) → (CM1 .Mon A₁ → CM2 .Mon A₂ → Set)

    Runit : ∀ {A₁ A₂} {R : A₁ → A₂ → Set} →
            ∀ {a₁ a₂} → R a₁ a₂ → RMon R (CM1 .unit a₁) (CM2 .unit a₂)

    Rbind : ∀ {A₁ A₂ B₁ B₂} {R : A₁ → A₂ → Set} {S : B₁ → B₂ → Set} →
            ∀ {c₁ c₂ k₁ k₂} →
            RMon R c₁ c₂ →
            (∀ {a₁ a₂} → R a₁ a₂ → RMon S (k₁ a₁) (k₂ a₂)) →
            RMon S (CM1 .bind c₁ k₁) (CM2 .bind c₂ k₂)

    Rchoose : RMon _≡_ (CM1 .choose) (CM2 .choose)
open ChoiceMonadR


module R {CM1 CM2 : ChoiceMonad} (RCM : ChoiceMonadR CM1 CM2) where

  open Language

  module I1 = Interpretation CM1
  module I2 = Interpretation CM2

  ⟦_⟧ty : (T : Type) → I1.⟦ T ⟧ty → I2.⟦ T ⟧ty → Set
  ⟦ `nat ⟧ty       n₁        n₂        = n₁ ≡ n₂
  ⟦ `bool ⟧ty      b₁        b₂        = b₁ ≡ b₂
  ⟦ S `× T ⟧ty     (s₁ , t₁) (s₂ , t₂) = ⟦ S ⟧ty s₁ s₂ × ⟦ T ⟧ty t₁ t₂
  ⟦ S `⇒ T ⟧ty    f₁        f₂        = ∀ {s₁ s₂} → ⟦ S ⟧ty s₁ s₂ → ⟦ T ⟧ty (f₁ s₁) (f₂ s₂)
  ⟦ `choices T ⟧ty c₁        c₂        = RCM .RMon ⟦ T ⟧ty c₁ c₂

  ⟦_⟧ctx : (Γ : Ctx) → I1.⟦ Γ ⟧ctx → I2.⟦ Γ ⟧ctx → Set
  ⟦ ε ⟧ctx      tt        tt        = ⊤
  ⟦ Γ ,- T ⟧ctx (γ₁ , t₁) (γ₂ , t₂) = (⟦ Γ ⟧ctx γ₁ γ₂) × (⟦ T ⟧ty t₁ t₂)

  ⟦_⟧var : (x : Var Γ T) → ∀ {γ₁ γ₂} → ⟦ Γ ⟧ctx γ₁ γ₂ → ⟦ T ⟧ty (I1.⟦ x ⟧var γ₁) (I2.⟦ x ⟧var γ₂)
  ⟦ zero ⟧var  (_ , r) = r
  ⟦ suc x ⟧var (ρ , _) = ⟦ x ⟧var ρ

  ⟦_⟧tm : (M : Term Γ T) → ∀ {γ₁ γ₂} → ⟦ Γ ⟧ctx γ₁ γ₂ → ⟦ T ⟧ty (I1.⟦ M ⟧tm γ₁) (I2.⟦ M ⟧tm γ₂)
  ⟦ `var x ⟧tm    ρ = ⟦ x ⟧var ρ
  ⟦ `lam M ⟧tm    ρ = λ r → ⟦ M ⟧tm (ρ , r)
  ⟦ `app M N ⟧tm  ρ = ⟦ M ⟧tm ρ (⟦ N ⟧tm ρ)
  ⟦ `pair M N ⟧tm ρ = (⟦ M ⟧tm ρ) , (⟦ N ⟧tm ρ)
  ⟦ `fst M ⟧tm    ρ = ⟦ M ⟧tm ρ .proj₁
  ⟦ `snd M ⟧tm    ρ = ⟦ M ⟧tm ρ .proj₂
  ⟦ `true ⟧tm     ρ = refl
  ⟦ `false ⟧tm    ρ = refl
  ⟦ `ifte L M N ⟧tm {γ₂ = γ₂} ρ rewrite ⟦ L ⟧tm ρ with I2.⟦ L ⟧tm γ₂
  ... | false = ⟦ N ⟧tm ρ
  ... | true  = ⟦ M ⟧tm ρ
  ⟦ `const x ⟧tm ρ = refl
  ⟦ `pure M ⟧tm  ρ = RCM .Runit (⟦ M ⟧tm ρ)
  ⟦ `let M N ⟧tm ρ = RCM .Rbind (⟦ M ⟧tm ρ) (λ s → ⟦ N ⟧tm (ρ , s))
  ⟦ `choose ⟧tm  ρ = RCM .Rchoose


------------------------------------------------------------------------------
-- Part V: Relating Choices and Selection
------------------------------------------------------------------------------

module ChoicesAndSelections where

  CS-R : ∀ {A₁ A₂} → (A₁ → A₂ → Set) → (Choices A₁ → Selection ℕ A₂ → Set)
  CS-R {A₁} {A₂} R c s =
    ∀ {cost₁ : A₁ → ℕ} {cost₂ : A₂ → ℕ} →
      (∀ {a₁ a₂} → R a₁ a₂ → cost₁ a₁ ≡ cost₂ a₂) →
      R (argmin cost₁ c) (s cost₂)

  CS-unit : ∀ {A₁ A₂} {R : A₁ → A₂ → Set} →
              ∀ {a₁ a₂} → R a₁ a₂ → CS-R R (success a₁) (λ _ → a₂)
  CS-unit r _ = r

  lemma0 : ∀ {A B : Set}{x y : A}(f : A → B) (b : 𝔹) →
           (if b then f x else f y) ≡ f (if b then x else y)
  lemma0 f false = refl
  lemma0 f true = refl

  lemma : ∀ {A B} (cost : B → ℕ) (c : Choices A) (k : A → Choices B) →
          argmin cost (Choices-bind c k)
            ≡ argmin cost (k (argmin (λ x → cost (argmin cost (k x))) c))
  lemma cost (success a)    k = refl
  lemma cost (branch c₁ c₂) k
    rewrite lemma cost c₁ k
    rewrite lemma cost c₂ k =
      lemma0 (λ x → argmin cost (k x)) _

  CS-bind : ∀ {A₁ A₂ B₁ B₂} {R : A₁ → A₂ → Set} {S : B₁ → B₂ → Set} →
            ∀ {c₁ c₂ k₁ k₂} →
            CS-R R c₁ c₂ →
            (∀ {a₁ a₂} → R a₁ a₂ → CS-R S (k₁ a₁) (k₂ a₂)) →
            CS-R S (Choices-bind c₁ k₁) (Selection-bind c₂ k₂)
  CS-bind {c₁ = c₁} {k₁ = k₁} c k {cost₁ = cost₁} cost rewrite lemma cost₁ c₁ k₁
    = k (c (λ a → cost (k a cost))) cost

  CS-choose : CS-R _≡_ (branch (success true) (success false)) Selection-choose
  CS-choose cost rewrite cost {true} refl rewrite cost {false} refl = refl

  RMonads : ChoiceMonadR ChoicesChoiceMonad SelectionChoiceMonad
  RMonads .RMon = CS-R
  RMonads .Runit = CS-unit
  RMonads .Rbind {c₁ = c₁} {k₁ = k₁} c k = CS-bind {c₁ = c₁} {k₁ = k₁} c k
  RMonads .Rchoose = CS-choose

  module ChoicesAndSelections = R RMonads

  open Language

  result : (M : Term ε (`choices `nat)) →
           argmin (λ x → x) (ChoiceInterp.⟦ M ⟧tm tt) ≡ SelectionInterp.⟦ M ⟧tm tt (λ x → x)
  result M = ChoicesAndSelections.⟦ M ⟧tm tt (λ eq → eq)


------------------------------------------------------------------------------
-- Part IV: Changing the Objective
------------------------------------------------------------------------------

choose-f : ∀ {R} → (R → ℕ) → Selection R 𝔹
choose-f u cost =
  if u (cost true) ≤ᵇ u (cost false) then true else false

{-
prisoner's-dilemma : Term ε (`choices (`nat `× `nat))
prisoner's-dilemma =
  do m₁ ← choose fst
     m₂ ← choose snd
     return (if m₁ then (if m₂ then (2,  2)
                               else (10, 0))
                   else (if m₂ then (0,  10)
                               else (5,  5)))
-}

data Choices2 (R : Set) (A : Set) : Set where
  success : A → Choices2 R A
  branch  : (R → ℕ) → Choices2 R A → Choices2 R A → Choices2 R A

argmin2 : ∀ {R A} → (A → R) → Choices2 R A → A
argmin2 cost (success x) = x
argmin2 cost (branch u c₁ c₂) =
  let a₁ = argmin2 cost c₁
      a₂ = argmin2 cost c₂
   in if u (cost a₁) ≤ᵇ u (cost a₂) then a₁ else a₂

Choices-choose-f : ∀ {R} → (R → ℕ) → Choices2 R 𝔹
Choices-choose-f u = branch u (success true) (success false)

-- Claims:
--
-- 1. The language can be extended with these relativised choice
--    operators
--
-- 2. The logical relation can be adapted to relate these two
--    interpretations in a similar way.
--
-- 3. Every strategic game in normal form can be represented as above,
--    and the selected outcome is a Nash Equilibrium in pure
--    strategies.
--
-- 4. With a bit more work, we can argmin over mixed strategies, and
--    take expected payoffs, to get _a_ Nash Equilibrium in mixed
--    strategies.

------------------------------------------------------------------------------
-- Part V: Nominated Choices
------------------------------------------------------------------------------

data Choices3 (R : Set) (A : Set) : Set where
  success : A → Choices3 R A
  branch  : (R → ℕ) → 𝔹 → (𝔹 → Choices3 R A) → Choices3 R A

selectC : ∀ {R} → (R → ℕ) → 𝔹 → Choices3 R 𝔹
selectC u b = branch u b success

outcome : ∀ {R A} → Choices3 R A → A
outcome (success a)    = a
outcome (branch u b k) = outcome (k b)

abam : ∀ {R} → Choices3 R R → 𝔹
abam (success _)    = true
abam (branch u b k) =
  (u (outcome (k b)) ≤ᵇ u (outcome (k (not b)))) ∧ abam (k b)






Select3 : Set → Set → Set
Select3 R A = A × ((A → R) → 𝔹)

Select3-unit : ∀ {R A} → A → Select3 R A
Select3-unit a .proj₁ = a
Select3-unit a .proj₂ cost = true

Select3-bind : ∀ {R A B} → Select3 R A → (A → Select3 R B) → Select3 R B
Select3-bind (a , ϕ) k .proj₁ = k a .proj₁
Select3-bind (a , ϕ) k .proj₂ cost =
  ϕ (λ a → cost (k a .proj₁)) ∧ k a .proj₂ cost

selectS : ∀ {R} → (R → ℕ) → 𝔹 → Select3 R 𝔹
selectS u b .proj₁ = b
selectS u b .proj₂ cost = u (cost b) ≤ᵇ u (cost (not b))

{-
prisoner's-dilemma : Term (ε ,- `bool ,- `bool) (`choices (`nat `× `nat))
prisoner's-dilemma σ₁ σ₂ =
  do m₁ ← choose fst σ₁
     m₂ ← choose snd σ₂
     return (if m₁ then (if m₂ then (2,  2)
                               else (10, 0))
                   else (if m₂ then (0,  10)
                               else (5,  5)))
-}

-- Claims:
--
-- 1. The language can be extended with these nominated and
--    relativised choice operators.
--
-- 2. The logical relation can be adapted to relate these two
--    interpretations in a similar way.
--
-- 3. Every strategic game in normal form can be represented as above,
--    and the 'abam' predicate identifies exactly the Nash equilibria.
--
-- 4. With a bit more work, we can argmin over mixed strategies, and
--    take expected payoffs, to get all Nash Equilibria in mixed
--    strategies.


------------------------------------------------------------------------------
-- Part VI: Feedback
------------------------------------------------------------------------------

-- The “category writer monad”
Lens : Set → Set → Set → Set
Lens R S A = A × (S → R)

Lens-unit : ∀ {R A} → A → Lens R R A
Lens-unit a = a , (λ r → r)

Lens-bind : ∀ {R S T A B} → Lens R S A → (A → Lens S T B) → Lens R T B
Lens-bind (a , f) k = let (b , g) = k a in b , λ t → f (g t)

-- Nomination + Selection + Feedback
SelectF : Set → Set → Set → Set
SelectF R S A = A × ((A → S) → 𝔹) × (S → R)

-- Claims:
--
--   Functions  A → SelectF R S B are Open Games (A, R) → (B, S)
--