A type-assignment of linear erasure and duplication

DOI10.1016/J.TCS.2020.05.001zbMATH Open1484.03128arXiv1912.12837OpenAlexW3024200455MaRDI QIDQ2193281FDOQ2193281

Authors: Gianluca Curzi, Luca Roversi 

Publication date: 25 August 2020

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

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.

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

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

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)

Cites Work

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

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)