Tak, możliwe jest wyrażenie dokładnego typu dla procedury sortowania, tak że każda funkcja tego typu musi rzeczywiście posortować listę wejściową.
Chociaż może być bardziej zaawansowane i eleganckie rozwiązanie, naszkicuję tylko elementarne.
Użyjemy notacji typu Coq. Zaczynamy od zdefiniowania wymaganego predykatu, który f: nat -> natdziała jak permutacja na 0..n−1 :
Definition permutation (n: nat) (f: nat -> nat): Prop :=
(* once restricted, its codomain is 0..n-1 *)
(forall m, m < n -> f m < n) /\
(* it is injective, hence surjective *)
(forall m1 m2, m1 < n -> m2 < n -> f m1 = f m2 -> m1 = m2) .
Prosty lemat można łatwo udowodnić.
Lemma lem1: forall n f, permutation n f -> m < n -> f m < n.
... (* from the def *)
Możemy określić, co jest th element listy mającej długość . Ta funkcja wymaga dowodu potwierdzającego, że rzeczywiście się utrzymuje.mnhm<n
Definition nth {A} {n} (l: list A n) m (h : m < n): A :=
... (* recursion over n *)
Biorąc pod uwagę zamówienie A, możemy wyrazić, że lista jest posortowana:
Definition ordering (A: Type) :=
{ leq: A->A->bool |
(* axioms for ordering *)
(forall a, leq a a = true) /\
(forall a b c, leq a b = true -> leq b c = true -> leq a c = true) /\
(forall a b, leq a b = true -> leq b a = true -> a = b)
} .
Definition sorted {A} {n} (o: ordering A) (l: list A n): Prop :=
...
Wreszcie jest typ algorytmu sortowania:
Definition mysort (A: Type) (o: ordering A) (n: nat) (l: list A n):
{s: list A n | sorted o s /\
exists f (p: permutation n f),
forall (m: nat) (h: m < n),
nth l m h = nth s (f m) (lem1 n f p h) } :=
... (* the sorting algorithm, and a certificate for its output *)
Typ danych wyjściowych stwierdza, że lista wyników sma długość elementów, jest sortowana i że istnieje permutacja która odwzorowuje elementy na liście danych wejściowych na te na liście wyników . Zauważ, że musimy odwołać się do powyższego lematu, aby udowodnić , co jest wymagane przez .n0..n−1lsf(m)<nnth
Zauważ jednak, że to użytkownik, tj. Programista, musi udowodnić poprawność algorytmu sortowania. Kompilator nie tylko zweryfikuje poprawność sortowania: wystarczy sprawdzić dostarczony dowód. Rzeczywiście, kompilator nie może zrobić dużo więcej: właściwości semantyczne, takie jak „ten program jest algorytmem sortującym” są nierozstrzygalne (według twierdzenia Rice'a), więc nie możemy mieć nadziei, że krok sprawdzania będzie w pełni automatyczny.
W dalekiej, dalekiej przyszłości nadal możemy mieć nadzieję, że automatyczne dowody twierdzeń staną się tak inteligentne, że „większość” praktycznie używanych algorytmów może zostać automatycznie udowodniona, że są poprawne. Twierdzenie Rice'a tylko stwierdza, że nie można tego zrobić we wszystkich przypadkach. Wszystko, na co możemy mieć nadzieję, to poprawny, szeroko stosowany, ale z natury niekompletny system.
Na koniec czasami zapomina się, że nawet proste systemy typów są niekompletne ! Np. Nawet w Javie
int f(int x) {
if (x+2 != 2+x)
return "Houston, we have a problem!";
return 42;
}
jest semantycznie bezpieczny (zawsze zwraca liczbę całkowitą), ale moduł sprawdzania typu będzie narzekał na nieosiągalny zwrot.