Precisamente, ¿qué es una definición recursiva primitiva?

Question

Si he entendido bien, el lenguaje de la aritmética recursiva primitiva tiene un símbolo de función distinguido $S$ junto con un símbolo de función para cada definición recursiva primitiva (en adelante PRD).

Por ejemplo, el PRD $$f(x,0) = x, \quad f(x,S(y)) = S(f(x,y))$$

corresponde a un símbolo de función que podemos denotar $+$ .

Del mismo modo, el PRD

$$f(x,0) = 0, \quad f(x,S(y)) = f(x,y)+x$$

corresponde a un símbolo de función que podemos denotar $\times$ .

Pregunta. ¿Cómo precisar el concepto de PRD?

Por ejemplo, me gustaría saber si existe un sistema formal que genere todas las definiciones válidas por recursión primitiva, pero ninguna definición no válida.

Answer 1

Una manera de definir lo que es un "primitivo recursivo definición" es hacer uso de algunos de los mayores objetos de tipo. Vamos a llamarlos $C$ $R$ para nuestros propósitos. También existe una única función sucesor $S(x)$, un único cero de la función $Z(x)$, y para cada una de las $i \leq j$ hay una función de proyección $$ \pi^j_i(x_1,\ldots,x_j) = x_i $$

Vamos a definir las funciones de uso de los símbolos "$C$", "$R$", "$S$", "$Z$", y "$\pi^j_i$" para todos los $i \leq j$, y dos más símbolos "(" y ")". Este es un infinito alfabeto de símbolos. Las definiciones de funciones recursivas primitivas será de un determinado conjunto finito de palabras en este alfabeto.

Por comodidad yo uso los mismos personajes aquí para la función y para el símbolo que denota la función: el símbolo "$S$" representa la única función sucesor $S(x)$. Si yo estaba fastidioso podía distinguir. Pero no tengo que poner todas las cadenas de símbolos en las comillas para asegurarse de que no hay confusión: todo lo que entre comillas es una cadena de símbolos, no una función.

Definición

Aquí es el inductivo definición de "$\sigma$ es una definición de una función recursiva primitiva de $n$ variables", de forma simultánea para todos los $n$:

• "S" es una definición de una primitiva recursiva de la función de una variable

• "Z" es una definición de una primitiva recursiva de la función de una variable

• Para todos $i \leq j$, "$\pi^j_i$" es una definición de una función recursiva primitiva de $j$ variables

• Si $\sigma_1, \ldots, \sigma_k$ son las definiciones de las funciones del mismo número, $m$, las variables y las $\tau$ es una definición de una función de $k$ variables, a continuación, "$C(\tau)(\sigma_1)(\sigma_2)\ldots(\sigma_k)$ " es una definición de una función de $m$ variables. El significado es que esta es la función $$ \tau\sigma_1(x_1,\ldots,x_m),\sigma_2(x_1,\ldots,x_m),\ldots,\sigma_k(x_1,\ldots,x_m)) $$

• Si $\sigma$ es una definición de una función de $k$ variables e $\tau$ es una definición de una función de $k+2$ variables, a continuación, "$R(\tau)(\sigma)$ " es una definición de una función de $k+1$ variables. El significado es que esta es la función $$ f(x_1,\ldots,x_k,0) = \sigma(x_1,\ldots, x_k)\\ f(x_1, \ldots, x_k, y+1) = \tau(f(x_1,\ldots,x_k,y),y,x_1,\ldots,x_k) $$

El conjunto de definiciones de funciones recursivas primitivas es el conjunto más pequeño $\mathcal{D}$ de las cadenas de la satisfacción de esta definición inductiva.

Ejemplo

