Доказать лемму, что для всех арифметических выражений e истинно: | MetodPro.ru

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

Доказать лемму, что для всех арифметических выражений e истинно:


40) Доказать лемму, что для всех арифметических выражений e истинно:
<CA [[e]], e, s> #>* < e, A[[e]]s, s>.   

Лемма
• Для всех арифметических выражений e истинно:
<CA [[e]], e, s> #>* < e , A [[e]]s, s>   .
• И ещё: все промежуточные конфигурации последовательности вычислений имеют непустой стек.
Докажем эту лемму структурной индукцией по выражению e.
Доказательство
• Случай n. Тогда CA [[n]] = PUSH-n. Из семантики АМ имеем: <PUSH-n:c, e, s> #> <c,?[n]:e, s>. Поскольку A [n] => ?[n], случай доказан.
• Случай x. Тогда CA [[x]] = LOAD-x. Из семантики АМ имеем: < LOAD-x:c, e, s> #> <c,(s[x]):e, s>. Поскольку A [x]s => s[x], случай доказан.
• Отметим, что все промежуточные конфигурации последовательности вычислений имеют непустой стек.
• Случаи для арифметических операций доказываются все одинаково. Рассмотрим один из них.
• Случай e1+e2.
Тогда CA [[e1+e2]] = CA [[e2]] ++ CA [[e1]] ++ ADD.
По индукции считаем, что
<CA [[e1]], e, s> #>* < e , A [e1] s, s> и
<CA [[e2]], e, s> #>* < e , A [e2] s, s>  .
• Используя лемму: если за k шагов из конфигурации
<c1, e1, s> получили состояние s’, то добавив что либо к коду или к стеку за те же k шагов получим то же состояние s’, а добавленные части останутся нетронутыми, получим:
< CA [[e2]] ++ CA [[e1]] ++ ADD, e, s> #>* < CA [[e1]] ++ ADD , A [e2] s, s> .
Используя вторую индуктивную гипотезу и туже лемму, получим:
<CA [[e1]] ++ ADD, A [[e2]] s, s> #>*  <ADD , (A [e1] s) : (A [e2] s), s>.
 Из семантики АМ имеем:
 <ADD:c, (A [e1] s) : (A [e2] s): e, s> #> <c, A [e1]s + A [e2]s :e, s>.
 Поскольку A [e1+e2]s => A [e1]s + A [e2]s,
 случай доказан.
• Отметим, что все промежуточные конфигурации последовательности вычислений имеют непустой стек.



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

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