es3 (By Guastella and Tumbarello)

Una strategia di riduzione, vista come relazione di riduzione su insiemi di coppie del tipo (M,N), è deterministica quando, dato un termine M, esiste, nell' insieme di tutte le possibili coppie , una ed una sola coppia che ha M come primo termine. Per verificare il determinismo della strategia in esame, dovremmo quindi analizzare tutte le possibili coppie; ma ciò sarebbe possibile solo se l' insieme delle possibili coppie è finito e ragionevolmente piccolo, cosa non sempre vera. D' altro canto è possibile generare l'insieme (anche infinito) di tutte le possibili coppie tramite assiomi e regole di inferenza che ci dicono quale regola applicare se un termine è di un paritcolare tipo. In questo caso il determinismo può essere dimostrato dimostrando che ogni regola si applica esattamente ad un tipo di termine e quindi per ogni M esiste al più un termine N tale che M->N ed N ha la struttura di una regola predefinita oppure nessuna regola è più applicabile e quindi N è in forma normale.
Supponiamo di usare la seguente grammatica:
M::= x | MN | \x:s.M

Determinismo della strategia Leftmost-Outermost

N.B. scriveremo -> intendendo ->left
Assiomi:
(1) (\x : s.M)N -> M[N/x]

Regole di inferenza:
(2) M -> M' se M non è nella forma \x:s.P
MN -> M'N

(3) N -> N' se M è in forma normale
MN -> MN'

(4) M -> M'
\x:s.M -> \x:s.M'

Potremmo aggiungere altre regole in base alla grammatica ovvero in base all' insieme dei possibili termini; in PCF, ad esempio, per ogni costante dovrei aggiungere un nuovo assioma: ad esempio:
...
succ n -> n+1 zero? 0 -> tt

Dato un termine P esso è in forma normale se la sua struttura non figura a sinistra di nessuna delle regole di inferenza o degli assiomi e ciò porta l' interprete a fermarsi.
L' interprete, dato un termine P, analizza la struttura del termine ovvero dei suoi possibili sottotermini e si trova dunque in uno dei seguenti possibili casi:

P è una variabile x che è dunque in forma normale
P è una lambda astrazione cioè è nella forma \x :s.M e quindi l'interprete dovrà applicare l' assioma (4) riducendo M
P una applicazione del tipo MN ed allora esaminerà M trovando:

M è nella forma \x:s.T e quindi l'interprete dovrà applicare univocamente l' assioma (1)
M non è nella forma \x:s.T e non è in forma normale cioè la sua struttura è contemplata in una delle regole o degli assiomi e quindi applicherò (2) cioè l' algoritmo riparte dal primo passo per M
M ha una struttura non contemplata cioè è in forma normale e allora applicherò la (3) ovvero applicherò l' algoritmo dall' inizio per N

In definitiva il determismo si ha perchè in ogni istante di computazione l' interprete è in grado di scegliere quale regola applicare in maniera univoca.
Questi ragionamenti valgono con le oppotune modifiche anche per una grammatica diversa o più estesa tipo quella del PCF a meno di dare le regole per tutti i possibili termini in maniera non ambigua.

Determinismo della strategia Lazy

N.B. scriveremo -> intendendo ->lazy
Assiomi:
(1) (\x : s.M)N -> M[N/x]

Regole di inferenza:
(2) M -> M' se M non è nella forma \x : s.P
MN -> M'N

Anche qui potremmo aggiungere, ad esempio, il termine M+N come nel PCF alla grammatica e quindi gli assiomi :
M -> M' N -> N' con n numerale ...
M + N -> M' + N n +N -> n + N'

Anche qui il determinismo è facilmente dimostrabile con gli stessi ragionamenti di prima col vantaggio di avere meno regole da applicare per il fatto che la lazy è una restrizione della leftmost outermost.