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

Ssuch that for every elements∈S, there exists a unique “inverse”s* ∈Ssuch thats s*s=sands*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*.