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:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:The way of the empty proof - Jean-Louis Lassez
DTSTART;TZID=Europe/London:20191011T140000
DTEND;TZID=Europe/London:20191011T150000
UID:TALK128332AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/128332
DESCRIPTION:There is a strong conceptual link between proofs a
nd algorithms and their eventual simplicity. With
the right data structures algorithms become simple
r\, sometimes much simpler. With the right definit
ions proofs become simpler to the point where they
might vanish. But there is a dark side to simplic
ity. If you find a simple proof or a simple algori
thm\, it may be dismissed as being “simple”\, even
if it is new and interesting. The challenge is to
find a simple proof or a simple algorithm that br
ings a solution to a hard problem. Examples are dr
awn from Automata Theory applied to Theater\, word
equations arising from Lie Algebras\, coding theo
ry as applied to the genetic code. And a striking
example where a graphic visualization of Symbolic
Gaussian elimination leads to a better understandi
ng of Ershov’s theorem and Perron Frobenius’ theor
em as most relevant to Google’s search engine. In
Linear programming and Geometry we have major theo
rems and algorithms and open problems which can be
viewed in much simpler ways using an old eliminat
ion algorithm due to Fourier\, when we understand
the link between Fourier elimination and Gaussian
elimination\, when inequalities are in fact implic
it equalities.
LOCATION:FW26
CONTACT:Anuj Dawar
END:VEVENT
END:VCALENDAR