Linear Additives
share
We introduce 𝖫𝖠𝖬, a subsystem of 𝖨𝖬𝖠𝖫𝖫_2 with restricted additive rules able to manage duplication linearly, called linear additive rules. 𝖫𝖠𝖬 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 𝖫𝖠𝖬 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 𝖫𝖠𝖬's proofs into 𝖨𝖬𝖫𝖫_2's linear lambda terms, and we study its complexity.
READ FULL TEXT
