资源控制与强正规化
逻辑
2013-05-20 v3 计算机科学中的逻辑
摘要
我们引入“资源控制立方体”，这是一个由八个直觉主义λ演算组成的系统，这些演算具有隐式或显式的资源控制，并采用自然演绎或矢列演算。该立方体中对应于自然演绎的四个演算已由Kesner和Renaud提出，而对应于矢列λ演算的四个演算则在本文中引入。其表述以资源集合（弱化或收缩）为参数，从而能够统一处理该立方体的八个演算。简单类型的资源控制立方体一方面将Curry-Howard对应扩展到具有隐式或显式结构规则的直觉主义自然演绎和直觉主义矢列逻辑，另一方面与子结构逻辑相关联。我们为资源控制立方体演算提出了一个通用的交集类型系统。我们的主要贡献是对该立方体中归约的强正规化进行了刻画。首先，我们通过改编可归约性方法，证明了在立方体的“自然演绎基”中，可赋型性蕴含强正规化。然后，我们通过使用良序的组合以及在“自然演绎基”中的适当嵌入，证明了在立方体的“矢列基”中，可赋型性蕴含强正规化。最后，我们使用首部主体扩展证明了在立方体中强正规化蕴含可赋型性。所有证明都是通用的，并且可以通过实例化资源集合而具体适用于立方体中的每个演算。
引用
@article{arxiv.1112.3455,
title = {Resource control and strong normalisation},
author = {Silvia Ghilezan and Jelena Ivetic and Pierre Lescanne and Silvia Likavec},
journal= {arXiv preprint arXiv:1112.3455},
year = {2013}
}