语境语义、线性逻辑与计算复杂性

我们表明语境语义可被有效应用于线性逻辑中证明归约的定量分析。特别是，语境语义允许我们定义证明网络的权重作为其固有复杂性的度量：它既是归约时间的上界（独立于归约策略，仅需多项式开销），也是归约至正常形态步骤数的下界（对于某些归约策略而言）。随后，这些权重被用于证明线性逻辑各种子系统的强健全称性定理，包括初等线性逻辑、软线性逻辑和轻量级线性逻辑。