From Brouwer's Thesis to the Fan Functional

Add to your list(s) Download to your calendar using vCal

• Ulrich Berger (Swansea University)
• Friday 21 February 2020, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

If you have a question about this talk, please contact Vincent Rahli.

The usual formulation of Brouwer’s Thesis (‘every bar is inductive’) uses quantification over infinite sequences of natural numbers to define what a bar is. We propose an alternative formulation that avoids infinite sequences and instead uses a coinductive definition to express the bar property. This coinductive formulation leads to a (new?) abstract version of Bar Induction which, combined with a modality for trivial truth, makes it possible to prove constructively that every continuous fuction on Cantor space is uniformly continuous. The computational content of that proof is a purely functional implementation of Tait’s Fan Functional computing the minimal modulus of uniform continuity of such functions.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.