Nivel 8 · Quicksort verificado (experto)

Qué significa «correcto»

El módulo anterior aplicó el marco de Lean a una lógica: el teorema de completitud de la

quedó certificado por el núcleo. Este módulo lo aplica a un algoritmo: el mismo principio de «pruebas como términos» de la correspondencia de Curry–Howard y la misma auditoría de axiomas certifican ahora la corrección de un programa. Es el segundo estudio de caso de la teoría de los módulos anteriores, y antes de probar nada hay que fijar, con precisión total, qué se va a probar.

Dos mitades independientes

Un algoritmo de ordenamiento toma una secuencia finita de elementos de un dominio totalmente ordenado y los reorganiza en orden no decreciente. «Reorganiza» es la palabra clave: un algoritmo de ordenamiento no puede inventar, descartar ni duplicar elementos. Por ello la corrección tiene dos partes independientes, ambas necesarias:

Ordenamiento. La salida está en orden no decreciente.
Permutación. La salida contiene exactamente los mismos elementos que la entrada, con las mismas multiplicidades (es una reorganización).

Definición 12.1 (Función de ordenamiento)

Sea $(\alpha,\leq)$ un tipo linealmente ordenado. Una función $f:\mathrm{List}\,\alpha\to\mathrm{List}\,\alpha$ ordena si para toda lista $\ell$ ,

f(\ell)\ \sim\ \ell \qquad\text{y}\qquad \mathsf{Sorted}\big(f(\ell)\big),

donde $\sim$ denota «es una permutación de» y $\mathsf{Sorted}$ «está en orden no decreciente». El objetivo del módulo es probar que quicksort satisface ambos conyuntos.

Nota (Ninguna mitad basta por sí sola)

Este es el punto metodológico central de la especificación, y la tesis lo ilustra con los dos contraejemplos mínimos. La función constante que devuelve $[\,]$ produce siempre una lista ordenada, pero no es una permutación de la entrada: satisface la mitad de ordenamiento y viola la de permutación. La función identidad devuelve siempre una permutación de la entrada (la trivial), pero no la ordena: satisface la mitad de permutación y viola la de ordenamiento. Solo la conjunción de las dos mitades caracteriza «ordenar». Una especificación incompleta es una especificación falsa: un teorema que probara únicamente $\mathsf{Sorted}(f(\ell))$ sería verificado por el núcleo con la misma solemnidad para la función constante $[\,]$ .

«Ordenada», con precisión

Se toma la definición de teoría del orden más cómoda para razonar por inducción: una lista está ordenada cuando cada elemento precede (o iguala) a todo elemento posterior.

Definición 12.2 (Ordenada)

Una lista $\ell=[a_0,a_1,\dots,a_{n-1}]$ está ordenada si $a_i\leq a_j$ siempre que $i\leq j$ . De forma equivalente, escribiendo el predicado como una relación por pares,

\mathsf{Sorted}(\ell)\ :\Longleftrightarrow\ \mathrm{Pairwise}\,(\leq)\,\ell,

es decir, para cualquier elección de un elemento anterior $a$ y uno posterior $b$ en $\ell$ , se tiene $a\leq b$ .

La formulación por pares es conveniente porque se reparte limpiamente sobre la concatenación, que es exactamente la operación con la que quicksort ensambla su salida (véase el lema de la página de ordenamiento). En Lean la definición es un traslado literal, en Thesis/Sort/Quicksort.lean:

def Sorted (l : List α) : Prop := l.Pairwise (· ≤ ·)

«Permutación», con precisión

Definición 12.3 (Permutación)

Dos listas son permutaciones una de otra, escrito $\ell_1\sim\ell_2$ , si una se obtiene de la otra reordenando. Formalmente, $\sim$ es la menor relación de equivalencia sobre listas cerrada bajo el intercambio de elementos adyacentes; equivalentemente, $\ell_1\sim\ell_2$ si y solo si cada valor aparece el mismo número de veces en $\ell_1$ que en $\ell_2$ (igualdad como multiconjuntos). La permutación es reflexiva, simétrica y transitiva, es una congruencia para la concatenación ( $\ell_1\sim\ell_1'$ y $\ell_2\sim\ell_2'$ implican $\ell_1 +\!\!+\, \ell_2\sim\ell_1' +\!\!+\, \ell_2'$ ) e implica igualdad de pertenencia ( $a\in\ell_1\leftrightarrow a\in\ell_2$ ).

Estas propiedades de clausura estándar de $\sim$ son los únicos hechos sobre permutaciones que se usarán; en Lean son Perm.append, Perm.cons, Perm.trans, perm_middle y Perm.mem_iff. La condición de multiplicidad importa: $[2,1,2,1]$ debe ordenarse a $[1,1,2,2]$ , no a $[1,2]$ ; un ordenamiento no es una deduplicación.

Nota (Alcance)

Lo que se verifica por máquina en este módulo es la corrección funcional de quicksort (permutación y ordenamiento) sobre listas de un tipo linealmente ordenado cualquiera, en su versión funcional (basada en filter, no en una variante in-place sobre arreglos). Quedan fuera del alcance el análisis de complejidad (los casos promedio $O(n\log n)$ y peor $O(n^2)$ ), el uso de memoria y las estrategias de elección de pivote: aquí interesa qué calcula el algoritmo, no cuán rápido.

El plan del módulo

Con la especificación fijada, el desarrollo tiene cuatro etapas, cada una con su matemática y su realización en Lean lado a lado: la definición del algoritmo y su terminación (que no es gratuita, porque la recursión no es estructural), la mitad de permutación, la mitad de ordenamiento, y la combinación final con su auditoría de axiomas. Como en el módulo anterior, el desarrollo no usa ningún sorry ni lema postulado; los archivos fuente son Thesis/Sort/Quicksort.lean, Thesis/Sort/Examples.lean y Thesis/Sort/Audit.lean. El marco teórico que hace posible todo esto es el de (Avigad et al., 2015) sobre la base del CIC de (Coquand y Huet, 1988) y (Coquand y Paulin, 1990) .