% 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}