A lot of progress
This commit is contained in:
parent
01b36c6e48
commit
db0a4a5a29
|
|
@ -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}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue