Computability in Europe 2006
Logical Approaches to Computational Barriers

Print current page  Print this page

Invited Plenary Talk:
Inverting monotone continuous functions in constructive analysis

Speaker: Helmut Schwichtenberg

Abstract

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 Valid HTML 4.01! Valid CSS! eXTReMe Tracker hit counters by www.free-counters.net