diff --git a/slides/slides.tex b/slides/slides.tex index b7dee97..c56860c 100644 --- a/slides/slides.tex +++ b/slides/slides.tex @@ -1,17 +1,25 @@ -% vim: :spell spelllang=fr_fr +% 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{my_listings} -\usepackage{my_hyperref} +\usepackage{concurgames} +\usepackage{theorems} +\usepackage{todo} \usepackage{math} +\usepackage{tikz} + +\usetikzlibrary{positioning} + \setbeamertemplate{navigation symbols}{} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -29,12 +37,274 @@ jeux} \begin{frame} \titlepage{} +% \tableofcontents +\end{frame} + +\begin{frame} \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} + +\begin{frame}{Interprétation de \llccs} + \begin{columns}[t] + \column{0.5\textwidth} + + \begin{align*} + \seman{\proc} &\eqdef + \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} +\end{frame} \end{document}