Ya, dimungkinkan untuk mengekspresikan tipe yang tepat untuk rutin penyortiran, sehingga fungsi apa pun yang memiliki tipe itu harus mengurutkan daftar input.
Meskipun mungkin ada solusi yang lebih maju dan elegan, saya akan membuat sketsa solusi dasar saja.
Kami akan menggunakan notasi seperti Coq. Kita mulai dengan mendefinisikan predikat yang membutuhkan yang f: nat -> natbertindak sebagai permutasi pada :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) .
Lemma sederhana dapat dengan mudah dibuktikan.
Lemma lem1: forall n f, permutation n f -> m < n -> f m < n.
... (* from the def *)
Kami mendefinisikan apa yang th elemen dari daftar yang memiliki panjang . Fungsi ini membutuhkan bukti yang menyatakan bahwa memang berlaku.mnhm<n
Definition nth {A} {n} (l: list A n) m (h : m < n): A :=
... (* recursion over n *)
Dengan adanya pemesanan A, kami dapat menyatakan bahwa daftar diurutkan:
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 :=
...
Akhirnya inilah tipe untuk algoritma penyortiran:
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 *)
Tipe output menyatakan bahwa daftar hasil sadalah elemen panjang, diurutkan, dan bahwa ada permutasi yang memetakan elemen dalam daftar input ke yang ada di daftar output . Perhatikan bahwa kita harus memanggil lemma di atas untuk membuktikan , yang diperlukan oleh .0 .. n - 1 f ( m ) < nn0..n−1lsf(m)<nnth
Namun perlu dicatat bahwa itu adalah pengguna, yaitu programmer, yang harus membuktikan algoritma pengurutan mereka dengan benar. Kompiler tidak akan hanya memverifikasi bahwa pengurutan sudah benar: yang dilakukannya hanyalah memeriksa bukti yang diberikan. Memang, kompiler tidak dapat melakukan lebih dari itu: sifat semantik seperti "program ini adalah algoritma penyortiran" tidak dapat dipungkiri (oleh teorema Rice), jadi kita tidak bisa berharap untuk membuat langkah pembuktian sepenuhnya otomatis.
Sejauh ini, jauh di masa depan, kita masih bisa berharap bahwa prover teorema otomatis menjadi sangat pintar sehingga "kebanyakan" algoritma yang digunakan secara praktis dapat secara otomatis terbukti benar. Teorema Padi hanya menyatakan bahwa ini tidak dapat dilakukan dalam semua kasus. Yang bisa kita harapkan adalah sistem yang benar, dapat diterapkan secara luas, tetapi secara inheren tidak lengkap.
Sebagai catatan akhir, kadang-kadang dilupakan bahwa sistem tipe sederhana pun tidak lengkap ! Misalnya bahkan di Jawa
int f(int x) {
if (x+2 != 2+x)
return "Houston, we have a problem!";
return 42;
}
adalah tipe aman semantik (selalu mengembalikan bilangan bulat), tetapi pemeriksa tipe akan mengeluh tentang pengembalian yang tidak terjangkau.
