A recently introduced general framework of Memoryful Geometry of Interaction (mGoI) provides a sound translation of lambda-terms (on the high-level) to their realizations by stream transducers (on the low-level), where the internal states of the latter (called memories) are exploited for accommodating algebraic effects of Plotkin and Power. The translation is compositional, hence “denotational,” where transducers are inductively composed using an adaptation of Barbosa’s coalgebraic component calculus.

However, to the current authors’ best knowledge, there has not been any systematic treatment of recursion in this mGoI framework. This is the goal of the current paper. We introduce two new fixed-point operators in the coalgebraic component calculus. The two follow the previous work on recursion in GoI and are called Girard style and Mackie style: the former obviously exhibits some nice domain-theoretic properties, while the latter gives simple construction of resulting transducers. Their equivalence is established on the categorical (or, traced monoidal) level of abstraction, and is therefore generic with respect to the choice of algebraic effects. Our main result is an adequacy theorem of our mGoI translation, against Plotkin and Power’s operational semantics for algebraic effects.