paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Size-Change Principle for Mixed Inductive and Coinductive types

混合归纳与余归纳类型的 size-change 原理
LMCS vol.Volume 21, Issue 32025匹配度 3/10 · 该论文属于程序验证与静态分析理论，讨论函数式语言中 size-change 原理对归纳/余归纳类型下递归定义的全性检查。但它不涉及 LLM/Agentic 程序、浮点程序分析或贝叶斯程序分析，与用户当前研究画像的核心交叉方向匹配度较低。引用 2 inbox
Pierre Hyvernat
程序验证函数式编程
crossref: 2026-09-10

AI 速览

一句话：将 size-change 原理推广为 totality 检查，以在混合归纳与余归纳类型下可靠验证递归定义。

本文研究在 ML/Haskell 风格、同时包含归纳与余归纳类型的语言中，如何用 size-change 原理检查任意递归定义的正确性。朴素的用法分别检查终止性与 productivity，但在归纳与余归纳类型嵌套时并不可靠（unsound）。作者将 size-change 原理加以改造，使其检查“totality”，即递归定义相对于相应（余）归纳类型的正确性。该性质恰好对应语义上所需的总性，从而在嵌套情形下也保持可靠性。论文通过理论分析论证了这一适配的合理性，为混合（余）归纳类型下的递归定义验证提供了统一框架。

问题
在混合归纳与余归纳类型嵌套时，朴素地用 size-change 原理分别检查终止性与 productivity 不可靠，因此需要一种能正确检查递归定义相对于（余）归纳类型正确性的方法。
方法
将 size-change 原理从分别检查终止性与 productivity 推广为检查 totality，该性质恰好对应递归定义相对于相应（余）归纳类型的正确性。
评估
理论论证；通过分析说明朴素方法在嵌套类型下不可靠，而适配后的 totality 检查是可靠的。摘要未给出实现或实验评估。
原文摘要（Abstract）

This paper shows how to use Lee, Jones and Ben Amram's size-change principle to check correctness of arbitrary recursive definitions in an ML / Haskell like programming language with inductive and coinductive types. Naively using the size-change principle to check productivity and termination is straightforward but unsound when inductive and coinductive types are nested. We can however adapt the size-change principle to check ``totality'', which corresponds exactly to correctness with respect to the corresponding (co)inductive type.

链接与引用

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

BibTeX 
@article{abs-2407-05715,
  title = {The Size-Change Principle for Mixed Inductive and Coinductive types},
  author = {Pierre Hyvernat},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 3},
  year = {2025},
  doi = {10.46298/lmcs-21(3:20)2025}
}