Análisis de terminación

void f ( int n ) { mientras ( n > 1 ) si ( n % 2 == 0 ) n = n / 2 ; demás n = 3 * n + 1 ; }

A partir de 2021, todavía no se sabe si este C -programa termina por cada entrada; ver la conjetura de Collatz .

En informática , el análisis de terminación es un análisis de programa que intenta determinar si la evaluación de un programa dado 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 detención , que consiste en determinar si un programa dado se detiene para una entrada determinada y cuál es indecidible . El análisis de terminación es incluso más difícil que el problema de Halting: 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 es en el nivel de la jerarquía aritmética y, por lo tanto, es estrictamente más difícil que el problema de Detención.${\displaystyle \Pi _{2}^{0}}$

Ahora bien, como la pregunta 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) está incompleto , es decir, debe fallar al determinar la terminación para infinitos terminando programas, ya sea ejecutándolos para siempre o deteniéndolos con una respuesta indefinida.

Prueba de terminación

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 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 terminación pueden generar automáticamente o implicar la existencia de una prueba de terminación.

Ejemplo

Un ejemplo de una construcción de lenguaje de programación que puede terminar o no es un bucle , ya que pueden ejecutarse 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 ejemplo de pseudocódigo a continuación:

i: = 0 bucle hasta i = SIZE_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, fijo y finito, el bucle terminará eventualmente, asumiendo que process_data también termina.

Se puede mostrar que algunos bucles siempre terminan o nunca terminan mediante inspección humana. Por ejemplo, el siguiente ciclo, 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 de 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 alguna entrada desconocida. El siguiente ejemplo ilustra este problema.

i: = 1 bucle hasta i = DESCONOCIDO yo: = yo + 1

Aquí la condición de bucle se define usando 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 averiguar 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 en bucle se detendrá, incluso cuando se encomiende a seres humanos la inspección. La razón teórica de esto es la indecidibilidad del problema de detención: no puede existir algún algoritmo que determine si un programa dado se detiene después de un número finito de pasos de cálculo.

En la práctica, uno no muestra la terminación (o no terminación) porque cada algoritmo trabaja con un conjunto finito de métodos que pueden extraer información relevante de un programa dado. Un método podría observar cómo cambian las variables con respecto a alguna condición de ciclo (posiblemente mostrando la terminación de ese ciclo), 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 solo puede "ver" algunas razones específicas para la (no) terminación, incluso mediante 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 implique 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 en sí. 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 ordenamiento correcto 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)

Tipos dependientes

La verificación de terminación es muy importante en sistemas de prueba de teoremas y lenguajes de programación de tipo dependiente 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 de forma recursiva con coincidencia de patrones es una forma más natural de probar que usar los 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 eso Agda y Coq tienen comprobadores de terminación incorporados.

Tipos de tamaño

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 que 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.

La investigación actual

Hay varios equipos de investigación que trabajan en nuevos métodos que pueden mostrar (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 formación matemática de estos lenguajes). La comunidad de investigadores también trabaja en nuevos métodos para analizar el comportamiento de terminación de programas escritos en lenguajes imperativos como C y Java.

Debido a la indecidibilidad del problema de la detención, la investigación en este campo no puede llegar a ser completa. Siempre se pueden pensar en nuevos métodos que encuentren nuevas (complicadas) razones para la terminación.

Ver también

• Análisis de complejidad : el problema de estimar el tiempo necesario para terminar
• Variante de bucle
• Programación funcional total : un paradigma de programación que restringe el rango de programas a aquellos que están terminando de manera comprobable.
• Recursividad de Walther

Referencias

1. Rogers, Jr., Hartley (1988). Teoría de funciones recursivas y computabilidad efectiva . Cambridge (MA), Londres (Inglaterra): The MIT Press. pag. 476. ISBN 0-262-68052-1.
2. Herramientas en termination-portal.org
3. Giesl, J. y Swiderski, S. y Schneider-Kamp, P. y Thiemann, R. Pfenning, F. (ed.). Análisis de terminación automatizado para Haskell: de la reescritura de términos a los lenguajes de programación (conferencia invitada) (posdata) . Reescritura de términos y aplicaciones, 17th Int. Conf., RTA-06. LNCS. 4098 . págs. 297–312. (enlace: springerlink.com ).
4. Opciones del compilador para el análisis de terminación en Mercury
5. http://verify.rwth-aachen.de/giesl/papers/lopstr07-distribute.pdf

Los artículos de investigación sobre el análisis automatizado de terminación de programas incluyen:

