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ó