Fixpoints
Definition
For a function f:XXf : X \to X and x0Xx_0 \in X, tfae:
f(x0)=x0f(x_0) = x_0
x0x_0 is fixed by ff
x0x_0 is a fixpoint of ff
ff fixes x0x_0
Relation to Infinities
Warning: this section is colloquial rather than mathematical. It is intended to aid cognition and intuition, but does not present rigorous mathematics. Fixpoints often turn up alongside infinities. For instance, consider the function cons1:NN=x1x\begin{align*} \text{cons1} &: \mathbb N^* \to \mathbb N^* \\ &= \mathbf x \mapsto 1 \oplus \mathbf x \end{align*} Taking in a sequence of natural numbers, such as [5,0,2][5, 0, 2] and prepending a 11, in this case producing [1,5,0,2][1, 5, 0, 2]. One fixpoint of this function is the list of ininite ones [1,1,1,][1, 1, 1, \dots], because prepending a 11 to this list has no effect. Loose justification for the presence of infinity with relation to fixpoints is to note that the fixpoint equation x=f(x)x = f(x) is in some sense equivalent to the infinite equation x=f(f(  f(f(x))  ))x = f(f(\ \cdots\ f(f(x))\ \cdots\ )) or just x=f(f(  ))x = f(f(\ \cdots\ )) To see why, note that we can go from the first equation to the second with infinitely-repeated substitution, and we can go from the second to the first with a single substitution. This means we can roughly interpret “fixpoint of ff" to mean “value obtained by infinitely-repeated applications of ff".


Referenced by: