We introduce LAM, a subsystem of IMALL2 with restricted additive rules able to manage duplication linearly, called linear additive rules. LAM is presented as the type assignment system for a calculus endowed with copy constructors, which deal with substitution in a linear fashion. As opposed to the standard additive rules, the linear additive rules do not affect the complexity of term reduction: typable terms of LAM enjoy linear strong normalization. Moreover, a mildly weakened version of cut-elimination for this system is proven which takes a cubic number of steps. Finally, we define a sound translation from proofs of LAM into linear lambda terms of IMLL2, and we study its complexity.
翻译：我们引入了IMALL2的子系统,即IMALL2, 其限制添加规则可以线性地管理重复,称为线性添加规则。LAM被描述为具有复制体构造体的微积分的分类系统,该微积分系统以线性方式处理替代。与标准的添加规则相反,线性添加规则并不影响缩短任期的复杂性:LAM的典型术语具有线性很强的正常化。此外,这个系统的轻度削弱的切除版本得到了证明,它需要立方步骤。最后,我们定义了从LAM的证明转变为IMLL2的线性羊巴术语的正确翻译,我们研究了其复杂性。
相关内容
微信扫码咨询专知VIP会员