Corecursión

En informática , la corecursión es un tipo de operación dual a la recursión (estructural) . Mientras que la recursión consume una estructura de datos manejando primero la capa superior antes de descender a sus partes internas, la corecursión produce una estructura de datos definiendo primero la capa superior antes de definir sus partes internas. La corecursión es particularmente importante en los lenguajes totales , ya que permite codificar computaciones potencialmente no terminantes en un contexto donde toda función debe terminar. Es compatible con los demostradores de teoremas Agda ^{[ 1 ]} y Rocq ^{[ 2 ]} .

Tanto la corecursión como la recursión pueden considerarse operaciones sobre árboles , que incluyen estructuras de datos.como listas y flujos como casos especiales. Dado que la recursión debe terminar, solo funciona en árboles que están bien fundados , es decir, que no son infinitamente profundos, que se llaman datos o tipos de datos iniciales ; por otro lado, la correcursión produce codatos o tipos de datos finales , que incluyen árboles infinitamente profundos. Los codatos no se pueden representar directamente en la memoria, por lo que a menudo se implementan usando estructuras de datos autorreferenciales o evaluación perezosa .

En todos los lenguajes de programación, los números naturales se pueden definir de la siguiente manera (usando la sintaxis de Haskell ^{[ a ]} ​​):

datos Nat = Cero | Succ Nat

Esto establece que cada número natural es cero o el sucesor de un número natural existente. Por ejemplo, el número uno se representa como Succ Zero, el dos como Succ (Succ Zero), el tres como Succ (Succ (Succ Zero))y así sucesivamente.

Si interpretamos la declaración anterior de forma inductiva , entonces todos los números naturales se generan de esta manera, y obtenemos nuestro conjunto familiar de números naturales. Es importante destacar que podemos realizar recursión ^{[ b ]} en este conjunto: por ejemplo, podemos usarlo para crear una lista que repita un valor nveces:

repetir :: a -> Nat -> [ a ] ​​repetir x Cero = [] -- Caso base repetir x ( Succ n ) = x : repetir x n -- Paso inductivo

Nótese que el uso de repeat x nes crucial: no podríamos haber escrito repeat x (Succ n), porque esa es la función que estamos tratando de definir, y por lo tanto, entraría en un bucle infinito. Más específicamente, la entrada debe hacerse más pequeña —o más bien más profunda, si se considera como una estructura de datos— cada vez que llamamos recursivamente.

La declaración también puede interpretarse de forma coinductiva , lo que puede denotarse como:

codata CoNat = Cero | Succ CoNat

CoNattiene todos los números naturales que Nattiene automáticamente. Pero debido a que los codatos pueden ser infinitamente profundos, tiene un término adicional Succ (Succ (Succ (Succ …)))que continúa indefinidamente, a menudo denotado ∞. ^{[ 3 ]} Esto es único de los números conaturales, por lo que solo se puede construir usando la corecursión:

infinito :: CoNat infinito = Succ infinito

Mientras que la recursión requiere que la entrada de la llamada recursiva sea cada vez menor, la correcursión requiere que la salida de la llamada recursiva sea cada vez mayor. Por eso debemos escribir Succ infinity; simplemente infinity = infinityno estaría permitido, ya que generaría un bucle infinito.

Para ilustrar la dualidad entre recursión y corecursión, podemos encapsularlas en dos funciones, recy corec. La existencia de estas funciones, junto con los dos constructores regulares de Naty CoNat, identifican de forma única sus respectivos tipos y, por lo tanto, permiten reescribir todas las formas de recursión y corecursión en términos de ellas. ^{[ 4 ]}

rec :: Nat -> ( Quizás c -> c ) -> c rec Cero f = f Nada rec ( Succ n ) f = f ( Solo ( rec n f ))corec :: ( c -> Quizás c ) -> c -> CoNat corec f base = caso f base de Nada -> Cero Solo x -> Succ ( corec f x )

Conceptualmente, CoNatpuede pensarse como una máquina de estados , donde ces un tipo que encapsula el "estado actual". La función c -> Maybe ces una función de transición de estado que resulta en la terminación con Zeroo la continuación con Succ. Podemos reescribir los ejemplos anteriores usando las funciones:

repetir x n = rec n ( \ s -> caso s de Nothing -> [] Just a -> x : a ) infinito = corec ( \ () -> Just () ) ()

Un ejemplo más complejo de codata es el de los árboles binarios , donde cada nodo es un nodo hoja, que contiene algunos datos, o es un nodo rama que tiene exactamente dos hijos:

