[Solved]: What is a fixed point in the context of Roger's fixed-point theorem?

Problem Detail: 

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.

Asked By : Philip White

Answered By : Yuval Filmus

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/22684

 Ask a Question

 Download Related Notes/Documents