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'