Quantitative Models and Implicit Complexity

我们给出了 Elemental Affine Logic、LFPL（一种接近真实函数式编程的多项式时间计算语言，由本文作者之一提出）、Light Affine Logic 和 Soft Affine Logic 的新型 soundness 证明（即所有可表示的基本类型函数均落在特定复杂度类中）。这些证明基于一种通用的语义框架，通过四种不同的方式进行实例化。该框架是对实izability 的一种创新性修改，使我们能够将受资源限制的计算用作实现者，而通常情况下实izability 构造中会将所有可图灵可计算的函数作为实现者。例如，LFPL 模型中所有实现者都是多项式有界的计算，从而通过模型的构造方式自然实现了 soundness。本工作的核心在于能够在模型中解释所有所需的构造。虽然这是对 Light Logic 多项式时间 soundness 首个完全语义证明，但我们的证明也为 LFPL 原已较为语义化的多项式时间 soundness 证明提供了显著的简化。由该语义框架实现的新结果是：向 LFPL 添加多态性和模态，从而允许内部定义归纳数据类型。