Aniello Murano » 16.Esercitazione in aula sui tipi e sul non-determinismo

IMPnd

Precisazioni su IMPnd

Si precisa che la scelta su un comando nondeterministico di IMPnd è univoca nello stesso istante sullo stesso insieme di comandi.
Dunque, se in un certo istante utilizzo il comando “c₀ or c₁“, posso utilizzare alternativamente il comando “c₀ or c₁“. Infatti, in entrambi i casi, qualsiasi sarà la scelta tra c₀ e c₁, essa sarà la stessa su entrambi i comandi, se utilizzati alternativamente nello stesso istante. In effetti, scegliere un elemento dell’insieme {c₀,c₁} è equivalente a sceglierlo nell’insieme {c₁,c₀} = {c₀,c₁}.
Un’altra precisazione: l’operatore “or” usa lo stesso principio non deterministico dell”operatore alternativo “Y” utilizzato per formare i comandi con guardia in IMPGC. A tal proposito e rispondendo alla domanda di alcuni, si precisa che in presenza di un comando “if b₁ ! c₁ Y b₂ ! c₂ “, se entrambi le guardie b₁ e b₂ sono valutate true, non deterministicamente solo uno dei comandi c₁ o c₂ viene eseguito. Si vedano le regole di derivazione corrispondenti!