A type-assignment of linear erasure and duplication

DOI10.1016/J.TCS.2020.05.001MaRDI QIDQ2193281zbMATH OpenOpenAlexFDO

Authors Gianluca Curzi, Luca Roversi

Publication date 25 August 2020

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1912.12837

zbMATH Keywords

Boolean circuitsnumeralscut-elimination (cost)hereditarily finite permutationslinear \(\lambda\)-calculussecond-order multiplicative linear logictype-assignment

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Networks and circuits as models of computation; circuit complexity (68Q06)

Abstract: We introduce $mathsfLEM$, a type-assignment system for the linear $lambda$-calculus that extends second-order $mathsf{IMLL}_2$, i.e., intuitionistic multiplicative Linear Logic, by means of logical rules that weaken and contract assumptions, but in a purely linear setting. $mathsfLEM$ enjoys both a mildly weakened cut-elimination, whose computational cost is cubic, and Subject reduction. A translation of $mathsfLEM$ into $mathsf{IMLL}_2$ exists such that the derivations of the former can exponentially compress the dimension of the derivations in the latter. $mathsfLEM$ allows for a modular and compact representation of boolean circuits, directly encoding the fan-out nodes, by contraction, and disposing garbage, by weakening. It can also represent natural numbers with terms very close to standard Church numerals which, moreover, apply to Hereditarily Finite Permutations, i.e. a group structure that exists inside the linear $lambda$-calculus.

Recommendations

• Erasure and Polymorphism in Pure Type Systems
• Linear sized types in the calculus of constructions
• Linear types and locality
• Linear types and approximation
• Linear types and non-size-increasing polynomial time computation.
• Type assignment and conservation properties
• A decidable theory of type assignment
• A type theory for memory allocation and data layout
• Typed equivalence, type assignment, and type containment

Cites work

• scientific article; zbMATH DE number 1722667 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 3611324 (Why is no real title available?)
• scientific article; zbMATH DE number 1161568 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 1424054 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• scientific article; zbMATH DE number 7324256 (Why is no real title available?)
• A Local Criterion for Polynomial-Time Stratified Computations
• A certified study of a reversible programming language
• A class of reversible primitive recursive functions
• BCK-combinators and linear \(\lambda\)-terms have types
• Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus
• FUNCTIONAL PEARL Linear lambda calculus and PTIME-completeness
• From light logics to type assignments: a case study
• Linear logic
• Linear logic and elementary time
• On the computational complexity of cut-elimination in linear logic.
• Reversible simulations of elastic collisions
• Soft linear logic and polynomial time
• The Power of Linear Functions
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Uniform Circuits, & Boolean Proof Nets
• Weak typed Böhm theorem on IMLL

Cited in

(1)

• Linear additives

This page was built for publication: A type-assignment of linear erasure and duplication

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2193281)