[build] Polished some of the slides up

sections/circuits.tex

@@ -9,16 +9,15 @@ \section{Categorical semantics for digital~circuits}
 
     \pause
 
-    \alert{Gates} $g$ with associated monotonic functions $\morph{\bar{g}}{\textbf{V}^m}{\textbf{V}}$.
-
+    \[\textbf{V} = \tikzfig{streams/lattice}\]
 
     \pause
 
-    \[\textbf{V} = \tikzfig{streams/lattice}\]
+    \alert{Gate symbols} $g$ with associated monotonic functions $\morph{\bar{g}}{\textbf{V}^m}{\textbf{V}}$.
 
     \pause
 
-    \[\Sigma = (\textbf{V}, \{\morph{\ \mf{AND}}{\textbf{V}^2}{\textbf{V}},\ \morph{\mf{OR}}{\textbf{V}^2}{\textbf{V}}\ \})\]
+    \[\{\morph{\ \mf{AND}}{\textbf{V}^2}{\textbf{V}},\ \morph{\mf{OR}}{\textbf{V}^2}{\textbf{V}}\ \}\]
 
 \end{frame}
 
@@ -27,10 +26,12 @@ \section{Categorical semantics for digital~circuits}
 
     \pause
 
-    Circuits are morphisms generated freely over a signature $\Sigma$.
+    Circuits are morphisms in the prop generated freely over a signature $\Sigma$.
 
     \pause
 
+    e.g:
+
     \begin{center}
         \tikzfig{circuits/components/bot}
         \tikzfig{circuits/components/t}
@@ -59,12 +60,16 @@ \section{Categorical semantics for digital~circuits}
         \tikzfig{circuits/components/stub}
     \end{center}
 
+    \pause
+
     Composed together in sequence or parallel with identities and symmetries.
 
 \end{frame}
 
 \begin{frame}
     \frametitle{Combinational circuits: axioms}
+
+    \pause
     \begin{center}
         \vspace{2em}
 

sections/evaluation.tex

@@ -29,7 +29,6 @@ \section{Evaluating digital circuits}
 
     \begin{center}
         \tikzfig{circuits/productivity/step-0}
-        \pause
         \quad$=$\quad
         \tikzfig{circuits/productivity/delay-guarded}
     \end{center}
@@ -47,7 +46,7 @@ \section{Evaluating digital circuits}
 \end{frame}
 
 \begin{frame}
