递归的一种静默模态

A Generalized Modality for Recursion

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. Unfortunately, existing guarded type theories suffer from significant limitations for programming purposes. These limi…

Intensionality, Intensional Recursion, and the Gödel-Löb axiom

The use of a necessity modality in a typed $λ$-calculus can be used to separate it into two regions. These can be thought of as intensional vs. extensional data: data in the first region, the modal one, are available as code, and their description can be examined. In contrast, data in the second region are only available as values up to ordinary equality. This allows us to add non-functional operations at modal types whilst maintaining consistency. In this setting, the Gödel-Löb axiom acquires a novel constructive reading: it affords the programmer the possibility of a very strong kind of recu…

轻型逻辑分层记法的安全递归

Safe Recursion on Notation into a Light Logic by Levels

我们嵌入安全递归记法（SRN）到轻仿射逻辑的水平（LALL），来自逻辑L4。LALL是一个直观的演绎系统，具有多项式时间割消策略。嵌入允许将SRN的每个项t表示为LALL中的证明网族|t| ^l。族中的每个证明网|t| ^l在其位长度由整数l限制的参数上模拟t。嵌入基于两个关键特征。一种是LALL中的递归类型，它将Scott二进制数字（即Scott单词）编码为证明网。斯科特词代表t的参数，而不是更标准的丘奇二进制数。此外，嵌入利用LALL从L4继承的段落框的“模糊”边界来“自由”复制t的参数，特别是安全的参数。最后，|t| ^l的类型取决于用于定义t的复合和递归方案的数量，即t的结构复杂度。此外，|t| ^l的大小是l中的多项式，其次数取决于t的结构复杂度。因此，这项工作使SRN所依赖的谓词递归理论原则和基于Light Linear Logic的证明理论原则（称为/分层/）更加接近。

弱仿射光类型化关于记法上的安全递归是完备的

Weak Affine Light Typing is complete with respect to Safe Recursion on Notation

弱仿射轻类型化（WALT）将轻仿射线性公式作为类型分配给系统F的一个子集。WALT是多时间声音：如果一个非线性项M在WALT中有类型，那么M可以用一个多项式成本在给它一个类型的推导的维度上进行计算。评估在重写关系的任何策略下进行，该重写关系是按名称调用和按值调用的beta约简的混合。WALT削弱，即概括，概念“分层的扣除”，共同的一些光系统-这些逻辑系统，来自线性逻辑，以表征一套多项式函数-。一个较弱的分层允许定义一个组合嵌入安全递归符号（SRN）到WALT。事实证明，WALT的表现力比已知的光系统强得多。嵌入通过SRN的子系统的表示。它是通过限制SRN的合成方案只能线性使用其安全变量而得到的。一方面，这表明SRN实际上可以用更原始的结构来重新定义。另一方面，将SRN嵌入到WALT中具有以下两个显著的方面。嵌入所需的每个数据类型都是从头开始表示的，显示了WALT强大的结构证明理论根源。此外，嵌入突出了一个分层结构的正常和安全的参数，通常隐藏在世界的SRN正常/安全变量：少一个参数是“多项不可预测的”，更深，在一个正式的，证明理论的意义上，它是表示内WALT。最后，由于WALT是SRN完备的，它也是多项式时间完备的，因为SRN是。

线性逻辑分层的抽象方法

An Abstract Approach to Stratification in Linear Logic

我们研究分层的概念，用于子系统的线性逻辑与低复杂性界限上的削减消除程序（所谓的轻逻辑），从抽象的角度来看，引入一个逻辑系统，其中分层是由一个单独的模态处理。这种模态是吉拉德的轻线性逻辑的段落模态的概括，它产生于一种适用于线性逻辑所有模型的一般范畴结构。因此，我们了解到，分层可以制定独立的指数模态;当它被迫连接到指数模态，它产生有趣的复杂性属性。特别是，从我们的分析干三个替代的重新制定的Baillot和Mazza的线性逻辑的水平：一个几何，一个互动，一个语义。

可靠程序等价性的定量逻辑

Quantitative Logics for Equivalence of Effectful Programs

为了对效果进行推理，我们可以定义定量公式来描述有效程序的行为方面。这些公式可以例如表示程序满足属性的概率（或正确的起始状态的集合）。这种方法的基础是定量模态的概念，它用于将值的属性提升为计算的属性。把所有的公式放在一起，我们说两个项是等价的，如果它们在相同的数量程度上满足所有的公式。在数量模态的充分条件下，这种等价性等于阿布拉姆斯基的应用双相似性的概念，而且是一个同余。我们调查这些结果的背景下，利维的呼叫推值一般递归和代数效果。特别是，结果适用于（组合）不确定性的选择，概率的选择，和全球商店。