弱仿射光类型：多项式时间内的内涵表达能力、完备性和可靠性
摘要：弱仿射光类型（WALT）将轻量级仿射线性公式分配给System F中的λ项子集作为类型。WALT在多项式时间内可靠：如果λ项M在WALT中具有类型，则可以用给定其类型的推导的维度的多项式成本对M进行评估。特别地，评估可以在以call-by-name/call-by-value β-规约的任何策略下进行。WALT是多项式时间完备的，因为它可以表示任何多项式时间图灵机。WALT弱化了某些轻量级系统常见的推导分层的概念，我们称这些逻辑系统为Light Systems，这些系统源自线性逻辑，用于描述多项式函数的集合FP。更弱的分层允许将安全递归表示法（SRN）的准线性片段QlSRN嵌入到WALT中。QlSRN是SRN的子集，SRN是描述FP的递归理论系统，其中只有复合方案限制为线性安全变量。因此，相对于已知的Light Systems，WALT的表达能力更强。特别地，使用这些类型，嵌入显示了在QlSRN中隐藏的正常和安全参数的分层：参数为非谓词的程度越小，在形式上证明论意义上，它在WALT中的表示就越深入。
作者：Luca Roversi
论文ID：0712.4222
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-03-31