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

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

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


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

Теорема: для каждой команды языка 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.

Случай [iftns].
Допустим, что <if b then S1 else S2,s> => s’ и B[b]s = true. Тогда <S1,s> => s’. Поскольку  B[b]s = true, получим <if b then S1 else S2,s> -> <S1,s> ->* s’. Первое отношение следует из правила [iftsos], а второе из индуктивной гипотезы  для <S1,s> => s’.
Случай [iffns]  доказывается аналогично.

Часть 2.

• Нужно доказать, что для каждой команды S, любых состояний s и s’ и натурального числа k справедливо, что из <S,s > ->k s’ следует <S,s > => s’.
• Доказывается индукцией по длине последовательности вывода для <S,s > ->k s’ .
• Для к=0 считаем условие выполненным, так как в нём не используются такие случаи.
• Теперь докажем индуктивные шаги для k0+1 при условии, что условие выполняется для k ? k0 .
Мы будем рассматривать получение первого шага вывода <S,s> ->k0+1 s’
• Случай [iftsos].
Допустим, что <if b then S1 else S2,s> -> <S1,s> ->k0 s’ и B[b]s = true.
Тогда по индукции из <S1,s> ->k0 s’ получим <S1,s> => s’, из чего по правилу [iftns],  следует <if b then S1 else S2,s> => s’ .
Случай  доказан.
• Случай [iffsos] аналогичен.

О теореме в целом

Для каждой команды S языка While и состояния s мы доказали, что если Sns[S] s = s’, то Ssos[S]s = s’; и наоборот, если Ssos[S]s = s’, то Sns[S] s = s’.  Этого достаточно для того, чтобы утверждать о равенстве функций, то есть что Sns[S] = Ssos[S].



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

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