## By Pavel Panchekha

### 27 December 2013

Share under CC-BY-SA.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.

# Fixed Points, Part 1: What is a Fixed Point?

A fixed point of a function is an input the function maps to itself. When we study the fixed points of a function, we can learn many interesting things about the function itself. This first of four parts defines fixed points, and looks at a few examples.

Part 2: Fixed behaviors
Generalizes a fixed point into a fixed behavior. Every function has a fixed behavior, so behaviors are a better starting point if we want to use fixed points to learn more about functions.
Part 3: Attraction and orders
If we use the iterative method to find fixed points, we will find some fixed points more often than others. The set of all inputs that lead to a fixed behavior is that behavior’s attraction basin. Attraction basins provide a “map” of the input space that lets us better understand the function itself.
Part 4: Stability
An attractive fixed point is easy to find because many inputs lead to it. This means that if you meant to start with a particular input, but messed up and started with a slightly-incorrect input, you’ll still probably end up with the same output. This captures a “stability” that attractive fixed points. Stability is useful for understanding systems design.

## What is a fixed point?

A fixed point of a function `f` is some object `x` so that

```f x = x
```
Gaiane
Why does the equation you wrote, `f x = x`, make sense?
Plautus
I say it does make sense. For we require that `f` is a function, so we can write `f x`, and of course we can test for equality, so we can write `f x = x`.
Gaiane
But not every object is a valid input to `f`. We cannot, for example, discuss what would happen if we incremented a body of water, since bodies of water are not numbers.
Plautus
Indeed, this seems to be a mistake…

Then we say that a fixed point of a function `f` is some object `x`, which is a valid input for `f`, for which

```f x = x
```
Gaiane
I agree now that `f x` makes sense. But does the equality test make sense?
Plautus
Certainly! Two objects are equal or they are not; it is as simple as that.
Gaiane
Would you say that Stravinsky’s Rite of Spring is either equal to the concept of justice, or it is unequal?
Plautus
I would say it is unequal. For the Rite of Spring is a musical composition, and justice is a concept. And things that are different in kind must be different in fact.
Gaiane
I suppose this is reasonable. Nonetheless, I am bothered by the possibility of comparing two things that are different in kind.
Plautus
I understand. Perhaps the theory of types can clarify.

Suppose we can compare objects of type `α`. Then we can say that some `x : α` is a fixed point of `f : α → α`, if

```f x = x
```

In other words, we define

```x “is fixed point of” f ≡ (f x = x)
```

## Are there fixed points?

Gaiane
I am satisfied with this definition. But is it empty? Are there `α` that can be compared, objects `x : α`, and functions `f : α → α`?
Plautus
I endeavor to demonstrate that there are, so:

There are `α` which can be compared. For consider the type `1`, which has the single element `⋆`. Objects of this type can be compared, where they are always equal. Furthermore, if we consider sums `α + β` and pairs `α × β` of comparable types, these types too are comparable. And finally, an inductive type (of which more later) is also comparable. This gives us quite a rich universe of types which are comparable. [1]

There are objects `x : α`. In fact, the type `1` is inhabited (by `⋆`), and so are sums and pairs and some inductions of inhabited types. Thus we have quite a rich universe even of comparable, inhabited types.

Finally, there are functions `f : α → α`. For there exists at least the identity function `id : ∏ α · α → α`, and for some `α` there may exist others.

Thus the study of the fixed points of functions is not vacuous.

## A demonstration

Gaiane
In this case, can you demonstrate a fixed point?
Plautus
Certainly. First, I will demonstrate a simple example.

Consider the type `1`, which is comparable. Then consider `x ≡ ⋆ : 1` and the function `f ≡ id₁ : 1 → 1`. It is true that `f x ≡ id₁ ⋆ ≡ ⋆ ≡ x`, so that `⋆` is a fixed point of `id₁`.

There are functions which are not the identity, which also have fixed points. Consider the type `1 + 1`, which is comparable. Then consider `x ≡ lft ⋆ : 1 + 1`, and `f : 1 + 1 → 1 + 1` defined by

```f (lft a) ≡ (lft a)
f (rgt a) ≡ (lft a)
```

Then `x` is a fixed point of `f`.

Also consider the function `id₁₊₁ : 1 + 1 → 1 + 1`. Both `lft ⋆` and `rgt ⋆` are its fixed points.

Finally, consider the function `g : 1 + 1 → 1 + 1` defined by

```g (lft a) = (rgt a)
g (rgt a) = (lft a)
```

`g` does not have a fixed point.

Gaiane
So the study of fixed points has content, and there are functions with no fixed points, and functions with fixed points one and several.

[1] A rigorous and beautiful treatment of equality in abstract type theory is given in Homotopy Type Theory, which you can read for free.