A type-assignment of linear erasure and duplication

Autor: Gianluca Curzi, Luca Roversi
Rok vydání: 2020
Předmět:
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
Hereditarily finite permutations
General Computer Science
Computer science
Boolean circuit
Natural number
0102 computer and information sciences
02 engineering and technology
01 natural sciences
Second-order multiplicative linear logic
Type-assignment
Linear -calculus
Cut-elimination (cost)
Boolean circuits
Numerals
Hereditarily finite permutations
Theoretical Computer Science
Cut-elimination (cost)
0202 electrical engineering
electronic engineering
information engineering
Derivation
Contraction (operator theory)
Boolean circuits
Discrete mathematics
Second-order multiplicative linear logic
Linear -calculus
Multiplicative function
03B15
03B47
03F52
03F05
Linear logic
Logic in Computer Science (cs.LO)
Mathematics::Logic
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Numerals
010201 computation theory & mathematics
Subject reduction
Church encoding
Erasure
020201 artificial intelligence & image processing
Type-assignment
Zdroj: Theoretical Computer Science. 837:26-53
ISSN: 0304-3975
DOI: 10.1016/j.tcs.2020.05.001
Popis: We introduce $\mathsf{LEM}$, 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. $\mathsf{LEM}$ enjoys both a mildly weakened cut-elimination, whose computational cost is cubic, and Subject reduction. A translation of $\mathsf{LEM}$ into $\mathsf{IMLL}_2$ exists such that the derivations of the former can exponentially compress the dimension of the derivations in the latter. $\mathsf{LEM}$ 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.
Comment: 43 pages (10 pages of technical appendix). The final version will appear on Theoretical Computer Science https://doi.org/10.1016/j.tcs.2020.05.001
Databáze: OpenAIRE
Externí odkaz: