 ## By Pavel Panchekha

### 27 December 2013

Share under CC-BY-SA.

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

###### Series

This is post 1 of the Fixed Points series.

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.

## 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. 

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.

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