Logical Approaches to Computational Barriers

Inverting monotone continuous functions in constructive analysis

Speaker:
| Helmut Schwichtenberg |

We prove constructively (in the style of Bishop) that every monotone continuous function with a lower bound on its slope has a continuous inverse. The proof is formalized, and a realizing term extracted. This term can be applied to concrete continuous functions and arguments, and then normalized to a rational approximation of say a zero of a given function. It turns out that even in the logical term language `normalization by evaluation}'is reasonably efficient.

websites: Arnold Beckmann | 2006-06-21 |