Notices by maonu (maonu@mathstodon.xyz)

One can use the Escardó-Oliva functional to write an assembler; it handles the "backtracking." On X86 the encoding of a jump instruction can vary depending on the distance of the jump... which in turn depends on the size of the encoding! So you need more than just the tardis monad

http://blog.vmchale.com/article/escardo-oliva-functional

@julesh kinda crasy to see logic so central, I guess FP has been carrying the torch for "languages we can treat theoretically" but still cool!

backprop/machine learning fits into functional programming as "new form of control"/effect(?) with linear negation the dual from linear algebra

basically "peek around locally on differentiable stuff and use that to improve the program"

Turns out to resemble logic programming's "AI" maybe, cf. Pédrot/Kerjean's recent dialectica work

https://hal.science/hal-02400927/document

dialectica puts counter-witnesses where modus ponens (aka cut elimination, \( \beta \)-reduction is...

differential dialectica shows the chain rule in the same place!

Lots of depth in this work

https://inria.hal.science/hal-04583978/document

Gödel’s dialectica interpretation looks like pattern-match deconstruction—counter-“witness” (aka way to deal with, accept as an argument) to \( A \vee B \) is *both* a way to deal with A and a way to deal with B (after inspecting tags)

https://link.springer.com/article/10.1007/BF02025118

Pédrot/Kerjean point out that dialectica places chain rule where dialectica translation of modus ponens (aka beta reduction) needs counterwitnesses.

Seems interesting “machine learning reasoning” people haven’t caught up?

van Laarhoven (2009) describes lenses based on continuation-passing style (CPS) and how to compose them

@julesh points out this looks like how modus ponens/cut elimination works in Gödel's dialectica interpretation (1958)

https://julesh.com/2018/08/16/lenses-for-philosophers/