Effectful Mealy Machines
This work provides a theoretical foundation for modeling causal processes with effects, benefiting researchers in automata theory and semantics of computation.
The paper introduces effectful Mealy machines, a generalization of Mealy machines with global effects, and provides semantics for bisimilarity and traces, showing that the framework characterizes standard causal processes and existing Mealy machine variants.
Effectful Mealy machines, which we introduce, are a generalization of Mealy machines with global effects determined by an effectful triple. We provide semantics of effectful Mealy machines in terms of both bisimilarity and traces: bisimilarity is characterized syntactically, via uniform feedback; traces are constructed coinductively in terms of streams. We prove that this framework characterizes standard causal processes and existing flavours of Mealy machine, bisimilarity, and trace equivalence. In the commutative case, we introduce a monoidal generalization of Raney's causal functions: monoidal causal processes.