"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/ - .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. . FRIAM Applied Complexity Group listserv Zoom Fridays 9:30a-12p Mtn GMT-6 bit.ly/virtualfriam un/subscribe http://redfish.com/mailman/listinfo/friam_redfish.com archives: http://friam.471366.n2.nabble.com/ FRIAM-COMIC http://friam-comic.blogspot.com/
