Resumen Técnico: Semántica Axiomática No Estándar

Planteamiento del Problema

El artículo aborda una ambigüedad fundamental en la semántica axiomática basada en la lógica de Hoare. Análogamente a los modelos no estándar de la aritmética de Peano de Skolem, el autor demuestra que la lógica de Hoare admite modelos no estándares de ejecución de programas. Específicamente, la lógica no caracteriza de manera única la semántica operacional pretendida (semántica de trazas) de los lenguajes de programación hasta el isomorfismo.

El problema central surge en la Regla de Iteración. Mientras que la lógica de Hoare utiliza invariantes inductivos para razonar sobre bucles, la teoría lógica estándar no puede distinguir entre:

1. Trazas estándar: Ejecuciones finitas y ejecuciones infinitas indexadas por números naturales estándar ($\mathbb{N}$).
2. Trazas no estándares: Ejecuciones indexadas por números naturales no estándares (por ejemplo, modelos de Skolem que contienen "pasados infinitos" o "futuros infinitos" más allá de $\omega$ estándar).

Consecuentemente, una prueba de lógica de Hoare válida para un modelo de traza estándar también es válida para modelos no estándares donde los bucles pueden tener longitudes no estándares (por ejemplo, comenzando en un pasado no estándar o continuando hacia un futuro no estándar). Esto implica que la lógica de Hoare, tal como se formula tradicionalmente, no especifica una semántica operacional única y bien definida.

Metodología

El autor emplea un análisis comparativo entre la semántica de traza estándar y la semántica de traza no estándar, utilizando conceptos de la interpretación abstracta y la teoría de puntos fijos.

1. Formalización de la Semántica de Trazas:

   • Semántica Estándar: Definida mediante puntos fijos de mínimo ($lfp$) y máximo ($gfp$) en el retículo de trazas finitas ($\Sigma^*$) e infinitas ($\Sigma^\infty$) indexadas por $\mathbb{N}$.
   • Semántica No Estándar: Extendida a trazas indexadas por conjuntos no estándares como $\mathbb{N} + \delta$ (trazas no estándar hacia adelante con un futuro infinito) y $\mathbb{N} - \delta$ (trazas no estándar hacia atrás con un pasado infinito), donde $\delta > 0$. Estos conjuntos modelan estructuras de tipo Skolem.

2. Abstracción y Equivalencia:

   • El artículo define una función de abstracción $\alpha_S$ que mapea la semántica de trazas al conjunto de triples de Hoare válidos.
   • El Teorema 1 demuestra que el conjunto de triples de Hoare válidos para la semántica estándar ($H(L)$) es idéntico al conjunto de triples válidos para la semántica no estándar ($\tilde{H}(L)$). Esto confirma que las reglas de prueba de la lógica de Hoare estándar son insuficientes para descartar interpretaciones no estándares.

3. Remedio Propuesto (Estandarización):
   Para resolver esta ambigüedad, el autor propone enriquecer la semántica axiomática con obligaciones de prueba adicionales inspiradas en los métodos de prueba de terminación (específicamente el método de Knuth y variantes ordinales).

   • Prevención de Trazas Hacia Adelante No Estándares: La lógica se extiende para requerir la existencia de una función creciente $K$ que mapea las posiciones de la traza a ordinales ($\mathcal{O}$) de tal manera que el contador del bucle esté acotado por el primer límite infinito $\omega$. Dado que las partes enteras no estándares no pueden ser orden-isomorfas a ordinales bien fundados, este requisito elimina las trazas hacia adelante infinitas no estándares.
   • Prevención de Trazas Hacia Atrás No Estándares: Se introduce un requisito dual para las trazas hacia atrás, requiriendo una función decreciente $K$ (antitónica) que asegure que el recorrido hacia atrás termine dentro de un límite estándar.

Contribuciones Clave

• Identificación de Modelos No Estándares: El artículo establece formalmente que la lógica de Hoare sufre del mismo problema de no unicidad que la aritmética de Peano sin la condición de categoricidad de Dedekind. Demuestra que los invariantes de bucle en la lógica de primer orden no pueden distinguir entre modelos de traza estándar y no estándar debido al teorema de compacidad.
• Equivalencia de Teorías: Prueba que las teorías de la lógica de Hoare estándar y no estándar son idénticas ($H(L) = \tilde{H}(L)$), lo que significa que las pruebas existentes no excluyen inherentemente las ejecuciones no estándares.
• Estandarización mediante Restricciones Ordinales: El artículo propone un método para restringir la semántica axiomática a modelos estándar mediante la adición de obligaciones de prueba que involucran contadores ordinales (acotados por $\omega$ para trazas hacia adelante y requiriendo terminación para trazas hacia atrás).
• Preservación de Pruebas Estándar: Un resultado crucial es que estas obligaciones de prueba adicionales son siempre satisfechas por la semántica de traza estándar. Por lo tanto, si se asume la interpretación estándar (como es implícito en la mayoría de los usos de la lógica de Hoare), las pruebas de Hoare existentes permanecen válidas y sin cambios. Las nuevas obligaciones sirven para excluir formalmente los modelos no estándares sin alterar la verificación práctica de los programas estándar.

Resultados

• Equivalencia Teórica: El conjunto de triples de Hoare válidos para modelos de traza no estándar es exactamente el mismo que para los modelos estándar.
• Resolución de la Ambigüedad: Al imponer las condiciones de acotación ordinal (Ecuaciones 9 y 10), la semántica axiomática se restringe al modelo estándar.
• Aplicabilidad: La estandarización propuesta es compatible con los algoritmos de análisis estático y de tipado existentes que dependen de la lógica de Hoare, siempre que la suposición de la semántica estándar se haga explícita o se verifiquen las nuevas obligaciones (lo cual es trivial para los modelos estándar).
• Limitaciones: El artículo señala que en las Lógicas de Hoare Abstractas, donde el dominio concreto es reemplazado por un dominio abstracto que puede no ser lo suficientemente expresivo para definir las funciones ordinales requeridas, los métodos de estandarización podrían no ser directamente aplicables.

Significado

El artículo argumenta que la afirmación común de que "la semántica axiomática define el significado de un programa mediante sus efectos sobre las aserciones lógicas" es técnicamente errónea porque el significado definido no es único hasta el isomorfismo. La importancia radica en:

1. Clarificación de los Fundamentos: Destaca que la lógica de Hoare, al igual que la aritmética de Peano, requiere una condición de "categoricidad" (en este caso, la estandarización mediante límites ordinales) para asegurar una interpretación operacional única.
2. Formalización de Supuestos Implícitos: Hace explícita la hipótesis implícita de que la lógica de Hoare se interpreta sobre modelos de computación estándar.
3. Puente entre Lógica y Semántica: Demuestra cómo las técnicas de prueba de terminación (usando ordinales) pueden integrarse en la semántica axiomática para eliminar las interpretaciones no estándares, alineando así la semántica axiomática de manera más rigurosa con la semántica de trazas operacional.

El autor concluye que, si bien las pruebas de la lógica de Hoare no necesitan ser cambiadas para los modelos estándar, el marco teórico debe reconocer y excluir formalmente los modelos no estándar para reclamar una definición única de la semántica de programas.