Perché call-by-value strategia di valutazione non è Turing completa?

Question

sto leggendo un articolo su diversi href="http://en.wikipedia.org/wiki/Evaluation_strategy" (ho linkato articolo wiki, ma io sto leggendo un altro non in lingua inglese). E dice che a differenza di strategie call-by-name e call-by-need, la strategia call-by-value è non Turing completa .

Qualcuno può spiegare, per favore, perché è così? Se è possibile, aggiungere un esempio pls.

Answer 1

Mi contestano in questo articolo che state leggendo. (Io non sono pagati per questo, quindi ho intenzione di fornire un argomento suggestivo, non è una prova.)

E 'noto che, almeno sotto la riduzione normale ordine (aka chiamano per nome), il lambda calcolo puro è Turing-completo. Ma se guardiamo la carta seminale di John Reynolds definizionale Interpreti per ordine superiore Linguaggi di Programmazione , possiamo vedere che Reynolds discute a lungo la differenza tra chiamata per nome e chiamata per valore. Una parte fondamentale del ragionamento è che, al fine di fare una distinzione adeguata, possiamo trasformare un programma in continuazione-passing style . I CPS trasformano è diverso per la chiamata dal bisogno e la chiamata per valore, ma i termini trasformati risultanti possono essere valutati in uno stile.

Quindi, ecco che arriva l'argomento: scrivere un programma di lambda-calcolo che simula una macchina di Turing, allora Cps trasformarla con il CBN trasforma, e si può valutare il codice risultante usando una strategia di riduzione CBV. Scoppio! Turing-completo.

In pratica, scommetto che è possibile scrivere un programma CBV per emulare una macchina di Turing; è probabilmente sufficiente per scegliere un adeguato combinatore a punto fisso, come T per esempio. (Il più famoso combinatore Y funziona solo sotto una strategia di riduzione chiamata per nome, vale a dire, la riduzione normale ordine.)

Avviso: non ho studiato lambda calcolo in età, e sono sicuro che ci sono molti dettagli errate nell'argomento sopra. Ma sono fiducioso nella sostanza. Non sarebbe la prima volta che ho notato qualcosa di sbagliato clamorosamente in risorse online sulla teoria dei linguaggi di programmazione.

Answer 2

La tua domanda non ha molto senso senza riferimento ad un linguaggio specifico, ma farò del mio meglio per rispondere rispetto al calcolo non tipizzati Lambda.

L'esistenza di un valore chiamata per punto fisso combinatore (cioè "Y combinatore") per il lambda calcolo tipizzato sembra rifiutare la richiesta di base (vedi: Fixed Point Combinator ). L'esistenza di tale un combinatore rompe forte normalizzazione, il che suggerisce che ci sia almeno una lingua che è Turing completo che utilizza una strategia di valutazione chiamata per valore.

Molto più probabile che colpiscono il turing-completezza di una lingua è l'esistenza (o mancanza di) un sistema di tipo. Ad esempio, il lambda calcolo semplicemente digitato non può codificare un combinatore punto fisso, ed è fortemente normalizzazione (cioè tutti i termini digitati ben-riducono al valore), tuttavia, questo è vero indipendentemente dalla strategia di valutazione impiegata. Piuttosto, si tratta di una conseguenza del sistema tipo.