Oublis \sigma + cohérence

dm.tex

@@ -44,7 +44,7 @@
 
 \section{Exercise 1}
 
-\subsection{Denotational semantic for expressions}
+\subsection{Denotational Semantic for expressions}
 
 % $State = Var -> ((Field \rightharpoonup Value) \cup Value)$
 \begin{align*}
@@ -66,7 +66,9 @@
   \mathcal{A} |[ e_1{f \mapsto e_2} |] \sigma f &= \mathcal{A}|[ e_1 |] \sigma [f \mapsto \mathcal{A}|[ e_2 |] \sigma ]\\
 \end{align*}
 
-For the undefined cases, for example when we try to add records, we also note $\mathcal{A}|[e|] = \bot$.
+For the undefined cases, for example when we try to add records, we also note $\mathcal{A}|[e|] \sigma = \bot$.
+
+% TODO fin de la question : explications
 
 \subsection{Structural Operational Semantic for commands}
 
@@ -77,7 +79,7 @@ For all $\sigma \neq \bot$:
   \inference{}{(skip, \sigma) -> \sigma}
 \]
 \[
-  \inference{}{(x := a, \sigma) -> \sigma[x \mapsto \mathcal{A}|[a|] \sigma]}{\mathcal{A}|[a|] \sigma \neq \bot}
+  \inference{}{(x := a, \sigma) -> \sigma[x \mapsto \mathcal{A}|[a|] \sigma]}{\text{if }\mathcal{A}|[a|] \sigma \neq \bot}
 \]
 \[
   \inference{(S_1, \sigma) -> (S_1', \sigma')}{(S_1 ; S_2, \sigma) -> (S_1' ; S_2, \sigma')}
@@ -86,16 +88,16 @@ For all $\sigma \neq \bot$:
   \inference{(S_1, \sigma) -> \sigma'}{(S_1 ; S_2, \sigma) -> (S_2, \sigma')}
 \]
 \[
-  \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> (S ; \<while>\ b\ \<do> S, \sigma')}{\text{if } \mathcal{B}|[b|] = \text{tt}}
+  \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> (S ; \<while>\ b\ \<do>\ S, \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{tt}}
 \]
 \[
-  \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> \sigma)}{\text{if } \mathcal{B}|[b|] = \text{ff}}
+  \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{ff}}
 \]
 \[
-  \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_1, \sigma)}{\text{if } \mathcal{B}|[b|] = \text{tt}}
+  \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_1, \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{tt}}
 \]
 \[
-  \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_2, \sigma)}{\text{if } \mathcal{B}|[b|] = \text{ff}}
+  \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_2, \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{ff}}
 \]
 
 Error cases: % TODO
@@ -104,10 +106,10 @@ Error cases: % TODO
   \inference{}{(S, \bot) -> \bot}
 \]
 \[
-  \inference{}{(x := a, \sigma) -> \bot}{\mathcal{A}|[a|] \sigma = \bot}
+  \inference{}{(x := a, \sigma) -> \bot}{\text{if }\mathcal{A}|[a|] \sigma = \bot}
 \]
 
-\subsection{Système de type}
+\subsection{Type system}
 
 
 \end{document}