A type-assignment of linear erasure and duplication

TL;DR

This paper introduces a new type-assignment system, LEM, for linear lambda calculus that supports weakening and contraction, enabling efficient representation of boolean circuits and natural numbers, with applications to Hereditarily Finite Permutations.

Contribution

LEM extends second-order IMLL with weakening and contraction rules, providing a modular, compact, and computationally feasible system for representing boolean circuits and natural numbers.

Findings

LEM achieves cubic cut-elimination cost and subject reduction.

Derivations in LEM can exponentially compress those in IMLL_2.

LEM effectively encodes boolean circuits and natural numbers.

Abstract

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.