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 determinado se detiene ante una entrada determinada 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 las máquinas de Turing como modelo de programas que implementan funciones computables tendría el objetivo de decidir si una determinada máquina de Turing es una máquina de Turing total , y este problema es al nivel de la jerarquía aritmética y, por tanto, es estrictamente más difícil que el problema de 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 al determinar la terminación de una cantidad infinita finalizar programas, ya sea ejecutándolos para siempre o deteniéndolos con una respuesta indefinida.
Una prueba de terminación es un tipo de prueba matemática que desempeña un papel fundamental en la verificación formal porque la corrección total de un algoritmo depende de la terminación.
Un método general simple 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 fundada , como por ejemplo de los números ordinales . Si la medida "disminuye" según la relación a lo largo de cada paso posible del algoritmo, debe terminar, porque no hay infinitas cadenas descendentes con respecto a una relación bien fundada.
Algunos tipos de análisis de rescisión pueden generar o implicar automáticamente la existencia de una prueba de rescisión.
Un ejemplo de una construcción de lenguaje de programación que puede terminar o no es un bucle , ya que se pueden ejecutar repetidamente. Los bucles implementados usando una variable de contador como se encuentra típicamente en los algoritmos de procesamiento de datos generalmente terminarán, como lo demuestra el siguiente ejemplo de pseudocódigo :
i := 0 bucle hasta i = TAMAÑO_OF_DATA Process_data(data[i])) // procesa el fragmento de datos en la posición i i := i + 1 // pasa al siguiente fragmento de datos a procesar
Si el valor de SIZE_OF_DATA no es negativo, es fijo y finito, el ciclo eventualmente terminará, suponiendo que Process_data también termine.
Se puede demostrar que algunos bucles siempre terminan o nunca terminan mediante 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 provocando una excepción o provocando que el contador se ajuste a un valor negativo y permitiendo 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 dependiendo de alguna entrada desconocida. El siguiente ejemplo ilustra este problema.
i := 1 bucle hasta i = DESCONOCIDO yo := yo + 1
Aquí la condición del bucle se define utilizando algún valor DESCONOCIDO, donde el valor de DESCONOCIDO 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 DESCONOCIDO y descubrir que en el posible caso de DESCONOCIDO = 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 se encargue a humanos la inspección. La razón teórica de esto es la indecidibilidad del problema de la detención: no puede existir algún 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 mostrar la terminación (o no terminación) porque cada algoritmo funciona con un conjunto finito de métodos que pueden extraer información relevante de un programa determinado. Un método podría observar cómo cambian las variables con respecto a alguna condición de bucle (posiblemente mostrando la terminación de ese bucle), otros métodos podrían intentar transformar el cálculo del programa en alguna construcción matemática y trabajar en eso, posiblemente obteniendo información sobre el comportamiento de terminación de Algunas propiedades de este modelo matemático. Pero debido a que cada método sólo es capaz de "ver" algunas razones específicas para la (no) terminación, incluso mediante la combinación de dichos métodos no se pueden cubrir todas las razones posibles para la (no) terminación. [ cita necesaria ]
Las funciones recursivas y los bucles son equivalentes en expresión; cualquier expresión que incluya bucles se puede escribir mediante recursividad y viceversa. Por 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 función en la expresión recursiva de la función factorial siguiente siempre disminuirá en 1; Por la propiedad de buen orden de los números naturales , el argumento eventualmente llegará a 1 y la recursividad 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 verificación de terminación es muy importante en lenguajes de programación de tipo dependiente 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 mediante una función definida de forma recursiva con coincidencia de patrones es una forma más natural de demostrar que utilizar principios de inducción directamente. Desafortunadamente, permitir definiciones no terminantes conduce a una inconsistencia lógica en las teorías de tipos [ cita necesaria ] , razón por la cual Agda y Coq tienen verificadores de terminación incorporados.
Uno de los enfoques para la verificación de terminaciones en lenguajes de programación de tipo dependiente son los tipos de tamaño. La idea principal es anotar los tipos sobre los cuales podemos recurrir con anotaciones de tamaño y permitir llamadas recursivas solo en argumentos más pequeños. Los tipos dimensionados se implementan en Agda como una extensión sintáctica.
Hay varios equipos de investigación que trabajan en nuevos métodos que puedan demostrar 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 trabajos de investigación sobre análisis automatizado de terminación de programas incluyen:
Las descripciones del sistema de herramientas de análisis de terminación automatizadas incluyen:
