near final?

This commit is contained in:
Théophile Bastian 2016-09-08 00:23:45 +02:00
parent db0a4a5a29
commit 8e2f478e2a
3 changed files with 95 additions and 4 deletions

View file

@ -1,6 +1,10 @@
TEX=slides.tex TEX=slides.tex
BASE=slides
all: $(TEX) all: $(TEX)
pdflatex $(TEX) pdflatex $(TEX)
pdflatex $(TEX) pdflatex $(TEX)
upload:
scp $(BASE).pdf www.tobast:~/tobast.fr/public_html/l3/slides.pdf

View file

@ -228,7 +228,7 @@ jeux}
\begin{definition}{structure d'événement (déterministe)} \begin{definition}{structure d'événement (déterministe)}
$(E, \leq_E)$ ensemble d'\emph{événements} partiellement ordonné. $(E, \leq_E)$ ensemble d'\emph{événements} partiellement ordonné.
\end{definition} \end{definition}
-\pause% \pause%
\begin{definition}{structure d'événement polarisée (SEP) / \alert{jeu}} \begin{definition}{structure d'événement polarisée (SEP) / \alert{jeu}}
$(E, \leq_E, \rho_E)$$(E, \leq_E)$ est une structure d'événements $(E, \leq_E, \rho_E)$$(E, \leq_E)$ est une structure d'événements
et $\rho_E : E \to \set{\ominus, \oplus}$. et $\rho_E : E \to \set{\ominus, \oplus}$.
@ -286,12 +286,24 @@ jeux}
\section{Interprétation de \llccs} \section{Interprétation de \llccs}
\subsection{Sémantique dénotationnelle}
\begin{frame}{Interprétation de \llccs} \begin{frame}{Interprétation de \llccs}
\begin{columns}[t] \begin{columns}[c]
\column{0.5\textwidth} \column{0.5\textwidth}
\begin{align*} \begin{align*}
\seman{\proc} &\eqdef \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*} \end{align*}
\column{0.5\textwidth} \column{0.5\textwidth}
@ -304,6 +316,81 @@ jeux}
\seman{\lambda x^A \cdot t} &\eqdef \seman{t} \seman{\lambda x^A \cdot t} &\eqdef \seman{t}
\end{align*} \end{align*}
\end{columns} \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}
$\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{frame}
\end{document} \end{document}

View file

@ -1,5 +1,5 @@
% vim: :spell spelllang=fr % vim: :spell spelllang=fr
\renewenvironment{definition}[1]{\begin{block}{Définition~: #1.}}{\end{block}} \renewenvironment{definition}[1]{\begin{block}{Définition~: #1.}}{\end{block}}
\renewenvironment{theorem}[1]{\begin{block}{Théorème~: #1.}}{\end{block}} \renewenvironment{theorem}[1]{\begin{alertblock}{Théorème~: #1.}}{\end{alertblock}}
\renewenvironment{lemma}[1]{\begin{block}{Lemme~: #1.}}{\end{block}} \renewenvironment{lemma}[1]{\begin{block}{Lemme~: #1.}}{\end{block}}