<div dir="auto">Thank you, Jon.  I'll have to ponder that but I probably won't have time to grok it.<br><br><div data-smartmail="gmail_signature">---<br>Frank C. Wimberly<br>140 Calle Ojo Feliz, <br>Santa Fe, NM 87505<br><br>505 670-9918<br>Santa Fe, NM</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Oct 15, 2020, 11:20 AM jon zingale <<a href="mailto:jonzingale@gmail.com">jonzingale@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">"What's the function associated with it?  Words like derivative,<br>
differential, directional derivative, etc. mean something to me."<br>
<br>
Let me attempt a brief and likely rough answer. Terms from lambda calculus<br>
correspond to algorithms. There is a model of lambda calculus (as-well-as<br>
full linear logic) where types are interpreted as vector spaces over<br>
algebraically closed fields and the terms as power series on these spaces.<br>
In these models all functions are differentiable and a paper by Ehrhard and<br>
Regnier gives this derivative. Clift and Murfet then go on to flesh out (and<br>
coin) "Sweedler semantics" for this differential linear logic, named after<br>
the mathematician who studied these structures in the domain of Hopf<br>
algebras.<br>
<br>
In light of the recent discussions regarding maximally stateful and purely<br>
functional computation, this work is interesting exactly because of the<br>
differences which exist between theories of lambda calculi and Turing<br>
machines. While they both specify the same class of functions<br>
(Church-Turing), the former knows nothing of intensionality (time or space<br>
complexity, say). Clift and Murfet then follow the Church-Turing<br>
correspondence, using linear logic as the bridge, to show how<br>
differentiation of programs manifests in the real application of program<br>
synthesis, training neural nets for example.<br>
<br>
<br>
<br>
--<br>
Sent from: <a href="http://friam.471366.n2.nabble.com/" rel="noreferrer noreferrer" target="_blank">http://friam.471366.n2.nabble.com/</a><br>
<br>
- .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. .<br>
FRIAM Applied Complexity Group listserv<br>
Zoom Fridays 9:30a-12p Mtn GMT-6  <a href="http://bit.ly/virtualfriam" rel="noreferrer noreferrer" target="_blank">bit.ly/virtualfriam</a><br>
un/subscribe <a href="http://redfish.com/mailman/listinfo/friam_redfish.com" rel="noreferrer noreferrer" target="_blank">http://redfish.com/mailman/listinfo/friam_redfish.com</a><br>
archives: <a href="http://friam.471366.n2.nabble.com/" rel="noreferrer noreferrer" target="_blank">http://friam.471366.n2.nabble.com/</a><br>
FRIAM-COMIC <a href="http://friam-comic.blogspot.com/" rel="noreferrer noreferrer" target="_blank">http://friam-comic.blogspot.com/</a> <br>
</blockquote></div>