Existem várias maneiras de ver isso. O mais fácil para mim é pensar sobre a relação entre "indutivo" e "definições co-indutivas"
Uma definição indutiva de um conjunto é assim.
O conjunto "Nat" é definido como o menor conjunto tal que "Zero" está em Nat, e se n está em Nat "Succ n" está em Nat.
Qual corresponde ao seguinte Ocaml
type nat = Zero | Succ of nat
Uma coisa a notar sobre essa definição é que um número
omega = Succ(omega)
não é um membro deste conjunto. Por quê? Suponha que era, agora considere o conjunto N que tem todos os mesmos elementos que Nat, exceto que ele não tem ômega. Claramente Zero está em N, e se y está em N, Succ (y) está em N, mas N é menor que Nat, o que é uma contradição. Então, o ômega não está em Nat.
Ou talvez mais útil para um cientista da computação:
Dado algum conjunto "a", o conjunto "Lista de um" é definido como o menor conjunto tal que "Nil" está em Lista de um, e que se xs está em Lista de a e x está em um "Cons x xs" está na lista de um.
Que corresponde a algo como
type 'a list = Nil | Cons of 'a * 'a list
A palavra operativa aqui é "menor". Se não disséssemos "menor", não teríamos como dizer se o conjunto Nat continha uma banana!
Mais uma vez,
zeros = Cons(Zero,zeros)
não é uma definição válida para uma lista de nats, assim como o omega não era um Nat válido
Definir dados indutivamente assim nos permite definir funções que funcionam com
let rec plus a b = match a with
| Zero -> b
| Succ(c) -> let r = plus c b in Succ(r)
podemos então provar fatos sobre isso, como "mais um Zero = a" usando indução (especificamente, indução estrutural)
Nossa prova procede por indução estrutural em um. Para o caso base, deixe um zero.plus Zero Zero = match Zero with |Zero -> Zero | Succ(c) -> let r = plus c b in Succ(r) , então sabemos plus Zero Zero = Zero .
Deixe a ser um nat. Assuma a hipótese indutiva de que plus a Zero = a . Agora mostramos que plus (Succ(a)) Zero = Succ(a) é óbvio, pois 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)
Assim, por indução plus a Zero = a para todo a in nat
Podemos, claro, provar coisas mais interessantes, mas essa é a ideia geral.
Até agora, lidamos com dados definidos indutivamente , o que conseguimos com o conjunto "menor". Então, agora queremos trabalhar com codata coindutivamente definida, o que conseguimos ao permitir que seja o maior conjunto.
Então
Deixe um ser um conjunto. O conjunto "Fluxo de um" é definido como o maior conjunto tal que para cada x no fluxo de a, x consiste no par ordenado (cabeça, cauda) tal que a cabeça está em um e cauda está em Fluxo de um
Em Haskell, nós expressamos isso como
data Stream a = Stream a (Stream a) --"data" not "newtype"
Na verdade, em Haskell usamos normalmente as listas internas, que podem ser um par ordenado ou uma lista vazia.
data [a] = [] | a:[a]
Banana também não é membro desse tipo, pois não é um par ordenado ou uma lista vazia. Mas agora podemos dizer
ones = 1:ones
e esta é uma definição perfeitamente válida. Além do mais, podemos realizar co-recursão nesses co-dados. Na verdade, é possível que uma função seja co-recursiva e recursiva. Embora a recursão tenha sido definida pela função que possui um domínio que consiste em dados, a co-recursão significa apenas que possui um co-domínio (também chamado de intervalo) que é co-dados . A recursão primitiva significava sempre "chamar a si mesmo" em dados menores até alcançar alguns dados menores. Co-recursão primitiva sempre "chama a si mesma" em dados maiores ou iguais ao que você tinha antes.
ones = 1:ones
é primitivamente co-recursivo. Enquanto a função map (como "foreach" em linguagens imperativas) é primitivamente recursiva (tipo de) e primitivamente co-recursiva.
map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = (f x):map f xs
O mesmo vale para a função zipWith , que pega uma função e um par de listas e as combina usando essa função.
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith f (a:as) (b:bs) = (f a b):zipWith f as bs
zipWith _ _ _ = [] --base case
o exemplo clássico de linguagens funcionais é a seqüência de Fibonacci
fib 0 = 0
fib 1 = 1
fib n = (fib (n-1)) + (fib (n-2))
que é primitivamente recursivo, mas pode ser expresso de forma mais elegante como uma lista infinita
fibs = 0:1:zipWith (+) fibs (tail fibs)
fib' n = fibs !! n --the !! is haskell syntax for index at
um exemplo interessante de indução / co-indução está provando que essas duas definições computam a mesma coisa. Isso é deixado como um exercício para o leitor.