An Abstract Factorization Theorem for Explicit Substitutions
An Abstract Factorization Theorem for Explicit Substitutions
复制标题
显式替换的抽象因式分解定理
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Beniamino Accattoli
中科院分区：
文献类型：
--
作者：
Beniamino Accattoli
我们研究了显式替换演算的一种简单的标准化形式，这里称为因式分解，即Lambda演算，其中Beta-归约被分解为各种规则。尽管这些演算是非终止和非正交的，但它们有一个关键特征：当单独考虑时，每个规则都终止。众所周知，在存在终止的情况下，重写性质的研究被简化(例如，合流简化为局部合流)。利用这一注解，从局部图上的一些公理推导出一个抽象的分解定理。这些公理很简单，很容易检查，特别是它们没有提到残差。然后将抽象定理应用于与证明网有关的显式替换演算。我们展示了如何按级别恢复标准化，我们对按名称和按值调用演算进行了建模，并通过线性代换演算的因式分解定理刻画了线性头部缩减。
We study a simple form of standardization, here called factorization, for explicit substitutions calculi, i.e. lambda-calculi where beta-reduction is decomposed in various rules. These calculi, despite being non-terminating and non-orthogonal, have a key feature: each rule terminates when considered separately. It is well-known that the study of rewriting properties simplifies in presence of termination (e.g. confluence reduces to local confluence). This remark is exploited to develop an abstract theorem deducing factorization from some axioms on local diagrams. The axioms are simple and easy to check, in particular they do not mention residuals. The abstract theorem is then applied to some explicit substitution calculi related to Proof-Nets. We show how to recover standardization by levels, we model both call-by-name and call-by-value calculi and we characterize linear head reduction via a factorization theorem for a linear calculus of substitutions.