From 9c452f5f22cc87554a28e33bb864bb0ebbe7e41d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Sun, 21 Aug 2016 01:50:16 +0200
Subject: [PATCH] Add details about full abstraction

---
 concurgames.sty |  2 ++
 math.sty        |  7 +++++++
 report.tex      | 27 ++++++++++++++++++++++-----
 3 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/concurgames.sty b/concurgames.sty
index ba21e2c..a114cac 100644
--- a/concurgames.sty
+++ b/concurgames.sty
@@ -14,6 +14,8 @@
 \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\,}}}
diff --git a/math.sty b/math.sty
index 46466a5..370dd70 100644
--- a/math.sty
+++ b/math.sty
@@ -9,6 +9,13 @@
 \usepackage{mathtools}
 
 \newcommand{\eqdef}{{~\coloneqq~}}
+\newcommand{\lAnd}{~\&~}
+
+\newcommand{\overOr}[2]{\begin{array}{r l}
+	& #1 \\
+	\textit{or} & \\
+	& #2
+\end{array}}
 
 \newcommand{\id}{\operatorname{id}}
 
diff --git a/report.tex b/report.tex
index a322d4c..bca1cf9 100644
--- a/report.tex
+++ b/report.tex
@@ -1089,11 +1089,28 @@ not be too hard to lift it to a language closer to real-world programming
 languages, through the inclusion of the imperative primitives found in the
 literature.
 
-I also explored the possibility to reach a full-abstraction result, but
-abandoned this path by lack of time. Indeed, this would have required either to
-modify \llccs{} or to restrict the authorized strategies, because of the
-following legal strategy, which cannot be expressed as the semantics of a term
-in \llccs{}:
+\medskip
+
+I also explored the possibility to reach a full-abstraction result. The
+full-abstraction property states that two terms are \emph{observationally
+equivalent} if and only if their (denotational) semantics are equal, that is,
+in this context,
+for all $P,Q$ two \llccs{} terms such that $\Gamma \vdash P,Q : A$,
+
+\[
+	\left[ \forall \calC[-] \text{ a context }\,:\,
+		\left( \vdash \calC[P] : \proc \right),~
+		\calC[P] \Downarrow \iff \calC[Q] \Downarrow
+		\right]
+	\quad\iff\quad
+	\left( \seman{P} = \seman{Q} \right)
+\]
+
+Yet, by lack of time, I had to abandon this path. Indeed, this would have
+required either to modify \llccs{} or to restrict the authorized strategies,
+because of the following legal strategy, which cannot be expressed as the
+semantics of a term in \llccs{}:
+
 \[ \begin{tikzpicture}
 	\node (0P) at (2,2) {$\proc$};
 	\node (0C) at (0,2) {$\chan$};