2.10.16. ВЫБОРЫ

Вычисление источника S : \{Snt1; ... Sntn;} всегда дает тот же результат, что и вычисление тропы S : Ve, \{Ve : Snt1; ... Ve : Sntn;}, при условии, что Ve - некоторая e-переменная, которая больше нигде не используется в программе.

Источник S : {Snt1; ... Sntn;} эквивалентен источнику

S : \{Snt1; ... Sntn; e $error(Fname "Unexpected fail");}, где

Fname - имя функции, в которой находится данная конструкция.

 

S : {Snt1; ... Sntn;} =>=>

S : \{Snt1; ... Sntn;

e $error(Fname "Unexpected fail");}

Fname - имя функции, в которой находится конструкция.

 

Env,0,St |- S => Oe,St'

Env,m,St'|- \{Oe : Snt1; ... Oe : Sntn;} => X,St"

-------------------------------------------------

Env,m,St |- S : \{Snt1; ... Sntn;} => X,St"

 

Env,0,St |- S => $fail(k),St'

--------------------------------------------------

Env,m,St |- S : \{Snt1; ... Sntn;} => $fail(0),St'

 

Env,0,St |- S => $error(Oe),St'

----------------------------------------------------

Env,m,St |- S : \{Snt1; ... Sntn;} => $error(Oe),St'