Nivel 8 · Quicksort verificado (experto)

El algoritmo y su terminación

Quicksort ( (Hoare, 1961) ; (Hoare, 1962) ) es un algoritmo de divide y vencerás. Dada una lista no vacía, elige un elemento como pivote (se toma la cabeza) y reparte los elementos restantes en los que son $\leq$ el pivote y los que son $>$ el pivote. Cada parte se ordena recursivamente y las partes ordenadas se concatenan con el pivote en medio. La lista vacía ya está ordenada.

Definición 12.4 (Quicksort funcional)

Sobre un tipo linealmente ordenado $\alpha$ , se define $\mathsf{qsort}:\mathrm{List}\,\alpha\to\mathrm{List}\,\alpha$ por

\mathsf{qsort}([\,]) = [\,], \qquad \mathsf{qsort}(p :: r) = \mathsf{qsort}(\ell_{\leq})\ +\!\!+\ \big(p :: \mathsf{qsort}(\ell_{>})\big),

donde, a partir de la cola $r$ , las dos mitades de la partición son

\ell_{\leq} = \mathsf{filter}\,(\lambda x.\,x\leq p)\,(r), \qquad \ell_{>} = \mathsf{filter}\,(\lambda x.\,\neg(x\leq p))\,(r).

Aquí $p$ es el pivote, $::$ es «cons» (anteponer) y $+\!\!+$ es la concatenación. Nótese que $\ell_{>}$ recoge exactamente los elementos que fallan la prueba $x\leq p$ , es decir, los que cumplen $p < x$ .

El hecho estructural clave, el que impulsará la prueba de ordenamiento, es que todo lo que queda a la izquierda del pivote es $\leq p$ y todo lo que queda a su derecha es $>p$ . Desplegar la recursión sobre una entrada concreta produce un árbol binario: cada nodo lleva su pivote, el hijo izquierdo trata los elementos $\leq$ el pivote y el derecho los elementos $>$ el pivote. Leer las hojas y los pivotes en orden (subárbol izquierdo, pivote, subárbol derecho) produce la salida ordenada. Para $[3,1,2,5,4,9]$ el pivote raíz es $3$ ; la mitad izquierda $[1,2]$ recurre con pivote $1$ , la derecha $[5,4,9]$ con pivote $5$ , y el recorrido en orden da $1,2,3,4,5,9$ .

Explóralo tú mismo

El widget despliega el árbol de recursión de cualquier entrada y comprueba en cada nodo los tres invariantes del desarrollo: la partición separa ( $\ell_{\leq}\leq p < \ell_{>}$ ), cada llamada recursiva es estrictamente más corta, y el recorrido en orden está ordenado.

Quicksort verificado, paso a paso

Los tres ingredientes de la corrección (terminación, permutación, cotas de separación) comprobados en cada nodo del árbol de recursión.

qs(3,1,4,1,5,9,2,6)pivote3⟶1,1,2++ [3] ++4,5,9,6

✓ terminación: |3| y |4| < |8|✓ Perm(entrada, salida)✓ separación: izq ≤ 3 < der

salida: 1,1,2,3,4,5,6,9(Sorted: las cotas garantizan que la concatenación queda ordenada)

nivel 1 / 5✓ Perm ∧ Sorted: la especificación completa se cumple

Lean: la definición y sus obligaciones

El texto de Lean siguiente, de Thesis/Sort/Quicksort.lean, es la definición literal. La prueba booleana decide (x ≤ p) convierte la proposición decidible $x\leq p$ en un Bool para que pueda dirigir List.filter; su negación ! decide (x ≤ p) selecciona la mitad complementaria.

def quicksort : List α → List α
  | [] => []
  | p :: rest =>
      quicksort (rest.filter (fun x => decide (x ≤ p)))
        ++ p :: quicksort (rest.filter (fun x => ! decide (x ≤ p)))
  termination_by l => l.length
  decreasing_by
    all_goals simp_wf
    all_goals exact le_trans (length_filter_le _ _) (le_of_eq (by simp))

Las dos líneas finales no son decoración. Quicksort no recurre sobre un subtérmino estructural: las mitades se computan por filtrado, no se obtienen por ajuste de patrones. Como se vio en el módulo sobre el CIC, una definición que no sigue la estructura de un tipo inductivo no es estructuralmente recursiva y exige una justificación de terminación frente al recursor bien fundamentado; antes de poder siquiera hablar de $\mathsf{qsort}$ como función total, hay que probar que la recursión termina. Aquí la medida es la longitud del argumento.

