Свойства перечислимых языков. Теорема Успенского-Райса — различия между версиями
AMaltsev (обсуждение | вклад) м |
AMaltsev (обсуждение | вклад) |
||
Строка 38: | Строка 38: | ||
Приведём доказательство от противного. | Приведём доказательство от противного. | ||
− | Предположим, что <tex>A</tex> разрешимо | + | Предположим, что <tex>A</tex> разрешимо. |
− | + | Пусть <tex>p_\infty</tex> {{---}} всегда зацикливающийся алгоритм. Для упрощения предположим, что <tex>p_\infty \in A</tex>. В противном случае доказательство аналогично. | |
− | + | Рассмотрим <tex>p_a</tex> {{---}} программу, такую что <tex>a \in \overline A</tex> (такое <tex>a</tex> существует, т.к. А - нетривиально). Рассмотрим также произвольное перечислимое неразрешимое множество <tex>X</tex>. Пусть <tex>p_X(n)</tex> - полуразрешитель <tex>X</tex>. | |
− | + | Зафиксируем произвольное <tex>n \in \mathbb{N}</tex> и построим следующую функцию | |
+ | <tex>Vn(x) = \begin{cases} | ||
+ | a(x), n \in X; \\ | ||
+ | p_\infty(x), n \notin X; \\ | ||
+ | \end{cases} </tex> | ||
− | + | <code> | |
− | + | '''function''' <tex>V_n</tex>(x): | |
− | + | '''if''' <tex>p_X</tex>(n) | |
− | '''return''' <tex> | + | '''return''' <tex>p_a</tex>(x) |
− | + | '''while''' ''true'' | |
− | + | </code> | |
− | + | Получили, что если <tex>n \in X</tex>, то <tex>Vn(x) \in L(\overline S)</tex>, а если <tex>n \notin X</tex>, то <tex>Vn(x) \in L(S)</tex>. Таким образом, <tex>n \in X \iff V_n(x) \in L(\overline S)</tex>. | |
− | + | ||
− | + | Так как <tex>\overline S</tex> - разрешимо, то можно проверить для любого <tex>a</tex>, лежит ли оно в <tex>\overline{S}</tex>. Но это тоже самое, что и проверка <tex>n \in X</tex>. Тогда можно для каждого <tex>n</tex> проверить лежит ли оно в <tex>X</tex>, а следовательно и построить разрешитель для <tex>X</tex>. Так как <tex>X</tex> - неразрешимо, получили противоречие. | |
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
}} | }} | ||
Версия 20:54, 20 ноября 2016
Содержание
Свойства языков
Рассмотрим множество всех перечислимых языков .
Определение: |
Свойством языков (англ. property of languages) называется множество | .
Определение: |
Свойство называется тривиальным (англ. trivial), если | или .
Определение: |
Язык свойства (англ. language of property) | — множество программ, языки которых обладают этим свойством: .
Определение: |
Свойство разрешимым. | называется разрешимым (англ. recursive), если является
Примеры
Примеры свойств:
- Язык должен содержать слово hello.
- Язык должен содержать хотя бы одно простое число.
Псевдокод для разрешителя
, где// — полуразрешитель некоторого языка return true
Псевдокод для программы в общем случае, то есть для проверки того, что язык удовлетворяет свойству :
return
Псевдокод полуразрешителя для языка свойства из первого примера:
теореме Райса-Шапиро) return ('hello')// — перечислимый язык в общем случае, поэтому — полуразрешитель (по
Теорема Успенского-Райса
Теорема: |
Язык никакого нетривиального свойства не является разрешимым. |
Доказательство: |
Приведём доказательство от противного. Предположим, что разрешимо.Пусть — всегда зацикливающийся алгоритм. Для упрощения предположим, что . В противном случае доказательство аналогично.Рассмотрим — программу, такую что (такое существует, т.к. А - нетривиально). Рассмотрим также произвольное перечислимое неразрешимое множество . Пусть - полуразрешитель .Зафиксируем произвольное и построим следующую функцию
function(x): if (n) return (x) while true
Получили, что если Так как , то , а если , то . Таким образом, . - разрешимо, то можно проверить для любого , лежит ли оно в . Но это тоже самое, что и проверка . Тогда можно для каждого проверить лежит ли оно в , а следовательно и построить разрешитель для . Так как - неразрешимо, получили противоречие. |
См. также
Источники информации
- Wikipedia — Rice's theorem
- Rice, H. G. "Classes of Recursively Enumerable Sets and Their Decision Problems." Trans. Amer. Math. Soc. 74, 358-366, 1953.
- Хопкрофт Д., Мотванн Р., Ульманн Д. Введение в теорию автоматов, языков и вычислений страница 397.