¿Cuál es la diferencia entre recursión y corecursión?

Hay una serie de buenas maneras de ver esto. Lo más fácil para mí es pensar en la relación entre "Inductivo" y "Definiciones coinductivas"

Una definición inductiva de un conjunto es así.

El conjunto "Nat" se define como el conjunto más pequeño, de manera que "Cero" está en Nat, y si n está en Nat "Succ n" está en Nat.

Que corresponde al siguiente Ocaml

type nat = Zero | Succ of nat

Una cosa a tener en cuenta acerca de esta definición es que un número

omega = Succ(omega)

NO es un miembro de este conjunto. ¿Por qué? Supongamos que era, ahora considere el conjunto N que tiene todos los mismos elementos que Nat, excepto que no tiene omega. Claramente, el cero está en N, y si y está en N, Succ (y) está en N, pero N es más pequeño que Nat, lo que es una contradicción. Entonces, omega no está en Nat.

O, quizás más útil para un científico informático:

Dado un conjunto "a", el conjunto "Lista de a" se define como el conjunto más pequeño de manera que "Nil" está en la Lista de a, y que si xs está en la Lista de a y x está en a "Contras x xs" está en la Lista de a.

Lo que corresponde a algo como

type 'a list = Nil | Cons of 'a * 'a list

La palabra clave aquí es "más pequeña". ¡Si no dijéramos "más pequeño" no tendríamos ninguna manera de saber si el juego Nat contenía un plátano!

De nuevo,

zeros = Cons(Zero,zeros)

no es una definición válida para una lista de nats, al igual que omega no era un Nat válido.

La definición de datos inductivamente de esta manera nos permite definir las funciones que funcionan en ella utilizando recursion

let rec plus a b = match a with
                   | Zero    -> b
                   | Succ(c) -> let r = plus c b in Succ(r)

luego podemos probar hechos sobre esto, como "más un cero = a" usando inducción (específicamente, inducción estructural)

Nuestra prueba procede por inducción estructural en a.
Para el caso base dejemos que sea cero. plus Zero Zero = match Zero with |Zero -> Zero | Succ(c) -> let r = plus c b in Succ(r) por lo que sabemos plus Zero Zero = Zero . Sea a un nat. Supongamos la hipótesis inductiva de que plus a Zero = a . Ahora mostramos que plus (Succ(a)) Zero = Succ(a) esto es obvio ya que plus (Succ(a)) Zero = match a with |Zero -> Zero | Succ(a) -> let r = plus a Zero in Succ(r) = let r = a in Succ(r) = Succ(a) Por lo tanto, por inducción plus a Zero = a para todos a en nat

Por supuesto, podemos demostrar cosas más interesantes, pero esta es la idea general.

Hasta ahora hemos tratado con los datos definidos inductivamente que obtuvimos al dejar que fuera el conjunto "más pequeño". Así que ahora queremos trabajar con codata definidos coinductivamente, lo que obtenemos al permitir que sea el conjunto más grande.

Entonces

Sea un set. El conjunto "Stream of a" se define como el conjunto más grande, de manera que para cada x en el stream de a, x consiste en el par ordenado (cabeza, cola) tal que head está en a y tail está en el stream de a

En Haskell expresaríamos esto como

data Stream a = Stream a (Stream a) --"data" not "newtype"

En realidad, en Haskell usamos las listas integradas normalmente, que pueden ser un par ordenado o una lista vacía.

data [a] = [] | a:[a]

El plátano tampoco es un miembro de este tipo, ya que no es un par ordenado o la lista vacía. Pero, ahora podemos decir

ones = 1:ones

y esta es una definición perfectamente válida. Además, podemos realizar co-recursión en este co-data. En realidad, es posible que una función sea tanto recursiva como recursiva. Si bien la recursión fue definida por la función que tiene un dominio que consiste en datos, la recursión simplemente significa que tiene un co-dominio (también llamado rango) que es co-datos . La recursión primitiva significaba siempre "llamarse a sí mismo" en los datos de más pequeños hasta alcanzar algunos de los datos más pequeños. La recursión primitiva siempre se "llama a sí misma" en datos mayores o iguales a los que tenía anteriormente.

ones = 1:ones

es primitivamente co-recursivo. Mientras que la función map (algo así como "foreach" en lenguajes imperativos) es primitivamente recursiva (tipo de) y primitivamente co-recursiva.

map :: (a -> b) -> [a] -> [b]
map f []     = []
map f (x:xs) = (f x):map f xs

lo mismo ocurre con la función zipWith , que toma una función y un par de listas y las combina juntas usando esa función.

zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith f (a:as) (b:bs) = (f a b):zipWith f as bs
zipWith _ _ _           = [] --base case

el ejemplo clásico de lenguajes funcionales es la secuencia de Fibonacci

fib 0 = 0
fib 1 = 1
fib n = (fib (n-1)) + (fib (n-2))

que es primitivamente recursivo, pero puede expresarse de manera más elegante como una lista infinita

fibs = 0:1:zipWith (+) fibs (tail fibs)
fib' n = fibs !! n --the !! is haskell syntax for index at

un ejemplo interesante de inducción / coinducción está demostrando que estas dos definiciones computan lo mismo. Esto se deja como un ejercicio para el lector.

Básicamente, la correcursión es un estilo de acumulador , generando su resultado en el camino hacia adelante desde el caso inicial, mientras que la recursión regular genera su resultado en el camino de regreso desde el caso base.

(habla Haskell ahora). Es por eso que foldr (con una función de combinación estricta) expresa recursión, y foldl' (con peine estricto. F.) / scanl / until / iterate / unfoldr / etc. expresa la co-conversión. La corecursión está en todas partes. foldr con peine no estricto. F. expresa contrato de recursión de cola modulo .

Y la recursión vigilada de Haskell es simplemente como tail recursion modulo cons .

Esto es recursión:

fib n | n==0 = 0
      | n==1 = 1
      | n>1  = fib (n-1) + fib (n-2)

fib n = snd $ g n
  where
    g n | n==0 = (1,0)
        | n>0  = let { (b,a) = g (n-1) } in (b+a,b)

fib n = snd $ foldr (\_ (b,a) -> (b+a,b)) (1,0) [n,n-1..1]

(lea $ como "de"). Esto es corecursion:

fib n = g (0,1) 0 n where
  g n (a,b) i | i==n      = a 
              | otherwise = g n (b,a+b) (i+1)

fib n = fst.snd $ until ((==n).fst) (\(i,(a,b)) -> (i+1,(b,a+b))) (0,(0,1))
      = fst $ foldl (\(a,b) _ -> (b,a+b)) (0,1) [1..n]
      = fst $ last $ scanl (\(a,b) _ -> (b,a+b)) (0,1) [1..n]
      = fst (fibs!!n)  where  fibs = scanl (\(a,b) _ -> (b,a+b)) (0,1) [1..]
      = fst (fibs!!n)  where  fibs = iterate (\(a,b) -> (b,a+b)) (0,1)
      = (fibs!!n)  where  fibs = unfoldr (\(a,b) -> Just (a, (b,a+b))) (0,1)
      = (fibs!!n)  where  fibs = 0:1:map (\(a,b)->a+b) (zip fibs $ tail fibs)
      = (fibs!!n)  where  fibs = 0:1:zipWith (+) fibs (tail fibs)
      = (fibs!!n)  where  fibs = 0:scanl (+) 1 fibs
      = .....

Pliegues: enlace

Marque esto en blog de Vitomir Kovanovic . Lo encontré hasta el punto:

  

Evaluación perezosa en una característica muy agradable que se encuentra en la programación   lenguajes con capacidades de programación funcionales tales como lisp,   haskell, python, etc. Se considera que la evaluación del valor variable es   retrasado en el uso real de esa variable.

     

Significa que, por ejemplo, si desea crear una lista de millones   Los elementos con algo como esto (defn x (range 1000000)) no es   realmente creado, pero se acaba de especificar y cuando realmente usas   esa variable por primera vez, por ejemplo, cuando quieres décimo   elemento de esa lista intérprete crea sólo los primeros 10 elementos de   esa lista Así que la primera ejecución de (toma 10 x) en realidad crea estos   Los elementos y todas las llamadas posteriores a la misma función están funcionando.   con elementos ya existentes.

     

Esto es muy útil porque puedes crear listas infinitas sin salir   de errores de memoria. La lista será grande solo cuánto solicitó.   Por supuesto, si su programa está trabajando con grandes colecciones de datos,   Puede alcanzar el límite de memoria en el uso de estas listas infinitas.

     

Por otra parte, corecursion es dual a la recursión. ¿Lo que esto significa?   Bueno, al igual que las funciones recursivas, que se expresan en el   términos de sí mismos, variables corecursivas se expresan en los términos   de ellos mismos.

     

Esto se expresa mejor en el ejemplo.

     

Digamos que queremos una lista de todos los números primos ...

Aquí hay una serie de diapositivas que dan una respuesta bastante clara.

Según esas notas, una definición corecursiva es similar a una definición recursiva, excepto que no tiene un caso base.