Эквивалентность естественной и структурно-операционной семантик языка While. Доказать, что для каждой команды S и любых состояний s и s’ справедливо, что из <S,s > => s’ следует <S,s > ->* s’ (случаи ass, skip, comp). | MetodPro.ru

Реклама на сайте

Эквивалентность естественной и структурно-операционной семантик языка While. Доказать, что для каждой команды S и любых состояний s и s’ справедливо, что из => s’ следует ->* s’ (случаи ass, skip, comp).


29. Эквивалентность естественной и структурно-операционной семантик языка While. Доказать, что для каждой команды S и любых состояний s и s’ справедливо, что из <S,s > => s’ следует <S,s > ->* s’ (случаи ass, skip, comp).
Теорема: для каждой команды языка While выполняется равенство Sns[S] = Ssos[S].
Доказательство имеет две части:
1) для каждой команды S и любых состояний s и s’ справедливо, что из <S,s > => s’ следует
<S,s> ->* s’;
2) для каждой команды S, любых состояний s и s’ и натурального числа k справедливо, что из <S,s > ->k s’ следует <S,s > => s’.
Первая часть доказывается индукцией по структуре дерева вывода <S,s > => s’.
Вторая часть доказывается индукцией по длине последовательности вывода для <S,s > ->k s’ .
Часть 1
Случай [assns]. Допустим, что < x:=e,s> => s[x/A[e]s]. В СОС результат будет тот же :
 < x:=e,s> -> s[x/A[e]s].
Случай [skipns]  доказывается аналогично.
Случай [compns]. Допустим, что < S1;S2,s> => s”.
Поскольку < S1,s> => s’ и < S2,s’> => s” то применив индуктивные гипотезы получим
 < S1,s> ->* s’ и < S2,s’> ->* s”. Вычисление первой команды композиции не зависит от второй команды, следовательно < S1;S2,s> ->* s”.
Часть 2
Нужно доказать что для каждой команды S, любых состояний s и s’ и натурального числа k справедливо что из <S,s > ->k s’ следует <S,s>=>s’.
Доказывается индукцией по длине последовательности вывода <S,s > ->k s’.
Для k=0 считаем условие выполненным, т.к. в нем не используются такие случаи. Теперь докажем индуктивные шаги для k0+1 при условии что условие выполняется для k <= k0.
Будем рассматривать получение 1-ого шага вывода <S,s > -> k0+1  s’
Случай [asssos] очевиден, k0=1
Случай [skipsos] очевиден, k0=1
В случаях [comp1sos] и [comp2sos] имеем < S1;S2,s> ->k0+1 s” . В соответствии с леммой:
<S1,s> ->k1 s’ и <S2,s’> ->k2 s” , причём k1+k2=k0+1. Поскольку k1 <= k0 и k2 <= k0 по индукции имеем <S1,s> => s’ и <S2,s’> => s” , и тогда по правилу [compns] получим <S1;S2,s> => s”.  Случай  доказан.
О теореме в целом:
Для каждой команды S языка While и состояния s мы доказали, что если Sns[S] s = s’, то Ssos[S]s = s’; и наоборот, если Ssos[S]s = s’, то Sns[S] s = s’.  Этого достаточно для того, чтобы утверждать о равенстве функций, то есть что Sns[S] = Ssos[S].



Методические пособия

  • Системы автоматизированного проектирования
  • Социология молодёжи
  • Общая социология
  • Криптография
  • Проектирование трансляторов
  • Компьютерная графика
  • Моделирование систем
  • Информационная безопасность
  • Теория вычислительных процессов
  • Логические основы искусственного интелекта
  • Проектирование распределённых информационных систем