Circuits via topoi

Arnaud Spiwack (1, 2)

1 Mines Paris - PSL (École nationale supérieure des mines de Paris)
2 CRI - Centre de Recherche en Informatique

Leveraging topos theory a semantics can be given to sequential circuits where time-sensitive gates, such as unit delay, are treated uniformly with combinational gates. Both kinds of gates are functions in a particular topos: the topos of presheaves over the natural ordering of N. This is used to show that sequential circuits validate the equational theory of traced categories. When giving semantics to circuits (typically boolean circuits), it is customary to treat the combinational – i.e. time-independent – parts of the circuits differently from time sensitive ones. Since it is usually assumed that the only time-sensitive gate is the unit delay, each outgoing wire from a delay is considered an additional input, and each incoming wire an additional output. Some care is taken to feed the right output into the right input at next iteration, and so time-sensitivity is eliminated and one can reason on a purely combinational circuit. This is not very convenient to reason equationally about moving unit delays for better placement. But this approach really breaks down when considering time-sensitive gates which are not simple unit delay. This article takes its root in the study of compilation of the circuit programming language Faust [13]. Faust features a somewhat unusual kind of delay gate, written s@d, where s is an arbitrary signal, and d is a time-varying bounded natural number signal whose value at time t determines how far in the past of s to fetch the value of the delayed signal. With such a construct, it becomes impossible to " cut " a circuit into a combinational circuit. At least not without heavy modifications (the constraint that d is bounded is imposed in order to be able to compile the program in constant memory, so such a circuit can be reduced to use only unit delays). To address this issue, let us turn to presheaves and topos theory. The critical property which we shall use is that topoi are models of constructive mathematics. Therefore we shall first develop a theory of combinational circuits in ordinary constructive mathematics, then lift it to sequential circuits via a presheaf construction. Much work has been put [3, 1], recently, in using category theory to explain and exploit the linear algebraic aspects of circuits from control-theory. This article explores an orthogonal axis of the design space. Both can, and should, in principle be combined to obtain linear algebra with time. It is what signal processing is made of. Before we move on, I have to start with an apology: despite the subject of topoi and presheaves being rather technical, I will be assuming quite a bit of familiarity with them in this article. I realise that this will make this article unnecessarily arduous for many. But in order for this article to be written at all, I felt I had to limit its scope so. A good, exhaustive, introduction to topos theory can be found in Mac Lane & Moerdijk’s Sheaves in geometry and logic.

Domaines: Informatique et langage [cs.CL]

Arnaud Spiwack. Circuits via topoi. [Technical Report] E/421/CRI, Mines ParisTech - PSL Research University - Centre de Recherche en Informatique (CRI). 2015. ⟨hal-01537455⟩