Fixed Points, Part 1: 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)

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.

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.