Доказать теорему о том, что каждого выражения e?Exp3 если r =FVar(e) r’, то из ?? e => n следует, что ?’? e => n. | MetodPro.ru

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

Доказать теорему о том, что каждого выражения e?Exp3 если r =FVar(e) r’, то из ?? e => n следует, что ?’? e => n.


8) Доказать теорему о том, что для каждого выражения e э Exp3 если r =FVar(e) r’,  то из р|- e => n следует, р|- e => n следует  р’|- e => n.
• Для каждого выражения  e э Exp3
если r =FVar(e) r’,  то из р|- e => n следует,  что р’|- e => n
• В доказательстве применим метод структурной индукции. Свойство P(e) формулируется так:  Для любых двух окружений р и р’, если r =FVar(e) r’, то из  р|- e => n следует  р’|- e => n.
Нужно рассмотреть четыре варианта
• P(n) для каждого числа n.
• P(x) для каждой переменной x.
• P(e’ op e”) для каждого оператора op, считая, что P(e’) и P(e”) – истинны.
• P(let x = e’ in e”), полагая истинность P(e’) и P(e”) .
Доказательство по 4у варианту:
1. Допустим, что р|- let x = e’ in e” => n.
2.  Это значение могло быть получено только применением правила LocR. По этому должно существовать значение v’, такое, что р|-e’=> v’ и р[x/v’]|- e” => n.
3. Из определения множества FVar следует, что FVar(e’) C_ FVar (e), т.е. r =FVar(e’) r’.
4. По индукции предполагаем, что р’|-e’=> v’    (1)
(то есть и в окружении р’ вычисление e’ приведёт к тому же результату v’).
5. Можно утверждать, что r[x/v’] ={x} r’[x/v’] (поскольку и в r[x/v’] и в r’[x/v’] с x связывается одно и то же значение).
6. Из посылки r =FVar(e) r’, и предыдущего утверждения можно заключить, что r[x/v’] =FVar(e) U{x} r’[x/v’].
7. А, поскольку, FVar(e”) C_ FVar(e) U {x} получим
 r[x/v’] =FVar(e”) r’[x/v’]
8. Из r[x/v’]|-e”=> n следует, что r’[x/v’]|-e”=> n (2). ( Это индуктивное предположение, т.к. e”  это составляющая e )
9. Применив правило LocR к (1) и (2) получим
 р’|- let x = e’ in e” => n



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

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