Halting Teoria do problema vs. prática

Question

Muitas vezes é afirmado que o problema da parada é indecável.E provando que é de fato trivial.

Mas isso só se aplica a um programa arbitrário.

Houve algum estudo sobre as classes de programas que os seres humanos geralmente fazem?

às vezes pode ser fácil analisar um programa e enumerar todos os seus graus de liberdade e concluir que ele vai parar.

Por exemplo, já houve um esforço para criar uma linguagem de programação (scripting realmente) que garante a parada?Não seria amplamente aplicável, mas ainda poderia ser útil para módulos críticos de missão.

Answer 1

idiomas que são garantidos para impedir que vejam amplo uso de propagação. Idiomas como COQ / AGDA / IDRIS estão todos nesta categoria. Muitos sistemas de tipos são de fato garantidos para parar como o sistema f ou qualquer uma de suas variantes, por exemplo. É comum que a solidez de um sistema de tipo se resume a provar que todos os programas se normalizam nele. A normalização forte é uma propriedade muito desejável em geral na pesquisa de idiomas de programação.

Eu não tenho visto muito sucesso em capturar loops infinitos na prática, no entanto, "assegurar a rescisão no ESFP" por Telford e Turner mostra um verificador de terminação mais robusto que foi capaz de provar que o algoritmo de Euclid sempre terminou e lida com casos parciais. O algoritmo de Euclid é um exemplo faturado de uma função recursiva primitiva que não é diretamente provável ser primitiva recursiva. Ele falha os verificadores que simplesmente procuram um parâmetro decrescente (ou algum padrão simples de diminuir parâmetros como o verificador de terminação do feto). Para implementar isso usando combinadores recursivos primitivos, você deve codificar uma prova de rescisão para o algoritmo como parâmetro na função essencialmente.

Não consigo pensar em quaisquer resultados para os idiomas processuais fora do topo da minha cabeça e a maioria dos resultados em idiomas funcionais use algum tipo de restrição que faz o finalmente terminar em vez de tentar realizar algum tipo de análise complexa para garantir que mais programas naturais terminam.

Answer 2

Há pesquisas passadas e atuais sobre isso. Tal problema é chamado Análise de terminação e uma rápida aparência no Google (acadêmico) fornece vários antigos como bem como novas publicações sobre isso:

.
1. 2005, Análise de terminação de programas funcionais de ordem superior ;
2. 2006, Análise de terminação automatizada para Haskell < / a>;
3. 2008, Análise de terminação de programas lógicos baseados na dependência Gráficos ;
4. 2010, Análise de Loop e Análise de Terminação
5. 2014, Análise de rescisão por meio de programas de terminação de aprendizagem ;
6. 2015, análise de terminação com gráficos de chamada recursivos ;
7. 2019, Análise de terminação estática para algoritmos distribuídos acionados por eventos < / a>;
8. 2019, Implementação de análise de terminação na programação quântica ;

Incluindo idiomas existentes com mecanismos embutidos para que, como:

• mercúrio ;
• 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.