name=bookmark254>VIII.
1.
Теория
вычислений

Теория вычислений включает в себя
ту часть математики, в которой рассматриваются эффективно вычислимые отношения.
В ней изучаются математические свойства самих отношений, их определимость в той
или иной формальной системе, вычислимость на конкретных машинах и их значения
относительно конкретных схем интерпретации. Эти и другие аспекты данной теории
традиционно развивались в рамках отдельных направлений, таких как теория
рекурсивных функций, теория вычислимости, формальная семантика и т. д. Основной
принцип, поддерживаемый многими сторонниками логического программирования,
заключается в том, что оно позволяет объединить все эти различные подтеории,
подвести под них общий фундамент и дать им рационалистическое обоснование. Он
поддерживается не только в том теоретическом смысле, что логика вообще лежит в
основании математики, но и в более практическом смысле: логическое
программирование, по-видимому, способно естественным образом охватить
репрезентативные и операционные характеристики широкого класса вычислительных
формализмов и связанных с ними теорий. В этом разделе мы кратко очертим те
пути, на которых логическое программирование сделало вклад в теорию вычислений.

VIII.1.1. Представимость и вычислимость ·.·: 4-

В связи с каждым предлагаемым
вычислительным формализмом естественно поставить вопрос: что с его помощью
можно представлять и вычислять? Минимальным требованием почти для всех
практических целей является возможность представления натуральных чисел. В
логическом программировании это требование может быть удовлетворено наличием
любой фиксированной константы, например константы O, для
представления «нуля» и любого фиксированного функтора, например s, для
представления «следующего числа». Натуральные числа можно тогда представить
термами O, s(0), s(s(0)) и т. д.
Менее тривиально, у нас может возникнуть также желание иметь возможность
определять на любом таком представлении все те отношения, которые может
потребоваться вычислять на множестве натуральных чисел. Возможность определения
всех таких отношений была впервые доказана Робертом Хиллом. А именно он
показал, что логики хорновских дизъюнктов достаточно для определения всех
эффективно вычислимых функций на множестве {O, s(0), ...} и что для
этой цели не требуется никаких других функторов, кроме Ons. Более общее
описание адекватности логики хорновских дизъюнктов дается в его отчете (Хилл, 1974).