tobast/L3-internship-report
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Compare commits

base: tobast:testing
Branches Tags
tobast:master
tobast:testing
..
compare: tobast:master
Branches Tags
tobast:testing
tobast:master

No commits in common. "testing" and "master" have entirely different histories.
testing ... master

13 changed files with 97 additions and 739 deletions
Show stats Expand all files Collapse all files

0
README.md → report/README.md
View file

4
report/biblio.bib
View file

@ -34,7 +34,7 @@
}
@article{abramsky2000pcf,
title={{Full abstraction for PCF}},
title={Full abstraction for PCF},
author={Abramsky, Samson and Jagadeesan, Radha and Malacaria, Pasquale},
journal={Information and Computation},
volume={163},
@ -82,7 +82,7 @@
}
@article{laird2001game,
title={{A game semantics of Idealized CSP}},
title={A game semantics of Idealized CSP},
author={Laird, James},
journal={Electronic Notes in Theoretical Computer Science},
volume={45},

5
report/my_hyperref.sty
View file

@ -1,8 +1,7 @@
\usepackage{hyperref}
\usepackage{xcolor}
\usepackage[dvipsnames]{xcolor}
\definecolor{link_blue}{RGB}{0,0,97}
\definecolor{cite_green}{HTML}{009B55}
\hypersetup{
% bookmarks=true, % show bookmarks bar?
@ -20,7 +19,7 @@
% pdfnewwindow=true, % links in new PDF window
colorlinks=true, % false: boxed links; true: colored links
linkcolor=link_blue, % color of internal links (change box color with linkbordercolor)
citecolor=cite_green, % color of links to bibliography
citecolor=ForestGreen, % color of links to bibliography
filecolor=magenta, % color of file links
urlcolor=link_blue % color of external links
}

191
report/report.tex
View file

@ -83,13 +83,14 @@ the two strategies.
\paragraph{Concurrency in game semantics.} In the continuity of the efforts put
forward to model imperative primitives in game semantics, it was natural to
focus at some point on modelling concurrency. The problem was first tackled by
focus at some point on modelling concurrency. The problem was tackled by
\fname{Laird}~\cite{laird2001game}, introducing game semantics for a \lcalc{}
with a few additions, as well as a \emph{parallel execution} operator and
communication on channels. \fname{Ghica} and \fname{Murawski} then simplified
\textsc{Laird}'s approach, and gave a fully abstract model for a slightly more
realistic concurrent programming language with shared memory
in~\cite{ghica2004angelic}.
communication on channels. It is often considered, though, that \fname{Ghica}
and \fname{Murawski}~\cite{ghica2004angelic} really took the fundamental step
by defining game semantics for a fine-grained concurrent language including
parallel execution of ``threads'' and low-level semaphores --- a way more
realistic approach to the problem.
However, both of these constructions are based on \emph{interleavings}. That
is, they model programs on \emph{tree-like games}, games in which the moves
@ -104,15 +105,15 @@ combination of moves is a valid path.
However, this approach introduces non-determinism in the strategies: if two
moves are available to a player, the model states that they make a
non-deterministic uniform choice. Yet, even for concurrent programs it is
often a desirable property that they should behave consistently with the
environment, meaning that they are deterministic up to the choice of the
scheduler. Such determinism can be ensured statically, via typing. This idea
was explored outside of the game semantics context, for instance
by~\cite{reynolds1978syntactic}, establishing a type-checking system to
restrict concurrent programs to deterministic ones. Some recent work makes use
of linear logic~\cite{caires2010session} for similar purposes as well. Yet,
the interleavings game semantics of these languages remains non-deterministic.
non-deterministic uniform choice. Yet, one could reasonably argue that a
program should behave consistently with the environment, which would mean that
the semantics of a program --- even a concurrent one --- should still be
deterministic. This idea was explored outside of the game semantics context,
for instance by~\cite{reynolds1978syntactic}, establishing a type-checking
system to restrict concurrent programs to deterministic ones. Some recent work
makes use of linear logic~\cite{caires2010session} for similar purposes as
well. Yet, the interleavings game semantics of these languages remains
non-deterministic.
\paragraph{The purpose of this internship} was to try to take a first step
towards the reunification of those two developments. For that purpose, my
@ -141,7 +142,7 @@ synchronization of processes through \emph{channels} ---, lifted up to the
higher order through a \lcalc. The language was then restricted to a
\emph{linear} one --- that is, each identifier declared must be referred to
exactly once ---, partly to keep the model simple, partly to meet the
determinism requirements through the banning of interference.
determinism requirements.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{A linear variant of CCS~: \linccs}
@ -230,7 +231,7 @@ where $a$ denotes a channel and $x$ denotes any possible label.
\frac{P \redarrow{x} P'}
{P \cdot Q \redarrow{x} P' \cdot Q} & &
\frac{P \redarrow{x} P'}
{(\nu a)P \redarrow{x} (\nu a)P'} & (x \not\in \set{a,\tau_a})
{(\nu a)P \redarrow{x} (\nu a)P'} & (a \not\in \set{x,\tau_a})
\end{align*}
\caption{\linccs{} operational semantics}\label{fig:lccs:opsem}
\end{figure}
@ -244,7 +245,11 @@ necessary. Consider the reduction of $(\nu a) (a \cdot 1 \parallel \bar{a}
to reduce to $1$; but if we replaced that $\tau_a$ with a $\tau$, the whole
term would reduce to $(\nu a) 1$, which has no valid type since $a$ and
$\bar{a}$ are not consumed (linearity). Our semantics would then not satisfy
subject reduction for $\tau$-reductions.
subject reduction.
Switching to an \emph{affine} \linccs{} while keeping it wrapped in a
\emph{linear} \lcalc{} was considered, but yielded way too many problems, while
switching to a fully-affine model would have modified the problem too deeply.
\subsection{Lifting to the higher order: linear \lcalc}
@ -252,7 +257,7 @@ In order to reach the studied language, \llccs, we have to lift up \linccs{} to
a \lcalc. To do so, we add to the language the constructions of
figure~\ref{fig:llam:syntax}, which are basically the usual \lcalc{}
constructions slightly transformed to be linear (which is mostly reflected by
the typing rules).
the typing rules). In particular, the only base types are $\proc$ and $\chan$.
\begin{figure}[h]
\begin{minipage}[t]{0.55\textwidth}
@ -333,17 +338,15 @@ To lift the operational semantics to \llccs, we only need to add one rule:
\left(\left(\left(\bar{f} \cdot 1\right) \cdot
\left(\bar{g} \cdot 1\right)\right) \parallel \left(g \cdot 1\right)
\right)\right)$. Note that the function has no idea whether two
channels are dual or not, that is, its declaration ignores duality
relations between its parameters. In practice, it means that no
synchronization can happen before the term is $\beta$-reduced.
channels are dual or not.
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{A games model}
Our goal is now to give a deterministic games model for the above language. For
that purpose, we will use \emph{event structures}, providing an alternative
formalism to the often-used tree-like games.
Our goal is now to give a games model for the above language. For that purpose,
we will use \emph{event structures}, providing an alternative formalism to
the often-used tree-like games.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{The event structures framework}
@ -368,9 +371,9 @@ corresponds to the game tree
\]
This can of course be used to describe much larger games, and is often useful
to reason concurrently. The different configurations of the game that can be
reached are quite easily read: one only has to concatenate the events found
along path starting at the root of the tree.
to reason concurrently, since the causal histories appears clearly: the
possible states of the game can be read easily by concatenating the events
found along a path from the root of the tree.
But it also has the major drawback of growing exponentially in size: let us
consider a game in which Opponent must play $A$ and $B$ in no particular order
@ -392,14 +395,10 @@ before Player can play $C$. The corresponding tree-like game would be
\end{tikzpicture}
\]
This goes even worse with less structure: since there are $n!$ % chktex 40
This goes even worse with less structure: since there is $n!$ % chktex 40
permutations for $n$ elements, the tree can grow way larger.
The previous example also points out a kind of \textit{obfuscation} of the
causal histories: reading the diagram above does not make it obvious to the
reader that $A$ and $B$ must be played before $C$.
This problem can be solved by using \emph{event structures} as a formalism to
This problem motivated the use of \emph{event structures} as a formalism to
describe such games~\cite{rideau2011concurrent}. Informally, an event structure
is a partial order $\leq$ on \emph{events} (here, the game's moves), alongside
with a \emph{consistency} relation.
@ -434,9 +433,7 @@ look like
\leq_E e}$ is finite.
The partial order $\leq_E$ naturally induces a binary relation $\edgeArrow$
over $E$ that is defined as the transitive reduction of $\leq_E$, \ie{} the
minimal subset of $\leq_E$ such that the transitive closures of $\leq_E$
and $\edgeArrow$ are the same.
over $E$ that is defined as the transitive reduction of $\leq_E$.
\end{definition}
In this context, the right intuition of event structures is a set of events
@ -445,7 +442,7 @@ a given move cannot occur before another move.
Event structures are often represented as a directed acyclic graph (DAG)
where the vertices are the elements of $E$ and the edges are the transitive
reduction of $\leq_E$ (\ie{} $\edgeArrow_E$).
reduction of $\leq_E$.
\begin{definition}[event structure with polarities]
An \emph{event structure with polarities} (\textit{ESP}) is an event
@ -488,9 +485,8 @@ strategies.
\begin{notation}
For $x,y \in \config(A)$, $x \forkover{e} y$ states that $y =
x \sqcup \set{e}$ (and that both are valid configurations), where $\sqcup$
is used to mean that the standard union ($\cup$) is disjoint. It is also
possible to write $x \forkover{e}$, stating that $x \sqcup \set{e} \in
\config(A)$, or $x \fork y$.
denotes the disjoint union. It is also possible to write $x \forkover{e}$,
stating that $x \sqcup \set{e} \in \config(A)$, or $x \fork y$.
\end{notation}
%%%%%
@ -538,7 +534,7 @@ drink.
\]
The ``call'' event will be triggered by Opponent (the system) when the
process is started, and Player will play ``done'' when the process has
finished, if it ever does. The relation $\texttt{call} \leq \texttt{done}$
finished, if it ever does. The relation $\text{call} \leq \text{done}$
means that a process cannot finish \emph{before} it is called: unlike what
happened in the previous example, it is here a ``hardwired'' relation that
the software cannot bypass.
@ -548,8 +544,7 @@ drink.
A \emph{pre-strategy} on the game $A$, written $\sigma: A$, is an ESP such
that
\begin{enumerate}[(i)]
\item $\sigma \subseteq A$ (inclusion over set of events, not including
the order);
\item $\sigma \subseteq A$;
\item $\config(\sigma) \subseteq \config(A)$;
\item $\forall s \in \sigma, \rho_A(s) = \rho_\sigma(s)$
\end{enumerate}
@ -605,26 +600,23 @@ int main() {
But as it is defined, a pre-strategy does not exactly capture what we expect of
a \emph{strategy}: it is too expressive. For instance, the relation
$\text{call}_0 \leq \text{call}_1$ on a variant of the above strategy would be
allowed, stating that the operating system cannot decide to start the process
$1$ before the process $0$. It is not up to the program to decide that, this
strategy is thus unrealistic. We then have to restrict pre-strategies to
\emph{strategies}:
$\text{call}_0 \leq \text{call}_1$ on the above strategy is allowed, stating
that the operating system cannot decide to start the process $1$ before the
process $0$. It is not up to the program to decide that, this strategy is thus
unrealistic. We then have to restrict pre-strategies to \emph{strategies}:
\begin{definition}[strategy]
A \emph{strategy} is a pre-strategy $\sigma : A$ that
``behaves well'', \ie{} that is
\begin{enumerate}[(i)]
\item\label{def:receptive}
\textit{receptive}: $\forall x \in \config(\sigma), x \sqcup
\set{e} \in \config(A) \land \rho(e) = \ominus \implies x \sqcup
\set{e} \in \config(\sigma)$
\textit{receptive}: for all $x \in \config(A)$ \st{}
$x \forkover{e^-}$, $e \in \sigma$;
\item\label{def:courteous}
\textit{courteous}: $\forall e \edgeArrow_\sigma e' \in \sigma$,
$(\rho(e),\rho(e')) \neq (-,+) \implies
e \edgeArrow_A e'$.
\textit{courteous}: $\forall x \edgeArrow_\sigma x' \in \sigma$,
$(\rho(x),\rho(x')) \neq (-,+) \implies
x \edgeArrow_A x'$.
\end{enumerate}
\end{definition}
@ -642,8 +634,8 @@ to consider an arrow ${\ostar \edgeArrow \ominus}$, which would mean forcing
Opponent to wait for a move (either from Player or Opponent) before playing
their move; but ${\oplus \edgeArrow \oplus}$ is also unreasonable, since we're
working in a concurrent context. Intuitively, one could think that when playing
$e$ then $e'$, it is undefined whether Opponent will receive $e$ then $e'$ or
$e'$ then $e$.
$x$ then $y$, it is undefined whether Opponent will receive $x$ then $y$ or $y$
then $x$.
%%%%%
\subsubsection{Operations on games and strategies}\label{sssec:es_operations}
@ -688,7 +680,7 @@ one strategy plays against the other''.
${(\leq_\sigma \cup \leq_\tau)}^\ast$ (transitive closure) that may not
respect antisymmetry, that is, may have causal loops. The event structure
$\sigma \wedge \tau$ is then obtained by removing all the elements
contained in such loops from $\sigma \cap \tau$, yielding a partial order.
contained in such loops from $\sigma \cap \tau$, yielding a regular order.
\end{definition}
\textit{This construction is a simplified version of the analogous one
@ -715,8 +707,8 @@ f$).
\begin{definition}[compositional interaction]
Given two strategies $\sigma : A^\perp \parallel B$ and $\tau : B^\perp
\parallel C$, their \emph{compositional interaction} $\tau \strInteract
\sigma$ is an event structure defined as $(\sigma \parallel C^\perp) \wedge
(A \parallel \tau)$, where $A$ and $C^\perp$ are seen as strategies.
\sigma$ is an event structure defined as $(\sigma \parallel C) \wedge
(A^\perp \parallel \tau)$, where $A^\perp$ and $C$ are seen as strategies.
\end{definition}
The idea is to put in correspondence the ``middle'' states (those of $B$) while
@ -754,8 +746,7 @@ the other player from each board on the other.
The copycat strategy of a game is indeed an identity for the composition of
\emph{strategies}. In fact, it even holds that for a \emph{pre-}strategy
$\sigma : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma =
\sigma$~\cite{rideau2011concurrent}.
$\sigma : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma = \sigma$.
\begin{example}[copycat]
If we consider the following game $A$
@ -817,7 +808,8 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
\node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge [bend right] (2)
(0) edge (1)
edge [bend right] (2)
edge [bend right] (4)
(2) edge (3)
(4) edge (5)
@ -840,7 +832,8 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
\node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge [bend right] (4)
(0) edge (1)
edge [bend right] (4)
(2) edge (3)
(4) edge (5)
(3) edge [bend right] (1)
@ -862,7 +855,8 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
\node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge [bend right] (2)
(0) edge (1)
edge [bend right] (2)
(2) edge (3)
(4) edge (5)
(3) edge (4)
@ -884,7 +878,8 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
\node (0) at (7.5,0.65) [draw=red,ellipse] {call};
\node (1) at (7.5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge [bend right] (2)
(0) edge (1)
edge [bend right] (2)
(2) edge (3)
(3) edge [bend right] (1)
(4) edge (5)
@ -897,21 +892,10 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
\caption{\llccs{} interpretation as strategies}\label{fig:llccs:interp}
\end{figure}
In the representation above, the drawn strategies are organized in columns: for
instance, the strategy involved in $\seman{P \parallel Q}$ has type $P^\perp
\parallel P^\perp \parallel P$. Each column of events stands for one of those
games, in this order.
The $\seman{-}$ operator always sends a term $x_1 : A_1, \ldots, x_p : A_p
\vdash t : B$ to a strategy $\seman{t} : \seman{A_1}^\perp \parallel \ldots
\parallel \seman{A_p}^\perp \parallel \seman{B}$. For brevity purposes, the
associativity and commutativity steps ---~up to isomorphism~--- will be kept
implicit here, although those are handled very formally in the implementation.
A lot of these interpretations is what was expected: $\proc$ has the same
interpretation as presented before, and that of $\chan$ is set to the same, $1$
is interpreted as the game playing \textit{done} while $0$ does not, the arrow
is the type introduced for functions.
A lot of these interpretations is what was expected: $\proc$ and $\chan$ have
the same interpretation as presented before, $1$ is interpreted as the game
playing \textit{done} while $0$ does not, the arrow is the type introduced for
functions.
A variable is represented by a \emph{copycat} of its type, to keep a version of
the variable in the environment, reflecting the judgement $x:A \vdash x:A$.
@ -924,15 +908,21 @@ copycat wires up perfectly $\seman{t} \parallel \seman{u}$: the version of $x$
from the environment of $t$ is connected to $u$, and the output of $t$ is
connected to the output of the term.
In the representation above, the drawn strategies are organized in columns: for
instance, the strategy involved in $\seman{P \parallel Q}$ has type $P^\perp
\parallel P^\perp \parallel P$. Each column of events stands for one of those
games, in this order.
%%%%%%%%%%%%%%%%%%%%%
\subsection{Adequacy}
We will now describe the main steps of the proof of the major result of this
study, the \emph{adequacy} of the game semantics.
We will now prove the major result of this study, the \emph{adequacy} of the
game semantics.
\begin{theorem}[adequacy]
The previous interpretation is \emph{adequate} with respect to the
operational semantics, that is
The previous interpretation is \emph{adequate} with the operational
semantics, that is
\[ \forall P \textit{ st. } \left(\vdash P : \proc\right),~
\left(P \Downarrow\right) \iff \left(\seman{P} = \seman{1}\right) \]
\end{theorem}
@ -956,10 +946,6 @@ required.
\item $\forall a : \chan,~a \in l \implies \bar{a} \not\in l$.
\end{enumerate}
where $\freevars(P)$ denotes the set of free variables of $P$, defined as
usual by induction over the syntax as the set of variables unbound in the
term.
\end{definition}
\begin{lemma}
@ -1024,10 +1010,7 @@ The theorem is mostly a consequence of the following lemma:
We prove its contrapositive judgement, $P \neq 1\,\&\,\seman{P} =
\seman{1} \implies \exists Q\,:\,P \redarrow{\tau} Q$ by induction over the
syntax of \linccs{} (\wlogen, we can assume that $P
\not\longrightarrow_\beta$, because we can always do every
$\beta$-reduction before any other $\tau$-reduction, and because the
$\beta$-reduced term corresponding to a counter-example is a
counter-example as well; thus the terms are in \linccs): for each
\not\longrightarrow_\beta$, thus the terms are in \linccs): for each
syntactic construction, we prove that under the induction hypotheses, there
is such a $Q$.
\end{proof}
@ -1040,13 +1023,10 @@ can compute its associated strategy and check whether it is $\seman{1}$.
\section{Implementation of deterministic concurrent games}
\hfill\href{https://tobast.fr/l3/demo.html}
{\includegraphics[height=2em]{tryme32.png}~\raisebox{0.5em}{Try
online\footnotemark}}
\footnotetext{\url{{https://tobast.fr/l3/demo.html}}}
{\includegraphics[height=2em]{tryme32.png}~\raisebox{0.5em}{Try online}}
\qquad \href{https://github.com/tobast/cam-strategies/}
{\includegraphics[height=2em]{github32.png}~\raisebox{0.5em}{Github
repository\footnotemark}}
\footnotetext{\url{https://github.com/tobast/cam-strategies/}}
repository}}
\vspace{1em}
@ -1115,9 +1095,9 @@ literature.
I also explored the possibility to reach a full-abstraction result. The
full-abstraction property states that two terms are \emph{observationally
equivalent} if and only if their (denotational) semantics are also
observationally equivalent, that is, in this context, for all $P,Q$ two
\llccs{} terms such that $\Gamma \vdash P,Q : A$,
equivalent} if and only if their (denotational) semantics are equal, that is,
in this context,
for all $P,Q$ two \llccs{} terms such that $\Gamma \vdash P,Q : A$,
\[
\left[ \forall \calC[-] \text{ a context }\,:\,
@ -1125,14 +1105,7 @@ observationally equivalent, that is, in this context, for all $P,Q$ two
\calC[P] \Downarrow \iff \calC[Q] \Downarrow
\right]
\quad\iff\quad
\left( \seman{P} \simeq \seman{Q} \right)
\]
where $\simeq$ denotes the observational equivalence on strategies, that is,
\[
(\sigma : A) \simeq (\tau : A) \iff \forall (\alpha : A^\perp \parallel
\proc), \alpha \strComp \sigma = \alpha \strComp \tau
\left( \seman{P} = \seman{Q} \right)
\]
Yet, by lack of time, I had to abandon this path. Indeed, this would have

7
report/todo.sty
View file

@ -1,9 +1,6 @@
\usepackage{xcolor}
\definecolor{note_text}{HTML}{671800}
\definecolor{note_back}{HTML}{00A2E3}
\usepackage[dvipsnames]{xcolor}
\newcommand{\qtodo}[1]{\colorbox{orange}{\textcolor{blue}{#1}}}
\newcommand{\todo}[1]{\qtodo{\textbf{TODO:}\.#1}}
\newcommand{\qnote}[1]{\colorbox{note_back}{\textcolor{note_front}{[#1]}}}
\newcommand{\qnote}[1]{\colorbox{Cerulean}{\textcolor{Sepia}{[#1]}}}
\newcommand{\note}[1]{\qnote{\textbf{NOTE:}\.#1}}

4
slides/Makefile
View file

@ -1,10 +1,6 @@
TEX=slides.tex
BASE=slides
all: $(TEX)
pdflatex $(TEX)
pdflatex $(TEX)
upload: all
scp $(BASE).pdf www.tobast:~/tobast.fr/public_html/l3/slides.pdf

63
slides/concurgames.sty
View file

@ -1,63 +0,0 @@
%% By Théophile Bastian
%% Useful commands for concurrent games as event structures
\usepackage[normalem]{ulem}
\usepackage{MnSymbol}
\usepackage{stmaryrd}
\usepackage{tikz}
\usepackage{relsize}
\usetikzlibrary{shapes,arrows,positioning}
\newcommand{\fname}[1]{\textsc{#1}}
\newcommand{\con}{\operatorname{Con}}
\newcommand{\confl}{\raisebox{0.5em}{\uwave{\hspace{2em}}}}
\newcommand{\obseq}{\simeq_\text{obs}}
\newcommand{\cov}{{{\mathrel-\joinrel\subset}}}
\newcommand{\longcov}[1]{{\stackrel{#1}
{\mathrel-\joinrel\relbar\joinrel\subset\,}}}
\newcommand{\forkover}[1]{\longcov{#1}}
\newcommand{\fork}{\cov}
\newcommand{\edgeArrow}{\rightarrowtriangle}
\newcommand{\linarrow}{\rightspoon}
\newcommand{\redarrow}[1]{\overset{#1}{\longrightarrow}}
\newcommand{\config}{\mathscr{C}}
\newcommand{\downclose}[1]{\left[#1\right]}
\newcommand{\strComp}{\odot}
\newcommand{\strInteract}{\ostar}
\newcommand{\strParallel}{\parallel}
\newcommand{\seman}[1]{\llbracket{} #1 \rrbracket}
\newcommand{\tens}{\otimes}
\newcommand{\Tens}{\mathlarger\otimes}
% LCCS
\newcommand{\newch}[1]{\left(\nu #1\right)}
\newcommand{\linearmark}{$\mathcal{L}$}
\newcommand{\lcalc}{$\lambda$-calculus}
\newcommand{\lccs}{$\lambda$CCS}
\newcommand{\linccs}{{\linearmark}CCS}
\newcommand{\llccs}{$\lambda${\linearmark}CCS}
\newcommand{\proc}{\mathbb{P}}
\newcommand{\chan}{\mathbb{C}}
\newcommand{\validctx}{\mathcal{L}}
\newcommand{\freevars}{\operatorname{fv}}
% Copycat
\newcommand{\CC}{{\rm C\!\!\!C}}
\newcommand{\cc}{\mathrm{\,c\!\!\!\!c\,}}
\newcommand{\includedot}[2][]{%
\begin{tikzpicture}[>=latex,line join=bevel,#1]
\input{_build/dot/#2.tex}
\end{tikzpicture}}

80
slides/math.sty
View file

@ -1,80 +0,0 @@
\usepackage{stmaryrd}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{fancybox}
\usepackage{mathrsfs}
\usepackage{mathtools}
\newcommand{\eqdef}{{~\coloneqq~}}
\newcommand{\lAnd}{~\&~}
\newcommand{\overOr}[2]{\begin{array}{r l}
& #1 \\
\textit{or} & \\
& #2
\end{array}}
\newcommand{\id}{\operatorname{id}}
% Intervalle discret.
\newcommand{\discrIv}[1]{\llbracket #1 \rrbracket}
% ensembliste
\newcommand{\set}[1]{\left\{ #1 \right\}}
\newcommand{\card}[1]{\left\vert{} #1 \right\vert}
\newcommand{\abs}[1]{\left\vert{} #1 \right\vert}
\newcommand{\interior}[1]{\left({#1}\right)^\circ}
\newcommand{\floor}[1]{\left\lfloor{} #1 \right\rfloor}
\newcommand{\ceil}[1]{\left\lceil{} #1 \right\rceil}
% Abréviations courrantes
\newcommand{\ie}{\textit{ie.}}
\newcommand{\eg}{\textit{eg.}}
\newcommand{\Eg}{\textit{Eg.}}
\newcommand{\wrt}{\textit{wrt.}}
\newcommand{\wlogen}{\textit{wlog.}}
\newcommand{\st}{\textit{st.}}
% Notations à polices étranges
\newcommand{\domain}{\mathcal{D}}
\newcommand{\bigO}{\mathcal{O}}
\newcommand{\calA}{\mathcal{A}}
\newcommand{\calC}{\mathcal{C}}
\newcommand{\calG}{\mathcal{G}}
\newcommand{\calV}{\mathcal{V}}
\newcommand{\calT}{\mathcal{T}}
\newcommand{\calP}{\mathcal{P}}
% Ensembles
\newcommand{\realset}{\mathbb{R}}
\newcommand{\natset}{\mathbb{N}}
\newcommand{\relset}{\mathbb{Z}}
% Probas
\newcommand{\prob}{\mathbb{P}}
\newcommand{\probP}[1]{\mathbb{P}\left(#1\right)}
\newcommand{\expec}{\mathbb{E}}
\newcommand{\expecP}[1]{\mathbb{E}\left[#1\right]}
\newcommand{\variance}{\mathbb{V}}
\newcommand{\ber}{\mathcal{B}er}
\newcommand{\bin}{\mathcal{B}in}
\newcommand{\poi}{\mathcal{P}oi}
% Suppression des points
\newcommand{\ibar}{\overline{\imath}}
\newcommand{\jbar}{\overline{\jmath}}
% Fonctions
%\newcommand{\functiondef}[4]{\left\lbrace \begin{tabular}{r l} #1 & \rightarrow #2 \\ #3 & \mapsto #4\end{tabular} \right.}
\newcommand{\functiondef}[4]{\begin{cases}
#1 & \to #2 \\
#3 & \mapsto #4
\end{cases}}
% Preuve par équivalence - puces
\newcommand{\impliesbullet}{\ovalbox{$\implies$}}
\newcommand{\impliedbybullet}{\ovalbox{$\impliedby$}}

26
slides/my_hyperref.sty
View file

@ -1,26 +0,0 @@
\usepackage{hyperref}
\usepackage{xcolor}
\definecolor{link_blue}{RGB}{0,0,97}
\definecolor{cite_green}{HTML}{009B55}
\hypersetup{
% bookmarks=true, % show bookmarks bar?
% unicode=false, % non-Latin characters in Acrobat’s bookmarks
% pdftoolbar=true, % show Acrobat’s toolbar?
% pdfmenubar=true, % show Acrobat’s menu?
% pdffitwindow=false, % window fit to page when opened
% pdfstartview={FitH}, % fits the width of the page to the window
% pdftitle={My title}, % title
% pdfauthor={Author}, % author
% pdfsubject={Subject}, % subject of the document
% pdfcreator={Creator}, % creator of the document
% pdfproducer={Producer}, % producer of the document
% pdfkeywords={keyword1} {key2} {key3}, % list of keywords
% pdfnewwindow=true, % links in new PDF window
colorlinks=true, % false: boxed links; true: colored links
linkcolor=link_blue, % color of internal links (change box color with linkbordercolor)
citecolor=cite_green, % color of links to bibliography
filecolor=magenta, % color of file links
urlcolor=link_blue % color of external links
}

63
slides/my_listings.sty
View file

@ -1,63 +0,0 @@
\usepackage{listings}
\usepackage{algorithmicx}
\usepackage{algpseudocode}
\usepackage{color}
\usepackage{xcolor}
\usepackage{courier}
\definecolor{color_comment}{HTML}{2D6F19}
\definecolor{color_linenum}{HTML}{9E9E9E}
\definecolor{color_strings}{HTML}{D300F3}
\lstset{ %
% backgroundcolor=\color{white}, % choose the background color; you must add \usepackage{color} or \usepackage{xcolor}
basicstyle=\footnotesize\ttfamily, % the size of the fonts that are used for the code
breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace
breaklines=true, % sets automatic line breaking
captionpos=b, % sets the caption-position to bottom
commentstyle=\color{color_comment}, % comment style
% deletekeywords={...}, % if you want to delete keywords from the given language
% escapeinside={\%*}{*)}, % if you want to add LaTeX within your code
extendedchars=true, % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8
frame=none, % adds a frame around the code
keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
keywordstyle=\color{blue}, % keyword style
morekeywords={*,...}, % if you want to add more keywords to the set
numbers=left, % where to put the line-numbers; possible values are (none, left, right)
numbersep=5pt, % how far the line-numbers are from the code
numberstyle=\tiny\color{color_linenum}, % the style that is used for the line-numbers
rulecolor=\color{black}, % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here))
showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
showstringspaces=false, % underline spaces within strings only
showtabs=false, % show tabs within strings adding particular underscores
stepnumber=1, % the step between two line-numbers. If it's 1, each line will be numbered
stringstyle=\color{color_strings}, % string literal style
tabsize=4, % sets default tabsize to 2 spaces
% title=\lstname, % show the filename of files included with \lstinputlisting; also try caption instead of title
% inputencoding=utf8/latin1 % To accept utf8 encoding
}
\lstset{literate=
{á}{{\'a}}1 {é}{{\'e}}1 {í}{{\'i}}1 {ó}{{\'o}}1 {ú}{{\'u}}1
{Á}{{\'A}}1 {É}{{\'E}}1 {Í}{{\'I}}1 {Ó}{{\'O}}1 {Ú}{{\'U}}1
{à}{{\`a}}1 {è}{{\`e}}1 {ì}{{\`i}}1 {ò}{{\`o}}1 {ù}{{\`u}}1
{À}{{\`A}}1 {È}{{\'E}}1 {Ì}{{\`I}}1 {Ò}{{\`O}}1 {Ù}{{\`U}}1
{ä}{{\"a}}1 {ë}{{\"e}}1 {ï}{{\"i}}1 {ö}{{\"o}}1 {ü}{{\"u}}1
{Ä}{{\"A}}1 {Ë}{{\"E}}1 {Ï}{{\"I}}1 {Ö}{{\"O}}1 {Ü}{{\"U}}1
{â}{{\^a}}1 {ê}{{\^e}}1 {î}{{\^i}}1 {ô}{{\^o}}1 {û}{{\^u}}1
{Â}{{\^A}}1 {Ê}{{\^E}}1 {Î}{{\^I}}1 {Ô}{{\^O}}1 {Û}{{\^U}}1
{œ}{{\oe}}1 {Œ}{{\OE}}1 {æ}{{\ae}}1 {Æ}{{\AE}}1 {ß}{{\ss}}1
{ű}{{\H{u}}}1 {Ű}{{\H{U}}}1 {ő}{{\H{o}}}1 {Ő}{{\H{O}}}1
{ç}{{\c c}}1 {Ç}{{\c C}}1 {ø}{{\o}}1 {å}{{\r a}}1 {Å}{{\r A}}1
{€}{{\EUR}}1 {£}{{\pounds}}1 {¬}{{$\lnot$}}1 {∞}{{$\infty$}}1
}
\newcommand{\true}{\lstinline$true$}
\newcommand{\false}{\lstinline$false$}
\newcommand{\lstbash}[1]{\lstinline[language=bash]$#1$}
\newcommand{\lstocaml}[1]{\lstinline[language=Caml]$#1$}
\newcommand{\lstcpp}[1]{\lstinline[language=C++]$#1$}
\newcommand{\lstc}[1]{\lstinline[language=C]$#1$}
\newcommand{\lstpython}[1]{\lstinline[language=python]$#1$}

379
slides/slides.tex
View file

@ -1,397 +1,36 @@
% vim: :spell spelllang=fr
\documentclass[11pt]{beamer}
\usetheme{Warsaw}
%\usecolortheme{wolverine}
\usepackage[utf8]{inputenc}
\usepackage[french]{babel}
\usepackage[T1]{fontenc}
%\usepackage{my_hyperref}
\usepackage{my_listings}
\usepackage{libertine}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{concurgames}
\usepackage{theorems}
\usepackage{todo}
\usepackage{my_listings}
\usepackage{my_hyperref}
\usepackage{math}
\usepackage{tikz}
\usetikzlibrary{positioning}
\setbeamertemplate{navigation symbols}{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author[Théophile \textsc{Bastian}]{Théophile \textsc{Bastian}\\
\author{Théophile \textsc{Bastian}\\
\small{Sous la supervision de Glynn \textsc{Winskel} et Pierre
\textsc{Clairambault}}}
\title{Soutenance de stage}
%\subtitle{Structures d'événements dans la sémantique des jeux}
\subtitle{Sémantique déterministe de langage concurrentiel en sémantique des
jeux}
\date{Juin\,--\,juillet 2016}
\title{Soutenance de stage\\
Structures d'événements dans la sémantique des jeux}
\date{Juin\,--\,Juillet 2016}
%\logo{}
\institute{Computer Laboratory --- Cambridge, UK}
\begin{document}
\begin{frame}
\titlepage{}
% \tableofcontents
\end{frame}
\begin{frame}
\tableofcontents
\end{frame}
\section{Langage étudié}
\begin{frame}{\llccs~: syntaxe}
\begin{columns}[t]
\column{0.5\textwidth}
\begin{center}Termes\end{center}\vspace{-1em}
\begin{align*}
t,u,\ldots ::=~&1 & \text{(succès)}\\
\vert~&0 & \text{(erreur)}\\
\vert~&t \parallel u & \text{(parallèle)}\\
\vert~&t \cdot u & \text{(séquentiel)}\\
\vert~&(\nu a) t & \text{(nouveau canal)} \\
& & \\
\vert~&x \in \mathbb{V} & \text{(variable)} \\
\vert~&t\,u & \text{(application)}\\
\vert~&\lambda x^A \cdot t & \text{(abstraction)}\\
\end{align*}
\column{0.5\textwidth}
\begin{center}Types\end{center}\vspace{-1em}
\begin{align*}
A,B,\ldots ::=~&\proc & \text{(processus)} \\
\vert~&\chan & \text{(canal)} \\
\vert~&A \linarrow B & \text{(flèche linéaire)}
\end{align*}
\end{columns}
\end{frame}
\begin{frame}{\llccs~: règles de typage}
\begin{align*}
\frac{~}{\,\vdash 0:\proc} & (\textit{Ax}_0) &
\frac{~}{\,\vdash 1:\proc} & (\textit{Ax}_1) &
\alert{\frac{~}{t:A \vdash t:A}} & \alert{(\textit{Ax})} &
\end{align*}\vspace{-1em}\begin{align*}
\frac{\Gamma \vdash P : \proc \quad \Delta \vdash Q : \proc}
{\Gamma,\Delta \vdash P \cdot Q : \proc}
& (\cdot_\proc) &
\frac{\Gamma \vdash P : \proc}
{\Gamma,a:\chan \vdash a \cdot P: \proc}
& (\cdot_\chan)
\end{align*} \vspace{-1em} \begin{align*}
\alert{\frac{\Gamma \vdash P : \proc \quad \Delta \vdash Q : \proc}
{\Gamma,\Delta \vdash P \parallel Q : \proc}}
& \alert{(\parallel)} &
\frac{\Gamma, a:\chan, \bar{a}:\chan \vdash P : \proc}
{\Gamma \vdash (\nu a) P : \proc}
& (\nu)
\end{align*}
\begin{align*}
\frac{~}{x : A \vdash x : A} & (\textit{Ax}) &
\frac{\Gamma \vdash t : A \linarrow B \quad \Delta \vdash u : A}
{\Gamma,\Delta \vdash t~u : B} & (\textit{App}) &
\end{align*} \vspace{-1em} \begin{align*}
\frac{\Gamma, x : A \vdash t : B}
{\Gamma \vdash \lambda x^{A} \cdot t : A \linarrow B} & (Abs)
\end{align*}
\end{frame}
\begin{frame}{\llccs~: sémantique opérationnelle}
\begin{align*}
\frac{~}{a \cdot P \redarrow{a} P} & &
\frac{~}{1 \parallel P \redarrow{\tau} P} & &
\frac{~}{1 \cdot P \redarrow{\tau} P} & &
\end{align*}\begin{align*}
\frac{P \longrightarrow_\beta Q}
{P \redarrow{\tau} Q} & &
\frac{P \redarrow{\tau_c} Q}
{(\nu a) P \redarrow{\tau} Q} & (c \in \set{a,\bar{a}})&
\end{align*}\begin{align*}
\alert{\frac{P \redarrow{a} P'\quad Q \redarrow{\bar{a}} Q'}
{P \parallel Q \redarrow{\tau_a} P' \parallel Q'}} & &
\frac{P \redarrow{x} P'}
{(\nu a)P \redarrow{x} (\nu a)P'} & (x \not\in \set{a,\tau_a}) &
\end{align*}\begin{align*}
\frac{P \redarrow{x} P'}
{P \parallel Q \redarrow{x} P' \parallel Q} & &
\frac{Q \redarrow{x} Q'}
{P \parallel Q \redarrow{x} P \parallel Q'} & &
\frac{P \redarrow{x} P'}
{P \cdot Q \redarrow{x} P' \cdot Q} & &
\end{align*}
\end{frame}
\begin{frame}{Quelques exemples}
\begin{itemize}
\item $(1 \parallel 1) \cdot 1$~: succès
\pause%
\item $\newch{a} (a \cdot 1 \parallel \bar{a} \cdot 1)$
\pause%
\item $\newch{a} (a \cdot \bar{a} \cdot 1)$~: \textit{deadlock}
\pause%
\item $F := \lambda x^\chan \cdot \lambda y^\chan \cdot x \cdot y \cdot
1$
\pause%
\item $\newch{a} F\,a\,\bar{a}$~: \textit{deadlock}
\pause%
\item $\newch{a} \newch{b} (F\,a\,b \parallel \bar{a} \cdot \bar{b}
\cdot 1)$~: termine
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Structures d'événements}
\begin{frame}{Sémantique des jeux}
\begin{itemize}
\item Programme $\longrightarrow$ jeu à deux joueurs
\pause\vspace{1em}
\item \textit{Player}~: joue pour le programme
\item \textit{Opponent}~: joue pour l'environnement (OS, utilisateur,
\ldots)
\pause\vspace{1em}
\item \textit{Jeu}~: structure imposée (architecture physique, \ldots)
\item \textit{Stratégie}~: modélisation du programme
\end{itemize}
\end{frame}
\subsection{Sémantique par entrelacements}
\begin{frame}{Sémantique usuelle~: par entrelacements}
\begin{itemize}
\item Jeux en arbres\\
\begin{columns}
\column{0.5\textwidth}
\begin{center}\begin{tikzpicture}[node distance=0.5cm]
\node (1) {a};
\node (2) [below left=of 1] {b};
\node (3) [below right=of 1] {c};
\path [->]
(1) edge (2)
edge (3);
\end{tikzpicture}
\end{center}
\column{0.5\textwidth}
États du jeu~: $\varepsilon,~a,~a \cdot b,~a \cdot c$
\end{columns}
\pause%
\item \og{}Exécution parallèle~\fg{}:
\begin{columns}
\column{0.5\textwidth}
\begin{center}\begin{tikzpicture}[node distance=0.5cm]
\node (1) {a};
\node (2) [below left=of 1] {b};
\node (3) [below right=of 1] {c};
\node (5) [right=of 3] {e};
\node (4) [above right=of 5] {d};
\node (6) [below right=of 4] {f};
\path [->]
(1) edge (2)
edge (3)
(4) edge (5)
edge (6);
\end{tikzpicture}
\end{center}
\column{0.5\textwidth}
États du jeu~: $\varepsilon,~a,~d,~a \cdot b,~a \cdot d \cdot e
\cdot b, \ldots$
\end{columns}
\pause%
\item Comment représenter \og{}proprement~\fg{} le jeu suivant~?
\begin{center}\begin{tikzpicture}[node distance=0.5cm]
\node (3) {c};
\node (1) [above left=of 3] {a};
\node (2) [above right=of 3] {b};
\path [->]
(1) edge (3)
(2) edge (3);
\end{tikzpicture}
\end{center}
\end{itemize}
\end{frame}
\subsection{Structures d'événements}
\begin{frame}{Structures d'événements}
\begin{definition}{structure d'événement (déterministe)}
$(E, \leq_E)$ ensemble d'\emph{événements} partiellement ordonné.
\end{definition}
\pause%
\begin{definition}{structure d'événement polarisée (SEP) / \alert{jeu}}
$(E, \leq_E, \rho_E)$ où $(E, \leq_E)$ est une structure d'événements
et $\rho_E : E \to \set{\ominus, \oplus}$.
$E^\perp$~: SEP $E$ avec $\rho^\perp$.
\end{definition}
$\qquad\longrightarrow$ DAG
\pause%
\begin{definition}{configuration}
$x \subseteq E$ tel que $\forall e \in E, e' \in x, e \leq e' \implies
e \in x$.\\
$\config(E)$~: ensemble des configurations de $E$.\\
Pour $e \in E$, $[e]$ configuration induite par $e$.
\end{definition}
\end{frame}
\begin{frame}{Structures d'événements (suite)}
\begin{definition}{stratégie}
$\left(\sigma : A\right)$~: stratégie sur $A$ si $\sigma$ SEP
\textit{tq.}\\
\begin{itemize}
\item $\sigma \subseteq A$
\item $\config(\sigma) \subseteq \config(A)$
\item $\rho_\sigma = {\rho_A}_{\vert \sigma}$
\item $\cc_A \strComp \sigma = \sigma$ ($\cc_A$~:
\og{}identité~\fg)
\end{itemize}
\end{definition}
\end{frame}
\begin{frame}{Opérations sur structures d'événements}
\begin{definition}{parallèle}
$A \parallel B := \set{0} \times A \cup \set{1} \times B$~: mise
en parallèle de deux SE\@.
\end{definition}
\begin{definition}{interaction}
Pour $\sigma : A$, $\tau : A^\perp$, $\sigma \wedge \tau$~: $\sigma
\cap \tau$ où les boucles causales sont retirées.
\end{definition}
\begin{definition}{composition}
Pour $\sigma : A^\perp \parallel B$, $\tau : B^\perp \parallel C$,
\[ \tau \strComp \sigma := \left(\sigma \parallel C^\perp\right) \wedge
\left(A \parallel \tau\right) \]
\end{definition}
\begin{definition}{copycat}
$\cc_A : A^\perp \parallel A$~: $(A^\perp \parallel \emptyset) \cup
(\emptyset \parallel A)$, plus les $\ominus \rightarrow \oplus$ d'une
composante à l'autre.
\end{definition}
\end{frame}
\section{Interprétation de \llccs}
\subsection{Sémantique dénotationnelle}
\begin{frame}{Interprétation de \llccs}
\begin{columns}[c]
\column{0.5\textwidth}
\begin{align*}
\seman{\proc} &\eqdef \begin{tikzpicture}[baseline]
\node (1) at (0,0.5) [draw=red,ellipse] {call};
\node (2) at (0,-0.5) [draw=green,ellipse] {done};
\draw [->] (1) -- (2);
\end{tikzpicture}
= \seman{\chan} \\
%
\seman{1} &\eqdef \seman{P} \\
\seman{0} &\eqdef \begin{tikzpicture}[baseline]
\node (1) at (0,0.2) [draw=red,ellipse] {call};
\end{tikzpicture}
\end{align*}
\column{0.5\textwidth}
\begin{align*}
\seman{x^A} &\eqdef \cc_{\seman{A}} \\
\seman{A \linarrow B} &\eqdef \seman{A}^\perp \parallel \seman{B}\\
\seman{t^{A \linarrow B}~u^{A}} &\eqdef
\cc_{A \linarrow B} \strComp \left( \seman{t} \parallel
\seman{u} \right) \\
\seman{\lambda x^A \cdot t} &\eqdef \seman{t}
\end{align*}
\end{columns}
\vspace{1em}
\hrule{}
\vspace{0.5em}
\emph{Suit les règles de typage}~:
\[
u_1 : A_1, \ldots, u_p : A_p \vdash t : B \implies \seman{t} :
\seman{A_1}^\perp \parallel \ldots \parallel \seman{A_p}^\perp
\parallel \seman{B}
\]
\end{frame}
\subsection{Adequacy}
\begin{frame}{Adequacy}
\begin{theorem}{adequacy}
La sémantique dénotationnelle est \emph{adéquate} à la sémantique
opérationnelle, \ie{}
\[
\forall P\,/\,(\vdash P : \proc),~(P \redarrow{\tau}^\ast 1) \iff
(\seman{P} = \seman{1})
\]
\end{theorem}
\end{frame}
\begin{frame}{Adequacy, preuve}
\begin{itemize}
\item Sens direct~: induction sur $P \redarrow{\tau}^\ast 1$, en
utilisant une induction auxiliaire~: $\forall P \redarrow{x} Q,\,
\forall l \in \mathcal{L}_{P \redarrow{x} Q}$,
\begin{itemize}
\item si $x = \tau$, $\seman{P}_l = \seman{Q}_l$~;
\item si $x = a : \chan$, $\seman{P} = \seman{a \cdot Q}_l$~;
\item si $x = \tau_a$, $\seman{P}_{a::l} = \seman{Q}_l$~;
\end{itemize}
où $\seman{u}_{h::t} \eqdef \seman{\newch{h}u}_t$, $\seman{u}_{[]}
\eqdef \seman{u}$.
\pause\vspace{1em}
\item Sens réciproque~: on prouve par induction sur la syntaxe la
contraposée, $P \neq 1 \land \seman{P} = \seman{1} \implies P
\redarrow{\tau}$.
\end{itemize}
\end{frame}
\section{Implémentation}
\begin{frame}{Implémentation --- backend}
\begin{itemize}
\item Implémentation des opérations sur jeux/stratégies
\item Utilisable comme backend ou en toplevel
\item Représentation Dot de jeux/stratégies
\item Essentiellement OCaml
\item SLOCCount~: 2330 lignes
\item Nécessité de travailler très formellement (associativité, \ldots)
\end{itemize}
\end{frame}
\begin{frame}{Frontend \llccs}
\begin{itemize}
\item Parseur/lexeur \llccs{}
\item Transformation des termes en stratégies
\item Passage par le backend $\leadsto$ stratégie
\item Adequacy~: permet de décider si $P \redarrow{\tau}^\ast 1$
\item Frontend javascript~: entrée de stratégie et retour graphique sur
page web
\end{itemize}
\vfill
\hfill\url{https://tobast.fr/l3/demo.html}
\end{frame}
\section*{}
\begin{frame}{Conclusion}
\begin{center}\begin{Huge}Merci~!\end{Huge}\end{center}
\end{frame}
%\begin{frame}
%\tableofcontents
%\end{frame}
\end{document}

5
slides/theorems.sty
View file

@ -1,5 +0,0 @@
% vim: :spell spelllang=fr
\renewenvironment{definition}[1]{\begin{block}{Définition~: #1.}}{\end{block}}
\renewenvironment{theorem}[1]{\begin{alertblock}{Théorème~: #1.}}{\end{alertblock}}
\renewenvironment{lemma}[1]{\begin{block}{Lemme~: #1.}}{\end{block}}

9
slides/todo.sty
View file

@ -1,9 +0,0 @@
\usepackage{xcolor}
\definecolor{note_text}{HTML}{671800}
\definecolor{note_back}{HTML}{00A2E3}
\newcommand{\qtodo}[1]{\colorbox{orange}{\textcolor{blue}{#1}}}
\newcommand{\todo}[1]{\qtodo{\textbf{TODO:}\.#1}}
\newcommand{\qnote}[1]{\colorbox{note_back}{\textcolor{note_front}{[#1]}}}
\renewcommand{\note}[1]{\qnote{\textbf{NOTE:}\.#1}}