paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A Generalized Modality for Recursion

一种用于递归的广义模态
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 该论文是类型论中关于递归模态（guarded recursion）的范畴论推广，属于形式语义基础理论，与用户关注的LLM/Agent在静态分析/形式化验证中的应用、浮点或贝叶斯程序分析没有直接联系，且未涉及工程实现或AI交叉。引用 19 inbox
Adrien Guatto
类型系统形式语义
crossref: 2026-09-12

AI 速览

一句话：提出递归的广义模态，将 Nakano 的 later modality 推广到更一般的范畴框架。

Nakano 的 later modality 使类型能够表达函数输出不立即依赖其输入，从而保证不动点的计算安全，这一思想称为 guarded recursion，已用于无限数据结构与类型论内部的 step-indexing 等场景。本文研究递归的广义模态，并借助范畴模型说明 later modality 本质上对应于离散时间尺度上的一种重新索引。由此，论文将 later modality 与 guarded recursion 置于更一般的范畴与类型论框架中，为递归模态提供统一视角。摘要未报告具体实验评估，论证主要基于范畴模型分析。

问题
如何理解并推广 Nakano 的 later modality，使其成为更一般的递归模态，同时保持 guarded recursion 的安全性。
方法
使用范畴模型分析 later modality，揭示其对应离散时间尺度的重新索引，并据此构造广义递归模态。
评估
摘要未给出实验或基准评估；主要依据范畴模型与类型论层面的理论论证。
原文摘要（Abstract）

Nakano's later modality allows types to express that the output of a function does not immediately depend on its input, and thus that computing its fixpoint is safe. This idea, guarded recursion, has proved useful in various contexts, from functional programming with infinite data structures to formulations of step-indexing internal to type theory. Categorical models have revealed that the later modality corresponds in essence to a simple reindexing of the discrete time scale.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot4352,
  title = {A Generalized Modality for Recursion},
  author = {Adrien Guatto},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209148}
}