LCME Четверг, 28.03.2024, 14:42
Главная | Регистрация | Вход Приветствую Вас Гость | RSS
[ Новые сообщения · Участники · Правила форума · Поиск · RSS ]
  • Страница 1 из 1
  • 1
Форум » Билеты к экзаменам » Программирование » 05 Ромбовидное свойство
05 Ромбовидное свойство
freidomДата: Понедельник, 28.12.2009, 18:04 | Сообщение # 1
Главный тут
Группа: Администраторы
Сообщений: 273
Репутация: 20
Статус: Offline
Ромбовидное свойство отношений. Редукционный граф бета-редукции. Отсутствие у бета-редукции ромбовидного свойства. Отношение бета-редуцируемости.

Назовём отношение R обладающим ромбовидным свойством, если из того, что aRb и aRc следует, что найдётся элемент d, такой, что bRd и cRd.

Так как бета-редукция является бинарным отношением, можно изобразить её граф или часть его. Если изображаются только термы, которые можно получить из некоторого терма A путём n шагов бета-редукции всевозможных его частей (n >= 0), то такой граф называется редукционным графом терма A.

Заметим, что отношение бета-редукции НЕ обладает ромбовидным свойством. Действительно, рассмотрим терм w (I d). Очевидно, редуцируя внутренний редекс, за 2 шага приходим к нормальной форме, в то время как редуцируя внешний, до нормальной формы добираемся за 3 шага. Таким образом, этот терм является контрпримером к утверждению о существовании ромбовидного свойства у бета-редукции.

Отношением бета-редуцируемости называется рефлексивное и транзитивное замыкание отношения бета-редукции. Теорема Чёрча-Россера утверждает о наличии ромбовидного свойства у отношения бета-редуцируемости.

 
Форум » Билеты к экзаменам » Программирование » 05 Ромбовидное свойство
  • Страница 1 из 1
  • 1
Поиск:

Copyright Freidom © 2024 Хостинг от uCoz