Inverting Monotone Continuous Functions in Constructive Analysis

We prove constructively (in the style of Bishop) that every monotone continuous function with a uniform modulus of increase 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.

• Type: Conference
• Year: 2006
• Where: CIE
• Authors: Helmut Schwichtenberg
• Keywords: Applied Computing, CIE 2006, Continuous Functions, Continuous Inverse, Monotone Continuous Function