Foundations of a theory of synchronous systems (Q1199824)

A synchronous system as a syntactic object is defined to be a finite, edge weighted directed multigraph \(G=(V,E)\). The vertices represent ``functional elements'', which are interpreted as functions \(A^ m\to A^ p\), for a fixed set \(A\) of data elements. There are some additional enhancements, so that one can say for example that \(G\) has \(q\) ``input'' channels and \(p\) ``output'' channels. The semantics of \(G\) itself is a sequence of functions \(g_ 1,g_ 2,\dots,g_ n,\dots\) where the \(i\)-th function \(g_ i:\overbrace{A^{q+\dots q^{q_ i}}}\to A^ p\). The author shows how to obtain a much more general class of semantic models of synchronous systems in certain pointed (Lawvere algebraic) theories, \(T^ \infty\), obtained as a certain inverse limit. For any pointed theory \(T\), the author shows how to define a theory \(n\text{-res} T\), whose morphisms \(p\to q\) are \(n\)-tuples \((f_ 1,\dots,f_ n)\) of morphisms \(p\to nq\) in \(T\). The map from \(n\)-tuples to \(n-1\) tuples in a theory morphism \(n\text{-res} T\to n-1\text{-res} T\). The inverse limit of the corresponding diagram \(F^ \infty T\) is shown to be an iteration theory [\textit{S. L. Bloom}, \textit{C. C. Elgot} and \textit{J. B. Wright}, SIAM J. Comput. 9, 525-540 (1980; Zbl 0461.68047)] with a strong functorial dagger. The theory \(n\text{-res} T\) models the behavior of \(n\)-steps of the system, and \(F^ \infty T\) thus models the stepwise behavior in general. A generalization of the \(F^ \infty\) construction to triples [\textit{E. G. Manes}, Algebraic theories, Springer-Verlag, Berlin (1976; Zbl 0353.18007)] is indicated at the end of the paper.