En lógica matemática , los funcionales recursivos primitivos son una generalización de las funciones recursivas primitivas en la teoría de tipo superior . Consisten en una colección de funciones en todos los tipos finitos puros.
Los funcionales recursivos primitivos son importantes en la teoría de la demostración y 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 , los funcionales recursivos primitivos son un ejemplo de computabilidad de tipo superior, ya que las funciones recursivas primitivas son ejemplos de computabilidad de Turing.
Cada funcional recursivo primitivo tiene un tipo, que dice qué tipo de entradas toma y qué tipo de salida produce. Un objeto de tipo 0 es simplemente un número natural; también se puede ver como una función constante que no recibe 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 τ. Así 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 el segundo elemento tiene tipo τ. Por ejemplo, considere que el funcional A 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, por Currying .