L3-internship-report/slides/slides.tex

% 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{math}
\usepackage{tikz}

\usetikzlibrary{positioning}

\setbeamertemplate{navigation symbols}{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author[Théophile \textsc{Bastian}]{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}
%\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}

\end{document}