Template games, simple games, and Day
convolution
Clovis Eberhart1 , Tom Hirschowitz2 , and Alexis Laouar2
1 ERATO MMSD, National Institute of Informatics, Tokyo
2 Université Grenoble Alpes, Université Savoie Mont Blanc, CNRS, Chambéry

GaLoP 2019, Prague, April 6-7, 20191 / 27

Introduction
Two abstract approaches to game semantics:
I game settings (E. and Hirschowitz, 2018):
I rather complex (sheaves, polynomial functors. . . ),I general (several instances: HON, AJM, Tsukada-Ong. . . ),I template games (Melliès, 2019):
I very simple and elegant,I maybe less general, differs from classic models.

Here:
I retelling of template games,
I extended to cover simple games,
I brings formal connection to Day convolution.

2 / 27

Overview

I Template games:
I games,
I strategies,
I copycats, composition.

I Weak double categories:
I internal monads,
I template games.

I Recovering simple game semantics:
I games,
I strategies,
I copycats, composition.

3 / 27

Template games

Definition
Let g be the category freely generated by the graphPO.

Definition
A template game is a category A equipped with a functor
p : A → g .

4 / 27

Simple games → template games
Simple game A:
I rooted tree
posetcategory,
I projection pA : A → g :I nodes at even depth to O,
I nodes at odd depth to P.

Example: booleans B
εOqp

B
7 →−qtqt

Pfqf

O

5 / 27

Template strategies
Definition
Let s be the category freely generated byPPOPOO.

Definition
A template strategy from A to B is a category S equipped withprojections
As0pgSt0ssB
qrtg .

6 / 27

Template strategies
Definition
Let s be the category freely generated byPOsPPOPtOOPO

Definition
A template strategy from A to B is a category S equipped withprojections
As0p

gS

t0ssBqrt

g .

6 / 27

Simple strategies: the arrow game
Definition
For A and B simple games, A → B:
I polarity of moves in A reversed,
I O starts in B,
I only P switches sides.

Example: B → B
B

qrql

tr

tl

fl

fr

tr

qr

fr

tr

Bql
frtl
fr
7 / 27

Boolean simple strategies
Definition
A boolean simple strategy from A to B is a non-empty,
prefix-closed set of even-length plays of A → B.

Example
B

qr
ql

tr

tl

fl

fr

tr

qr

fr

tr

B

ql
fr

tl
fr

Can be encoded by red nodes.
8 / 27

Simple strategies

Definition∗Let (A → B)P be the full subcategory of A → B spanning
non-empty, even-length plays.

DefinitionV∗

Simple strategies from A to B: (A → B)P .

9 / 27

Simple strategies → template strategies
V∗

Simple strategy σ ∈ (A → B)P :I el(σ): all possible “states” of the strategy after playing anon-empty, even-length play,I el(σ): all possible states, adding initial state and receptivity.

Translationel(σ)
As0pgt0(A → B)

qrs

s

Bt

g .

10 / 27

Template strategies: identities (copycats)
g

η

gs

sOη

PPP

gt

OPOOCopycatAAAppp

gηgsstg
11 / 27

The template of interactions

issµg
gst

stggsgts
PPPOPPOOPOOO

µPPOP

OO

12 / 27

Template strategies: composition

STABssgsstµgCsgtggt

13 / 27

Template strategies: composition
PSTABCissµggsst

s

gt

ggt

13 / 27

Template strategies: composition
PSTAB

C

is

sµg
gsts

s

gtggts

13 / 27

Weak double categoriesAsCf0B
αftuFAsBαDtgE

βt0ChCβ◦αDs0sf 0 ◦fg0Ef7→DβAguA7→DAD

Bid s id BCAβ•α hfFBt 0 •tsid AAs 0 •sB

Bsid •A

Aid •f fid •BB

CγαEβGFfFAg 0 ◦gF
δHI
14 / 27

Span(C)
ApCS

AB
qα
T=

Dsp

C

Stq

αs0T

Bt0

D

Horizontally:
I composition of spans by pullback,I composition of cells by universal property,
I choice of pullbacks

