diff --git a/sections/circuits.tex b/sections/circuits.tex index bfb8e13..28754c6 100644 --- a/sections/circuits.tex +++ b/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} diff --git a/sections/evaluation.tex b/sections/evaluation.tex index 9052a17..a8c39c3 100644 --- a/sections/evaluation.tex +++ b/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} diff --git a/sections/future.tex b/sections/future.tex index 7cc2672..1e6ce33 100644 --- a/sections/future.tex +++ b/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} \ No newline at end of file diff --git a/sections/intro.tex b/sections/intro.tex index 2b33f18..10c529b 100644 --- a/sections/intro.tex +++ b/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 diff --git a/sections/mealy.tex b/sections/mealy.tex index b225d44..5baf018 100644 --- a/sections/mealy.tex +++ b/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 diff --git a/sections/streams.tex b/sections/streams.tex index 54fcfd9..3c7aac0 100644 --- a/sections/streams.tex +++ b/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} \ No newline at end of file