[Solved]: The minimization operator is an effective operator

Problem Detail: 

Assume $\{f_i^{(n)}\}_{i=0}^\infty$ is a Gödel enumeration of the $\mu$-recursive functions of $n$ arguments, such that the $S^m_n$ theorem and the universal function theorem hold. Denote the set of (total and partial) functions $\{f:\mathbb N^k\to\mathbb N\ \}$ by $\mathfrak F^k$

Definition: We call an operator $G:\mathfrak F^n\to\mathfrak F^k$ effective, if $(\forall j\in\mathbb N)(G(f^{(n)}_j)=f^{(k)}_{g(j)})$ for some total recursive function $g$.

Claim: The minimization operator $\mu:\mathfrak F^{k+1}\to\mathfrak F^k$ defined by $$\mu(f)(\overline x)=\mu y[f(y,\overline x)=0]=y\iff (f(y,\overline x)=0\land(\forall i<y) (f(i,\overline x)>0))$$ is an effective operator.

Question: How can I go about proving the statement? Hints are welcome.

Thought: By definition the $\mu$-recursive functions are closed with respect to the $\mu$-operator. Therefore, $\mu(f^{(k+1)}_j)=f^{(k)}_{h(j)}$, for some unique total function $h$. But why is $h$ a computable function?

Note that I would really like to stay within the Partial Recursive Functions Formalism. Pseudo code means nothing to me. I cannot read it. I am not familiar with most of the notation from the programming world. I would also prefer not go into Register Machine Formalisms.

Asked By : Student

Answered By : Raphael

It's a direct application of the smn-theorem if you don't let the currying get in your way.

Since $\mu : \mathbb{N}^{k+1} \to \mathbb{N}$ is computable (by definition), there is $i \in \mathbb{N}$ so that

$\qquad\displaystyle \mu = f^{(k+1)}_i$.

Now the smn-theorem asserts the existence of a recursive and total $g' : \mathbb{N}^2 \to \mathbb{N}$ with

$\qquad\displaystyle f^{(k+1)}_i(x_0, x_1, \dots, x_k) = f^{k}_{g'(i,x_0)}(x_1, \dots, x_k)$

for all $(x_0,\dots,x_k) \in \mathbb{N}^{k+1}$. Because $i$ is fixed, we get (again via smn-theorem) a recursive and total $g : \mathbb{N} \to \mathbb{N}$ with

$\qquad \mu(f,\overline{x}) = f^{(k+1)}_i(f,\overline{x}) = f^{k}_{g'(i,f)}(\overline{x}) = f^{k}_{g(f)}(\overline{x})$

for all $\overline{x} \in \mathbb{N}^k$.

Best Answer from StackOverflow

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