AALIE

Loop Invariant (Invariante de Ciclo)

Demostración de correctitud mediante invariantes de ciclo, aplicada a algoritmos de ordenamiento.

2. Loop Invariant (Invariante de Ciclo)

El loop invariant (invariante de ciclo) es el mecanismo que usamos para demostrar que un algoritmo es correcto, es decir, que hace lo que dice que hace. Reemplaza la costumbre de probar con casos, ya que los casos nunca demuestran correctitud general.

El invariante es una propiedad lógica que:

Captura la razon de ser del algoritmo (su semantica).
Esta asociada al ciclo principal del algoritmo.
Debe demostrarse en exactamente 3 momentos.

Los 3 momentos del Loop Invariant

inicialización: La propiedad es cierta antes de la primera iteración del ciclo.
mantenimiento: Si la propiedad es cierta antes de una iteración, sigue siendo cierta antes de la siguiente iteración.
finalización: Cuando el ciclo termina, la propiedad combinada con la condición de parada demuestra que el algoritmo funciona correctamente.

2.1 Nociones de Secuencia y Conjunto

Para formular invariantes correctamente, es crucial distinguir:

Secuencia

El orden importa. $S_{1} = ⟨ 3, 7, 1, 5, 4 ⟩$ es diferente de $S_{2} = ⟨ 7, 3, 5, 4, 1 ⟩$ aunque tengan los mismos elementos.

Conjunto

El orden no importa. $A = {3, 7, 1, 5, 4}$ es igual que $B = {7, 1, 5, 3, 4}$ .

Regla para invariantes

En los invariantes siempre se trabaja con secuencias cuando el orden de los elementos importa (como en ordenamiento).

2.2 Ejemplo: Algoritmo de Inserción

El algoritmo de ordenamiento por inserción funciona bajo el paradigma incremental: mantiene un subarreglo ordenado que crece en cada iteración.

InsertionSort

InsertionSort (E/S int A[n]) {
  for i <- 2 to n do
    x <- A[i]
    j <- i - 1
    while (j >= 1) and (x < A[j]) do
      A[j+1] <- A[j]
      j <- j - 1
    endwhile
    A[j+1] <- x
  endfor
}

¿Cómo funciona? Empieza en la posición 2 ( $i = 2$ ). Para cada posición $i$ , extrae el elemento $A [i]$ y lo inserta en la posición correcta dentro del subarreglo ya ordenado $A [1.. i - 1]$ .

Invariante del ciclo for

Los elementos en las posiciones $A [1.. i - 1]$ son los mismos elementos que estaban en $A [1.. i - 1]$ al inicio, pero organizados en orden no decreciente.

Demostración de los 3 momentos

Demostración del invariante de Insertion Sort

Momento	i	Estado del arreglo	¿Se cumple?
Inicialización	$i = 2$	$A [1..1]$ tiene un solo elemento. Por definición, un arreglo de un elemento está ordenado.	Si
Mantenimiento	$i = k$	Antes de la iteración $k$ , $A [1.. k - 1]$ está ordenado. El while inserta $A [k]$ en su lugar correcto, dejando $A [1.. k]$ ordenado.	Si
Finalización	$i = n + 1$	Cuando el for termina ( $i = n + 1$ ), la propiedad dice que $A [1.. n]$ está ordenado. El arreglo completo está ordenado.	Correctitud demostrada

Nota

En la formulacion del invariante nunca se habla de $j$ (variable del ciclo interno). El invariante del for solo habla de $i$ . Cada ciclo tiene su propio invariante.

2.3 Análisis de Eficiencia — Insertion Sort

Mejor Caso (arreglo ya ordenado)

El while nunca se ejecuta porque la condición $x < A [j]$ es siempre falsa (el elemento a insertar ya está en su lugar).

Mejor caso de Insertion Sort

Linea	Costo
for i <- 2 to n	$n$
x <- A[i]	$n - 1$
j <- i-1	$n - 1$
while (condición)	$n - 1$
A[j+1] <- x	$n - 1$

Resultado del mejor caso

$T_{b es t} (n) = A n — B$ -> lineal $O (n)$ .

Peor Caso (arreglo en orden inverso)

El while se ejecuta el máximo numero de veces. Para la iteración $i$ , el while se ejecuta $i - 1$ veces (hay que mover el elemento hasta la posición 1).

i = 2 \sum n (i - 1) = 1 + 2 + 3 + \dots + (n - 1) = \frac{n ( n - 1 )}{2}

Peor caso de Insertion Sort

Linea	Costo
for i <- 2 to n	$n$
x <- A[i]	$n - 1$
j <- i-1	$n - 1$
while (condición)	$\frac{n ( n - 1 )}{2}$
A[j+1] <- x	$n - 1$

Resultado del peor caso

$T_{w ors t} (n) = a n^{2} + bn + c$ -> cuadrática $O (n^{2})$ .

2.4 Ejemplo: Algoritmo Burbuja (Bubble Sort)

BubbleSort

BubbleSort (E/S int A[n]) {
  for i <- 1 to (n-1) do
    for j <- 1 to (n-i) do
      if A[j] > A[j+1] then
        swap(A[j], A[j+1])
      endif
    endfor
  endfor
}

Invariante del ciclo for externo (variable i)

Después de completar la iteración $i$ del ciclo externo, los $i$ elementos más grandes están en sus posiciones definitivas al final del arreglo $A [n - i + 1.. n]$ , en orden no decreciente.

Demostración de los 3 momentos

Inicialización (i=1):Antes de empezar, no hay elementos asegurados al final del arreglo. La propiedad es trivialmente cierta (0 elementos ordenados al final).
Mantenimiento:Durante la iteración $i$ , el ciclo interno empuja el máximo elemento del subarreglo no ordenado $A [1.. n - i + 1]$ hacia la posición $n - i + 1$ . Al terminar, ese elemento queda en su posición definitiva.
Finalización (i=n):Se han colocado los $n - 1$ elementos más grandes. El único restante es el más pequeño y ya está en su lugar. El arreglo está completamente ordenado.

Eficiencia de Bubble Sort

El for interno se ejecuta $n - i$ veces para cada valor de $i$ :

i = 1 \sum n - 1 (n - i) = (n - 1) + (n - 2) + \dots + 1 = \frac{n ( n - 1 )}{2}

Función de eficiencia de Bubble Sort

Función de eficiencia

T (n) = C_{1} n + (C_{2} + C_{3}) \frac{n ( n - 1 )}{2} + C_{4} \frac{n ( n - 1 )}{2}

Forma cuadrática

T (n) = a n^{2} + bn + c

Resultado

$T (n) = a n^{2} + bn + c$ -> $O (n^{2})$ en ambos casos.

Nota

Ojo: Bubble Sort es $O (n^{2})$ tanto en el mejor como en el peor caso, porque aunque no haga intercambios (mejor caso), sigue haciendo todas las comparaciones.