La teoria dei problemi di fermezza vs. Pratica

Question

Si afferma spesso che il problema di fermezza sia indecidabile.E dimostrando che è davvero banale.

Ma questo si applica solo a un programma arbitrario.

C'è stato uno studio relativo alle classi di programmi che gli umani di solito fanno?

A volte può essere facile analizzare un programma e enumerare tutti i suoi gradi di libertà e concludere che si fermerà.

Ad esempio, c'è mai stato uno sforzo per creare un linguaggio di programmazione (scripting) che garantisce l'arresto?Non sarebbe ampiamente applicabile ma potrebbe ancora essere utile per i moduli critici mission.

Answer 1

Lingue che sono garantite per fermarsi hanno visto un ampio uso di diffusione. Lingue come COQ / AGDA / IDRIS sono tutti in questa categoria. Molti molti sistemi di tipo sono infatti assicurati di fermarsi come il sistema F o una delle sue varianti per esempio. È comune che la solidità di un sistema di tipo deviarsi per dimostrare che tutti i programmi normalizzano in esso. La forte normalizzazione è una proprietà molto desiderabile in generale nella ricerca di lingue di programmazione.

Non ho visto un sacco di successo nel catturare anelli infiniti nella pratica, tuttavia "Garantire la risoluzione in ESFP" di Telford e Turner mostra un correttore di terminazione più robusto che è stato in grado di dimostrare che l'algoritmo di Euclid ha sempre terminato e gestisce casi parziali. L'algoritmo di Euclid è un esempio notoriamente ingannevole di una funzione primitiva ricorsiva che non è semplice dimostrabile essere ricorsive primitive. Non riesce a eseguire i controllore che cerca semplicemente un parametro decrescente (o un modello semplice di parametri decrescenti come il checker di terminazione del feto). Per implementare questo utilizzando i primitivi combinatori ricorsivi è necessario codificare una prova di risoluzione per l'algoritmo come parametro nella funzione essenzialmente.

Non riesco a pensare a nessun risultato per le lingue procedurali dalla parte superiore della mia testa e la maggior parte dei risultati nelle lingue funzionali utilizza una specie di restrizione che rende ovviamente la terminare piuttosto che cercare di eseguire una specie di analisi complessa per assicurarsi che altro Programmi naturali terminano.

Answer 2

C'è una ricerca passata e attuale su questo. Tale problema è definito Analisi di terminazione e un rapido sguardo su Google (Scholar) offre diversi vecchi come bene come nuove pubblicazioni su questo:

.
1. 2005, Analisi della terminazione dei programmi funzionali dell'ordine superiore ;
2. 2006, Analisi di terminazione automatizzata per Haskell < / a>;
3. 2008, Analisi della terminazione dei programmi logici basati sulla dipendenza Grafici ;
4. 2010, loop Summarization and Termination Analysis ;
5. 2014, analisi di terminazione imparando programmi terminazione ;
6. 2015, Analisi di terminazione con grafici di chiamata ricorsivo ;
7. 2019, Analisi di terminazione statica per algoritmi distribuiti a guida degli eventi < / a>;
8. 2019, Implementazione Analisi della terminazione sulla programmazione quantistica ;

comprese le lingue esistenti con meccanismi integrati per quanto:

.
• Mercury ; 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.