Формальні моделі алгоритмів та алгоритмічно обчислюваних функцій

Множина XT* породжувана за Постом, якщо iснують алфавiт TT та система Поста P=(T’, A, P) такi, що Th(P)(T*)=X.

Обчислюванiсть функцiй за Постом це породжуванiсть за Постом графiкiв таких функцiй.

Часткова функцiя f : Nk→N обчислювана за Постом, якщо породжуваною за Постом є множина { (x1,...,xk)Df }.

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

Приклад 2. Система Поста для функцiї f(x, y)=x+y :

ТЕЗА ЧОРЧА

Розглянемо співвідношення між різними формальними моделями поняття алгоритмічно обчислюваної функції. Обмежимося розглядом п-арних функцiй на множині N.

Теорема 8.1. Наступнi класи функцiй спiвпадають:

1) клас ЧРФ;

2) клас програмованих на N п-арних функцiй;

3) клас МНР-обчислюваних функцiй;

4) клас функцiй, обчислюваних за Тьюрiнгом;

5) клас функцiй, обчислюваних за Марковим;

6) клас функцiй, обчислюваних за ПостомОтже, розглянутi нами формалiзми задають один i той же клас п-арних функцiй на N. При цьому самi визначення формалiзмiв гарантують ефективну обчислюванiсть описуваних ними функцiй. Тому є всi пiдстави вважати, що такi формалiзми є рiзними математичними уточненнями iнтуїтивного поняття алгоритмiчно обчислюваної функцiї (АОФ). Вперше таке твердження стосовно рекурсивних функцiй було висунуте в 1936 роцi А. Чорчом, тому дiстало назву ”теза Чорча”. Узагальнення тези Чорча на випадок часткових функцiй в цьому ж роцi запропонував С. Клiнi. В такому розширеному виглядi теза Чорча формулюється наступним чином:

Tеза Чорча. Клас ЧРФ співпадає з класом п-арних АОФ, заданих на множині натуральних чисел.

Поняття АОФ не є строго визначеним математичним поняттям, тому теза Чорча математичному доведенню не пiдлягає. Теза Чорча є природно-науковим фактом, який засвідчує адекватність формальних моделей інтуїтивного поняття АОФ.

Із тези Чорча як наслiдок випливає:

клас РФ спiвпадає з класом тотальних АОФ, заданих на множинi натуральних чисел.

Значення тези Чорча (скорочено ТЧ) полягає в наступному.

1) Прийняття тези Чорча перетворює iнтуїтивнi поняття алгоритму, обчислюваностi, розв’язностi в об’єкти математичного вивчення.

2) Використання тези Чорча як своєрiдної аксiоми дозволяє в багатьох випадках замiнити формальнi завдання алгоритмiв на неформальнi їх описи. Це дає iстотне спрощення доведень, звiльняючи його вiд зайвих деталей. Проте доведення на основi тези Чорча має бути ретельно аргументованим! При виникненнi сумнiвiв треба вміти провести чисто формальне доведення.