zbMATH — the first resource for mathematics

The lax braided structure of streaming I/O. (English) Zbl 1247.68088
Bezem, Marc (ed.), Computer science logic (CSL’11). 25th international workshop, 20th annual conference of the EACSL, Bergen, Norway, September 12–15, 2011. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-32-3). LIPIcs – Leibniz International Proceedings in Informatics 12, 292-306, electronic only (2011).
Summary: We investigate and implement a model of typed streaming I/O. Each type determines a language of traces analogous to regular expressions on strings, and programs are modelled by certain monotone functions on these traces. We show that sequential composition forms a lax braided monoid in the category of types and programs. This lax braided structure allows programs to be represented diagrammatically using Joyal and Street’s string diagrams in 3D space. Monotone functions over traces cannot be executed efficiently, so we present an equivalent monoidal category of transducers. We demonstrate that transducers can be executed efficiently, theoretically by showing that programs with diagrams embedded in the plane can be executed in \(O(1)\) space, and experimentally by an implementation in the Agda dependently typed functional language. Agda supports machine-assisted proof: we have mechanically verified that the transducer implementation and the I/O model form lax braided monoidal categories.
For the entire collection see [Zbl 1237.68014].
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
18B20 Categories of machines, automata
18D10 Monoidal, symmetric monoidal and braided categories (MSC2010)
68N18 Functional programming and lambda calculus
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI Link