codata BinaryTree a = Hoja a | Rama ( BinaryTree a ) ( BinaryTree a )

Este ejemplo tiene muchos más términos infinitamente profundos que solo se pueden construir mediante correcursión. Por ejemplo, puede ser infinitamente profundo solo en el lado izquierdo, o en ambos lados, o alternando izquierda y derecha:

infiniteLeft :: a -> BinaryTree a infiniteLeft x = Branch ( infiniteLeft x ) ( Leaf x )infiniteBoth :: BinaryTree a infiniteBoth = Branch infiniteBoth infiniteBothinfiniteAlternating :: a -> Bool -> BinaryTree a infiniteAlternating x False = Branch ( infiniteAlternating x True ) ( Leaf x ) infiniteAlternating x True = Branch ( Leaf x ) ( infiniteAlternating x False )

Nuevamente, la correcursión en árboles binarios tiene una forma más general basada en un constructor tipo "máquina de estados":

corec :: ( c -> Either a ( c , c )) -> c -> BinaryTree a corec f base = case f base of Left x -> Leaf x Right ( x , y ) -> Branch ( corec f x ) ( corec f y )

codata M a ( b :: a -> * ) = M { raíz :: a , rama :: b raíz -> M a b } corec :: ( c -> ( raíz :: a , b raíz -> c )) -> c -> M a b corec f base = let ( raíz , rama ) = f base in M ​​{ raíz = raíz , rama = \ i -> corec f ( rama i ) }

f :: Bool -> * f False = Void -- Caso cero (sin ramificaciones) f True = () -- Caso exitoso (una ramificación)Nat = W Bool f CoNat = M Bool f

La sección anterior mostró que existe un vínculo íntimo entre los números naturales y conaturales y Maybe c, y de manera similar entre los árboles binarios y Either a (c, c). Este vínculo se precisa al mostrar que Natestá en biyección con Maybe Naty CoNatcon Maybe CoNat; explícitamente, esta biyección se asocia Zerocon Nothingy Succ ncon Just n. En otras palabras, Naty CoNatson puntos fijos ( salvo isomorfismo ) del mapa${\displaystyle X\mapsto X+1}$.

La diferencia entre datos y codatos radica en que los datos representan el menor número de puntos fijos, mientras que los codatos representan el mayor. De esta manera, la recursión puede resumirse como la afirmación de que "cada elemento del tipo fue generado únicamente por los constructores dados ( Zeroy Succen el caso de Nat/ CoNat)", mientras que la correcursión afirma que "existe cada valor que puede ser analizado utilizando los constructores como casos".

Desde una perspectiva de teoría de categorías, CoNatpuede definirse con precisión como la coalgebra final del endofunctor.${\displaystyle X\mapsto X+1}$. ^{[ 4 ]} Desarrollando esta definición, tenemos que:

• Hay una función . "Pred" significa "predecesor", y la intuición es que resta uno al número conatural o da otro resultado. En otras palabras, y . Esto muestra que es una coálgebra del functor, pero no necesariamente la final.pred :: CoNat -> Maybe CoNatNothingpred Zero = Nothingpred (Succ n) = Just nCoNat
• Para cada tipo cy función , existe una función tal que . Desglosando esto aún más, si entonces , mientras que si entonces —esto coincide con la definición de con la que estamos familiarizados.f :: c -> Maybe ccorec f :: c -> CoNatpred (corec f x) = fmap (corec f) (f x)f x = Just ycorec f x = Succ (corec f y)f x = Nothingcorec f x = Zerocorec
• coreces único en el siguiente sentido: para cualquier otra función que también satisfaga , . Esto garantiza que sea una coálgebra final .g :: c -> CoNatpred (g x) = fmap g (f x)g x = corec f xCoNat

Maybe cpuede reemplazarse con cualquier otro functor en la descripción anterior para obtener la definición de cualquier otro tipo coinductivo.

No todos los functores tienen coálgebras finales. Por ejemplo, el teorema de Cantor nos dice que ningún conjunto puede estar en biyección con su conjunto potencia, y por lo tanto el functor del conjunto potenciaa -> Bool no tiene coálgebra final. Sin embargo, en el caso de los functores polinomiales o los functores polinomiales cociente ^{[ 6 ]} , siempre existen coálgebras finales; los functores polinomiales son functores que pueden expresarse en la forma${\displaystyle \textstyle X\mapsto \sum _{a:\alpha }X^{\beta (a)}}$para una familia de tipos α y α -indexada β ( a ). El tipo M es exactamente la construcción de esta coálgebra final. ^{[ 5 ]}

