Nachweis eines Sortiervorgangs im Typsystem

9

Ich möchte wissen, inwieweit ein Typensystem in einer Programmiersprache von Vorteil sein kann. Ich weiß zum Beispiel, dass wir in einer abhängig typisierten Programmiersprache eine VectorKlasse erstellen können, die die Größe des Vektors in die Typensignatur einbezieht. Es ist wie ein De-facto-Beispiel. Wir können auch eine Funktion appendmit diesen Signaturen schreiben, damit der Compiler nachweist, dass die Größe der resultierenden Liste die Summe der Eingabelisten ist.

Gibt es eine Möglichkeit, beispielsweise die Typensignatur eines Sortieralgorithmus so zu codieren, dass der Compiler garantiert, dass die resultierende Liste eine Permutation der Eingabeliste ist? Wie kann das gemacht werden, wenn es möglich ist?

type-theory functional-programming dependent-types Meguli
quelle

Antworten:

13

Ja, es ist möglich, einen genauen Typ für eine Sortierroutine auszudrücken, sodass jede Funktion mit diesem Typ tatsächlich die Eingabeliste sortieren muss.

Während es eine fortgeschrittenere und elegantere Lösung geben könnte, werde ich nur eine elementare skizzieren.

f: nat -> nat0..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) .

Ein einfaches Lemma kann leicht bewiesen werden.

Lemma lem1: forall n f, permutation n f -> m < n -> f m < n.
... (* from the def *)

mnhm<n

Definition nth {A} {n} (l: list A n) m (h : m < n): A :=
... (* recursion over n *)

Bei einer Bestellung am Akönnen wir ausdrücken, dass eine Liste sortiert ist:

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 :=
...

Schließlich ist hier der Typ für einen Sortieralgorithmus:

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 *)

sn0..n−1lsf(m)<nnth

Beachten Sie jedoch, dass der Benutzer, dh der Programmierer, den korrekten Sortieralgorithmus nachweisen muss. Der Compiler überprüft nicht einfach, ob die Sortierung korrekt ist. Er überprüft lediglich einen bereitgestellten Beweis. In der Tat kann der Compiler nicht viel mehr als das: Semantische Eigenschaften wie "Dieses Programm ist ein Sortieralgorithmus" sind (nach dem Rice-Theorem) unentscheidbar , so dass wir nicht hoffen können, den Testschritt vollautomatisch zu machen.

In ferner, ferner Zukunft können wir immer noch hoffen, dass automatische Theoremprüfer so intelligent werden, dass "die meisten" praktisch verwendeten Algorithmen automatisch als korrekt erwiesen werden können. Der Reissatz besagt nur, dass dies nicht in allen Fällen möglich ist. Wir können nur auf ein korrektes, allgemein anwendbares, aber von Natur aus unvollständiges System hoffen.

Abschließend wird manchmal vergessen, dass selbst einfache Typsysteme unvollständig sind ! ZB auch in Java

int f(int x) {
   if (x+2 != 2+x)
      return "Houston, we have a problem!";
   return 42;
}

ist semantisch typsicher (es wird immer eine Ganzzahl zurückgegeben), aber die Typprüfung beschwert sich über die nicht erreichbare Rückgabe.

Chi
quelle