Linear Additives

TL;DR

This paper introduces LAM, a type system with linear additive rules that manage duplication linearly, ensuring linear strong normalization and efficient cut-elimination, with a translation to linear lambda calculus.

Contribution

It presents a novel type assignment system with linear additive rules, maintaining normalization and providing a complexity analysis and translation to linear lambda calculus.

Findings

Typable terms enjoy linear strong normalization.

Cut-elimination takes a cubic number of steps.

Sound translation to linear lambda calculus with complexity analysis.

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.