Jest na to wiele dobrych sposobów. Najłatwiej jest mi pomyśleć o związku między „indukcyjnymi” a „koindukcyjnymi definicjami”
Indukcyjna definicja zestawu wygląda następująco.
Zbiór „Nat” jest zdefiniowany jako najmniejszy zbiór, tak że „Zero” jest w Nat, a jeśli n jest w Nat, „Succ” jest w Nat.
Co odpowiada następującemu Ocamlowi
type nat = Zero | Succ of nat
Należy zwrócić uwagę na tę definicję, że liczba
omega = Succ(omega)
NIE jest członkiem tego zestawu. Dlaczego? Załóżmy, że tak było, rozważmy teraz zestaw N, który ma wszystkie te same elementy co Nat, z wyjątkiem tego, że nie ma omegi. Wyraźnie zero jest w N, a jeśli y jest w N, Succ (y) jest w N, ale N jest mniejsze niż Nat, co jest sprzecznością. Omegi nie ma w Nat.
Lub może bardziej przydatny dla informatyka:
Biorąc pod uwagę pewien zestaw „a”, zestaw „Lista a” jest zdefiniowany jako najmniejszy zbiór, taki że „zero” znajduje się na liście a, a jeśli xs jest na liście a, a x jest w „Cons x xs” jest na liście.
Co odpowiada coś takiego
type 'a list = Nil | Cons of 'a * 'a list
Słowo operacyjne jest tutaj „najmniejsze”. Gdybyśmy nie powiedzieli „najmniejszy”, nie mielibyśmy żadnego sposobu na stwierdzenie, czy zestaw Nat zawiera banana!
Jeszcze raz,
zeros = Cons(Zero,zeros)
nie jest poprawną definicją listy natów, tak jak omega nie była prawidłową Nat.
Definiowanie danych indukcyjnie w ten sposób pozwala nam definiować funkcje, które działają na nich za pomocą rekurencji
let rec plus a b = match a with
| Zero -> b
| Succ(c) -> let r = plus c b in Succ(r)
możemy następnie udowodnić fakty na ten temat, takie jak „plus zero = a” za pomocą indukcji (konkretnie indukcji strukturalnej)
Nasz dowód opiera się na indukcji strukturalnej na.
Dla przypadku podstawowego niech będzie zero. plus Zero Zero = match Zero with |Zero -> Zero | Succ(c) -> let r = plus c b in Succ(r)więc wiemy plus Zero Zero = Zero. Niech abędzie nat. Załóżmy hipotezę indukcyjną, że plus a Zero = a. Pokazujemy teraz, że plus (Succ(a)) Zero = Succ(a)jest to oczywiste, ponieważ w 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)
ten sposób przez indukcję plus a Zero = adla wszystkich aw nat
Możemy oczywiście udowodnić bardziej interesujące rzeczy, ale taka jest ogólna idea.
Do tej pory zajmowaliśmy się danymi zdefiniowanymi indukcyjnie, które otrzymaliśmy, pozwalając, aby był to „najmniejszy” zestaw. Więc teraz chcemy pracować z kododami zdefiniowanymi we współpracy, które otrzymujemy, pozwalając, aby był to największy zestaw.
Więc
Niech będzie zbiorem. Zbiór „Strumień a” jest zdefiniowany jako największy zbiór taki, że dla każdego xw strumieniu a x składa się z uporządkowanej pary (głowa, ogon) tak, że głowa jest w a, a ogon jest w strumieniu
W Haskell wyrazilibyśmy to jako
data Stream a = Stream a (Stream a) --"data" not "newtype"
Właściwie w Haskell normalnie używamy wbudowanych list, które mogą być uporządkowaną parą lub pustą listą.
data [a] = [] | a:[a]
Banan też nie jest członkiem tego typu, ponieważ nie jest to uporządkowana para ani pusta lista. Ale teraz możemy powiedzieć
ones = 1:ones
i jest to całkowicie poprawna definicja. Co więcej, możemy wykonywać rekurencję na tych współdanych. W rzeczywistości funkcja może być jednocześnie rekurencyjna i rekurencyjna. Podczas gdy rekurencja została zdefiniowana przez funkcję posiadającą domenę składającą się z danych, ko-rekurencja oznacza po prostu, że ma wspólną domenę (zwaną także zakresem), która jest współdanymi. Prymitywna rekurencja oznaczała zawsze „dzwonienie do siebie” na mniejszych danych, aż do osiągnięcia najmniejszych danych. Pierwotna ko-rekurencja zawsze „nazywa się” danymi większymi lub równymi temu, co posiadałeś wcześniej.
ones = 1:ones
jest pierwotnie ko-rekurencyjny. Podczas gdy funkcja map(rodzaj „foreach” w imperatywnych językach) jest zarówno pierwotnie rekurencyjna (niejako), jak i pierwotnie ko-rekurencyjna.
map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = (f x):map f xs
to samo dotyczy funkcji, zipWithktóra pobiera funkcję i parę list i łączy je ze sobą za pomocą tej funkcji.
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith f (a:as) (b:bs) = (f a b):zipWith f as bs
zipWith _ _ _ = [] --base case
klasycznym przykładem języków funkcjonalnych jest sekwencja Fibonacciego
fib 0 = 0
fib 1 = 1
fib n = (fib (n-1)) + (fib (n-2))
który jest pierwotnie rekurencyjny, ale można go wyrazić bardziej elegancko jako nieskończoną listę
fibs = 0:1:zipWith (+) fibs (tail fibs)
fib' n = fibs !! n --the !! is haskell syntax for index at
Interesującym przykładem indukcji / koindukcji jest udowadnianie, że te dwie definicje obliczają to samo. Pozostaje to jako ćwiczenie dla czytelnika.