Macchina che termina sempre

Nella teoria della computabilità una macchina che termina sempre, chiamata anche un decider^[1] o macchina di Turing totale,^[2] è un particolare di tipo di macchina di Turing per cui, al contrario del modello generale, vi è garanzia che termini per ogni input.

Poiché si ferma sempre, la macchina è in grado di decidere se una data stringa è membro di un linguaggio formale. La classe dei linguaggi che possono essere decisi da macchine di questo tipo è esattamente l'insieme dei linguaggi ricorsivi. Dato il problema della fermata, determinare se un'arbitraria macchina di Turing termini sempre è indecidibile,non c'è nessun algoritmo per determinarlo.

In pratica è possibile costruire una macchina che termini sempre, e già computa molte funzioni interessanti, come da esempio, quando si limita le capacità di controllo di flusso così che nessun programma farà entrare la macchina in un ciclo infinito. Per esempio, un albero di decisione finito non contiene cicli e quindi termina naturalmente. Non si richiede che la macchina non abbia capacità di svolgere cicli. Se si limitano i cicli ad un ben definito limite prevedibile (come il ciclo FOR in BASIC), si possono esprimere tutte le funzioni ricorsive primitive^[3]. Un esempio di questa macchina è fornito dal linguaggio di programmazione giocattolo PL-{GOTO} di Brainerd e Landweber^[4].

Inoltre si può definire un programma in cui è possibile assicurare che funzioni persino più sofisticate terminino sempre. Ad esempio la funzione di Ackermann, che non è ricorsiva primitiva, termina sempre e si può garantire questa proprietà considerandola un sistema di riscrittura con un buon ordine dei suoi argomenti^[5]. È una cosa simile ad usare l'induzione matematica per provare che una funzione ricorsiva raggiunge sempre il suo caso base.