From categorized neural architectures to subexponential proof theory
Provides a formal logical foundation for the architecture-to-category-to-logic programme, enabling theorem-proving about neural architectures with differentiated memory and context, but remains theoretical and incremental.
The paper extracts a subexponential proof theory from categorized neural architectures by reading off structural rules from zone-labelled blocks, proving that the resulting category is symmetric monoidal, the proof system admits cut elimination, and derivations are sound with respect to architectural diagrams.
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.