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.