Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Programming Backpropagation with Reverse Handlers for Arrows

Takahiro Sanada, Keisuke Hoshino, Kenshin Hirai, Shin-ya Katsumata

TL;DR

A new programming language is introduced and a novel handler mechanism for arrows for implementing backpropagation is introduced, together with new algebras of strong promonads on reverse differential restriction categories (RDRCs), whose string diagrams provide a formal graphical syntax and semantics for neural networks.

Abstract

We introduce a new programming language and its categorical semantics in order to design and implement neural networks within the framework of algebraic effects and handlers for arrows. Our language enables us to construct neural networks symbolically, in the same manner as algebraic effects, and to assign implementations -- such as backpropagation computations -- to them via handlers. The advantage of this language design is that network descriptions become abstract and high-level, while implementations can be flexibly assigned to networks. We establish a rigorous foundation for our language by developing a type system, an operational semantics, a categorical semantics, and soundness and adequacy theorems. The technical core is the introduction of \emph{reverse handlers}, a novel handler mechanism for arrows for implementing backpropagation, together with new algebras of strong promonads on reverse differential restriction categories (RDRCs), whose string diagrams provide a formal graphical syntax and semantics for neural networks.

Programming Backpropagation with Reverse Handlers for Arrows

TL;DR

A new programming language is introduced and a novel handler mechanism for arrows for implementing backpropagation is introduced, together with new algebras of strong promonads on reverse differential restriction categories (RDRCs), whose string diagrams provide a formal graphical syntax and semantics for neural networks.

Abstract

We introduce a new programming language and its categorical semantics in order to design and implement neural networks within the framework of algebraic effects and handlers for arrows. Our language enables us to construct neural networks symbolically, in the same manner as algebraic effects, and to assign implementations -- such as backpropagation computations -- to them via handlers. The advantage of this language design is that network descriptions become abstract and high-level, while implementations can be flexibly assigned to networks. We establish a rigorous foundation for our language by developing a type system, an operational semantics, a categorical semantics, and soundness and adequacy theorems. The technical core is the introduction of \emph{reverse handlers}, a novel handler mechanism for arrows for implementing backpropagation, together with new algebras of strong promonads on reverse differential restriction categories (RDRCs), whose string diagrams provide a formal graphical syntax and semantics for neural networks.
Paper Structure (31 sections, 14 theorems, 122 equations, 10 figures)

This paper contains 31 sections, 14 theorems, 122 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Challenge 1
  3. Challenge 2
  4. Challenge 3
  5. Overview
  6. Abstract Design of Neural Networks via Algebraic Effects for Arrows
  7. Handlers vs Reverse Handlers
  8. Implementation of inference
  9. Implementation of backpropagation
  10. Monads vs Arrows
  11. Monads
  12. Promonads
  13. Syntax
  14. Examples of Neural Networks
  15. Operational Semantics
  16. ...and 16 more sections

Key Result

Lemma 5.3

For well-typed values $\Gamma \vdash W : B$ and $\Gamma \vdash V : A$ and a well-typed term $\Gamma, x : A \vdash N : B$, the judgment $\Gamma \vdash {W}.\mathcal{R}_{V}(x.N) : A$ is derivable.

Figures (10)

  • Figure 1: An illustration of a MLP with three layers.
  • Figure 2: Typing rules for terms
  • Figure 3: Typing rules for commands and handlers
  • Figure 4: Depth of reverse handlers
  • Figure 5: Size of derivation trees
  • ...and 5 more figures

Theorems & Definitions (50)

  • Definition 3.1
  • Definition 3.2: signatures of function symbols
  • Definition 3.3: signatures of operation symbols
  • Definition 3.4: terms and commands
  • Definition 3.5: typing
  • Definition 3.6: depth of reverse handler
  • Definition 3.7: size of derivation trees
  • Definition 5.1
  • Definition 5.2: AbadiPlotkin2019
  • Lemma 5.3: AbadiPlotkin2019
  • ...and 40 more