一句话：论文将按值调用的守卫迭代语义推广到参数化单子，把守卫性刻画为程序内在的范畴性质。
该文研究按值调用（call-by-value）语言中守卫迭代（guarded iteration）的语义。已知带效应函数空间可在由强单子典范生成的 Freyd 范畴中解释；本文推广 Levy、Power 和 Thielecke 的结果，证明若要表示守卫且带效应的函数空间，需要使用 Uustalu 意义下的参数化单子，而非普通强单子。由此，守卫性不再仅被视为范畴上的谓词，而是被刻画为程序自身的内在范畴性质。该结果统一了守卫递归/守卫迭代与效应的范畴语义，并为按值调用语言中循环的良行为提供了更一般的语义基础。摘要未报告实现或实验，工作属于范畴语义理论。
Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles in various settings. In its most general form, the guardedness discipline applies to general symmetric monoidal categories and further specializes to Cartesian and co-Cartesian categories, where it governs guarded recursion and guarded iteration, respectively. Here, even more specifically, we deal with the semantics of call-by-value guarded iteration. It was shown by Levy, Power and Thielecke that call-by-value languages can be generally interpreted in Freyd categories, but in order to represent effectful function spaces, such a category must canonically arise from a strong monad. We generalize this fact by showing that representing guarded effectful function spaces calls for certain parameterized monads (in the sense of Uustalu). This provides a description of guardedness as an intrinsic categorical property of programs, complementing the existing description of guardedness as a predicate on a category.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{000123,
title = {Representing Guardedness in Call-by-Value and Guarded Parametrized Monads},
author = {Sergey Goncharov},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 1},
year = {2026},
doi = {10.46298/lmcs-22(1:9)2026}
}