Linear Additives

Gianluca Curzi

doi:10.4204/EPTCS.353.4

Linear Additives

Gianluca Curzi^*

^*Corresponding author for this work

Computer Science

Research output: Contribution to journal › Conference article › peer-review

Abstract

We introduce LAM, a subsystem of IMALL₂ 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 LAM's proofs into IMLL₂'s linear lambda terms, and we study its complexity.

Original language	English
Pages (from-to)	74-93
Number of pages	20
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	353
DOIs	https://doi.org/10.4204/EPTCS.353.4
Publication status	Published - 28 Apr 2021
Event	2nd Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity and TLLA 2020 - Virtual, Online Duration: 29 Jun 2020 → 30 Jun 2020

Bibliographical note

Publisher Copyright:
© Gianluca Curzi

ASJC Scopus subject areas

Software

Access to Document

10.4204/EPTCS.353.4Licence: Creative Commons: Attribution (CC BY)

Structure vs. Invariants in Proofs (StrIP)
Das, A. (Principal Investigator)
Medical Research Council
1/05/20 → 31/07/24
Project: Research Councils

Cite this

@article{1c7f83faf37d4bb48db2dc9ee44c302f,

title = "Linear Additives",

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 LAM's proofs into IMLL2's linear lambda terms, and we study its complexity.",

author = "Gianluca Curzi",

note = "Publisher Copyright: {\textcopyright} Gianluca Curzi; 2nd Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity and TLLA 2020 ; Conference date: 29-06-2020 Through 30-06-2020",

year = "2021",

month = apr,

day = "28",

doi = "10.4204/EPTCS.353.4",

language = "English",

volume = "353",

pages = "74--93",

journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

issn = "2075-2180",

publisher = "Open Publishing Association",

}

TY - JOUR

T1 - Linear Additives

AU - Curzi, Gianluca

N1 - Publisher Copyright: © Gianluca Curzi

PY - 2021/4/28

Y1 - 2021/4/28

N2 - 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 LAM's proofs into IMLL2's linear lambda terms, and we study its complexity.

AB - 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 LAM's proofs into IMLL2's linear lambda terms, and we study its complexity.

UR - https://www.scopus.com/pages/publications/85122453940

U2 - 10.4204/EPTCS.353.4

DO - 10.4204/EPTCS.353.4

M3 - Conference article

AN - SCOPUS:85122453940

SN - 2075-2180

VL - 353

SP - 74

EP - 93

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

T2 - 2nd Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity and TLLA 2020

Y2 - 29 June 2020 through 30 June 2020

ER -

Linear Additives

Abstract

Bibliographical note

ASJC Scopus subject areas

Access to Document

Fingerprint

Projects

Structure vs. Invariants in Proofs (StrIP)

Cite this