Ondulación

En informática , más concretamente en la demostración automática de teoremas , el rippling ^{[ 1 ]} es un conjunto de heurísticas de metanivel , desarrolladas principalmente en el Grupo de Razonamiento Matemático de la Escuela de Informática de la Universidad de Edimburgo , y utilizadas habitualmente para guiar las demostraciones inductivas en sistemas de demostración automática de teoremas . El rippling puede considerarse una forma restringida de sistema de reescritura , donde se utilizan anotaciones especiales a nivel de objeto para garantizar la fertilización al finalizar la reescritura, con un requisito de disminución de la medida que asegura la terminación para cualquier conjunto de reglas y expresiones de reescritura.

Raymond Aubin fue el primero en utilizar el término «propagación» mientras trabajaba en su tesis doctoral de 1976 ^{[ 2 ]} en la Universidad de Edimburgo. Reconoció un patrón común de movimiento durante la etapa de reescritura de las demostraciones inductivas. Posteriormente, Alan Bundy invirtió este concepto al definir la propagación como este patrón de movimiento, en lugar de un efecto secundario.

Desde entonces, se acuñaron expresiones como "ondular lateralmente", "ondular hacia adentro" y "ondular al pasar", por lo que el término se generalizó a "ondular". El concepto de ondular continúa desarrollándose en Edimburgo y otros lugares, a fecha de 2007.

El método de propagación por ondas se ha aplicado a muchos problemas tradicionalmente considerados difíciles en la comunidad de demostración de teoremas inductivos, incluidos los teoremas límite de Bledsoe y una demostración del microprocesador Gordon, una computadora en miniatura desarrollada por Michael JC Gordon y su equipo en Cambridge.

Muy a menudo, al intentar demostrar una proposición, se nos proporciona una expresión de origen y una expresión de destino que solo difieren por la inclusión de algunos elementos sintácticos adicionales.

Esto es especialmente cierto en las demostraciones inductivas , donde la expresión dada se considera la hipótesis inductiva y la expresión resultante, la conclusión inductiva. Por lo general, las diferencias entre la hipótesis y la conclusión son mínimas, como la inclusión de una función sucesora (por ejemplo, +1) alrededor de la variable de inducción.

Al inicio del proceso de ondulación, se identifican las diferencias entre las dos expresiones, conocidas como frentes de onda en la jerga de la ondulación. Por lo general, estas diferencias impiden completar la demostración y deben eliminarse. La expresión objetivo se anota para distinguir los frentes de onda (diferencias) y la estructura común entre ambas expresiones. Posteriormente, se pueden utilizar reglas especiales, denominadas reglas de onda, de forma secuencial para manipular la expresión objetivo hasta que la expresión original pueda utilizarse para completar la demostración.

Nuestro objetivo es demostrar que la suma de números naturales es conmutativa . Esta es una propiedad elemental, y la demostración se realiza mediante inducción rutinaria. Sin embargo, el espacio de búsqueda para encontrar dicha demostración puede ser bastante amplio.

Por lo general, el caso base de cualquier demostración inductiva se resuelve mediante métodos distintos al de propagación en cascada. Por esta razón, nos centraremos en el caso escalonado. Nuestro caso escalonado adopta la siguiente forma, donde hemos optado por usar x como variable de inducción:

También podemos poseer varias reglas de reescritura, derivadas de lemas, definiciones inductivas o de otras fuentes, que pueden utilizarse para formar reglas de onda. Supongamos que tenemos las siguientes tres reglas de reescritura:

Entonces, estos se pueden anotar para formar:

Nótese que todas estas reglas anotadas conservan el esqueleto (x + y = y + x, en el primer caso y x + y en el segundo/tercero). Ahora, al anotar el caso del paso inductivo, obtenemos:

Y estamos listos para realizar el efecto dominó:

Nótese que la reescritura final hace desaparecer todos los frentes de onda, y ahora podemos aplicar la fertilización, la aplicación de las hipótesis inductivas, para completar la demostración.

• David A. Basin y Toby Walsh (1996). "Un cálculo para la terminación de la ondulación" (PDF) . Journal of Automated Reasoning . 16 ( 1–2 ): 147–180 . doi : 10.1007/BF00244462 . S2CID 14427821 .