В теорії обчислюваності теорема Райса стверджує, що всі нетривіальні семантичні властивості програм є нерозв'язними. Семантичні властивості стосуються поведінки програм (наприклад, «чи завершується задана програма для всіх вхідних даних?») — напротивагу синтаксичним властивостям, що характеризують сирці або конкретне кодування програми (наприклад, «чи містить задана програма оператор if-then-else ?»). Тривіальні властивості — це такі, що повертають True на всіх програмах, або False на всіх програмах.

Ця теорема узагальнює фундаментальний результат Алана Тюрінга про нерозв'язність задачі зупинки. В такому формулюванні, вона веде до обширних наслідків в статичному аналізі програм. Висновок теореми означає, що неможливо повністю коректно реалізувати алгоритм, котрий перевірятиме семантичні властивості програм без їх запуску на виконання; кожна така реалізація буде недооцінювати або переоцінювати деякі програми, і загалом давати хибні відповіді. До прикладу, ідея сканеру вірусів підпадає в сферу застосовності цієї теореми.

Теорема названа на честь , який довів її у своїй докторській дисертації 1951 року в Сіракузькому університеті .

Формалізація Нехай — допустима нумерація частково обчислюваних функцій, і нехай підмножина . Припускаючи, що:

є нетривіальною: тобто не порожня множина, і також не є множиною всіх натуральних чисел . є екстенсіональна: для будь-яких та , із слідує .

Тоді маємо необчислювана.

Приклади Маючи програму P, що приймає на вхід натуральне число n та обчислює натуральне число P(n), всі наступні властивості є нерозв'язними:

Чи завершується P на даному n? (Це і є проблема зупинки.) Чи завершується P на 0? Чи завершується P на всіх n? (Тобто, чи P тотальна.) Чи завершується P повертаючи 0 на всіх входах n? Чи завершується P повертаючи 0 на хоч деяких входах n? Чи завершується P повертаючи однакове значення на всіх входах? Чи є P еквівалентною до заданої програми Q?

Доведення за теоремою Кліні про нерухому точку Припустимо від супротивного, що є нетривіальною, екстенсіональною та обчислювальною множиною натуральних чисел. Оскільки нетривіальна, існує натуральне число і натуральне число . Визначимо повну обчислювальну функцію від та , як у випадку коли , та коли . Згідно з теоремою Кліні, існує нерухома точка така, що . Отримуємо суперечення: якщо , то за визначенням , що порушує екстенсіональність через ; і навпаки, якщо , то маємо , що знову суперечить екстенсіональності, оскільки .

Доведення шляхом зведення до задачі зупинки

Ескіз доведення Без втрати загальності, припустімо наявність коректного алгоритму is_a_squaring_function, що приймає на вхід кодування програми p та безпомилково визначає, чи є p реалізацією функції зведення натурального числа у квадрат. Подальше доведення працюватиме з будь-яким іншим предикатом на програмах, як тільки він коректно визначає довільну семантичну нетривіальну властивість, як наведено в загальному вигляді нижче.

Далі покажемо, як сконвертувати is_a_squaring_function у предикат, що розв'язує проблему зупинки. Ми опишемо алгоритм halts(a,i) що приймає на вхід кодування програми a, її вхід i, та визначає чи програма a завершиться, якщо її запустити на вхідних даних i.

Предикат halts побудований наступним чином. Отримавши параметри a та i, спершу він конструює опис (або ж, кодування) нової програми t(n), котра виконує два кроки:

запуск програми a на вході i, та знищення її результату; обчислення квадрату n та зупинка з цим результатом.

У тому разі, коли a не завершується на вході i, програма t не досягає кроку 2, незалежно від значення n. Отже, легко побачити, що t є коректним алгоритмом обчислення квадрату тоді і тільки тоді, коли крок 1 завершується. В такому випадку, is_a_squaring_function(t) буде істина.

Спираючись на початкове припущення існування is_a_squaring_function, ми отримали функцію halts, що розв'язує проблему зупинки: def halts (a,i): def t(n): a(i) return n × n return is_a_squaring_function(t) Зауважимо, що halts ніколи не виконує програму t; лише створює її опис та передає той на вхід в is_a_squaring_function, котра за припущенням завжди завершується. Оскільки крок створення опису програми t також не зациклюється (прийнявши скінченність опису програми a, та її входу i) — отримуємо, що halts тотальна, завершується завжди.

І нарешті, дана конструкція не залежить безпосередньо від обчислення саме квадратів. Ми могли б припустити будь-яку іншу семантичну нетривіальну властивість замість is_a_squaring_function, відповідно адаптувавши крок 2 у визначенні функції t, так само отримуючи парадоксальний розв'язок проблеми зупинки.

Формальне доведення Надалі, приймемо що алгоритми визначають часткові функції над рядками та самі представлені рядками. Часткова функція, обчислювана алгоритмом, закодованим рядком a, позначається як Fa.

Наявне доведення здійснюється через reductio ad absurdum (методом «від супротивного»): ми припускаємо існування розв'язної нетривіальної властивості, і надалі показуємо, як з цього випливає суперечність (а саме, алгоритм що вирішує задачу зупинки, що неможливо) — зрештою роблячи висновок, що припущення було хибне.

Припустимо ж, що P(a) — це алгоритм, який визначає деяку нетривіальну властивість Fa. Без втрати загальності, можна прийняти, що P(no_halt) = false, де рядок no_halt є кодуванням алгоритму, який ніколи не зупиняється. В протилежному випадку, це вірно для алгоритму , що обчислює заперечення властивості P. За визначенням нетривіальної властивості, існує рядок b, який кодує алгоритм що обчислює функцію Fb, і разом з тим P(b) = true.

Тоді ми можемо задати алгоритм H(a, i) наступним чином:

1. Сконструювати рядок t, що кодує алгоритм T(j), використовуючи рядки a та b, так щоб: T спершу симулював обчислення Fa(i), потім T симулював обчислення Fb(j) та повертав його результат. 2. Повернути P(t).

Вичерпним аналізом альтернатив, тепер можна показати, що H вирішує проблему зупинки:

У випадку, коли алгоритм, закодований рядком a, зупиняється на вході i — маємо Ft = Fb, і оскільки P(b) = "yes", а результат P(x) залежить лише від Fx, то слідує, що P(t) = "yes", а отже, H(a, i) = "yes". У випадку, коли алгоритм, закодований рядком a, не зупиняється на вході i — маємо Ft = Fno_halt, тобто часткова функція, визначена ніде. Оскільки P(no_halt) = "no", а результат P(x) залежить лише від Fx, то слідує, що P(t) = "no", а отже, H(a, i) = "no".

Як добре відомо, задача зупинки є нерозв'язною, але як показано, ми побудували алгоритм H котрий її розв'язує. Це суперечність, і отже припущення про існування алгоритму P(a), що обчислює нетривіальну властивість алгоритму, представленого рядком a, повинно бути хибним.

Див. також

Проблема зупинки Теорія алгоритмів

Посилання