Si bien se puede razonar sobre los tipos de datos coinductivos utilizando la unicidad de corecdirectamente, a menudo es más conveniente usar la coinducción , que puede probar igualdades de codata. Dado un coálgebra final A de un functor polinomial F —es decir${\displaystyle \textstyle F(X)=\sum _{a:\alpha }X^{\beta (a)}}$— decimos que una relación${\displaystyle R\subsetequ A\times A}$es una bisimulación si, para todo${\displaystyle (a,b)\in R}$,${\displaystyle {\text{raíz}}(a)={\text{raíz}}(b)}$y${\displaystyle {\text{rama}}(a,i)R{\text{rama}}(b,i)}$a pesar de${\displaystyle i:B({\text{raíz}}(a))}$. Aquí,${\displaystyle {\text{raíz}}}$y${\displaystyle {\text{rama}}}$Consulte los mapas:

${\displaystyle {\begin{aligned}{\text{raíz}}&:A\rightarrow \alpha \\{\text{rama}}&:\prod _{a:A}\beta ({\text{raíz}}(a))\rightarrow A\end{aligned}}}$

El principio de coinducción establece que para todas las bisimulaciones R en A y${\displaystyle (a,b)\in R}$,${\displaystyle a=b}$.

De forma más general, para un mapa de coalgebra${\displaystyle {\text{obtener}}:A\rightarrow F(A)}$, una relación R en A es una bisimulación si existe una función${\displaystyle f:R\rightarrow F(R)}$Satisfactorio para todos.${\displaystyle (a,b)\in R}$,

• ${\displaystyle {\text{obtener}}(a)=F(\pi _{1})(f(a,b))}$y
• ${\displaystyle {\text{obtener}}(b)=F(\pi _{2})(f(a,b))}$,

donde π ₁ y π ₂ son los mapas de primera y segunda proyección.${\displaystyle R\rightarrow A}$. Esto puede verse como equivalente al caso polinómico al establecer${\displaystyle f(a,b)=({\text{raíz}}(a),i\mapsto ({\text{rama}}(a,i),{\text{rama}}(b,i)))}$Las igualdades requeridas también pueden expresarse como un diagrama conmutativo:

La coinducción es fácil de demostrar a partir de la unicidad de corec: π ₁ y π ₂ satisfacen la propiedad requerida de ser iguales a corec f, y por lo tanto son iguales entre sí, demostrando así que${\displaystyle a=\pi _{1}(a,b)=\pi _{2}(a,b)=b}$. ^{[ 4 ]}

agregar :: CoNat -> CoNat -> CoNat agregar a Cero = a agregar a ( Succ b ) = Succ ( agregar a b )

agregar cero Cero = Cero agregar ( Succ a ) Cero = Succ ( agregar un cero ) agregar a ( Succ b ) = Succ ( agregar un b )

iterar :: ( CoNat , CoNat ) -> Quizás ( CoNat , CoNat ) iterar Cero Cero = Nada iterar ( Succ a ) Cero = Just ( a , Cero ) iterar a ( Succ b ) = Just ( a , b )agregar a b = corec iterar ( a , b )

Si el dominio del discurso es la categoría de conjuntos y funciones totales (como en demostradores de teoremas como Agda y Rocq), entonces los tipos finales (codatos) pueden contener valores infinitos no bien fundados , mientras que los tipos iniciales (datos) no. ^{[ 8 ] [ 9 ]} Por otro lado, si el dominio del discurso es la categoría de órdenes parciales completos y funciones continuas , que corresponde aproximadamente al lenguaje de programación Haskell , entonces los tipos finales coinciden con los tipos iniciales, y la coálgebra final y el álgebra inicial correspondientes forman un isomorfismo. ^{[ 10 ]}

La corecursión, también conocida como programación circular, se remonta al menos a ( Bird 1984 ) , quien atribuye su desarrollo a John Hughes y Philip Wadler ; formas más generales se desarrollaron en ( Allison 1989 ) . Las motivaciones originales incluían la creación de algoritmos más eficientes (que permitían una sola pasada sobre los datos en algunos casos, en lugar de requerir múltiples pasadas) y la implementación de estructuras de datos clásicas, como listas doblemente enlazadas y colas, en lenguajes funcionales.

• Bisimulación
• Coinducción
• Recursión
• Anamorfismo