非均匀环境下的 Krivine 机与泰勒展开

Krivine 机是一种实现 λ演算 线性头归约的抽象机器。Ehrhard 与 Regnier 给出了一个资源敏感版本，返回 λ项 的注释形式，以记录线性头归约所使用的资源。这些注释采用资源 λ演算 中的项的形式。我们将这种资源驱动的 Krivine 机推广到代数 λ演算 的情形。后者是纯 λ演算 的扩展，允许以取自半环的系数对 λ项 进行线性组合。我们的机器将 λ项 M 与资源注释 t 关联至半环中的一个标量 k，该标量描述了 M 的线性头归约的某些定量性质。在非负实数以及表示概率分布的代数项 M 这一特殊情况下，系数 k 给出了线性头归约恰好使用 t 所注释资源的概率。在一般情形下，我们证明系数 k 可由 M 的泰勒展开中 t 的系数以及 t 的范式恢复得出。