HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

What's the correct definition of the $\Upsilon$ category of schedules?

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
definitionthewhatcategoryschedulescorrectupsilon

Problem

I'm reading this article about game semantics and I'm a bit puzzled with the definition given for $\Upsilon$ in section $3.3$. There are some points that are either unintelligible or that don't make sense at all.

The definition provided is based on the concept of schedule:


A schedule $e:\{1, \ldots, n\} \rightarrow {0, 1}$ is a sequence of
$0$ and $1$s. We also define $|e| = n$, $|e|_0$ is the number of $0$s
in $e$ and $|e|_1$ is the number of $1$s. The notation $e \upharpoonright m$ denotes the restriction of $e$ to its first $m$ terms.

(Where $e$ is actually a function, but we can view $e$ as the sequence $e(1)\cdot e(2)\cdots e(n)$.)

Now the definition of the category $\Upsilon$ is:



  • The objects are the natural numbers. We think of $p \in \Upsilon_0$ as the totally ordered set $(p) = \{1, \ldots, p\}$. We


write $(p)^+$ for the set of even elements and $(p)^-$ for the set of
odd elements of $(p)$.

-
The morphism in $\Upsilon(p, q)$ are schedules $e$ such that $|e|_0 = p$ and $|e|_1 = q$.


A schedule $e: p \rightarrow q$ corresponds to obvious order preserving (collectively surjective) embeddings $l:(p) \rightarrow (p+q)$
and $r : (q) \rightarrow (p+q)$ and thus to order relations
$l(x)

-
The identity in $\Upsilon(p, p)$ is the copy-cat function $c$ of length $2p$, such that $c(2k+1) \neq c(2k+2)$. The induced orders are
$\leq$ on $(p)^+$ and on $(p)^-$

-
Let $e:p \rightarrow q$ and $f: q \rightarrow r$ be morphisms in $\Upsilon$, then their composition $e;f:p \rightarrow r$ is defined by
taking the corresponding order relations , composing them as relations
and reconstructing the function


Where I emphasized in bold the parts I don't understand. In particular:

-
What's the meaning of embedding when he defined morphisms? I know what an embedding functor is, but this definition doesn't apply here.

-
What does "$l(x)

-
What's an induced order?

-
What does reconstructing a function mean?

I hope my questi

Solution

I remember finding this bit very elliptic too. To me, this is clearly research-level, but anyway...

One point that you seem to have missed is that a schedule is defined as a map $e \colon \{1,\ldots,n\} \to \{0,1\}$ satisfying $e(1) = 1$ and $e(2k+1) = e(2k)$.

The intuition behind this is that we're considering views, in the game semantical sense. That is, we have an arrow arena, say $A \to B$, and two opponents, one on the left, say $L$, one on the right, say $R$, and the arrow arena lets us play against both of them at the same time. Only, $A$ and $B$ are polarised' games, i.e., players should take turns and the starting player is specified, and $R$ is to start in $B$, whereas we are to start in $A$. Finally, we are only allowed to change side when its our turn on both sides (this is called the switching condition) and the first move of all is to be played by $R$.

Schedules model
shapes of plays' in such a setting. E.g., $0$'s and $1$'s stand for moves in $L$ and $R$, respectively. Hence, $e(1) = 1$ says that $R$ is to play first. Furthermore, $e(2k+1) = e(2k)$ says that all oour moves are immediately answered by the corresponding opponent.

Any schedule $p \to q$ is equivalently specified by the first point in $q$ after which we have played in $p$, then the first point after that in which we switched again to $q$, etc. The first relates an odd index in $q$ to an odd index in $p$, the second relates an even index in $p$ to an even one in $q$, etc, hence defining relations $R \colon (p)^+ \not\to (q)^+$ and $L \colon (q)^- \not\to (p)^-$.

Any such pair of relations comes from a schedule iff the union of $R$, $L$, and the underlying orders of $p$ and $q$ generates a total ordering on $p+q$. I haven't done the exercise of proving that such pairs $(R,L)$ are stable under composition...

Anyway, a graphical intuition is that instead of drawing schedules as (vertical) lists of $0$'s and $1$'s, you may draw any of them as two vertical lists of dots side by side ($0$'s to the left, $1$'s to the right!), plus arrows indicating when to switch from right to left and back.

The meaning of `induced orders' are the obtained relations $R$ and $L$. So for copycat, they are relations $p^+ \not\to p^+$ and $p^- \not\to p^-$.

A doubt remains, to me at least, about their definition of copycat. I'd have said copycat induces the discrete order on both $(p)^+$ and $(p)^-$. Am I missing anything?

Context

StackExchange Computer Science Q#14986, answer score: 2

Revisions (0)

No revisions yet.