BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Paul Taylor (University of Birmingham)
DTSTART;VALUE=DATE-TIME:20240426T100000Z
DTEND;VALUE=DATE-TIME:20240426T110000Z
DTSTAMP;VALUE=DATE-TIME:20241016T082956Z
UID:TheoryCSBham/18
DESCRIPTION:Title: Free algebras for functors\, with not an ordinal in sight\nby Pa
ul Taylor (University of Birmingham) as part of University of Birmingham t
heoretical computer science seminar\n\nLecture held in Old Gym\, LG10.\n\n
Abstract\nMartin Escardo challenged me to make Pataraia's fixed point\nthe
orem "predicative". Whilst I have never understood the\nmotivation for th
at notion\, I have eliminated one instance\nof impredicativity and isolate
d the infinitary aspects to\na single specific directed join.\n\nSo then I
looked for the categorical version. Pataraia's\nidea plays a quite small
part: the construction uses ideas\nfrom categorical algebra since its orig
ins\, and if I were\nto credit one person it would be Joachim Lambek.\n\nT
he problem breaks into two parts\, one finitary and the\nother infinitary.
The infinitary part says that the\ncategory of pointed endofunctors of a
small category\nwith coequalisers is filtered\, so has a terminal object\
nif the given category has the required filtered colimit.\nThis is probabl
y widely applicable as an alternative to\ntransfinite methods.\n\nThe fini
tary construction is that of fragments of the\ninitial algebra. It may be
done in several ways\, but\none is to consider coalgebras for the given f
unctor\nthat are have a cone over all algebras for it. We\nidentify a "sp
ecial condition" that this construction\nsatisfies and that ensures that t
he terminal endofunctor\n(applied to any object) yields the terminal objec
t of\nthe finitary category\, which is the required initial\nalgebra of th
e functor.\n\nThe hope is that a similar finitary category of\npartial mod
els could be found for more complex\nsystems of algebra and logic and that
these would\ncorrespond to the intermediate stages in proof\ntheoretic ar
guments for normalisation\, cut\nelimination etc.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/18/
END:VEVENT
END:VCALENDAR