• Christoph Walther (1988). "Algoritmos delimitados por argumentos como base para pruebas de terminación automatizadas". Proc. IX Jornadas de Deducción Automatizada . LNAI. 310 . Saltador. págs. 602–621.
• Christoph Walther (1991). "Sobre la prueba de la terminación de algoritmos por máquina" (PDF) . Inteligencia artificial . 70 (1).
• Xi, Hongwei (1998). "Hacia pruebas de terminación automatizadas mediante congelación " (PDF) . En Tobias Nipkow (ed.). Técnicas y aplicaciones de reescritura , 9º Int. Conf., RTA-98 . LNCS. 1379 . Saltador. págs. 271-285.
• Jürgen Giesl; Christoph Walther; Jürgen Brauburger (1998). "Análisis de terminación para programas funcionales". En W. Bibel; P. Schmitt (eds.). Deducción automatizada: una base para las solicitudes (posdata) . 3 . Dordrecht: Kluwer Academic Publishers. págs. 135-164.
• Christoph Walther (2000). "Criterios de rescisión". En S. Hölldobler (ed.). Intellectics and Computational Logic (posdata) . Dordrecht: Kluwer Academic Publishers. págs. 361–386.
• Christoph Walther; Stephan Schweitzer (2005). "Análisis de terminación automatizado para programas incompletamente definidos" (PDF) . En Franz Baader; Andrei Voronkov (eds.). Proc. 11 ° Int. Conf. en Lógica para Programación, Inteligencia Artificial y Razonamiento (LPAR) . LNAI. 3452 . Saltador. págs. 332–346.
• Adam Koprowski; Johannes Waldmann (2008). "Terminación ártica ... por debajo de cero". En Andrei Voronkov (ed.). Técnicas y aplicaciones de reescritura, XIX Int. Conf., RTA-08 (PDF) . Apuntes de conferencias en Ciencias de la Computación. 5117 . Saltador. págs. 202–216. ISBN 978-3-540-70588-8.

Las descripciones del sistema de herramientas de análisis de terminación automatizadas incluyen:

• Giesl, J. (1995). "Generación de pedidos polinomiales para pruebas de terminación (descripción del sistema)". En Hsiang, Jieh (ed.). Técnicas y aplicaciones de reescritura, 6th Int. Conf., RTA-95 (posdata) . LNCS. 914 . Saltador. págs. 426–431.
• Ohlebusch, E .; Claves, C .; Marché, C. (2000). "TALP: una herramienta para el análisis de terminación de programas lógicos (descripción del sistema)". En Bachmair, Leo (ed.). Técnicas y aplicaciones de reescritura, 11th Int. Conf., RTA-00 (posdata comprimida) . LNCS. 1833 . Saltador. págs. 270-273.
• Hirokawa, N .; Middeldorp, A. (2003). "Herramienta de terminación de Tsukuba (descripción del sistema)". En Nieuwenhuis, R. (ed.). Técnicas de reescritura y aplicaciones, 14th Int. Conf., RTA-03 (PDF) . LNCS. 2706 . Saltador. págs. 311–320.
• Giesl, J .; Thiemann, R .; Schneider-Kamp, P .; Falke, S. (2004). "Pruebas de terminación automatizadas con AProVE (descripción del sistema)". En van Oostrom, V. (ed.). Técnicas de reescritura y aplicaciones, 15th Int. Conf., RTA-04 (PDF) . LNCS. 3091 . Saltador. págs. 210–220. ISBN 3-540-22153-0.
• Hirokawa, N .; Middeldorp, A. (2005). "Herramienta de terminación tirolesa (descripción del sistema)". En Giesl, J. (ed.). Reescritura de términos y aplicaciones, 16th Int. Conf., RTA-05 . LNCS. 3467 . Saltador. págs. 175-184. ISBN 978-3-540-25596-3.
• Koprowski, A. (2006). "TPA: Terminación probada automáticamente (descripción del sistema)". En Pfenning, F. (ed.). Reescritura de términos y aplicaciones, 17th Int. Conf., RTA-06 . LNCS. 4098 . Saltador. págs. 257–266.
• Marché, C .; Zantema, H. (2007). "El Concurso de Terminación (descripción del sistema)". En Baader, F. (ed.). Reescritura de términos y aplicaciones, 18th Int. Conf., RTA-07 (PDF) . LNCS. 4533 . Saltador. págs. 303–313.

enlaces externos

• Análisis de terminación de programas funcionales de orden superior
• Lista de correo de herramientas de terminación
• Concurso de terminación - ver Marché, Zantema (2007) para una descripción
• Portal de terminación