BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Newton's Finger - Dr Conor McBride - University of Strathclyde
DTSTART:20171107T194500Z
DTEND:20171107T204500Z
UID:TALK94918@talks.cam.ac.uk
CONTACT:Hannah Earley
DESCRIPTION:This is CUCaTS' first talk of the year\, presented by Dr Conor
  McBride! The talk title is 'Newton's Finger' and will explore the relatio
 nship between Newton and Leibniz derivatives and computer data types\, it 
 should be a very interesting talk regardless of background knowledge! As a
 lways\, we will be heading to the pub after for free drinks\, so don't mis
 s out :)\n\nNewton's notion of "divided difference"\, D(F)(X\,Y) = (F(Y) -
  F(X))/(Y-X) makes perfect sense for container-like data structures\, F(-)
 \, even in the absence of "subtraction" or "division". We may rather consi
 der solutions to the equation (or type isomorphism)\n\nF(Y) + D(F)(X\,Y)*X
   = Y*D(F)(X\,Y) + F(X)\n\nwhich witnesses how to travel "left-to-right" t
 hrough an F(-)-structure\, gradually turning Ys into Xs. D(F)(X\,Y) repres
 ents a snapshot in the process\, where there is a finger over a place wher
 e a Y has been removed but an X has yet to be inserted\, but there are Xs 
 "left of the finger"\, and Ys "right of the finger". Just as various limit
 s of the divided differnce play a useful role in mathematics\, so the same
  limits have computational meaning. Leibniz's derivative F'(X) = D(F)(X\,X
 ) gives the type of "one-hole contexts" for an X in an F(X). Meanwhile\, D
 (F)(0\,Y) (i.e.\, nothing left of the finger) gives a formal notion of "di
 vision by Y with remainder F(0)"\, but also plays a vital role in Brzozows
 ki's differential analysis of regular expressions. Lastly\, D(F)(X\,1)\, a
 lso known as "Fox's free deriviative"\, captures F(-) structures under con
 struction\, with stubs right of the finger\, in place of values not yet co
 mputed.\n\nIn any functional programming language that treats datatype des
 criptions as first-class notions\, we can just do the mathematics and extr
 act the functionality in general\, once for all.
LOCATION:MR3\,  Centre for Mathematical Sciences\, Wilberforce Road\, Camb
 ridge
END:VEVENT
END:VCALENDAR