bicategory.

Template games
In Span(Cat):I game: A → g ,I strategy: cell over s .
15 / 27

Internal monads
Definition
Monad in double category: horizontal morphism M : XMXη

XandX

M

XX withMµX

M

satisfying the obvious generalisation of the usual monad laws.

Examples : g
g is a monad in Span(Cat):•I η : id g ⇒ s : synchronous copycat schedule,
I µ : i ⇒ s : parallel composition + hiding.

16 / 27

D/M
Candidate weak double category:I objects: vertical morphisms A → X ,I vertical morphisms from A → X to B → X : commuting
triangles of vertical morphisms,
I horizontal morphisms from A → X to B → X : cells over M,fApBqαXX,

MI cells: commuting “triangles” of cells.
A0B0γ

ABβα

X

M

X
17 / 27

Template game semantics: Span(Cat)/sTemplate strategy from A to B:
ASBpσqg

s

g

AASpid •ppp

g

ηg

g

Copycats and composition:AsBTCσqτrsgsgµsTheoremFor any monad M : X → X internal to a weak double category D,
D/M is again a weak double category.
18 / 27

Template games vs. simple games: first discrepancy
First discrepancy
I Simple games: initial object, polarity O (root).
I Template games:
I Z → g : no initial object,
I pPq : 1 → g : polarity P.

Second discrepancy
Simple games A → g are discrete Conduché fibrations:fPhQ

Rkv ◦uIu

FKJEBv

19 / 27

Recovering simple games
Change the template: Tg = O/g .

Definition
Refined template game: discrete fibration to Tg .

RemarkTg ∼=ω

discrete fibration into Tg = forest.

Lemma
Refined template game is isomorphic to simple game iff definite(fibre over id O singleton).

20 / 27

Naively refined template strategies
Same discrepancies as games

choose Ts = OO/s ?

Definition
Naively refined template strategy from A to B:
s0A
p

St0

B
qr

Tg

sTsTg ,twith r a discrete fibration.

Problem(A → B)

ABpTg

qsTstTg
21 / 27

Refined template strategies
We want strategies to be presheaves over (A → B)P
even-length plays of OO/s .

∗Ts spansDefinition
Refined template strategy from A to B: category S equipped withAs0p

Tg

St0sTsB
qrt

Tg ,with r a discrete fibration.

Lemma
Refined template strategy is isomorphic to simple strategy iffdefinite.
22 / 27

Copycats
Ts : Tg

Tg is still a monad.

CopycatAAAppp

Tg
ηTg

sTst

Tg

Problemηp is not always a discrete fibration.

23 / 27

Interlude: double factorisation systems
Given double category D, pair of factorisation systems:
I (Lv , Rv ) on Dv ,I (LV , RV ) on DV ,such that s, t : DV → Dv map LV (resp. RV ) to Lv (resp. Rv )
andA

SlB

αr

C

U

A0l0
B0=

A

S

A0l

λl0
B0

B

r0r

C0

CT
ρ
Ur0
C0

ExampleOn Span(C): (L, R) and componentwise (L, R).
24 / 27

Simple games: Span(Cat)/DFib T
Horizontal identities:ApA

λid •pρ

XpX.
ηM

Horizontal composition:
ASTBCλXMXρ MX.

µM

TheoremIf the double factorisation system is nice enough, then D/R M is aweak double category.
25 / 27

Day convolution
I Weak double category W:
I vertically trivial, i.e., essentially a monoidal category,
I WV = Cat,I horizontal composition = cartesian product in Cat.

I Monad C = strict monoidal category.
I (↑, DFib) forms a double factorisation system.

Corollary
I W/DFib C vertically trivial, i.e., a monoidal category.
VI W/DFib C ' C.
I Horizontal composition is Day convolution.

26 / 27

Conclusion
Done:
I characterisation of simple games among template games,
I composition of simple strategies as refinement of compositionof template strategies,
I general slicing construction,
I link with Day convolution.
To-do:
I more structure,
I get exactly simple games (unique initial state),
I get Day convolution for general monoidal categories.

27 / 27