From categorized neural architectures to subexponential proof theory

TL;DR

This paper develops a method to derive a subexponential logic from neural architecture categories, linking architecture design with proof theory through categorical and logical frameworks.

Contribution

It introduces a novel approach to extract subexponential signatures from neural architectures, establishing a formal connection between architecture categorization and logical proof systems.

Findings

The architectural category is shown to be symmetric monoidal.

The proof system admits cut elimination.

Derivations are sound with respect to categorical diagrams.

Abstract

We study a resource-sensitive fragment of the problem of extracting a logical discipline from a class of neural architectures by passing through categorization. The starting point is not a pre-existing logic but a category of zone-labelled parametrised blocks together with a disciplined record of which forms of copying, discarding, and zone coercion are architecturally licensed. From this categorized architecture we read off a subexponential signature and then define a tensorial sequent calculus whose structural rules are indexed by the extracted zones. The paper proves three kinds of results. First, the resulting architectural category is symmetric monoidal. Second, the extracted proof system admits cut elimination. Third, derivations are sound with respect to the licensed categorical diagrams generated by the architectural discipline. The outcome is a theorem-bearing core of the architecture-to-category-to-logic programme: subexponential structure is not postulated in advance but read from categorical data encoding differentiated memory and context behaviour.