Detener la teoría del problema vs.práctica

Question

A menudo se afirma que el problema de la detención es indecidible.Y demostrarlo es ciertamente trivial.

Pero eso sólo se aplica a un programa arbitrario.

¿Ha habido algún estudio sobre las clases de programas que los humanos suelen hacer?

A veces puede resultar fácil analizar un programa, enumerar todos sus grados de libertad y concluir que se detendrá.

Por ejemplo, ¿ha habido alguna vez un esfuerzo para crear un lenguaje de programación (en realidad, scripting) que garantice la detención?No sería ampliamente aplicable, pero aún podría ser útil para módulos de misión crítica.

Answer 1

Los idiomas que están garantizados para detener han visto un uso amplio de propagación. Los idiomas como COQ / AGDA / IDRIS están todos en esta categoría. De hecho, muchos muchos sistemas de tipo se garantizan para detenerse como el sistema F o cualquiera de sus variantes, por ejemplo. Es común que la solidez de un sistema de tipo se reduce para demostrar que todos los programas se normalizan en ella. La normalización fuerte es una propiedad muy deseable en general en la investigación de idiomas de programación.

No he visto mucho éxito en la captura de bucles infinitos en la práctica, sin embargo, "garantizar la terminación en el ESFP" por Telford y Turner, muestra un verificador de terminación más robusto que pudo demostrar que el algoritmo de Euclid siempre terminó y maneja los casos parciales. El algoritmo de Euclid es un ejemplo difícil de un ejemplo de una función recursiva primitiva que no es impreciso para ser primitivos. Falla falla que simplemente busque un parámetro decreciente (o algún patrón simple de los parámetros decrecientes como el verificador de terminación FETUS). Para implementar esto utilizando combinadores recursivos primitivos, debe codificar una prueba de terminación para el algoritmo como un parámetro en la función esencialmente.

No puedo pensar en ningún resultado para los idiomas procesales de la parte superior de mi cabeza y la mayoría de los resultados en idiomas funcionales, utilice algún tipo de restricción que hace que el obviamente termine en lugar de tratar de realizar algún tipo de análisis complejo para garantizar que más Los programas naturales terminan.

Answer 2

Hay investigaciones pasadas y actuales sobre esto.Tal problema se llama Análisis de terminación, y un vistazo rápido a Google (Scholar) proporciona varias publicaciones antiguas y nuevas sobre esto:

1. 2005, Análisis de terminación de programas funcionales de orden superior;
2. 2006, Análisis de terminación automatizado para Haskell;
3. 2008, Análisis de Terminación de Programas Lógicos Basados ​​en Gráficos de Dependencia;
4. 2010, Resumen de bucles y análisis de terminación.;
5. 2014, Análisis de terminación mediante programas de terminación de aprendizaje;
6. 2015, Análisis de terminación con gráficos de llamadas recursivas.;
7. 2019, Análisis de terminación estática para algoritmos distribuidos controlados por eventos;
8. 2019, Implementación de análisis de terminación en programación cuántica.;

Incluyendo lenguajes existentes con mecanismos incorporados para eso, como:

• Mercurio;
• Idris, Coq, Agda;

Answer 3

Microsoft has developed a practical code checker (whose name escapes me at the moment) which performs halt-testing. It exploits the fact that the code it checks is human-written and not arbitrary, just as you suggest. More importantly, it bypasses the impossibility proof by being allowed to return the answer 'Cannot decide' if it runs into code too difficult to check.

Answer 4

There are only 2 types of infinite programs:

1. Those that repeat their own state after a point (cyclical)
2. Those that grow indefinitely in used memory

Those in 1st type, follow this pattern:

Where there is a pair of distinct indices i and j such that xi = xj, and after which the cycle repeats itself again (thanks to the deterministic nature of programs). In this case the inputs x, contain the whole memory and variables used by the algorithm, plus the current instruction pointer.

Cycle detection algorithms work very well in practice for this type and can prove that a given cyclical program will never finish, usually after a small number of steps, for most random programs.

Proving those in the 2nd type is where the challenge is. One could argue that type 2 can never exist in reality (as all computers have finite memory) but that is not very useful in practice because the memory used may grow very slowly for a regular computer to ever be full. A simple example of that is a binary counter that never stops and never repeats its full state completely.

Answer 5

There is a huge class of functions that are trivially guaranteed to halt: Everything with a finite number of loops, with an upper limit for the number of iterations for each loop determined before the loop is started.

If you have a random program, it can be difficult to prove whether or not it halts. Programs that are written for a purpose are usually much easier.

Answer 6

The smart contracts functions in the Ethereum blockchain are an example of a system that needs the guarantee of halting, not to stall the whole chain.

Every function has a gas cost, and the gas cost translates into real Ethereum coins. A transaction fee must be paid to call the contract. If the gas used in the contract exceed the gas paid with the transaction fee, the computation terminates immediately.