Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

From categorized neural architectures to subexponential proof theory

Carlos Ramírez Ovalle

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.

From categorized neural architectures to subexponential proof theory

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.

Paper Structure

This paper contains 8 sections, 14 theorems, 336 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Categorized architectures
  3. Typed resource contexts and the architectural category
  4. Coherent zone disciplines and extracted subexponential data
  5. The extracted proof theory
  6. Soundness in the categorized architecture
  7. Positioning with respect to related work
  8. Conclusion

Key Result

Lemma 2.2

For all typed resource contexts $\Gamma$ and $\Delta$, there is a canonical isomorphism

Figures (1)

  • Figure 1: Sequential composition in $\mathbf{Arch}_Z$.

Theorems & Definitions (53)

  • Definition 2.1: Typed resource context
  • Lemma 2.2
  • proof
  • Definition 2.3: Parametrised resource block
  • Definition 2.4: Isomorphism of parametrised blocks
  • Lemma 2.5
  • proof
  • Definition 2.6: The architectural category $\mathbf{Arch}_Z$
  • Proposition 2.7
  • proof
  • ...and 43 more