2 Постановка задачи: о связном предъявлении теории информатики и практики программирования в теме исполнения для теоретического мышления. 13 (стр. 12 из 25)
Изоморфное вложение ¦: A®B составляется хитро:
Рассмотрим последовательно
¦o(a)={a}
¦1(a) = {a}È{{x}®a×x | xÎA}
¦2(a) = {a} È {{x}®a×x | xÎA} È {{x}®({y}®axy) | x,yÎA}
¦3(a) =¦2(a) È {{x}®({y}®({z}®axyz))) | x,y,zÎA}.
Тогда можем представить, чем является
. Легко доказывается, что ¦(а)*¦(b)=¦(a×b): 
Так как ¦(b) = {b} È {g®d | ¼}, а a={x}, где xÎA, то
По определению ¦i+1(a) {y | ({b}®y)Φi+1(a)} = {y | yΦi(a×b), yΦi-1(a×b),¼}.
Поэтому
¦: A®B является инъективным отображением. Действительно, если a¹b Þ ¦(a)¹¦(b), т.к. ¦(a)ÇA = {a}, а ¦(b)ÇA = {b}.
3.3.2 Îáùèå àñïåêòû, ñâÿçàííûå ñ íåïîäâèæíîé òî÷êîé.
В изложении многих теорий теорема о неподвижной точке тесно переплетается с понятием вычислимости и самовыразимости, поэтому для начала рассмотрим ее в свете теории вычислимых функций.
Важнейшим вопросом этой теории является вопрос разрешимости (или неразрешимости) проблемы, который в свою очередь неминуемо приводит к вопросу о формализации понятия алгоритма (т.е. процедуры) и вычислимой "с помощью алгоритма" функции (т.е. отображения, задаваемого процедурой). Один из методов такой формализации лежит через определение рекурсивной функции.
Трудности, возникающие в этой связи состоят в выборе рекурсивного определения для описания класса функций некоторого рода. Грубо говоря, рекурсивное определение - это определение, в котором значения функции для данных аргументов непосредственно определяются значениями той же функции для "более простых" аргументов или значениями более простых функций (например, констант). Формализация понятия "более простых" функций как констант удобна, так как тогда рекурсивные определения можно рассматривать как алгоритмы (например, ряд Фибоначчи).
Важно ввести рекурсивное определение так, чтобы описываемый им класс был формальным аналогом неформального понятия всюду определенной функции, вычислимой алгоритмом. (Частным случаем может быть определение примитивнорекурсивной функции [1,стр 22]). Попытки такой формализации наталкиваются на проблему, возникающую в связи с так называемым методом диагонализации [1,стр 25], который дает алгоритмическую функцию, не попадающую в данный формализованный класс. Чтобы избежать этих трудностей можно рассмотреть наравне с всюду определенными функциями и функции не всюду определенные (частичные). Такой подход дает хорошо известные формализации Тьюринга, Клини, Черча, Поста, Маркова, которые являются эквивалентными в смысле получаемого класса функций, дающего наряду с частичными (частичнорекурсивными) функциями и всюду определенные функции (общерекурсивные).
Для каждой функции из полученного класса определяется схема вычисления (набор инструкций). Можно найти алгоритм перечисления всех таких наборов, получаемых данной формализацией (в формализации Тьюринга - наборы четверок, удовлетворяющих условию совместимости), который каждому числу Х сопоставляет набор инструкций стоящий на (Х+1)-ом месте в перечислении. Тем самым мы можем перейти от класса функций к множеству натуральных чисел и проводить исследования на этом множестве.
В этих исследованиях мощным аппаратом и является понятие о "неподвижной точке". Теорема рекурсии (или теорема о неподвижной точке в теории рекурсивных функций) позволяет достаточно просто установить некоторые свойства множеств натуральных чисел. Например, полнота творческих (креативных) множеств и, что всякое продуктивное множество - вполне продуктивно [см.1].
Данные же свойства в свою очередь тесно перекликаются с таким свойством как рекурсивность (обладание рекурсивной характеристической функцией) наиболее важный аспект связанный с разрешимостью и неразрешимостью.
Теорема рекурсии также позволяет перенести понятия рекурсивности и рекурсивной перечислимости из области натуральных чисел в область более сложных объектов, а именно - N-ок чисел. Аппарат неподвижной точки дает простой метод порождения различных патологических структур в теории рекурсивных функций, дает возможность установить соотношения между некоторыми понятиями (например, существование для каждой частичнорекурсивной функции соответствующей примитивнорекурсивной функции особого рода - см. формулировку теоремы Клини в [2]). Теорема о неподвижной точке может быть использована (так же как и в анализе) для доказательства существования многих неявно заданных функций.
Приведем формулировку теоремы о неподвижной точке в теории рекурсивных функций и ее следствие.
Т е о р е м а. Пусть f - общерекурсивная функция, тогда существует число n, такое, что H(n)=H(f[n]), где H(n) - частичнорекурсивная функция, соответствующая n-ому геделеву номеру, а n - неподвижная точка.
С л е д с т в и е. f - произвольная обобщеннорекурсивная функция => существует n, такое, что W[n]=W[f(n)], где W[n] - перечислимое множество, определяющееся как W[n]= Arg j(n)/
Рассмотрим теперь использование теории рекурсивных функций в логике. Это становится возможным путем ввода понятия правильно построенной формулы (конечной цепочки символов конечного алфавита), совпадающим с понятием высказывания в логике предикатов, а также ввода процедуры, позволяющей определить какие цепочки являются правильно построенными формулами (ППФ), а какие нет. Для этого предпринимается кодирование ППФ натуральными числами (аналогично кодированию наборов инструкций в теории рекурсивных функций).
При изучении конкретных логических систем некоторые множества ППФ выделяются как "представляющие особый интерес" (например, "доказуемые", "истинные"). Эти множества называются теориями. ППФ теории оказываются часто эффективно перечисляемыми (например, "доказуемые"). Теория называется аксиоматизируемой, если соответствующее множество ППФ может быть эффективно пересчитано. Аналогично: теория разрешима, если она рекурсивна. Существование рекурсивно перечислимых, но не рекурсивных теорий показывает, что некоторые хорошо известные аксиоматизируемые теории могут быть неразрешимыми ("доказуемые" ППФ логики предикатов образуют неразрешимую теорию).
Иллюстрацией применения теоремы о неподвижной точке в логике могут быть аксиомы утверждающие свою собственную непротиворечивость.
Пусть логическая система с кодированными ППФ на натуральных числах, пусть также определено понятие "непротиворечивости" (множеств ППФ). Существует общерекурсивная функция С, такая, что для любого Х ППФ (с кодовым номером) С(Х) понимается как утверждение о непротиворечивости множества W[x] ППФ.
Пусть дано рекурсивно перечислимое множество W[p] ППФ. Возникает вопрос: можем ли мы добавить к W[p] ППФ с кодовым номером q, которая будет утверждать непротиворечивость W[p] U {q}? Ответ заключен в следующей
Т е о р е м е: каковы бы ни были натуральное число p и общерекурсивная функция С, существует натуральное число - n, такое, что W[n] = W[p] U {C(n)}.
(Доказательство вытекает из следствия [см.1]).
Мы применили теорему рекурсии в логике. Заметим также, что многие синтаксические и семантические понятия можно переформулировать в терминах теории рекурсивных функций.
Понятие неподвижной точки фигурирует также в логическом программировании при описании сути процедурной семантики с помощью семантики неподвижной точки.
Каждое правило А(0) <- A(1),...,A(m) логической программы Р можно рассматривать как m-арную частичную операцию на множестве всех основных атомов:
если правило QA(0) <- QA(1),...,QA(m) принадлежит программе P*, то эта операция применима к кортежу QA(1),...,QA(m) и QA(0) - ее результат. Тем самым на множестве основных атомов задается алгебра (с не всюду определенными и, вообще говоря, многозначными операциями). Операции этой алгебры задают оператор Фр, переводящий каждую интерпретацию Int в интерпретацию
Фр(Int) = {QA(0)| в P* существует правило QA(0) <- QA(1),...,QA(m) и {QA(1),...,QA(m)} ÎInt}.
Можно показать, что множество неподвижных точек этого оператора (т.е. множество таких интерпретаций, что Фр(Int)=Int) совпадает с множеством моделей программы Р для "если и только если” - семантики [см.3,стр.305]. Главная модель Int(р) программы Р - это наименьшая неподвижная точка оператора Фр, т.е. наименьшая подалгебра описанной выше алгебры. Для этой модели имеет место
Int(p) =
Фkn(Æ) (2)Эта алгебраическая структура проясняет "устройство" моделей программы. Соотношение (2) говорит о том, что каждый атом главной модели "получается" за конечное число шагов с помощью операций данной алгебры и тем самым быть установлена за конечное число шагов. На этом и основана процедурная семантика программы. Семантика неподвижной точки для логических программ аналогична денотационной семантике для "обычных" программ.