Recursión de barra

La recursión de barra es una forma generalizada de recursión desarrollada por C. Spector en su artículo de 1962. ^[1] Está relacionada con la inducción de barra 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 .

Definición técnica

Sean V , R y O tipos , e i un número natural cualquiera, que representa una secuencia de parámetros tomados de V . Entonces la secuencia de funciones f de funciones f _n desde V ⁱ⁺ⁿ → R hasta O se define por recursión de barras desde las funciones L _n : R → O y B con B _n : (( V ⁱ⁺ⁿ → R ) x ( V ⁿ → R )) → O si:

f _n ((λα: V ^{i + n} ) r ) = L _n ( r ) para cualquier r lo suficientemente largo como para que L _{n + k} en cualquier extensión de r sea igual a L _n . Suponiendo que L es una secuencia continua, debe existir tal r , porque una función continua solo puede usar una cantidad finita de datos.
f _n ( p ) = B _n ( p , (λ x : V ) f _{n +1} (cat( p , x ))) para cualquier p en V ^{i + n} → R .

Aquí "cat" es la función de concatenación , que envía p , x a la secuencia que comienza con p y tiene x como su último término.

(Esta definición está basada en la de Escardó y Oliva. ^[2] )

Siempre que para cada función suficientemente larga (λα) r de tipo V ⁱ → R , exista algún 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 extiende la secuencia arbitrariamente, utilizando el término de recursión B para determinar el efecto, hasta que se alcanza un nodo suficientemente largo del árbol de secuencias sobre V ; luego, el término base L determina el valor final de f . La condición de bien definido corresponde al requisito de que cada camino infinito debe pasar eventualmente por un nodo suficientemente largo: el mismo requisito que se necesita para invocar una inducción de barra.

Los principios de inducción de barras y de recursión de barras son los equivalentes intuicionistas del axioma de elecciones dependientes . ^[3]

Referencias

^ C. Spector (1962). "Funcionales recursivos demostrables del análisis: una prueba de consistencia del análisis mediante una extensión de principios en las matemáticas intuicionistas actuales". En FDE Dekker (ed.). Teoría de funciones recursivas: Proc. Simposios en matemáticas puras . Vol. 5. American Mathematical Society . págs. 1–27.
^ Martín Escardó; Paulo Oliva. "Funciones de selección, recursión de barras e inducción hacia atrás" (PDF) . Math. Struct. en Ciencias de la Computación .
^ Jeremy Avigad ; Solomon Feferman (1999). "VI: La interpretación funcional ("Dialectica") de Gödel". En SR Buss (ed.). Manual de teoría de la prueba (PDF) .

[1] C. Spector (1962). "Funcionales recursivos demostrables del análisis: una prueba de consistencia del análisis mediante una extensión de principios en las matemáticas intuicionistas actuales". En FDE Dekker (ed.). Teoría de funciones recursivas: Proc. Simposios en matemáticas puras . Vol. 5. American Mathematical Society . págs. 1–27.

[2] Martín Escardó; Paulo Oliva. "Funciones de selección, recursión de barras e inducción hacia atrás" (PDF) . Math. Struct. en Ciencias de la Computación .

[3] Jeremy Avigad ; Solomon Feferman (1999). "VI: La interpretación funcional ("Dialectica") de Gödel". En SR Buss (ed.). Manual de teoría de la prueba (PDF) .