BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Cambridge University Computing and Technology Soci
ety (CUCaTS)
SUMMARY:Newton's Finger - Dr Conor McBride - University of
Strathclyde
DTSTART;TZID=Europe/London:20171107T194500
DTEND;TZID=Europe/London:20171107T204500
UID:TALK94918AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/94918
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 relationship between
Newton and Leibniz derivatives and computer data t
ypes\, it should be a very interesting talk regard
less of background knowledge! As always\, we will
be heading to the pub after for free drinks\, so d
on't miss out :)\n\nNewton's notion of "divided di
fference"\, 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 consider 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" through an F(-)-structu
re\, gradually turning Ys into Xs. D(F)(X\,Y) repr
esents a snapshot in the process\, where there is
a finger over a place where a Y has been removed b
ut an X has yet to be inserted\, but there are Xs
"left of the finger"\, and Ys "right of the finger
". Just as various limits of the divided differnce
play a useful role in mathematics\, so the same l
imits have computational meaning. Leibniz's deriva
tive F'(X) = D(F)(X\,X) gives the type of "one-hol
e 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 "division by Y with remainder F(0
)"\, but also plays a vital role in Brzozowski's d
ifferential analysis of regular expressions. Lastl
y\, D(F)(X\,1)\, also known as "Fox's free derivia
tive"\, captures F(-) structures under constructio
n\, with stubs right of the finger\, in place of v
alues not yet computed.\n\nIn any functional progr
amming language that treats datatype descriptions
as first-class notions\, we can just do the mathem
atics and extract the functionality in general\, o
nce for all.
LOCATION:MR3\, Centre for Mathematical Sciences\, Wilberfo
rce Road\, Cambridge
CONTACT:Hannah Earley
END:VEVENT
END:VCALENDAR