BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Paul Taylor (University of Birmingham) DTSTART:20240426T100000Z DTEND:20240426T110000Z DTSTAMP:20260408T001444Z 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