-    \frametitle{`Instant' feedback}
+    \frametitle{Cyclic combinational circuits}
 
     But not all non-delay-guarded circuits are unproductive!
 
@@ -62,7 +61,7 @@ \section{Evaluating digital circuits}
 
     \pause
 
-    A clever way of \alert{sharing resources}.
+    These are called \alert{cyclic combinational circuits}.
 
 \end{frame}
 
@@ -149,12 +148,12 @@ \section{Evaluating digital circuits}
     \frametitle{Productivity, redux}
 
     \begin{theorem}
-        For any circuit $\,\tikzfig{circuits/components/fcirc-closed}\,$, there exists values $\,\tikzfig{circuits/components/values}\,$ and combinational $\,\tikzfig{circuits/components/gcirc-closed}\,$ such that 
+        For any circuit $\,\tikzfig{circuits/components/fcirc-closed}\,$, there exists values $\,\tikzfig{circuits/components/values}\,$ and circuit $\,\tikzfig{circuits/components/gcirc-closed}\,$ such that 
 
         \pause
 
         \begin{center}
-            \tikzfig{circuits/components/fcirc} 
+            \tikzfig{circuits/components/fcirc-closed} 
             \quad$=$\quad
             \tikzfig{circuits/productivity/productive} 
         \end{center}

sections/future.tex

@@ -1,39 +1,39 @@
 \section{Future work}
 
 \begin{frame}
-    \frametitle{Open circuits}
+    \frametitle{Conclusion}
 
-    We can recover a `black-box' Mealy machine from a periodic stream function. 
+    We have refined the \alert{categorical framework} for circuits by Ghica and Jung to eliminate \alert{instant feedback}.
 
     \pause
 
-    But can we recover a circuit morphism from a `black-box' Mealy machine?
+    Any closed circuit can now be reduced to a \alert{waveform} of values. 
 
     \pause
 
-    This is a fairly standard procedure in circuit design.
+    The axiomatisation `agrees' with the denotational semantics of \alert{Mealy machines}.
 
     \pause
 
-    We need to take into account \alert{monotonicity} and \alert{signatures}.
+    We can use the \alert{final coalgebra} of Mealy machines to establish a link between \alert{closed circuits} and \alert{periodic streams}.
 
 \end{frame}
 
 \begin{frame}
-    \frametitle{Conclusion}
+    \frametitle{Next step: open circuits}
 
-    We have refined the \alert{categorical framework} for circuits by Ghica and Jung to eliminate \alert{instant feedback}.
+    We can recover a `black-box' Mealy machine from a periodic stream function. 
 
     \pause
 
-    Any closed circuit can now be reduced to a \alert{waveform} of values. 
+    But can we recover a circuit morphism from a `black-box' Mealy machine?
 
     \pause
 
-    The axiomatisation `agrees' with the denotational semantics of \alert{Mealy machines}.
+    This is a fairly standard procedure in circuit design.
 
     \pause
 
-    We can use the \alert{final coalgebra} of Mealy machines to establish a link between \alert{closed circuits} and \alert{periodic streams}.
+    We need to take into account \alert{monotonicity} and \alert{signatures}.
 
 \end{frame}

sections/intro.tex

@@ -5,6 +5,14 @@
 
     \pause
 
+    Normally evaluated using \alert{denotational semantics}: automata
+
+    \pause
+
+    What about step-by-step \alert{operational semantics}?
+
+    \pause
+
     \alert{Previous work:} Ghica, Jung and Lopez (2016, 2017)
 
     \pause

sections/mealy.tex

@@ -9,7 +9,7 @@ \section{Mealy machines}
     \begin{itemize}
         \item \alert{State space} $S$ \pause
         \item \alert{Input space} $M$ \pause
-        \item \alert{Output space} $O$ \pause
+        \item \alert{Output space} $N$ \pause
         \item \alert{Transition function} $\morph{T}{S}{S^M}$ \pause
         \item \alert{Output function} $\morph{O}{S}{N^M}$ \pause
     \end{itemize}
@@ -29,6 +29,8 @@ \section{Mealy machines}
 
     Mealy machines have a notion of \alert{bisimilarity}.
 
+    \pause
+
     If two machines are \alert{observationally equivalent}, then they are bisimilar.
 
 \end{frame}
@@ -44,7 +46,7 @@ \section{Mealy machines}
 
     \pause
 
-    Composition, tensor, trace fairly straightforward.
+    We can define composition, tensor, trace...
 
     \pause
 
@@ -116,7 +118,7 @@ \section{Mealy machines}
     \pause
 
     \begin{theorem}
-        For any $F,G \in \scirc[\Sigma]$, if $F = G$ then $\tomm[F] \equiv \tomm[G]$.
+        For any $F,G \in \scirc[\Sigma]$, if $F = G$ then $\tomm[F]$ and $\tomm[G]$ are bisimilar.
     \end{theorem}
 
     \pause

sections/streams.tex

@@ -1,27 +1,33 @@
 \section{Streams}
 
 \begin{frame}
-    \frametitle{Periodic streams}
+    \frametitle{(Periodic) streams}
+
+    \pause
 
     A stream $\sigma : X^\omega$ is an \alert{infinite sequence} of values $v[0] :: v[1] :: v[2] :: \cdots$
 
     \pause
 
     A stream $\sigma$ is \alert{periodic} if it has a finite \alert{prefix} and an infinitely reoccurring \alert{period}.
+    %
+    \[ \textbf{v}_0 :: \textbf{v}_1 :: \cdots :: \textbf{v}_{p-1} :: \textbf{v}_{p} :: \textbf{v}_{p+1} :: \cdots \textbf{v}_{p+r-1} :: \textbf{v}_{p} :: \textbf{v}_{p+1} :: \cdots\]
 
     \pause
 
-    Formally, there exists $p,r \in \nat$ such that for all $i \in \nat$, $\sigma[p+i] = \sigma[p+r+i]$.
-    
+    We propose that the outputs of circuits over time form \alert{periodic streams}.
+
     \pause
 
-    Since circuits are \alert{finite}, they should correspond to the \alert{periodic streams}.
+    Streams are the \alert{final Mealy coalgebra}.
 
 \end{frame}
 
 \begin{frame}
     \frametitle{The final Mealy coalgebra}
 
+    \pause
+
     Mealy machines are a \alert{coalgebra} of the functor $R(S) = (S \times N)^M$ in \textbf{Set}.
 
     \pause
@@ -78,11 +84,12 @@ \section{Streams}
 
             \vspace{1em}
 
-            \pause
-
-            \scalebox{1.5}{$\text{Periodic streams over } ({\textbf{V}^n})^\omega = \pcsprop[\textbf{V}]$}
+            \scalebox{1.5}{$\text{Periodic streams over } {\textbf{V}^n} \text{ for some n} = \pcsprop[\textbf{V}]$}
         \end{center}
 
+        \vspace{1em}
+
+        \pause
 
         \begin{theorem}
             $\cscirc[\Sigma] \cong {\pcsprop}_{\textbf{V}}$.
@@ -104,8 +111,4 @@ \section{Streams}
 
     This is a form of \alert{normalisation by evaluation}.
 
-    \pause
-
-    Next step: develop for \alert{open circuits}...
-
 \end{frame}