Pavel Panchekha


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?


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
Why does the equation you wrote, f x = x, make sense?
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.
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.
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
I agree now that f x makes sense. But does the equality test make sense?
Certainly! Two objects are equal or they are not; it is as simple as that.
Would you say that Stravinsky’s Rite of Spring is either equal to the concept of justice, or it is unequal?
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.
I suppose this is reasonable. Nonetheless, I am bothered by the possibility of comparing two things that are different in kind.
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?

I am satisfied with this definition. But is it empty? Are there α that can be compared, objects x : α, and functions f : α → α?
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

In this case, can you demonstrate a fixed point?
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.

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.