Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: event: Topos Colloquium

Topic: Special Seminar in Honor's of Dana Scott's 90th Birthday


view this post on Zulip Steve Awodey (Oct 08 2022 at 18:33):

On Tuesday, October 11th, Topos will be celebrating Dana Scott's 90th birthday with a special seminar by Gordon Plotkin, titled "Does recursion help?". The seminar will be held both online and in person at the Topos Institute's Berkeley office, with Gordon and Dana both present in person. Dana will say some opening words before Gordon's talk.

An abstract for Gordon's talk, and links to join via Zoom or YouTube
livestream, are below. If you would like to attend in person, please email
juliet@topos.institute to register as a visitor.

See https://topos.site/berkeley-seminar/


Date: Tuesday October 11th, 2022
Time: 1700 UTC (10am Berkeley time)
Zoom Link:
https://topos-institute.zoom.us/j/87874851972?pwd=eWRjZlUvQWJoNmJFdHgycE1mUDEvQT09
Password: happybday
YouTube stream: https://youtu.be/n7moEQtv3qU
--
Title: Does recursion help?
Speaker: Gordon Plotkin

Abstract: As everyone knows, Alonzo Church proposed that the effectively calculable natural number functions are those definable in the untyped lambda calculus. (He used Church numerals to represent natural numbers.) The lambda-definable functions were shown to be the same as the Gödel-Herbrand general recursive functions and the same as the functions computable by Turing machines. The fixed-point combinator Y is crucial for the proofs, as it enables functions to be defined recursively.

If we switch to the typed lambda-calculus the situation changes drastically.
Helmut Schwichtenberg and Richard Statman showed that only the extended
polynomials can then be defined (they used a typed version of the Church
numerals).

It is natural, therefore, to ask what happens if one adds typed fixed-point
combinators to the typed lambda calculus. We present an answer to this
question. Our answer makes essential use of Dana Scott's domain theory to
model the fixed-point combinators.