Свойства перечислимых языков. Теорема Успенского-Райса — различия между версиями
ExileHell (обсуждение | вклад) (→Теорема Успенского-Райса) |
ExileHell (обсуждение | вклад) (→Альтернативное доказательство с использованием теоремы о рекурсии) |
||
| Строка 74: | Строка 74: | ||
Так как <tex>\overline{A}</tex> {{---}} нетривиально (как дополнение к нетривиальному множеству), то по первой части доказательства оно неразрешимо. Следовательно, <tex>A</tex> также неразрешимо. | Так как <tex>\overline{A}</tex> {{---}} нетривиально (как дополнение к нетривиальному множеству), то по первой части доказательства оно неразрешимо. Следовательно, <tex>A</tex> также неразрешимо. | ||
===Альтернативное доказательство с использованием теоремы о рекурсии=== | ===Альтернативное доказательство с использованием теоремы о рекурсии=== | ||
| + | По [[Теорема о рекурсии | теореме о рекурсии]], программа может знать свой исходный код. Значит, в неё можно написать функцию <tex> \mathrm{getSrc()} </tex>, которая вернёт строку {{---}} исходный код программы. | ||
<tex> A </tex> {{---}} разрешимое семейство языков. | <tex> A </tex> {{---}} разрешимое семейство языков. | ||
Версия 00:07, 26 декабря 2016
Содержание
Свойства языков
Рассмотрим множество всех перечислимых языков .
| Определение: |
| Свойством языков (англ. property of languages) называется множество . |
| Определение: |
| Свойство называется тривиальным (англ. trivial), если или . |
| Определение: |
| Язык свойства (англ. language of property) — множество программ, языки которых обладают этим свойством: . |
Отметим, что принадлежность программы языку свойства можно выразить двумя эквивалентными утверждениями:
Далее в конспекте будет употребляться .
| Определение: |
| Свойство называется разрешимым (англ. recursive), если является разрешимым. |
Примеры
Примеры свойств:
- Язык должен содержать слово hello.
- Язык должен содержать хотя бы одно простое число.
Псевдокод для разрешителя , где
// — полуразрешитель некоторого языка return true
Псевдокод для программы в общем случае, то есть для проверки того, что язык удовлетворяет свойству :
return
Псевдокод полуразрешителя для языка свойства из первого примера:
// — перечислимый язык в общем случае, поэтому — полуразрешитель (по теореме Райса-Шапиро) return ('hello')
Теорема Успенского-Райса
| Теорема: |
Язык никакого нетривиального свойства не является разрешимым. |
Доказательство
Пусть — всегда зацикливающийся алгоритм.
Рассмотрим случай, когда .
Приведём доказательство от противного. Предположим, что разрешимо.
Рассмотрим язык , такой что (такой язык существует, так как — нетривиально). Тогда .
Рассмотрим также произвольное перечислимое неразрешимое множество . Пусть — полуразрешитель .
Зафиксируем произвольное и построим следующую функцию
function (x): if (n) == 1 return (x) while true
Получили, что если , то , а если , то . Таким образом, .
Так как — разрешимо, то можно проверить для любого , лежит ли оно в . Но это тоже самое, что и проверка . Тогда можно для каждого проверить, лежит ли оно в , а следовательно и построить разрешитель для . Так как — неразрешимо, получили противоречие.
Теперь рассмотрим случай, когда .
Так как — нетривиально (как дополнение к нетривиальному множеству), то по первой части доказательства оно неразрешимо. Следовательно, также неразрешимо.
Альтернативное доказательство с использованием теоремы о рекурсии
По теореме о рекурсии, программа может знать свой исходный код. Значит, в неё можно написать функцию , которая вернёт строку — исходный код программы. — разрешимое семейство языков.
— множество программ, удовлетворяющих св-ву .
Теперь допустим, что язык разрешим. Тогда напишем такую программу:
propA(code): // программа, разрешающее свойство языка f(x): // такая программа , что ; существует потому что — нетривиальное свойство g(x): // такая программа , что ; существует потому что — нетривиальное свойство p(x): if propA(getSrc()) return g(x) else return f(x)
Если не удовлетворяет свойству , тогда будет выполняться всегда вторая ветка, и . Но язык программы принадлежит . Получили противоречие.
Если удовлетворяет свойству , то , а . Опять получили противоречие.
См. также
Источники информации
- 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.