Linearization via Rewriting (Long Version)

TL;DR

This work presents the structural resource $\lambda$-calculus, a finitary rewrite-based framework that embeds qualitative lambda-calculus systems while isolating a strictly quantitative fragment via an internal linearization mechanism. It introduces two independent rewrite relations—linear reduction and exponential reduction—annotated by type morphisms, and proves strong normalization and confluence for the structural reduction. By leveraging non-idempotent and idempotent intersection types, it shows every strongly normalizing $\lambda$-term has a natural representation as a resource term, with a unique, coherent typing derivation, and it connects linear approximants to classical semantics through an operational extensional collapse. The approach unifies qualitative and quantitative perspectives, enabling internal linearization, Taylor-like approximations, and potential extensions to richer type theories, with future directions including encodings of Gödel’s $\mathcal{T}$ and dependent polymorphic systems.

Abstract

We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time any type derivation can be internally rewritten to its linearization. The calculus is shown to be normalizing and confluent. Noticeably, every strongly normalizable lambda-term can be represented by a type derivation. This is the first example of a system where the linearization process takes place internally, while remaining purely finitary and rewrite-based.

Figures (13)

• Figure 1: Type Morphisms.
• Figure 2: Context Formation.
• Figure 3: Typing Assignment for Structural Resource Terms.
• Figure 4: Structural Resource Terms in $\eta$-long Form.
• Figure 5: Contravariant action on resource terms. We omit the explicit typing of morphisms to improve readability. In the variable rule we assume that $\overline{f} : \overline{a} \to \overline{b}.$ In the application rule for the variable, we assume that the value of $\eta$ on $x$ is $\overline{f} \multimap o .$

Theorems & Definitions (77)

• Example 1
• Remark 1
• Definition 1: Reflexive and Transitive Extension
• Definition 2: Labelled Confluence
• Example 2
• Definition 3: Structural Resource Terms
• Remark 2
• Example 3: Typing Some Resource Terms
• Proposition 1: Uniqueness of Derivations
• Proposition 2: Compositionality