• Stars
    star
    196
  • Rank 198,553 (Top 4 %)
  • Language
    TeX
  • Created almost 7 years ago
  • Updated almost 4 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

The simple essence of automatic differentiation

The simple essence of automatic differentiation

Abstract

Automatic differentiation (AD) in reverse mode (RAD) is a central component of deep learning and other uses of large-scale optimization. Commonly used RAD algorithms such as backpropagation, however, are complex and stateful, hindering deep understanding, improvement, and parallel execution. This talk develops a simple, generalized AD algorithm calculated from a simple, natural specification. The general algorithm is then specialized by varying the representation of derivatives. In particular, applying well-known constructions to a naive representation yields two RAD algorithms that are far simpler than previously known. In contrast to commonly used RAD implementations, the algorithms defined here involve no graphs, tapes, variables, partial derivatives, or mutation. They are inherently parallel-friendly, correct by construction, and usable directly from an existing programming language with no need for new data types or programming style, thanks to use of an AD-agnostic compiler plugin.

More Repositories

1

talk-2015-essence-and-origins-of-frp

A keynote talk for LambdaJam 2015 (July 15--16)
TeX
412
star
2

lambda-ccc

Convert lambda expressions to CCC combinators
Haskell
144
star
3

talk-2014-lambdajam-denotational-design

Talk material for LambdaJam 2014/2015 on denotational design
TeX
117
star
4

talk-2014-bayhac-denotational-design

Denotational Design: from programs to meanings
TeX
100
star
5

denotational-hardware

Denotational hardware design in Agda
Agda
95
star
6

MemoTrie

Trie-based memo functions
Haskell
87
star
7

Collaboration

Play/learn/work with me
87
star
8

talk-2021-can-tensor-programming-be-liberated

Talk: "Can Tensor Programming Be Liberated from the Fortran Data Paradigm?"
TeX
64
star
9

talk-2015-haskell-to-hardware

From Haskell to Hardware via CCCs
TeX
57
star
10

talk-2018-deep-learning-rebooted

"A Functional Reboot for Deep Learning", an invited talk for Summer BOB 2019 in Berlin
TeX
52
star
11

linalg

Linear algebra after Fortran
Haskell
47
star
12

talk-2016-generic-fft

A talk on type-generic FFT in Haskell
TeX
45
star
13

vector-space

Vector & affine spaces, linear maps, and derivatives
Haskell
44
star
14

paper-2021-language-derivatives

Paper and talk
TeX
42
star
15

felix

Agda category theory library for denotational design
Agda
42
star
16

paper-2020-higher-order-ad

Higher-order, higher-order automatic differentiation
TeX
30
star
17

Fran

First Haskell implementations of Fran/FRP
Haskell
30
star
18

circat

A categorical framework for circuit construction
Haskell
29
star
19

talk-2020-calculating-compilers-categorically

A talk
TeX
27
star
20

talk-2015-more-elegant-frp

A more elegant specification for FRP
TeX
24
star
21

shady-gen

Functional GPU programming - DSEL & compiler
Haskell
22
star
22

essence-of-ad

Paper: The simple essence of automatic differentiation
TeX
22
star
23

2017-talk-teaching-new-tricks-to-old-programs

Keynote talk for Lambda Jam 2017 in Sydney
TeX
19
star
24

convolution-paper

Generalized Convolution and Efficient Language Recognition
HTML
17
star
25

agda-machines

Denotational-categorical design of verified hardware in Agda
Agda
17
star
26

quotes

My favorite quotes
Makefile
16
star
27

total-map

Finitely represented /total/ maps
Haskell
15
star
28

denotational-arithmetic

Puzzle: arithmetic via denotational design
Agda
15
star
29

talk-2016-generic-parallel-scan

Talk on generic parallel scan
TeX
14
star
30

agda-generic-parallel

Generic parallel algorithms in Agda
Agda
14
star
31

linear-map-gadt

Linear maps as a GADT
Haskell
14
star
32

unamb

Unambiguous choice
Haskell
12
star
33

talk-2023-galilean-revolution

A Galilean revolution for computing: Unboundedly scalable reliability and efficiency
TeX
12
star
34

shady-graphics

Functional GPU programming - graphics
Haskell
12
star
35

calculating-compilers-agda

Calculating compilers categorically, in Agda
Agda
12
star
36

shaped-types

Experimenting with statically shaped types, GHC specialization, and reification
Haskell
9
star
37

functor-combo

Functor combinators with tries & zippers
Haskell
9
star
38

TypeCompose

Type composition classes & instances & misc
Haskell
9
star
39

talk-2017-generic-functional-parallel

A talk for ICFP 2017
TeX
8
star
40

generic-parallel-functional

Paper on generic parallel functional programming
TeX
8
star
41

DependentTypesAtWork-exercises

Exercises from "Dependent Types at Work"
Agda
7
star
42

ty

Typed type representations and equality proofs
Haskell
7
star
43

generic-fft

FFTs for functor combinators
Haskell
7
star
44

talk-2016-fp-parallel

Intro talk on functional programming, emphasizing parallelism
TeX
7
star
45

shady-examples

Playing with shady
Haskell
7
star
46

data-treify

Reify a recursive data structure into an explicit graph.
Haskell
7
star
47

NumInstances

Instances of numeric classes for functions and tuples
Haskell
7
star
48

type-unary

Type-level and typed unary natural numbers, vectors, inequality proofs
Haskell
6
star
49

reify-core-examples

Examples of core reification and Haskell-to-hardware compilation
Haskell
6
star
50

shady-render

Functional GPU programming - rendering
Haskell
6
star
51

numbers-vectors-trees

code for a blog post series
Haskell
6
star
52

felix-boolean

Agda
6
star
53

talk-2012-reimagining-matrices

A talk deriving matrix addition and multiplication from semantic specification
TeX
6
star
54

lub

information operators: least upper bound (lub) and greatest lower bound (glb)
Haskell
6
star
55

shady-tv

Functional GPU programming - user interfaces
Haskell
6
star
56

agda-linear

Denotative linear algebra in Agda
Agda
6
star
57

graphics-concat

Graphics via compiling-to-categories
6
star
58

gitit-to-blog

Convert a gitit-friendly markdown page to HTML, including various transformations
Haskell
6
star
59

reification-rules

GHC Core reification via rules
Haskell
6
star
60

talk-2012-folds-and-unfolds

Talk on folds & unfolds (and combinations) for general algebraic data types
Haskell
6
star
61

TV

Tangible Values -- composable interfaces
Haskell
5
star
62

talk-2014-elegant-memoization

A talk: "Elegant memoization"
TeX
5
star
63

adders-and-arrows

Composing adders with commutative diagrams
TeX
5
star
64

agda-fft

Verified FFT in Agda
Agda
5
star
65

talk-2017-compiling-to-categories

A talk for ICFP 2017
TeX
5
star
66

uniform-pair

Uniform pairs with class instances
Haskell
5
star
67

agda-cat-linear

Linear map categories in Agda
Agda
4
star
68

contractive

Experiments in contractivity and fixed points
Agda
4
star
69

ordinal-gitit-plugin

Gitit plugin: Format ordinals like 21st
Haskell
4
star
70

DeepArrow

Arrows for "deep application"
Haskell
4
star
71

simple-parallel

Simple model for parallel computation
Agda
4
star
72

.emacs.d

My Emacs environment
Emacs Lisp
4
star
73

nim

The game of Nim in Agda
Agda
4
star
74

Boolean

Generalized booleans
Haskell
4
star
75

agda-play

Miscellaneous experiments in Aga
Agda
4
star
76

gitit-birdtrack-shift

Gitit plugin: deconfuse HTML vs inverse-birdtrack
Haskell
3
star
77

hermit-extras

Some helpers for GHC Core and HERMIT
Haskell
3
star
78

plugin-import-id

GHC plugin experiment
Haskell
3
star
79

equation-transfer

Transferring equational properties backward through homomorphisms
Agda
3
star
80

fix-symbols-gitit

Gitit plugin: Turn some Haskell symbols into Greek and pretty math symbols.
Haskell
3
star
81

gitit-comment

Gitit plugin: remove comments like <!--[ ... ]-->
Haskell
3
star
82

ftree

Depth-typed functor-based trees, both top-down and bottom-up
Haskell
3
star
83

Fran-via-deepfire

Functional Reactive Animation
Haskell
3
star
84

type-encode

HERMIT-based GHC plugin: convert data types to sum-of-products form
Haskell
3
star
85

webgl-experiment-1

Some experiments with WebGL, toward resurrecting Shady
JavaScript
2
star
86

GtkTV

Gtk-based GUIs for Tangible Values
Haskell
2
star
87

applicative-numbers

Applicative-based numeric instances
Haskell
2
star
88

GtkGLTV

OpenGL support for Gtk-based GUIs for Tangible Values
Haskell
2
star
89

state-trie

Memoizing state monad
Haskell
2
star
90

talk-2012-linear-timing

Talk for IFIP Working Group 2.8
Haskell
2
star
91

agda-toggle

Simple experiments with recursively defined "circuits"
Agda
2
star
92

ShowF

Show for * -> *
Haskell
2
star
93

to-haskell

A type class and some utilities for generating Haskell code
Haskell
2
star
94

reify-core

Reify GHC Core into a GADT for further processing
Haskell
2
star
95

talk-2013-understanding-parallel-scan

Talk: "Understanding efficient parallel scan"
TeX
2
star
96

pixie

Circuit pictures
Haskell
2
star
97

monomorph

A GHC plugin for monomorphization
Haskell
2
star
98

agda-latex

Template for Agda-based talk and paper
TeX
2
star
99

dict-test

Test HERMIT-based dictionary construction
Haskell
2
star
100

cmos

Experiments in CMOS design
Agda
1
star