Skip to content

Instantly share code, notes, and snippets.

@Lysxia Lysxia/HTree.v
Created Oct 3, 2019

Embed
What would you like to do?
Indexed containers for game semantics
(** An (indexed) "container" encodes an indexed recursive type. *)
(** A container can also be seen as a game, with
- [ix] as the type of positions,
- [shape i] the Player moves at position [i],
- [pos i s] the Opponent moves after Player plays move [s] on position [i],
- [posix i s p] the new position after moves [s] and [p] from position [i].
*)
Module Export Container.
Record container :=
{ ix : Type (* Indices *)
; shape : ix -> Type (* Constructors *)
; pos : forall i : ix, shape i -> Type (* (Recursive) fields *)
; posix : forall (i : ix) (s : shape i), pos i s -> ix (* Index for each field *)
}.
End Container.
Definition _htree (c : container) (f : ix c -> Type) (i : ix c) (r : Type) : Type :=
forall (s : shape c i), (forall p : pos c i s, f (posix c i s p)) -> r.
(** The fixed-point associated with container [c]. *)
Inductive htree (c : container) (i : ix c) : Type :=
| ToFix : _htree c (htree c) i (htree c i)
.
(** A trivial container. [htree c I] is isomorphic to [t]. *)
Definition const (t : Type) : container :=
{| ix := True
; shape := fun _ => t
; pos := fun _ _ => False
; posix := fun _ _ v => match v : False with end
|}.
(** "Tensor product" of containers/games: sum their constructors, which act
independently on their indices. *)
Module Sum.
Section Sum.
Context (c1 c2 : container).
Definition ix : Type := ix c1 * ix c2.
Definition shape (i : ix) : Type := shape c1 (fst i) + shape c2 (snd i).
Definition pos (i : ix) (s : shape i) : Type :=
match s with
| inl s1 => pos c1 (fst i) s1
| inr s2 => pos c2 (snd i) s2
end.
Definition posix (i : ix) (s : shape i) : pos i s -> ix :=
match s with
| inl s1 => fun p => (posix c1 (fst i) s1 p, snd i)
| inr s2 => fun p => (fst i, posix c2 (snd i) s2 p)
end.
Definition sum : container :=
{| Container.ix := ix
; Container.shape := shape
; Container.pos := pos
; Container.posix := posix
|}.
End Sum.
End Sum.
(** Dual of a container. We take the initial Player move (who becomes the
Opponent) as an external parameter.
It is involutive modulo some isomorphism. *)
Module Dual.
Section Dual.
Context (c : container).
Definition ix : Type := { i : ix c & shape c i }.
Definition shape (i : ix) : Type := pos c _ (projT2 i).
Definition pos (i : ix) (p : shape i) : Type := Container.shape c (Container.posix c _ _ p).
Definition posix (i : ix) (p : shape i) (s : pos i p) : ix := existT _ (Container.posix c _ _ p) s.
Definition i0 (i : Container.ix c) (s : Container.shape c i) : ix := existT _ i s.
Definition dual : container :=
{| Container.ix := ix
; Container.shape := shape
; Container.pos := pos
; Container.posix := posix
|}.
End Dual.
End Dual.
(** Containers form a category [ARR]:
- objects are containers paired with initial indices/positions,
- morphisms are htrees/strategies, parameterized by an initial opponent move.
*)
(** "Arrow" constructor on containers/games. *)
Definition arr (c1 c2 : container) : container :=
Sum.sum (Dual.dual c1) c2.
(** "Arrow" constructor on container-index pairs. *)
Definition ARR (c1 c2 : container) (i1 : ix c1) (i2 : ix c2) : Type :=
forall (s : shape c1 i1), htree (arr c1 c2) (Dual.i0 c1 i1 s, i2).
(** Composition of morphisms. *)
Section Compose.
Context (c1 c2 c3 : container).
Fixpoint __compose (i1 : ix (Dual.dual c1)) (i2 : ix (Dual.dual c2)) (i3 : ix c3)
(u : htree (arr c2 c3) (i2, i3))
(k : forall (p : pos c2 _ (projT2 i2)) (i3 : ix c3)
(u : forall s2 : shape c2 (posix c2 _ _ p), htree (arr c2 c3) (Dual.i0 c2 _ s2, i3)),
htree (arr c1 c3) (i1, i3)) : htree (arr c1 c3) (i1, i3) :=
match u with
| ToFix _ _ s' k' =>
match s' return (forall p : _ s', htree _ (posix (arr c2 c3) (i2, i3) s' p)) -> _ with
| inl s2 => fun k' => k s2 _ (fun s => k' s)
| inr s3 => fun k' => ToFix _ _
(inr s3 : shape (arr c1 c3) (i1, i3))
(fun p => __compose i1 i2 _ (k' p) k)
end k'
end.
Fixpoint _compose (i1 : ix (Dual.dual c1)) (i2 : ix c2) (i3 : ix c3)
(t : htree (arr c1 c2) (i1, i2)) (u : forall s2 : shape c2 i2, htree (arr c2 c3) (Dual.i0 c2 i2 s2, i3))
: htree (arr c1 c3) (i1, i3) :=
match t with
| ToFix _ _ s k =>
match s return (forall p : _ s, htree _ (posix (arr c1 c2) (i1, i2) s p)) -> _ with
| inl s1 => fun k => ToFix _ _
(inl s1 : shape (arr c1 c3) (i1, i3))
(fun p => _compose (Dual.posix _ _ s1 p) i2 i3 (k p) u)
| inr s2 => fun k => __compose i1 _ i3 (u s2) (fun p i3 u => _compose i1 _ i3 (k p) u)
end k
end.
Definition compose (i1 : ix c1) (i2 : ix c2) (i3 : ix c3)
(a12 : ARR c1 c2 i1 i2) (a23 : ARR c2 c3 i2 i3)
: ARR c1 c3 i1 i3 :=
fun s => _compose (existT _ i1 s) i2 i3 (a12 s) a23.
End Compose.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.