Introduction

Multi-party HO

A playground for HO

Fibredness

Constructing Fibred Double Categories
Towards New Sheaf Models of Programming Languages

Clovis Eberhart and Tom Hirschowitz

GaLoP XI, Eindhoven, April 2-3, 2016

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Playgrounds
Game semantics: semantics = interaction.

Playgrounds
pseudo double category

notion of strategy.

Pseudo double category:with extra structure
and properties.

Strategies:
sheaf semantics ≈ presheaf semantics + innocenceor concurrent game strategies.

Conclusion

Introduction

Multi-party HOA playground for HO

Fibredness

Building playgrounds from signatures

Until now:
automatic: playground 7→ notion of strategy,
playground = pseudo double category + properties,
problem: prove properties by hand for each language.

This work:
signatures → playgrounds → strategies,
prove properties abstractly,
new playground for HO games.

Conclusion

Introduction

Multi-party HO

A playground for HO

Overview

1

Multi-party HO

2

A playground for HO

3

Fibredness

Fibredness

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

HO games: notations

Arena = finite forest of “moves”.
Polarity (O or P) of a move = parity of its depth.
Roots have polarity O.
Notation:
A an arena,m a root of A,
A · m is the forest below m.

Play = P-visible, alternated, justified sequence of even length.
View = non-empty play such that dse = s.

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

A framework for HO

First: construct a multi-party framework for HO games.
Then: organise it into a pseudo double category.
Overview:
Positions
Generator moves
MovesPlaysConclusion

Introduction

Multi-party HOA playground for HO

Fibredness

Positions
Position: (kind of) graph:

A1..
.

CAAn

B

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Positions
Position: (kind of) graph:vertices are players

A1..
.

CA
An

B

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Positions
Position: (kind of) graph:vertices are players

edges are “gameboards”
A1..
.

CA
An

B

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Positions
Position: (kind of) graph:vertices are players
multiple incoming edges

edges are “gameboards”
A1..
.

CA
An

B

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Positions
Position: (kind of) graph:vertices are players
multiple incoming edges
at most one outgoing edge
edges are “gameboards”
A1..
.

CA
An

B

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Positions
Position: (kind of) graph:vertices are players
multiple incoming edges
at most one outgoing edge
edges are “gameboards”
A1..
.

CA
An

labelled with arenas

BConclusion

Introduction

Multi-party HO

A playground for HO

FibrednessPositions
Position: (kind of) graph:vertices are players
multiple incoming edges
at most one outgoing edge
edges are “gameboards”
A1..
.

CA
AnB
may be danglinglabelled with arenas

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Positions
Position: (kind of) graph:vertices are players
multiple incoming edges
at most one outgoing edge
edges are “gameboards”
A1..
.

CAAn

B
may be danglinglabelled with arenas

at most one source

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Positions
Position: (kind of) graph:vertices are players
multiple incoming edges
at most one outgoing edge
edges are “gameboards”
A1..
.

CAAnB
may be dangling
multiple targets

labelled with arenas

at most one source

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Positions
Position: (kind of) graph:vertices are players
multiple incoming edges
at most one outgoing edge
edges are “gameboards”
A1..
.

CAAnB
may be dangling
multiple targets

labelled with arenas

at most one source

each player has a sequent A1 , . . . , An ` B or A1 , . . . , An ` ofarenas.

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Moves (1)
Typical move:
B·q

final position:

ACB

initial position:

ABCConclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Moves (1)
Typical move:
B·q

final position:

ACB

initial position:

A

B

Analogy with sequent calculus:
A, B · q `B, C ` B · q

A`B

B, C `CConclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Moves (2)More generally, embed into any context.
Example:B·q

final position:ACB

initial position:

AB

CConclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Plays

Sequences of moves?
Too naive.
Need expressive morphisms between plays (e.g.,Ong-Tsukada).
Solution: retain only causal dependencies between moves.
Problem: how to represent this formally?

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Representing positions
Consider the following category C1 :objects = sequents and arenas,
morphisms = occurrences of arenas in sequents.
A1 , . . . , An ` AsiAisiA1 , . . . , An `

...

A...

t

Any position yields a presheaf on C1 !

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Representing positions: examples
A1 , . . . , An ` AsisiAi

A1 , . . . , An `

...

A...

t

A dangling edge labelled with A: the representable presheafyA .
A player on any sequent: the representable presheaf on thatsequent.
The position

AByBC
s1:yB,C `tyA`B·Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Diagram associated to a position
The presheaf representing
A1..
.

CA
An

B

is a colimit ofA1..
.
An(A`)(A1 ,...,An `A)AB(A,B`C )C.

Conclusion

Introduction

Multi-party HO

A playground for HO

Representing moves

How to represent plays?
How to represent moves?
Moves are more than just relations.
Add objects to C1 to represent moves!
Glue them together to form plays.
Which objects?

Fibredness

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Conclusion

Adding objects to C1 : fill the shell!
New object µ for move:
final position:

initial position:

B·q

ABAB

CC

Add green and red arrows making the diagram commute:(A,B·q`)B·qA(C ,B`B·q)

C(C ,B`)CB
(A`B)
µA

(A`B)

B

Introduction

Multi-party HO

A playground for HOFibredness

The augmented base category

Add an object for each instanceΓ, B · q `∆1 , B, ∆2 ` B · qΓ`B∆1 , B, ∆2 `with associated morphisms.

Definition
Let C denote the augmented category.

Conclusion

Introduction

Multi-party HOA playground for HO

Fibredness

