ВУЗ:
Составители:
(на любом языке программирования), запущенная после введения в неё некоторого
конкретного набора данных. Смысл этого утверждения для теоретического
программирования очевиден: не существует совершенно общего метода проверки
программ на наличие в них бесконечных циклов.
Приведем два варианта доказательства. Первый вариант является эскизом
доказательства [20, стр. 123-125], и он следует первоначальному доказательству А.
Тьюринга
.
Второй вариант – строгое доказательство, сделанное в рамках ламбда–исчисления.
Доказательство 1. Не теряя общности, мы можем рассматривать только
программы, вычисляющие одноместные функции от натуральных чисел. Поскольку
вычислимых одноместных функций – счетное число, то пусть последовательность c
1
, c
2
,
c
3
,… – содержит все такие функции. Доказательство проведем от противного.
Пусть имеется такая программа (двуместная функция) A(q,n), что
1. Если завершается A(q,n), то не завершается C
q
(n).
(Т.е. мы считаем, что алгоритм A проверяет, остановится или нет вычисление функции.)
Тогда, в частности, для q=n
2. Если завершается A(n,n), то не завершается C
n
(n).
Функция A(n,n) зависит от одного параметра, следовательно, существует такое k, что
3. A(n,n) = C
k
(n).
Тогда
4. A(k,k) = C
k
(k) (следует из (3) при n=k).
Имеем из (2) при n=k
5. Если завершается A(k,k), то не завершается C
k
(k).
Подставляя (4) в (5), получаем
6. Если завершается C
k
(k), то не завершается C
k
(k).
Однозначное следствие:
C
k
(k) не завершается, а A(k,k) не может это установить (поскольку A(k,k) = C
k
(k) и,
следовательно, не останавливается).
Доказательство 2. Поскольку вычислимые функции – это в точности те, которые
ламбда–представимы (теорема Клини), то проблему остановки можно сформулировать в
терминах ламбда–исчисления: «Существует ли алгоритм, с помощью которого можно
установить, имеет ли нормальную форму данный ламбда–терм?».
Доказывать будем от противного. Предположим, что искомый алгоритм
существует: если терм t имеет нормальную форму, то алгоритм выдает 0, а если нет, то
алгоритм выдает 1. В силу тезиса Черча такой алгоритм представляется в виде ламбда–
определимой функции, следовательно, существует комбинатор H такой, что
⎩
⎨
⎧
><
><
=
.,1
,,0
ñëó÷àåïðîòèâíîìâ
ôîðìóíîðìàëüíóþèìååòtòåðìåñëè
Ht
Комбинаторы <0> и <1> – произвольные нумералы
, кодирующие соответственно 0
и 1. Обозначим через zero? , как обычно, комбинатор – тест на ноль:
zero? <0> → true,
zero? <1> → false.
Как обычно, true ≡ K, false ≡ KI.
Мы используем комбинатор H, чтобы построить комбинатор D такой, что
⎩
⎨
⎧
=
.,
,)(),(
ñëó÷àåïðîòèâíîìâS
ôîðìóíîðìàëüíóþèìååòttòåðìåñëèttK
Dt
Он
строится очевидным образом:
Страницы
- « первая
- ‹ предыдущая
- …
- 19
- 20
- 21
- 22
- 23
- …
- следующая ›
- последняя »