[FRIAM] now it's personal

[jon zingale]

"What's the function associated with it?  Words like derivative,
differential, directional derivative, etc. mean something to me."

Let me attempt a brief and likely rough answer. Terms from lambda calculus
correspond to algorithms. There is a model of lambda calculus (as-well-as
full linear logic) where types are interpreted as vector spaces over
algebraically closed fields and the terms as power series on these spaces.
In these models all functions are differentiable and a paper by Ehrhard and
Regnier gives this derivative. Clift and Murfet then go on to flesh out (and
coin) "Sweedler semantics" for this differential linear logic, named after
the mathematician who studied these structures in the domain of Hopf
algebras.

In light of the recent discussions regarding maximally stateful and purely
functional computation, this work is interesting exactly because of the
differences which exist between theories of lambda calculi and Turing
machines. While they both specify the same class of functions
(Church-Turing), the former knows nothing of intensionality (time or space
complexity, say). Clift and Murfet then follow the Church-Turing
correspondence, using linear logic as the bridge, to show how
differentiation of programs manifests in the real application of program
synthesis, training neural nets for example.



--
Sent from: http://friam.471366.n2.nabble.com/