Considere la función $g(x,y) = x + y$. Esto es definido por recursión primitiva como $$ g(x,0) = x\\ g(x,y+1) = S(g(x,y)) = S(\pi^3_1(g(x,y),y,x) $$

La función de base es $\sigma = \pi^1_1$. La recursividad de la función es la composición de $\pi^3_1$ en $S$: $\tau = S(\pi^1_3(z,y,x))$. Así que una primitiva recursiva definición de esta función, en los convenios anteriores, es el de la cadena $$ \text{"}R(C(S)(\pi^3_1))(\pi^1_1)" $$

La semántica

Usted puede probar por inducción que cada cadena en $\mathcal{D}$ que hace es definir una primitiva recursiva de la función con la intención semántica descrita anteriormente. Por el contrario, cada primitiva recursiva de la función está definida por al menos una cadena en $\mathcal{D}$ (de hecho, la misma función estará definida por un número infinito de cadenas en $\mathcal{D}$).

También, el conjunto de $\mathcal{D}$ es decidable, y cada cadena en $\mathcal{D}$ puede ser decodificado en un solo camino como una definición de una función recursiva primitiva.

Comentarios

La idea de ver $C$ $R$ como término de las operaciones de construcción es común en $\lambda$ cálculo y el tipo de teoría. En ese contexto, $R$ es a menudo llamado un "movimiento". Una forma alternativa de axiomatizing PRA es para evitar la inclusión de una función diferente símbolo para cada primitiva de la función recursiva. En su lugar hemos de incluir la función básica de los términos $S$, $Z$, y $\pi^j_i$, y el plazo de la construcción de las operaciones de $C$$R$, junto con la necesaria axiomas para todos estos.

También podemos pensar en estas definiciones como una especificación de un lenguaje de programación de funciones recursivas primitivas. Las definiciones que dan una forma de definir cada una primitiva de la función recursiva, y es totalmente factible (yo lo he hecho) para escribir un compilador que va a tomar una definición adecuada como entrada y evaluar la función en los insumos. Esto le da un juguete ejemplo de un lenguaje de programación funcional. Curiosamente, también hay una lengua de procedimiento, llamado BUCLE, que es capaz de calcular exactamente las funciones recursivas primitivas.

Answer 2

Hay un buen tratamiento en un viejo libro que debe ser cualquier biblioteca decente (también muy barato disponible como una reimpresión de Dover), Joel W. Robbin's Lógica matemática: Un primer curso (W. A Benjamin, 1969, reimpresión Dover 2006: pp. 212)

Robbin define las funciones recursivas primitivas de la forma habitual -- $f$ es recursiva primitiva si existe una secuencia finita de funciones $f_0, f_1, f_2, \ldots f_n = f$ donde cada $f_i$ es una función inicial o definida a partir de funciones anteriores en la secuencia por recursión primitiva o composición); y luego define un lenguaje que tiene una expresión de función para cada función p.r. $f$ . La idea clave es tener una expresión de función compleja construida para reflejar una definición completa de $f$ por recursión primitiva y/o composición en última instancia en términos de las funciones iniciales. Así pues, tenemos expresiones primitivas para cada función inicial, y dos formas de construir nuevas expresiones a partir de las antiguas correspondientes a las definiciones por recursión primitiva y composición.

El resultado es que, en sus palabras, en el lenguaje formal podemos construir una expresión formal que encapsule completamente cualquier definición recursiva primitiva informal. Y cualquier expresión construida del modo descrito expresará efectivamente una definición adecuada por recursividad primitiva (y no habrá definiciones "no válidas" construibles, tal como quieres).

Robbin introduce entonces un sistema de aritmética que él llama RA que tiene axiomas para la lógica más axiomas que gobiernan las expresiones para las funciones iniciales, y luego hay axiomas para tratar con expresiones funcionales complejas en términos de sus constituyentes. RA termina siendo más fuerte que PRA ya que Robbin permite una inducción más fuerte, pero a efectos de entender cómo se obtienen expresiones de función para cada función recursiva primitiva, su tratamiento es ejemplar, por lo que recuerdo.