On decision procedures for invariant properties of short algorithms

N. K. Kossovski

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VIII, Tome 88 (1979), pp. 73-77

Résumé

Lower bounds on Gödel numbers of decision procedures for invariant properties of short algorithms are established. Let $R$ be an enumerable class of partial (or general) recursive functions with partial recursive universal functions $u^1$ and $u^2$ for unary and binary functions of class $R$ respectively. Let also a function $S$ and constants $c$, $a$ satisfy the following conditions for every $x,y,z,u,v$. 1. $\{S(x,y)\}(z)\simeq\{x\}(y,z)$ 2. $\{S(c,x)\}(y,z)\simeq\{x\}(S(y,y),z)$ 3. $\{S^3(a,x,y,z)\}(u,v)\simeq$ if $\{z\}(u)\ne0$ then $\{x\}(v)$ else $\{y\}(v)$ where $\{x\}(y)$, $\{x\}(y,z)$ and $S^3(a,x,y,z)$ stand for instead of $u^1(x,y)$, $u^2(x,y,z)$ and $S(S(S(a,x),y),z)$ respectively. Many interesting classes of algorithms with natural numbering satisfy such conditions. Let $t(z)=\max(S(i,j,),z)$ for all $i,j\leq z$, $t^{-1}(z)=\mu y_{\leq z}[t(y)\leq z]$. Evidently, $t^{-1}(t(z))=z$. A property $A$ is called non-trivial up to $N_1$ if $\exists_{ab_{$. A property $A$ is called invariant up to $N$ ($N$ may be equal to $+\infty$) if for all $m$, $n$, $x$ $(\{m\}(x)\simeq\{n\}(x))\supset(A(m)\equiv A(n))$. This theorem is a generalization of the main theorem from [2], which entails the Rice theorem. Theorem. {\it Let an algorithm $\{m\}$ decide some property $A$ of unary algorithms of class $R$. If the property $A$ is non-trivial up to $N_1$, and invariant up to $N$, then for $N\geq\max(t^{\langle2\rangle}(c)$, $t^{\langle5\rangle}(N_1)$, $t^{\langle5\rangle}(a))$ we have $m\geq t^{\langle{-3}\rangle}(N)$, where $t^{\langle k\rangle}(x)$ and $t^{\langle{-k}\rangle}(x)$ stand for $t(\dots t(x)\dots)$ $k$ times and $t^{-1}(\dots t^{-1}(x)\dots)$ $k$ times respectively.}