Locally invertible floating point functions

Is the function x x + 2 invertible? Sure, its inverse is the function x x - 2.

Is the Python function

 def f(x): return x + 2

invertible? Not always.

You might reasonably think the function

 def g(x): return x - 2

is the inverse of f, and it is for many values of x. But try this:

 >>> x = 2**53 - 1.0 >>> g(f(x)) - x -1.0

The composition of f and g does not give us x back because of the limited length of a floating point significand. See Anatomy of a floating point number.

The function f as a function between floating point numbers is locally invertible. That is, it is invertible on a subset of its domain.

Now let's look at the function

 def f(x): return x*x

Is this function invertible? There is a function, namely sqrt that serves as an inverse to f for many values of x, but not all x. The function sqrt is a partial function because although it is ostensibly a function on floating point numbers, it crashes for negative inputs. The function's actual domain is smaller than its nominal domain.

Locally invertible functions are an inevitable part of programming, and are awkward to reason about. But there are tools that help. For example, inverse semigroups.

According to nLab

An inverse semigroup is a semigroup S such that for every element sS, there exists a unique inverse" s* S such that s s* s = s and s* s s*= s*.

The canonical example of an inverse semigroup, and in some sense the only example, is the following, also from nLab.

For any set X, let I(X) be the set of all partial bijections on X, i.e. bijections between subsets of X. The composite of partial bijections is their composite as relations (or as partial functions).

This is the only example in the sense that the Wagner-Preston theorem says every inverse semigroup is isomorphic to a group of this form.

In our case, the set X is the set of representable floating point numbers, and locally invertible functions are functions which are invertible, but only when restricted to a subset of X.

The post Locally invertible floating point functions first appeared on John D. Cook.