Provando uma operação de classificação no sistema de tipos

Quero saber até que ponto um sistema de tipos em uma linguagem de programação pode ser benéfico. Por exemplo, eu sei que em uma linguagem de programação de tipo dependente, podemos criar uma Vectorclasse incorporando o tamanho do vetor na assinatura do tipo. É como um exemplo de fato. Também podemos escrever uma função appendusando essas assinaturas para que o compilador prove que o tamanho da lista resultante será a soma das listas de entrada.

Existe uma maneira de codificar, por exemplo, na assinatura de tipo de um algoritmo de classificação para que o compilador garanta que a lista resultante seja uma permutação da lista de entrada? Como isso pode ser feito, se for possível?

Sim, é possível expressar um tipo preciso para uma rotina de classificação, de forma que qualquer função desse tipo precise classificar a lista de entrada.

Embora possa haver uma solução mais avançada e elegante, esboçarei apenas uma elementar.

Usaremos uma notação do tipo Coq. Começamos definindo um predicado que requer que f: nat -> natatue como uma permutação em :$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) .

Um lema simples pode ser facilmente provado.

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

Definimos qual é o ésimo elemento de uma lista com comprimento . Esta função requer uma prova afirmando que realmente é válido.$m$$n$h$m<n$

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

Dada uma ordem A, podemos expressar que uma lista está classificada:

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

Finalmente, aqui está o tipo de um algoritmo de classificação:

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

O tipo de saída afirma que a lista de resultados spossui elementos, é classificada e que existe uma permutação de que mapeia os elementos na lista de entrada para os da lista de saída . Observe que precisamos invocar o lema acima para provar , exigido por .$n$$0..n-1$ls$f(m) < n$nth

Note, no entanto, que é o usuário, ou seja, o programador, que deve provar seu algoritmo de classificação correto. O compilador não apenas verifica se a classificação está correta: tudo o que faz é verificar uma prova fornecida. De fato, o compilador não pode fazer muito mais do que isso: propriedades semânticas como "este programa é um algoritmo de classificação" são indecidíveis (pelo teorema de Rice), portanto, não podemos esperar tornar a etapa de prova totalmente automática.

Em um futuro distante, ainda podemos esperar que os provadores de teoremas automáticos fiquem tão inteligentes que "a maioria" dos algoritmos praticamente usados ​​possa ser automaticamente provada correta. O teorema de Rice apenas afirma que isso não pode ser feito em todos os casos. Tudo o que podemos esperar é um sistema correto, amplamente aplicável, mas inerentemente incompleto.

Como nota final, às vezes esquece-se que mesmo sistemas simples são incompletos ! Por exemplo, mesmo em Java

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

é semanticamente tipo seguro (sempre retorna um número inteiro), mas o verificador de tipos reclamará do retorno inacessível.

Twan van Laarhoven tem um bom exemplo totalmente elaborado na Agda, de "Correção e tempo de execução do mergesort, tipo de inserção e tipo de seleção".

Os comentários também são interessantes: neles, a solução de Bob Atkey, que envolve uma profunda incorporação da Linear Logic, é mencionada, por exemplo.