Abstracts.2018.SeeminglyImpossible

Seemingly impossible functional programs

by Ayberk Tosun

The set ℕ → Bool does not admit a decidable equality as this would amount to exhausting the infinite domain. Surprisingly though, the set (ℕ → Bool) → ℕ does admit a decidable equality even though the domain is infinite. Implementations of such algorithms that decide equality of infinite function types have been termed "seemingly impossible functional programs" by Martín Escardó. In my talk, I will present examples of such seemingly impossible programs and discuss why it is in fact possible for them to exist, following the blog post of the same name by Escardó.

• Link to the original blog post by Martín Escardó

Further Reading

• Escardó, 2007. Infinite sets that admit fast exhaustive search

  Investigates which kinds of infinite sets admit exhaustive search and gives algorithms for building searchable sets.

• Escardó, 2004. Synthetic topology of data types (and classical spaces)

  Comprehensive lecture notes on synthetic topology and the CS-topology connection in the sense of domain theory. Gives concrete examples in Haskell in the same manner as the blog post.

• Normann, 2004. Computing with functionals — computability theory or computer science?

  Historical survey of higher-type computability.

• Escardó and Oliva, 2010. What sequential games, the Tychonoff theorem, and the double-negation shift have in common

  A fun tutorial paper by Escardó that explains how the function that computes the product of selection functions can be seen (1) as the computational manifestation of the Tychonoff Theorem, (2) how one can generate optimal plays of sequential games using this function, and (3) its relation to the "computational content" of the double-negation translation. It also turns out that this function was already in the Haskell prelude under the name sequence!