Initial and final positionsRepresentable presheaf yµ : shapeless “blob”.
B·q
AC
B

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Conclusion

Initial and final positions
Representable presheaf yµ : shapeless “blob”.
B·q
AC
B

Organise it as a cospan Y → yµ ← X !
final position:

initial position:

AA

B·q
B

BCC

Introduction

Multi-party HO

A playground for HO

Fibredness

Summary

For each intended move:
new object µ in C,
cospan Y → yµ ← X , the generator move,
X initial position,
Y final position.
Next step: want moves to occur inside larger context:
glue the generator movealong some stable partto some position (the context).

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Stable part of a generator move

Any position I equipped with morphisms making
YIyµX

commute.

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Move
Gluing of a generator move to some context Z :
Y

Y0

yµ

M0IZ
X(levelwise pushout).

X0

Conclusion

Introduction

Multi-party HOA playground for HO

Fibredness

Conclusion

Example moveA

final position:

initial position:

AB·q

C

B

B

CY

Y0yµ

M0yA + y Cy(A`) + y(C `)X

X0Introduction

Multi-party HO

A playground for HOFibredness

PlayDefinitionbPlay = finite composite of moves in Cospan(C).
B·qq 0
B·q

AC

B

B·q

AA

B

CB

CConclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

A (pseudo) double category
Objects:
Horizontal morphisms:
Vertical morphisms:
Cells:
YkUU

αX

hY0
U0

X0Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

A (pseudo) double category
Objects: positions.
Horizontal morphisms: morphisms between positions.
Vertical morphisms: plays.
Cells: morphisms l making the diagram commute.
YkUU

αX

hY0YkY0U0U

l

U0

X0X

hX0Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Conclusion

Composition
Horizontal compositions: straightforward.
Vertical composition: by pushout.
Vertical composition of cells: by universal property of pushout.
Interchange law:
Z0Z

Y0

Y
βX

Z 00
α0α

X0

β0

Y 00
X 00

Introduction

Multi-party HO

A playground for HO

Fibredness

Comparison with Ong-TsukadaOng-Tsukada
views
plays
no players, no positions
time, sequential
P-view
P-visibility
composition, hiding=↔
=====

playgrounds
views
plays
players, positions
no time, causal∅∅hopelessConclusion

Introduction

Multi-party HOA playground for HO

Fibredness

Conclusion

Views

For Ong-Tsukada: VA,B = category of views on A → B(ordered by prefix).
In our sense: views are some (ad-hoc) non-empty plays onA ` B, EVA`B = category of views on A ` B, where morphisms
are “temporal inclusion”.

Lemma
VA,B and EVA`B are equivalent.

Introduction

Multi-party HO

A playground for HO

Fibredness

Plays
Wilder notion of play in our setting.
However:

Conjecture
Innocent strategies in our sense are equivalent to innocent
strategies in the sense of Ong-Tsukada.
Idea: prove that
VA,B

PA,B
idEV
A`B

EA`B

is an exact square.
Enough to prove: PA,B → EA`B fully faithful.

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Behaviours
Important construction of playgrounds: E.
Innocent strategies ≈ sheaves over E.

Eobjects: U : Ymorphisms (U : YX,X ) → (U 0 : Y 0ZlX 0 ):Y0W

YαU0UXh

X 0.

Conclusion

Introduction

Multi-party HO

A playground for HOFibredness

Composition in E
By pastingZel˜
γfWZl

Z0l0

W0Y0βWY

αY 00

U 00U0UX

hX0h0

where γ is a cartesian lifting of W 0 along l.

X 00 ,Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Crucial property: fibredness
Fibredness
A pseudo double category D is fibred if its “vertical codomain”
functor cod is a fibration.

Y 00U 00

X 00

Y0
U0

X0YUX

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Conclusion

Crucial property: fibredness
Fibredness
A pseudo double category D is fibred if its “vertical codomain”
functor cod is a fibration.

Y 00
U 00

X 00

Y 00
Y0
U0

X0

Y

U 00

Y0YU

X 00

U0U

X0XX

Introduction

Multi-party HO

A playground for HO

Fibredness

Factorisation systems(L, R) two classes of morphisms of C such that:every morphism of C can be decomposed as r ◦ l, for somel ∈ L and r ∈ R,L ⊥ R, i.e., for all l ∈ L, r ∈ R:··∃!

l·r·Properties:
L and R contain all isos, are stable under composition,
L is stable under pushouts,...

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Conclusion

Cofibrant generationM⊥ = class of morphisms g such that for all f of M, f ⊥ g .
M = idem.

⊥Small object argument (Bousfield)⊥
For any set J of morphisms of C, J ⊥ , (J ⊥ ) is a factorisation
system.
b J set of
Cofibrantly generated factorisation system on Cospan(C):X → yµ for Y → yµ ← X generator move.

Introduction

Multi-party HO

A playground for HO

Fibredness

Conclusion

Construction of the candidate lifting

YUU0r

Y

Y0YU

U0UX

X0Xl

X0X

X0Introduction

Multi-party HO

A playground for HO

Fibredness

Proof of fibration
Y 00
U 00

Y0

Y

X 00

U0U

X0X

U 00 → U 0 by the lifting property of factorisation systems,
Y 00 → Y 0 by universal property of pullback.

Conclusion

Introduction

Multi-party HO

A playground for HO

Fibredness

Conclusion
Done:
general construction of playgrounds,
better understanding of the link between playgrounds andclassical game semantics.
Work to do:prove full faithfulness of PA,B → EA`B ,influence of space,influence of time,
get the “right” views back,make hiding work.

Conclusion