# What is a fixed point in the context of Roger's fixed-point theorem?

In the Wikipedia article on Rogers' theorem, it is stated that all total computable functions have a fixed point. The notation is a little hard for me to understand; a symbol is used that is used to denote "semantic equivalence." I do not know what semantic equivalence is; I would appreciate it if someone could shed some light on what a fixed point is in this context, and on what semantic equivalence is in this context.

• My guess is that semantic equivalence just means, "the two programs compute the same function," but I don't know if that's right.
– user7317
Commented Mar 16, 2014 at 20:33

The notation is explained in the Wikipedia entry (though regrettably after its first use): for partial functions $f,g$, we say that $f\simeq g$ if for all inputs $x$, $f$ halts on $x$ iff $g$ halts on $x$, and if both halt on an input $x$, then $f(x) = g(x)$. In other words, $f$ and $g$ compute the same partial function, and so they are semantically equivalent: they result in the same outcome.

The idea behind semantic equivalence is that two programs might be different but could be equivalent in the sense that they compute the same function. For example, if there are two statements $x \gets 0; y \gets 1$ and we switch their order to $y \gets 1; x \gets 0$ then the resulting programs are different syntactically but equivalent semantically.

Roger's theorem shows that for every total computable function $P$, which we think of as a transformation rule for programs, there is some program $e$ that is equivalent to $P(e)$. The rest of the Wikipedia entry explains why this is useful.

Semantic equivalence can be contrasted with syntactic equivalence. You can think of something as being syntactically equivalent if it "looks" the same (the syntax of some expression is equivalent). Semantic equivalence means that something is equivalent in meaning.

Fixed-point semantics are generally used to describe loops and recursion for the denotational semantics of a programming language. When we are trying to define a recursive function, such as the factorial function $fact$, we cannot just write $fact(n) = \text{ if } n \leq 0 \text{ then } 1 \text { else } n \cdot fact(n-1)$ and be done, because this is not a definition of $fact$, it is a recursive equation. In order to define $fact$, we actually need to construct it as the union of a sequence of partial functions $F^i$.

I think to really understand how this works, you should try to think of functions as sets. For $fact$, we define $F^0(\emptyset) = \emptyset$, and $$F^{i+1}(\emptyset) = \text{ if } n \leq 0 \text{ then } 1 \text { else } n \cdot F^{i}(\emptyset)(n-1),$$ where $F^{i}(\emptyset)(n-1)$ denotes the application of the function given by $F^{i}(\emptyset)$ on $n-1$. Now we have that $fact = \bigcup_{i \geq 0} F^i(\emptyset)$, where $F: (\mathbb{N} \rightharpoonup \mathbb{N}) \rightarrow (\mathbb{N} \rightharpoonup \mathbb{N})$ (note that $\rightharpoonup$ denotes a partial function). Given our definition of $F$, each function $F^0, F^1, F^2, F^3, F^4,...$ is equivalent to

\begin{align} \emptyset &= \emptyset\\ F(\emptyset) &= \{ (0, 1) \}\\ F(F(\emptyset)) &= \{ (0, 1), (1, 1) \}\\ F(F(F(\emptyset))) &= \{ (0, 1), (1,1), (2,2) \}\\ F(F(F(F(\emptyset)))) &= \{ (0, 1), (1,1), (2,2), (3,6) \}\\ ... \end{align} As you can see, $F^4$ contains solutions up to $n=3$ for $fact$. The union of all of these functions is $fact$. Therefore, we say that $fact$ is the fixed-point of $F$ because if you apply $F$ to $fact$, you get $fact$, or $F(fact) = fact$.

In the example from the wiki article, $e = fact$, and $\varphi_{fact}$ is the denotation of $fact$. The denotation of some expression is the mathematical definition of that expression. We just defined $fact$ mathematically. Therefore we can define the denotation of $fact$ (using the notation from the wiki article) as $\varphi_{fact} = \bigcup_{i \geq 0} F^i(\emptyset)$. Since $fact$ is the fixed-point of $F$, we also have that $\varphi_{fact} = \varphi_{F(fact)}$, which implies that $fact$ is semantically equivalent to $F(fact)$. We can strengthen our notion of semantic equivalence here: If both functions are equivalent with respect to their definitions (their sets), then they are semantically equivalent.