breandan / kotlingrad

🧩 Shape-Safe Symbolic Differentiation with Algebraic Data Types
https://breandan.net/public/masters_thesis.pdf#page=49
Apache License 2.0
530 stars 21 forks source link

Establish the connection with GF(2) #12

Open breandan opened 4 years ago

breandan commented 4 years ago

Kotlin∇ tries to build a mathematically sound type system capturing the relationship between functions and fields. This design should be described more formally, but in short there are two approaches:

  1. The direct approach is to define Fun<X>: Field<X> where X is a member of some algebra over the reals, equipped with the usual arithmetic operators. When applying an operator, it is evaluated eagerly and you get back X immediately. This is a shallow eDSL, evaluated eagerly.
  2. Another way is to treat the function as a member of a field whose elements are themselves functions, e.g. Fun<X>: Field<Fun<X>>. Instead of returning X, operators return Fun<X> by default, which can be evaluated by using invoke(...): X (X and Fun<X> are both fields).

The second representation comes from finite field theory, which has important implications for expression parsing and language design. It would be useful to understand this connection more deeply.

References

breandan commented 2 years ago

An investigation pursuing the connection between GF(2) and automatic differentiation has been undertaken. Preliminary findings indicate that finite fields possess the remarkable ability to both recognize and parse context-free languages, with suspected extensions to LCFRS [Cohen et al. (2016)] and context-sensitive grammars [Tanaka and Fu (1978)]. These findings are noteworthy as they unlock a nearly-optimal compilation pathway from graph computation to Boolean circuits. To our surprise, rootfinding in GF(2) has adjacent applications to robust-parsing, error-correcting codes, type inference and sketch-based program synthesis. Further evidence is needed to support the postulated connection [Considine, 2019] between differential and algebraic geometry unifying derivatives of continuous functions [Leibniz, 1675], derivatives of regular languages [Brzozowski (1964), Antimirov (1996)] and derivatives of algebraic data types [McBride (2011)], however our findings indicate that automatic differentiation has a meaningful interpretation in discrete-valued spaces (contrary to verbal objections by illustrious professors who shall remain unnamed) and lends evidence to support the claim that binary matrix multiplication is a universal programming language conjectured by Considine (2020).