Доказать лемму, что если <S1;S2,s> ->k s” , то существует состояние s’ и натуральные числа k1 и k2 такие, что <S1,s> ->k1 s’ и <S2,s’> ->k2 s”, а k = k1 + k2 | MetodPro.ru

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

Доказать лемму, что если ->k s” , то существует состояние s’ и натуральные числа k1 и k2 такие, что ->k1 s’ и ->k2 s”, а k = k1 + k2


27. Доказать лемму что
Если <S1;S2,s> ->k s” , то существует состояние s’ и натуральные числа k1 и k2 такие, что
 <S1,s>->k1 s’ и <S2,s’> ->k2 s”, а k =  k1 + k2 .
Доказательство
Применим доказательство по индукции по длине последовательности вывода k.
Если k=0, то свойство выполняется тривиально.
Индуктивный шаг: предполагаем, что лемма истинна для всех k <= k0 и докажем, что она истинна и для k0 + 1.
Рассмотрим вывод: <S1;S2,s> ->k0+1 s”. Из него следует существование последовательности <S1;S2,s> -> y ->k0 s”, для некоторой конфигурации y.
Конфигурацию y можно получить двумя способами: по правилу [comp1sos] и по правилу [comp2sos] .
В первом случае имеем
 <S1;S2,s> -> <S’1;S2,s’> ->k0 s” ,
причём <S1,s> -> <S’1,s’>  (1).
К последовательности длины k0 применима индуктивная гипотеза, значит существует состояние s0 и натуральные числа k1 и k2 такие,
что <S’1,s’> ->k1 s0    (2)
и  <S2,s0> ->k2 s”                   (3)
и  k0 = k1 + k2 .
Используя (1)  и (2) получим <S1,s> ->k1+1 s0 , Добавив к этому (3)  и (k1+1) + k2 = k0 + 1 получим доказательство первого случая.
Во втором случае имеем
 <S1;S2,s> -> <S2,s’> ->k0 s” , причём <S1,s> -> s’.
Это удовлетворяет лемме с k1 = 1 и k2 = k0.
Можно доказать и то, что если <S1,s> ->k s’, то <S1;S2,s> ->k <S2,s’>. То есть то, что вычисление первой команды композиции не зависит от второй команды.



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

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