La recursión de barras es una forma generalizada de recursividad desarrollada por C. Spector en su artículo de 1962. [1] Está relacionado con la inducción de barras de la misma manera que la recursión primitiva está relacionada con la inducción ordinaria , o la recursión transfinita está relacionada con la inducción transfinita .
Sean V , R y O tipos , y sea i cualquier número natural, que representa una secuencia de parámetros tomados de V . Entonces, la secuencia de funciones f de funciones f n de V i + n → R a O se define mediante recursión de barras de las funciones L n : R → O y B con B n : (( V i + n → R ) x (V n → R )) → O si:
Aquí "cat" es la función de concatenación , enviando p , x a la secuencia que comienza con p y tiene x como último término.
Siempre que para toda función suficientemente larga (λα) r de tipo V i → R , existe alguna n con L n ( r ) = B n ((λα) r , (λ x : V ) L n +1 ( r ) ), la regla de inducción de barras asegura que f esté bien definida.
La idea es que uno extienda la secuencia arbitrariamente, usando el término de recurrencia B para determinar el efecto, hasta que se alcance un nodo suficientemente largo del árbol de secuencias sobre V ; entonces el término base L determina el valor final de f . La condición de bien definida corresponde al requisito de que todo camino infinito debe eventualmente pasar a través de un nodo suficientemente largo: el mismo requisito que se necesita para invocar una barra de inducción.
Los principios de inducción de barras y recursividad de barras son los equivalentes intuicionistas del axioma de elecciones dependientes . [3]