Análisis de terminación - Termination analysis

void f(int n) {
   while (n > 1)
      if (n % 2 == 0)
          n = n / 2;
      else
          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.

Ahora bien, como la pregunta de si una función computable es total no es semidecidible , 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 en la determinación de la terminación para un número infinito de programas que terminan, ya sea corriendo para siempre o deteniéndose 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 o no terminar 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 siguiente ejemplo de pseudocódigo : 

i := 0
loop until i = SIZE_OF_DATA
    process_data(data[i])) // process the data chunk at position i
    i := i + 1 // move to the next chunk of data to be processed

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 haciendo que el contador cambie a un valor negativo y permita que se cumpla la condición de ciclo. 

i := 1
loop until i = 0
    i := i + 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
loop until i = UNKNOWN
    i := i + 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.

Las funciones recursivas y los bucles son equivalentes en expresión; cualquier expresión que involucre bucles se puede escribir usando 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á. 

function factorial (argument as natural number)
    if argument = 0 or argument = 1
        return 1
    otherwise
        return argument * factorial(argument - 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. Es por eso que Agda y Coq tienen verificadores 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 de tamaño 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 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 (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.

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

Ver también

Referencias

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

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

enlaces externos