breandan/kotlingrad

Establish the connection with GF(2)

breandan opened this issue · 1 comments

breandan commented

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

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).