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:
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.
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.