我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：研究 Brouwer 连续性原则下单子流函数的连续性及其在类型论中的不一致性边界。

论文讨论 Brouwer 连续性原则在类型论中的表现。该原则断言，从自然数无穷序列到自然数的所有函数都连续：对任意序列，结果只依赖某个有限初始段。它是一条直觉主义公理，与经典数学不相容；Martín Escardó 最近进一步证明它在类型论中也不一致。标题中的 monadic stream functions 表明本文具体考察由单子与共归纳流定义的函数。论文关注这类函数是否满足连续性，即其结果能否由输入的有限前缀决定，并借此澄清连续性原则在类型论与共归纳数据结构上的适用边界。所给摘要未列出具体定理、证明方法或评估结果，因此以上为问题背景与研究对象概述。

问题

在 Brouwer 连续性原则与类型论不一致的背景下，单子流函数（monadic stream functions）是否连续、其结果是否只依赖输入的有限初始段。

方法

摘要未说明具体方法；从标题与背景看，论文在类型论/共归纳框架内以 monadic stream functions 为对象分析其有限前缀依赖性。

评估

摘要未给出评估方式、定理或形式化结果；仅可确认其论证背景涉及 Escardó 关于连续性原则在类型论中不一致的结果。

链接与引用

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

@inproceedings{CaprettaF17,
  title = {The continuity of monadic stream functions},
  author = {Venanzio Capretta and Jonathan Fowler},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005119}
}