Qual è la differenza tra ricorsione e corecursion?

Ci sono molti buoni modi per guardare a questo. La cosa più facile per me è pensare alla relazione tra "Induttivo" e "Definizioni coinduttive"

Una definizione induttiva di un set è così.

Il set "Nat" è definito come il set più piccolo tale che "Zero" è in Nat, e se n è in Nat "Succ n" è in Nat.

Che corrisponde al seguente Ocaml

type nat = Zero | Succ of nat

Una cosa da notare su questa definizione è che un numero

omega = Succ(omega)

NON è un membro di questo set. Perché? Supponiamo che lo fosse, ora considera l'insieme N che ha tutti gli stessi elementi di Nat tranne che non ha omega. Chiaramente Zero è in N, e se y è in N, Succ (y) è in N, ma N è minore di Nat che è una contraddizione. Quindi, omega non è in Nat.

Oppure, forse più utile per uno scienziato informatico:

Dato un certo set "a", l'insieme "List of a" è definito come il set più piccolo tale che "Nil" è in List of a, e che se xs è in List of a e x è in un "Cons x xs" è in List of a.

Che corrisponde a qualcosa di simile

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

La parola chiave qui è "la più piccola". Se non dicessimo "il più piccolo" non avremmo modo di dire se il set Nat contenesse una banana!

Ancora,

zeros = Cons(Zero,zeros)

non è una definizione valida per un elenco di nats, proprio come omega non era un Nat valido.

La definizione di dati in modo induttivo come questo ci consente di definire le funzioni che funzionano con ricorsione

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

possiamo quindi provare fatti su questo, come "più uno zero = a" usando induzione (in particolare, induzione strutturale)

La nostra prova procede per induzione strutturale su un.
Per il caso base lasciate che sia Zero. plus Zero Zero = match Zero with |Zero -> Zero | Succ(c) -> let r = plus c b in Succ(r) quindi sappiamo plus Zero Zero = Zero . Lascia che a sia un nat. Assumi l'ipotesi induttiva che plus a Zero = a . Ora dimostriamo che plus (Succ(a)) Zero = Succ(a) è ovvio poiché 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) Quindi, per induzione plus a Zero = a per tutto a in nat

Ovviamente possiamo provare cose più interessanti, ma questa è l'idea generale.

Finora abbiamo trattato i dati induttivamente definiti che abbiamo ottenuto lasciando che fosse il set "più piccolo". Quindi ora vogliamo lavorare con codata definito in modo coincertivo, che otteniamo lasciando che sia il set più grande.

Sia un set. Il set "Stream of a" è definito come il più grande set tale che per ogni x nel flusso di a, x consiste nella coppia ordinata (testa, coda) tale che la testa è in a e tail è in Stream of a

In Haskell lo esprimiamo come

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

In realtà, in Haskell usiamo normalmente gli elenchi integrati, che possono essere una coppia ordinata o una lista vuota.

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

Anche Banana non è un membro di questo tipo, dal momento che non è una coppia ordinata o la lista vuota. Ma ora possiamo dire

ones = 1:ones

e questa è una definizione perfettamente valida. Per di più, possiamo eseguire la ricorsione su questi co-dati. In realtà, è possibile che una funzione sia ricorsiva e ricorsiva. Mentre la ricorsione è stata definita dalla funzione con un dominio costituito da dati, la ricorsione coincide semplicemente con un co-dominio (chiamato anche l'intervallo) che è co-dati . La ricorsione primitiva significava sempre "chiamarsi" su più piccoli dati fino a raggiungere alcuni dati più piccoli. La co-ricorsione primitiva si "chiama sempre" su dati maggiori o uguali a quelli che avevi prima.

ones = 1:ones

è primitivo co-ricorsivo. Mentre la funzione map (un po 'come "foreach" nelle lingue imperative) è sia primitivamente ricorsiva (sorta di) che primitivamente co-ricorsiva.

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

lo stesso vale per la funzione zipWith che prende una funzione e una coppia di liste e le combina insieme usando quella funzione.

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

il classico esempio di linguaggi funzionali è la sequenza di Fibonacci

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

che è originariamente ricorsivo, ma può essere espresso in modo più elegante come una lista infinita

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

un interessante esempio di induzione / coinduzione sta dimostrando che queste due definizioni calcolano la stessa cosa. Questo è lasciato come esercizio per il lettore.

Fondamentalmente, il corecursion è ricorsivo stile accumulatore , costruendo il suo risultato sulla via da seguire dal caso di partenza, mentre la ricorsione regolare costruisce il suo risultato al ritorno dal caso base.

(parlando Haskell ora). Ecco perché foldr (con una rigida funzione di combinazione) esprime la ricorsione, e foldl' (con lo stretto pettine f.) / scanl / until / iterate / unfoldr / ecc. Corecursion espresso. La corecursione è ovunque. foldr con pettine non rigido. f. esprime coda ricorsione modulo contro .

E la ricorsione custodita di Haskell è solo come coda ricorsione modulo contro .

Questa è la ricorsione:

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]

(leggi $ come "di"). Questo è il 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
      = .....

Folds: link

Controlla questo blog di Vitomir Kovanovic . L'ho trovato al punto:

Lazy evaluation in one very nice feature found in programming languages with functional programming capabilities such as lisp, haskell, python etc. It mans that evaluation of variable value is delayed to the actual usage of that variable.

It means that for example if you wanted to create a list of million elements with something like this (defn x (range 1000000)) it is not actually created, but it is just specified and when you really use that variable for the first time, for instance when you want 10th element of that list interpreter creates only first 10 elements of that list. So the first run of (take 10 x) actually creates these elements and all subsequent calls to the same function are working with already existing elements.

This is very useful because you can create infinite lists without out of memory errors.The list will be large just how much you requested. Of course, if your program is working with large data collections it can hit memory limit in the usage of these infinite lists.

On the other hand corecursion is dual to recursion. What this means? Well just like the recursive functions, which are expressed in the terms of themselves, corecursive variables are expressed in the terms of themselves.

This is best expressed on the example.

Let’s say we want list of all prime numbers...

Ecco una serie di diapositive che danno una risposta abbastanza chiara.

Per queste note, una definizione corecursiva è simile a una definizione ricorsiva, tranne che non ha un caso base.