一句话：证明共归纳广义 resumption monad transformer 在基效应支持无守卫迭代时构成完备 Elgot monad，并给出其泛性质刻画。
本文研究带副作用进程的语义模型：从建模基本效应的 monad 出发，通过 cofree coalgebra 构造添加自由操作，得到可视为非良基带副作用树的类型，推广无限 resumption monad，相应的 monad transformer 称为共归纳广义 resumption transformer。已有工作表明这类 monad 支持 guarded iteration。本文进一步证明，在基础效应支持 unguarded iteration 的条件下，该构造也支持 unguarded iteration，即形成 complete Elgot monad；并利用 complete Elgot monad 的余积，给出共归纳 resumption monad transformer 的泛性质刻画。
We study a model of side-effecting processes obtained by starting from a monad modelling base effects and adjoining free operations using a cofree coalgebra construction; one thus arrives at what one may think of as types of non-wellfounded side-effecting trees, generalizing the infinite resumption monad. Correspondingly, the arising monad transformer has been termed the coinductive generalized resumption transformer. Monads of this kind have received some attention in the recent literature; in particular, it has been shown that they admit guarded iteration. Here, we show that they also admit unguarded iteration, i.e. form complete Elgot monads, provided that the underlying base effect supports unguarded iteration. Moreover, we provide a universal characterization of the coinductive resumption monad transformer in terms of coproducts of complete Elgot monads.Comment: 47 pages, extended version of http://www.sciencedirect.com/science/article/pii/S1571066115000791
@article{paperbot385,
title = {Unguarded Recursion on Coinductive Resumptions},
author = {Sergey Goncharov and Lutz Schröder and Christoph Rauch and Julian Jakob},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 3},
year = {2018},
doi = {10.23638/lmcs-14(3:10)2018}
}