A fixpoint semantics for "memory cells" in synchronous dataflows

Abstract

We study an iteration operation modeling the repeated behavior of syn-chronous dataflows in which all partial results are issued and also memorized for the next computation step. The definition is by means of a fixpoint equation. We prove some equational properties of iteration, comparing them to the ones of the Elgot iteration. We also prove a normal form theorem for dataflows and show that equality is decidable for canonical dataflows associated to freely generated algebraic theories.