Computability in Europe 2006
Logical Approaches to Computational Barriers

Invited Plenary Talk:
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

websites: Arnold Beckmann 2006-06-21