Función recursiva primitiva

En lógica matemática , las funciones recursivas primitivas son una generalización de las funciones recursivas primitivas en la teoría de tipos superior . Consisten en una colección de funciones de todos los tipos finitos puros.

Las funciones recursivas primitivas son importantes en la teoría de la demostración y en las matemáticas constructivas . Son una parte central de la interpretación dialéctica de la aritmética intuicionista desarrollada por Kurt Gödel .

En la teoría de la recursión , las funcionales recursivas primitivas son un ejemplo de computabilidad de tipo superior, así como las funciones recursivas primitivas son ejemplos de computabilidad de Turing.

Fondo

Cada función recursiva primitiva tiene un tipo, que indica qué tipo de entradas acepta y qué tipo de salida produce. Un objeto de tipo 0 es simplemente un número natural; también puede verse como una función constante que no acepta ninguna entrada y devuelve una salida en el conjunto N de números naturales.

Para dos tipos cualesquiera σ y τ, el tipo σ→τ representa una función que toma una entrada de tipo σ y devuelve una salida de tipo τ. Por lo tanto, la función f ( n ) = n +1 es de tipo 0→0. Los tipos (0→0)→0 y 0→(0→0) son diferentes; por convención, la notación 0→0→0 se refiere a 0→(0→0). En la jerga de la teoría de tipos, los objetos de tipo 0→0 se denominan funciones y los objetos que toman entradas de tipo distinto de 0 se denominan funcionales .

Para dos tipos cualesquiera σ y τ, el tipo σ×τ representa un par ordenado, cuyo primer elemento tiene tipo σ y cuyo segundo elemento tiene tipo τ. Por ejemplo, considere la función A que toma como entradas una función f de N a N , y un número natural n , y devuelve f ( n ). Entonces A tiene tipo (0 × (0→0))→0. Este tipo también se puede escribir como 0→(0→0)→0, mediante Currying .

El conjunto de tipos finitos (puros) es la colección más pequeña de tipos que incluye 0 y está cerrado bajo las operaciones de × y →. Se utiliza un superíndice para indicar que se supone que una variable x ^τ tiene un cierto tipo τ; el superíndice puede omitirse cuando el tipo se desprende claramente del contexto.

Definición

Las funciones recursivas primitivas son la colección más pequeña de objetos de tipo finito tales que:

• La función constante f ( n ) = 0 es una función recursiva primitiva
• La función sucesora g ( n ) = n + 1 es una función recursiva primitiva
• Para cualquier tipo σ×τ, la funcional K( x ^σ , y ^τ ) = x es una funcional recursiva primitiva
• Para cualquier tipo ρ, σ, τ, el funcional

  S( r ^ρ→σ→τ , s ^ρ→σ , t ^ρ ) = ( r ( t ))( s ( t ))

  es una función recursiva primitiva

• Para cualquier tipo τ, y f de tipo τ, y cualquier g de tipo 0→τ→τ, la función R ( f , g ) ^0→τ se define recursivamente como

  R ( f , g )(0) = f ,

  R ( f , g )( n + 1) = g ( n , R ( f , g )( n ))

  es una función recursiva primitiva

Véase también

• Interpretación dialéctica
• Función de orden superior
• Función recursiva primitiva
• Cálculo lambda de tipo simple

Referencias

• Jeremy Avigad y Solomon Feferman (1999). La interpretación funcional ("dialéctica") de Gödel (PDF) . en S. Buss ed., The Handbook of Proof Theory, North-Holland. pp. 337–405.