Linear Additives
Logic in Computer Science
2022-01-03 v2
Abstract
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.
Keywords
Cite
@article{arxiv.2104.13739,
title = {Linear Additives},
author = {Gianluca Curzi},
journal= {arXiv preprint arXiv:2104.13739},
year = {2022}
}
Comments
In Proceedings Linearity&TLLA 2020, arXiv:2112.14305