Lema 12.5 (El filtrado no aumenta la longitud)

Para todo predicado $q$ y lista $\ell$ , $\ |\mathsf{filter}(q)(\ell)|\leq|\ell|$ .

Demostración.

A probar: $|\mathsf{filter}(q)(\ell)|\leq|\ell|$ , para todo predicado $q$ y toda lista $\ell$ . Por inducción sobre $\ell$ .

$\ell=[\,]$ . $\mathsf{filter}(q)([\,])=[\,]$ , luego $|\mathsf{filter}(q)([\,])|=0=|[\,]|$ y $0\leq 0$ .
$\ell=a::\ell'$ . Por definición del filtrado se distinguen dos casos según $q\,a$ $q a$ :
- Si $q\,a$ se cumple: $\mathsf{filter}(q)(a::\ell')=a::\mathsf{filter}(q)(\ell')$ , luego $|\mathsf{filter}(q)(a::\ell')|=1+|\mathsf{filter}(q)(\ell')| \ \overset{\text{HI}}{\leq}\ 1+|\ell'|=|a::\ell'|.$
- Si $q\,a$ falla: $\mathsf{filter}(q)(a::\ell')=\mathsf{filter}(q)(\ell')$ , luego $|\mathsf{filter}(q)(a::\ell')|=|\mathsf{filter}(q)(\ell')| \ \overset{\text{HI}}{\leq}\ |\ell'|\ \leq\ 1+|\ell'|=|a::\ell'|.$

Proposición 12.6 (Terminación)

Cada llamada recursiva de $\mathsf{qsort}(p::r)$ es sobre una lista estrictamente más corta, de modo que $\mathsf{qsort}$ es una función total.

Demostración.

A probar: cada argumento recursivo de $\mathsf{qsort}(p::r)$ es una lista estrictamente más corta que $p::r$ .

Los dos argumentos recursivos son $\ell_{\leq}=\mathsf{filter}(\cdot\leq p)(r)$ y $\ell_{>}=\mathsf{filter}(\neg(\cdot\leq p))(r)$ .
Por el Lema 12.5, $|\ell_{\leq}|\leq|r|$ y $|\ell_{>}|\leq|r|$ .
Como $|p::r|=|r|+1$ , se sigue $|\ell_{\leq}|\leq|r| < |p::r| \qquad\text{y}\qquad |\ell_{>}|\leq|r| < |p::r|.$

Ambos argumentos son, pues, estrictamente menores en la medida $|\cdot|:\mathrm{List}\,\alpha\to\mathbb{N}$ . Esto justifica la recursión bien fundamentada y hace de $\mathsf{qsort}$ una función total.

Lean: descargar las obligaciones de terminación

Tras termination_by l => l.length, Lean pide probar que cada argumento recursivo es menor en el orden bien fundamentado. La táctica simp_wf reduce cada meta a $|\mathsf{filter}(q)(r)|\leq|r|$ , cerrada por length_filter_le (el Lema 12.5); el le_of_eq (by simp) final absorbe una reescritura contable de la longitud (el attach interno, usado para recordar que los elementos filtrados provienen de $r$ , satisface |r.attach| = |r|).

  decreasing_by
    all_goals simp_wf
    all_goals exact le_trans (length_filter_le _ _) (le_of_eq (by simp))

Nota (Las ecuaciones no son definicionales)

Como la definición usa recursión bien fundamentada (no estructural), la ecuación $\mathsf{qsort}([\,])=[\,]$ y el desplegado para $p::r$ no valen por mera computación del núcleo; Lean los provee como lemas de reescritura, que se nombran para usarlos en las pruebas de las dos páginas siguientes. También de Thesis/Sort/Quicksort.lean:

@[simp] theorem quicksort_nil : quicksort ([] : List α) = [] := by rw [quicksort]

theorem quicksort_cons (p : α) (rest : List α) :
    quicksort (p :: rest) =
      quicksort (rest.filter (fun x => decide (x ≤ p)))
        ++ p :: quicksort (rest.filter (fun x => ! decide (x ≤ p))) := by
  rw [quicksort]

Con la función total y sus ecuaciones a la mano, quedan las dos mitades de la Definición 12.1: la permutación y el ordenamiento.