ACG Talk by Yannick Foster from Saarland University

On November 30, we are glad to welcome Yannick Foster from Saarland University for an ACG talk. Yannick investigates, among other subjects, the analysis, formalization, and mechanization of computation in constructive type theory. Yannick Foster will give a talk about "Synthetic computability without choice". The talk starts at 1:30pm, will be online, via Zoom
  • ACG Talk by Yannick Foster from Saarland University
  • 2021-11-30T13:30:00+01:00
  • 2021-11-30T14:30:00+01:00
  • On November 30, we are glad to welcome Yannick Foster from Saarland University for an ACG talk. Yannick investigates, among other subjects, the analysis, formalization, and mechanization of computation in constructive type theory. Yannick Foster will give a talk about "Synthetic computability without choice". The talk starts at 1:30pm, will be online, via Zoom
  • What English Formal Methods
  • When 30-11-2021 from 13:30 to 14:30 (Europe/Amsterdam / UTC100)
  • Where https://cwi-nl.zoom.us/j/85074346559?pwd=dXdZWVpHWXFuMlk4SEFqbFRzTGJOZz09
  • Contact Name
  • Add event to calendar iCal

On November 30, we are glad to welcome Yannick Foster from Saarland University for an ACG talk.
Yannick investigates, among other subjects, the analysis, formalization, and mechanization of computation in constructive type theory.

Yannick Foster will give a talk about "Synthetic computability without choice".

The talk starts at 1:30pm, will be online, and is accessible with the following zoom link:
https://cwi-nl.zoom.us/j/85074346559?pwd=dXdZWVpHWXFuMlk4SEFqbFRzTGJOZz09
Meeting ID: 850 7434 6559
Passcode: 253241

Abstract:
In synthetic computability, pioneered by Richman, Bridges, and Bauer, one develops computability theory without an explicit model of
computation. This is enabled by assuming an axiom equivalent to postulating a function φ to be universal for the space N→N (CTφ , a
consequence of the constructivist axiom CT), Markov’s principle, and at least the axiom of countable choice. Assuming CT and countable choice
invalidates the law of excluded middle, thereby also invalidating classical intuitions prevalent in textbooks on computability. On the
other hand, results like Rice’s theorem are not provable without a form of choice.

In contrast to existing work, we base our investigations in constructive type theory with a separate, impredicative universe of propositions
where countable choice does not hold and thus a priori CTφ and the law of excluded middle seem to be consistent. We introduce various
parametric strengthenings of CTφ , which are equivalent to assuming CTφ and an Snm operator for φ like in the Snm theorem. The strengthened axioms allow developing synthetic computability theory without choice. I will discuss 3 applications of the axioms: Rice's theorem, Post's construction of simple and hypersimple predicates, and an uncomputability proof Kolmogorov complexity.

Notably, the proposed parametric axioms seem to be not in conflict with classical intuitions since they are consequences of the traditional
analytic form of CT.

The list of previous talks is accessible at https://event.cwi.nl/acg/category/presentations

Best regards,
Benjamin