Семантическая функция SNS.
23) Семантическая функция Sns
Смысл операторов языка While можно обобщить в виде функции из множества State на то же множество State.
Определим Sns :: Stm -> (State (-> State),
Это значит, что для каждой команды S имеем частичную функцию Sns [S] Э (State (-> State), которая определяется как:
? s’ если <S,s> => s’
Sns[S]s = ?
?_l_, иначе
Например, Sns [while true do skip] s = _l_.