Compare commits
3 commits
f1cad075f1
...
db0a4a5a29
| Author | SHA1 | Date | |
|---|---|---|---|
 Théophile Bastian
|
db0a4a5a29 | ||
|
Théophile Bastian
|
01b36c6e48 | ||
|
Théophile Bastian
|
c4961d148d |
|
|
@ -1,7 +1,8 @@
|
|||
\usepackage{hyperref}
|
||||
\usepackage[dvipsnames]{xcolor}
|
||||
\usepackage{xcolor}
|
||||
|
||||
\definecolor{link_blue}{RGB}{0,0,97}
|
||||
\definecolor{cite_green}{HTML}{009B55}
|
||||
|
||||
\hypersetup{
|
||||
% bookmarks=true, % show bookmarks bar?
|
||||
|
|
@ -19,7 +20,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=ForestGreen, % color of links to bibliography
|
||||
citecolor=cite_green, % color of links to bibliography
|
||||
filecolor=magenta, % color of file links
|
||||
urlcolor=link_blue % color of external links
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,9 @@
|
|||
\usepackage[dvipsnames]{xcolor}
|
||||
\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{Cerulean}{\textcolor{Sepia}{[#1]}}}
|
||||
\newcommand{\qnote}[1]{\colorbox{note_back}{\textcolor{note_front}{[#1]}}}
|
||||
\newcommand{\note}[1]{\qnote{\textbf{NOTE:}\.#1}}
|
||||
|
|
|
|||
|
|
@ -1 +0,0 @@
|
|||
../biblio.bib
|
||||
|
|
@ -1 +0,0 @@
|
|||
../concurgames.sty
|
||||
63
slides/concurgames.sty
Normal file
63
slides/concurgames.sty
Normal file
|
|
@ -0,0 +1,63 @@
|
|||
%% 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}}
|
||||
|
|
@ -1 +0,0 @@
|
|||
../math.sty
|
||||
80
slides/math.sty
Normal file
80
slides/math.sty
Normal file
|
|
@ -0,0 +1,80 @@
|
|||
\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$}}
|
||||
|
|
@ -1 +0,0 @@
|
|||
../my_hyperref.sty
|
||||
26
slides/my_hyperref.sty
Normal file
26
slides/my_hyperref.sty
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
\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
|
||||
}
|
||||
|
|
@ -1 +0,0 @@
|
|||
../my_listings.sty
|
||||
63
slides/my_listings.sty
Normal file
63
slides/my_listings.sty
Normal file
|
|
@ -0,0 +1,63 @@
|
|||
\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$}
|
||||
|
||||
|
|
@ -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}
|
||||
|
||||
|
|
|
|||
5
slides/theorems.sty
Normal file
5
slides/theorems.sty
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
% vim: :spell spelllang=fr
|
||||
|
||||
\renewenvironment{definition}[1]{\begin{block}{Définition~: #1.}}{\end{block}}
|
||||
\renewenvironment{theorem}[1]{\begin{block}{Théorème~: #1.}}{\end{block}}
|
||||
\renewenvironment{lemma}[1]{\begin{block}{Lemme~: #1.}}{\end{block}}
|
||||
|
|
@ -1 +0,0 @@
|
|||
../todo.sty
|
||||
9
slides/todo.sty
Normal file
9
slides/todo.sty
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
\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}}
|
||||
Loading…
Reference in a new issue