Entre la recursión mu- y la primitiva

Question

Es bien sabido que la recursión primitiva no es lo suficientemente potente para expresar todas las funciones, siendo la función de Ackermann probablemente el ejemplo conocido.

Ahora bien, en los cursos de lógica (que he hecho ver) siempre se procedía de la recursión primitiva a la mu-recursión. En términos de ciencias de la computación, esto significa básicamente que estamos saltando de un formalismo en el que se garantiza que los programas se detendrán a un formalismo Turing-completo en el que la detención es una propiedad no computable, es decir, no podemos decir para cada programa si finalmente se detendrá.

Tengo curiosidad por saber si hay alguna jerarquía entre la recursión primitiva y mu-recursión. Después de un tiempo encontré un lenguaje de programación llamado Charity. En Charity (según Wikipedia) todos los programas tienen la garantía de parar, por lo que no es Turing-completo, pero, por otro lado, es lo suficientemente expresivo para implementar la función de Ackermann.

Esto sugiere que hay al menos un nivel entre la mu-recursión y la recursión primitiva.

Mi pregunta es: ¿existe algún otro formalismo de parada segura que sea más expresivo que la recursión primitiva? O, mejor aún, ¿existen algunas jerarquías conocidas entre las funciones mu-recursivas y las recursivas primitivas? Tengo curiosidad por saber cuánto podemos calcular con un formalismo que garantice la parada.

Answer 1

Soy consciente de que estoy respondiendo a una pregunta muy antigua y que el autor original ya no está en MO, pero en aras de la exhaustividad, ya que el término no aparece en las otras respuestas, una palabra clave aquí es "jerarquías subrecursivas", y La tesis doctoral de Joel Robbin se trata de elaborar la conexión entre las clases de recursividad anidada, la jerarquía extendida de Grzegorczyk de las funciones de crecimiento rápido y las funciones universales de adición transitoria, todas ellas indexadas por notaciones ordinales.

Una clase estándar entre las recursivas primitivas y las recursivas/computables generales es la clase de funciones probadamente totales en la aritmética de Peano, o $\varepsilon_0$ -funciones recursivas.

Answer 2

Busque el artículo de John Reynolds "Programación funcional total", que trata de un lenguaje de programación en el que sólo se permiten funciones recursivas primitivas en un entorno en el que se permiten tipos de orden superior (como en el sistema T de Gödel). Tal vez eso se parezca a la Caridad que mencionó Kow. Reynolds cita un teorema (¿de Spector?) que dice que las funciones que su lenguaje puede expresar son exactamente las que se pueden probar como totales en la aritmética de segundo orden. Eso es enorme comparado con la función de Ackermann, pero todavía se queda corto con respecto a varias funciones totales que se pueden implementar en máquinas de Turing generales.

Answer 3

En cuanto a la jerarquía, es resultado básico de la teoría de la recursión que toda función recursiva f, es expresable como:

$f(x_{0},…,x_{n}) = u(\mu y.(T(e_{f},\langle x_{0},…,x_{n}\rangle))$

donde $T$ , $u$ son funciones primitivas recursivas fijas, y $e_{f}\in\mathbb{N}$ depende de $f$ (es un nombre en clave que describe cómo $f$ se construye). (Véase cualquier texto elemental como el de Schönfield).

Por lo tanto, la jerarquía es bastante corta.