En informática , el análisis de terminación es un análisis de programas que intenta determinar si la evaluación de un programa determinado se detiene para cada entrada. Esto significa determinar si el programa de entrada calcula una función total .
Está estrechamente relacionado con el problema de la detención , que consiste en determinar si un programa dado se detiene para una entrada dada y cuál es indecidible . El análisis de terminación es incluso más difícil que el problema de la detención: el análisis de terminación en el modelo de máquinas de Turing como modelo de programas que implementan funciones computables tendría el objetivo de decidir si una máquina de Turing dada es una máquina de Turing total , y este problema está en el nivel de la jerarquía aritmética y, por lo tanto, es estrictamente más difícil que el problema de la detención.
Ahora bien, como la cuestión de si una función computable es total no es semidecidible , [1] cada analizador de terminación de sonido (es decir, nunca se da una respuesta afirmativa para un programa que no termina) es incompleto , es decir, debe fallar en la determinación de la terminación para infinitos programas que terminan, ya sea ejecutándose para siempre o deteniéndose con una respuesta indefinida.
Una prueba de terminación es un tipo de prueba matemática que juega un papel crítico en la verificación formal porque la corrección total de un algoritmo depende de la terminación.
Un método simple y general para construir pruebas de terminación implica asociar una medida con cada paso de un algoritmo. La medida se toma del dominio de una relación bien fundada , como por ejemplo de los números ordinales . Si la medida "decrece" según la relación a lo largo de cada paso posible del algoritmo, debe terminar, porque no hay cadenas descendentes infinitas con respecto a una relación bien fundada.
Algunos tipos de análisis de terminación pueden generar o implicar automáticamente la existencia de una prueba de terminación.
Un ejemplo de una construcción de lenguaje de programación que puede o no terminar es un bucle , ya que se puede ejecutar repetidamente. Los bucles implementados mediante una variable de contador , como los que se encuentran normalmente en los algoritmos de procesamiento de datos , generalmente terminarán, como se demuestra en el siguiente ejemplo de pseudocódigo :
i := 0 bucle hasta que i = TAMAÑO_DE_DATOS process_data(data[i])) // procesar el fragmento de datos en la posición i i := i + 1 // pasar al siguiente fragmento de datos que se procesará
Si el valor de SIZE_OF_DATA no es negativo, es fijo y finito, el bucle eventualmente terminará, asumiendo que process_data también termina.
Se puede demostrar que algunos bucles siempre terminan o nunca terminan mediante una inspección humana. Por ejemplo, el siguiente bucle, en teoría, nunca se detendrá. Sin embargo, puede detenerse cuando se ejecuta en una máquina física debido a un desbordamiento aritmético : ya sea que genere una excepción o haga que el contador vuelva a un valor negativo y permita que se cumpla la condición del bucle.
i := 1 bucle hasta i = 0 yo := yo + 1
En el análisis de terminación también se puede intentar determinar el comportamiento de terminación de algún programa en función de una entrada desconocida. El siguiente ejemplo ilustra este problema.
i := 1 bucle hasta que i = DESCONOCIDO yo := yo + 1
Aquí la condición del bucle se define utilizando un valor UNKNOWN, donde el valor de UNKNOWN no se conoce (por ejemplo, definido por la entrada del usuario cuando se ejecuta el programa). Aquí el análisis de terminación debe tener en cuenta todos los valores posibles de UNKNOWN y descubrir que en el posible caso de UNKNOWN = 0 (como en el ejemplo original) no se puede mostrar la terminación.
Sin embargo, no existe un procedimiento general para determinar si una expresión que implica instrucciones de bucle se detendrá, incluso cuando la inspección la realizan seres humanos. La razón teórica de esto es la indecidibilidad del problema de la detención: no puede existir un algoritmo que determine si un programa determinado se detiene después de un número finito de pasos de cálculo.
En la práctica, no se puede demostrar la terminación (o no terminación) porque cada algoritmo trabaja con un conjunto finito de métodos capaces de extraer información relevante de un programa determinado. Un método puede observar cómo cambian las variables con respecto a alguna condición de bucle (posiblemente mostrando la terminación para ese bucle), otros métodos pueden intentar transformar el cálculo del programa en alguna construcción matemática y trabajar sobre eso, posiblemente obteniendo información sobre el comportamiento de la terminación a partir de algunas propiedades de este modelo matemático. Pero como cada método solo puede "ver" algunas razones específicas para la (no) terminación, incluso a través de la combinación de tales métodos no se pueden cubrir todas las posibles razones para la (no) terminación. [ cita requerida ]
Las funciones recursivas y los bucles son equivalentes en expresión; cualquier expresión que involucre bucles se puede escribir utilizando recursión, y viceversa. Por lo tanto, la terminación de expresiones recursivas también es indecidible en general. Se puede demostrar que la mayoría de las expresiones recursivas que se encuentran en el uso común (es decir, no patológicas ) terminan a través de varios medios, generalmente dependiendo de la definición de la expresión misma. Como ejemplo, el argumento de la función en la expresión recursiva para la función factorial a continuación siempre disminuirá en 1; por la propiedad de buen orden de los números naturales , el argumento eventualmente alcanzará 1 y la recursión terminará.
función factorial (argumento como número natural) si argumento = 0 o argumento = 1 devuelve 1 en caso contrario devuelve argumento * factorial(argumento - 1)
La comprobación de terminación es muy importante en lenguajes de programación de tipos dependientes y sistemas de demostración de teoremas como Coq y Agda . Estos sistemas utilizan el isomorfismo de Curry-Howard entre programas y pruebas. Las pruebas sobre tipos de datos definidos inductivamente se describían tradicionalmente utilizando principios de inducción. Sin embargo, más tarde se descubrió que describir un programa a través de una función definida recursivamente con coincidencia de patrones es una forma más natural de demostrar que usar principios de inducción directamente. Desafortunadamente, permitir definiciones no terminantes conduce a una inconsistencia lógica en las teorías de tipos [ cita requerida ] , por lo que Agda y Coq tienen comprobadores de terminación integrados.
Uno de los enfoques para la comprobación de terminación en lenguajes de programación con tipado dependiente son los tipos de tamaño. La idea principal es anotar los tipos sobre los que podemos realizar una recursión con anotaciones de tamaño y permitir llamadas recursivas solo en argumentos más pequeños. Los tipos de tamaño se implementan en Agda como una extensión sintáctica.
Existen varios equipos de investigación que trabajan en nuevos métodos que pueden mostrar la (no) terminación. Muchos investigadores incluyen estos métodos en programas [2] que intentan analizar el comportamiento de terminación automáticamente (es decir, sin interacción humana). Un aspecto en curso de la investigación es permitir que los métodos existentes se utilicen para analizar el comportamiento de terminación de programas escritos en lenguajes de programación del "mundo real". Para lenguajes declarativos como Haskell , Mercury y Prolog , existen muchos resultados [3] [4] [5] (principalmente debido a la sólida base matemática de estos lenguajes). La comunidad de investigación también trabaja en nuevos métodos para analizar el comportamiento de terminación de programas escritos en lenguajes imperativos como C y Java.
Los artículos de investigación sobre el análisis de la terminación automatizada de programas incluyen:
Las descripciones del sistema de herramientas de análisis de terminación automatizada incluyen:
