高阶语言中的分离和共享效应
Separated and Shared Effects in Higher-Order Languages
摘要：
高效的程序交互方式超越了简单的输入输出，这使得组合推理具有挑战性。现有的工作表明，当这些程序是“分离的”时，即，当程序之间互不干扰时，对它们的推理就更容易了。虽然关于分离资源的推理已经得到了很好的研究，但是关于分离效果的推理的工作很少，特别是对于函数式的高阶程序设计语言。我们提出了两种高阶语言，可以在有效的程序中进行共享和分离。我们的第一种语言$λ_{\text{INI}}$具有线性类型系统和概率语义，其中两种产品类型捕获独立和可能依赖的对。我们的第二语言$λ_{\text{INI}}^2$是两级的，分层的语言，灵感来自本顿的线性非线性（LNL）演算。我们激励这种语言的概率模型，但我们也提供了一个一般的分类语义，并表现出一系列的具体模型超出概率编程。我们证明我们所有的语言的合理性定理，我们的一般合理性定理，我们的分类模型$λ_{\text{INI}}^2$使用分类胶合建设。
英文摘要：
Effectful programs interact in ways that go beyond simple input-output, making compositional reasoning challenging. Existing work has shown that when such programs are ``separate'', i.e., when programs do not interfere with each other, it can be easier to reason about them. While reasoning about separated resources has been well-studied, there has been little work on reasoning about separated effects, especially for functional, higher-order programming languages. We propose two higher-order languages that can reason about sharing and separation in effectful programs. Our first language $λ_{\text{INI}}$ has a linear type system and probabilistic semantics, where the two product types capture independent and possibly-dependent pairs. Our second language $λ_{\text{INI}}^2$ is two-level, stratified language, inspired by Benton's linear-non-linear (LNL) calculus. We motivate this language with a probabilistic model, but we also provide a general categorical semantics and exhibit a range of concrete models beyond probabilistic programming. We prove soundness theorems for all of our languages; our general soundness theorem for our categorical models of $λ_{\text{INI}}^2$ uses a categorical gluing construction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
