Непейвода Н.Н., Скопин И.Н. Основания программирования

Подождите немного. Документ загружается.

B.1. ЛОГИЧЕСКИЕ ПАРАДОКСЫ

865

определимое при помощи предложения, содержащего менее ста

символов” содержит менее ста символов и определяет

Конструкция парадокса Берри интенсивно используется в современной те-

ории сложности вычислений для доказательства трудности решения задач.

Она практически сводится к общенаучному принципу, что система может

быть полностью познана лишь на порядок более сложной системой.

Примером нерефлексивного логического парадокса является парадокс утрен-

ней звезды.

Утренняя звезда — то же, что планета Венера. Сегодня вечером

я видел Венеру. Значит, я видел Утреннюю звезду.

Конструкция данного парадокса использована в доказательстве теоремы Рай-

са о неразрешимости нетривиальных свойств вычислимых функций (един-

ственные свойства вычислимых функций, которые могут определяться про-

граммой — тождественно истинное и тождественно ложное) и теоремы о

невозможности нетривиальных точных предсказателей (Е. Е. Витяев).

Как логические парадоксы часто трактуются законы материальной им-

пликации — “из лжи следует все, что угодно” и “истина следует из всего, что

угодно,” поскольку они позволяют получить формулы A ⇒ B, в которых A и

B никак не связаны по смыслу. Эти аномалии явились стимулом для развития

модальных, паранепротиворечивых и релевантных логик, в которых данные

парадоксы частично преодолеваются. На самом деле полностью преодолеть

их невозможно, поскольку любая успешная формализация является сильным

огрублением.

Еще один класс парадоксов, возникающих на границе логики и матема-

тики, основан на применении точных методов к неточным понятиям.

Человек,у которого на голове нет ни одного волоса — лыс.Если у

лысого вырастет еще один волосок, он останется лысым. Значит,

все люди лысые.

Данный класс парадоксов интенсивно используется при развитии ультраин-

туиционистской математики, имеющей дело с процессами, завершимыми в

реальное время.

866

ПРИЛОЖЕНИЕ B. МЕТОДОЛОГИЧЕСКИЕ РЕЗУЛЬТАТЫ

§ B.2. ТЕОРЕМЫ ТАРСКОГО И ГЕДЕЛЯ

Теория непротиворечива, если в ней нельзя вывести противоречие (фор-

мулу, эквивалентную лжи). Модель теории — интерпретация, в которой ис-

тинны все аксиомы. Теорема о корректности (Сколем, Гедель) классической

логики утверждает, что в любой модели теории истинны все ее теоремы. Та-

ким образом, логический вывод сохраняет истинность в интерпретации.

Теорема Геделя о полноте утверждает, что любая непротиворечивая те-

ория имеет модель. Тем самым оказывается, что классическое понятие тав-

тологии (формулы, истинной в любой интерпретации) описывается при по-

мощи сравнительно простого исчисления (классической логики предикатов).

Теорема о полноте эквивалентна аксиоме выбора, так что даже в принци-

пе никакого построения конкретной модели она дать не может. Конечно, в

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

строения» моделей для нетривиальных случаев сводятся к преобразованию

какой-либо иной конструкции, созданной при помощи аксиомы выбора, и ко-

торая сама построена быть не может (например, ультрафильтра). Из теоремы

Геделя о полноте следует теорема компактности Мальцева: если любое ко-

нечное число аксиом теории имеет модель, то и вся теория имеет модель.

В самом деле, для вывода противоречия используется конечная конструкция

доказательства, и в ней может быть использовано лишь конечное число ак-

сиом.

Теорема Геделя о неполноте говорит, что любая теория с разрешимым

множеством аксиом, содержащая натуральные числа и дающая возможность

выразить хотя бы примитивно-рекурсивные функции, неполна. Теорема Ге-

деля о неполноте доказывается при помощи построения, по сути дела являю-

щегося одним из парадоксов автореференции. А именно, строится формула,

утверждающая свою собственную недоказуемость. Она не может быть дока-

зана, потому что тогда мы получили бы прямое противоречие, она не может

быть и опровергнута, потому что тогда мы получили бы доказательство ее

недоказуемости и, следовательно, ее обоснование.

Причины, по которым возникла теорема Геделя о неполноте, проясняет

теорема Тарского о невыразимости истины. Если теория достаточно сильна,

чтобы выразить подстановку, то в ней невыразимо понятие истинности ее

формул. В противном случае мы могли бы построить формулу, утверждаю-

щую: «Я лгу.» Поэтому теорему о неполноте обойти практически невозмож-

но, любая попытка ее обойти сама дает контрпример.

Теорема о существовании нестандартных моделей является следствием

B.3. ИДЕАЛЬНЫЕ И РЕАЛЬНЫЕ ПОНЯТИЯ ПО ГИЛЬБЕРТУ

867

теоремы полноты. Поскольку, в частности, для любого бесконечного уни-

верса всегда можно добавить к теории без противоречия новую константу,

не равную (или большую, если определено понятие порядка) всем элементам

стандартной модели, то имеются, в частности, модели арифметики и анализа

с бесконечно большими (а для анализа, следовательно, и с бесконечно малы-

ми) числами. Все свойства, выразимые на исходном языке, в такой модели

сохраняются, и поэтому нестандартные числа можно без опаски использо-

вать для получения результатов о стандартных элементах.

Нестандартные модели, которые потребовали явного различения языка и

метаязыка, привели к следующим двум парадоксам.

Множество всех стандартных действительных чисел является ча-

стью нестандартного конечного множества. Таким образом, бес-

конечное может быть частью конечного.

Все подмножества нестандартной действительной оси сохраня-

ют все свойства стандартных множеств. Множество стандартных

действительных чисел ограничено сверху любым положительным

бесконечно большим числом. Значит, должно быть либо наиболь-

шее стандартное действительное число, либо наименьшее беско-

нечно большое. Но для любого стандартного

x x + 1

также стан-

дартно, а для бесконечно большого

x x − 1

также бесконечно.

Оба этих парадокса основаны на том, что свойство “быть стандартным” при-

надлежит метаязыку. Первый из них послужил основой теории полумно-

жеств, в которой классы могут быть подклассами множеств.

§ B.3. ИДЕАЛЬНЫЕ И РЕАЛЬНЫЕ ПОНЯТИЯ ПО ГИЛЬБЕРТУ

Нестандартные модели явно и бескомпромиссно высветили то, что по-

нималось ведущими мыслителями еще до их построения. Часто мы строим

в математике идеальные понятия, которые не имеют никакой (вычислитель-

ной) интерпретации, и при их помощи получаем реальные результаты.

Это наблюдение Д.Гильберт сделал основой своей методологической кон-

цепции математического знания. Согласно методологии Гильберта, основ-

ная часть математических понятий идеальна, и не стоит даже пытаться дать

им прямую интерпретацию. Но идеальные понятия могут привести к реаль-

ным результатам, которые, на самом деле, и составляют основную ценность

математики для приложений. Гильберт считал, что без идеальных понятий

868

ПРИЛОЖЕНИЕ B. МЕТОДОЛОГИЧЕСКИЕ РЕЗУЛЬТАТЫ

практически невозможно было бы достичь большинства ценных реальных

результатов современной математики (смотрите, например, фракталы и их

применение в машинной графике; этот пример, конечно же, еще не был из-

вестен Гильберту, но он исключительно ярко демонстрирует роль идеальных

понятий и полученных при их помощи реальных следствий). Но Гильберт

был уверен в возможности хотя бы в принципе устранить идеальные понятия

из математических рассуждений. Развитие логики опровергло эту его слиш-

ком оптимистичную надежду. Его трезвый и жесткий взгляд оказался все-

таки недостаточно жестким.

Если посмотреть чуть пристальнее, то видно, что оппозиция идеально-

сти и реальности не является бинарной и абсолютной. Для вычислителя дей-

ствительные числа являются идеальными объектами, поскольку в принципе

они могут быть вычислены сколь угодно точно, а у реального вычислителя

точность вычислений, да и исходных данных, ограничена. Но в сопоставле-

нии с нестандартными числами действительные числа выглядят реальными

объектами.

§ B.4. ПАРАДОКС ИЗОБРЕТАТЕЛЯ

Д. Пойа ввел понятие парадокса изобретателя независимо от концепции

идеальных объектов Д. Гильберта. Он использовал наблюдение, что при до-

казательстве по индукции часто необходимо усиливать доказываемое пред-

ложение, и индуктивное утверждение становится намного сложнее конеч-

ного результата. Эта необходимость усиливать результат, чтобы его строго

обосновать, на первый взгляд кажется парадоксальной.

Парадокс изобретателя связан со следующей логической и методологи-

ческой проблемой. В доказательствах порою встречаются вспомогательные

утверждения, более сложные, чем извлекаемые из них следствия. Можно ли

хотя бы в принципе устранить окольные пути в доказательствах, когда мы

доказываем лемму лишь затем, чтобы в дальнейшем применить ее в частных

случаях? Доказательства без окольных путей называют также прямыми.

Логические корни парадокса изобретателя оказались исключительно глу-

боки и связывают его с концепцией идеальных понятий и с современными

методологическими рассмотрениями.

Первым в данном ряду явился результат Хао Вана (1954 г.). Он постро-

ил последовательность примитивно-рекурсивных функций f

, таких, что для

доказательства утверждения ∀xf

(x) = 0 необходимо воспользоваться ин-

дукцией по формулам, содержащим не менее чем n кванторов. Таким обра-

B.5. ТИПЫ И ПОРЯДКИ

869

зом,даже в принципе в математических доказательствах внешне простых пред-

ложений нельзя обойтись без сложных лемм.

В. Оревков (1970) показал, что, хотя, как было известно ранее, в прин-

ципе в чистой логике можно устранить все леммы и пользоваться прямыми

доказательствами, проигрыш от их устранения непоправимо большой. Он

построил последовательность формул, такую, что длина доказательства n-

ной формулы с окольными путями пропорциональна 13n, а длина прямого

вывода не может быть меньше

...

(n раз).

Естественно, что сложность лемм при продвижении по данной последова-

тельности быстро возрастает.

В дальнейшем Р. Л. Гудстейн (1974) показал, что чем эффективнее про-

грамма, тем более высокие теоретические концепции могут понадобиться

для доказательства ее правильности.

Парадокс изобретателя показывает полную методологическую несостоя-

тельность редукционизма и эмпиризма (в том числе и такой его философской

профанации, как утилитаризм). Без концепций и идей высших уровней чело-

век обречен на умственное и духовное пресмыкание!

§ B.5. ТИПЫ И ПОРЯДКИ

Парадокс изобретателя остро ставит вопрос о критериях измерения слож-

ности формул и, в более общем виде, об иерархии идеальных концепций.

Простой, но весьма действенный, способ оценки уровня понятий и объектов

дал Б. Рассел. Он предложил классифицировать объекты по типам. Исходные

данные — объекты нулевого типа. Множества исходных данных и функции

над ними — объекты первого типа. Множества и функции над объектами

первого типа — объекты второго типа.

Соответственно, логические утверждения делятся на утверждения пер-

вого порядка, в которых нет ни переменных, ни кванторов по объектам вы-

ше нулевого типа, второго порядка, когда появляются кванторы по объектам

первого типа, и так далее. Классическая логика утверждений второго и бо-

лее высоких порядков уже неформализуема.

Оценка уровня теоретических концепций по уровню используемых объ-

ектов и порядку высказываний о них является прекрасным эвристическим

методом.

870

ПРИЛОЖЕНИЕ B. МЕТОДОЛОГИЧЕСКИЕ РЕЗУЛЬТАТЫ

Внутри утверждений одного и того же порядка есть также важная с прак-

тической точки зрения иерархия по числу перемен кванторов в формуле (гру-

бо говоря, по числу кванторов, но одинаковые кванторы обычно можно свер-

нуть в один квантор по структуре данных).

Внимание!

Есть важнейшее наблюдение, впервые явно высказанное Ю.

Л. Ершовым, а неявно следующее из трудов С. К. Клини. Вычи-

слимость определена на первом уровне в самых разных аспек-

тах. Абсолютное определение вычислимости (например, маши-

ны Тьюринга) однозначно, как следует из тезиса Черча. Относи-

тельное также достаточно однозначно. Определение с ресурсны-

ми ограничениями слегка зависит от кодирования данных, но воз-

никающие неоднозначности легко преодолимы.

Для объектов второго типа вычислимость определяется уже

неоднозначно. Более того,определив вычислимость для объектов

второго типа, мы опять-таки сталкиваемся с неоднозначностью

ее распространения на третий, и так далее.

У обычного человека уже утверждения первого порядка с тремя перемена-

ми кванторов, а второго порядка с одной переменой кванторов, вызывают

затруднения при понимании. Примером такого утверждения является стан-

дартное определение непрерывности или предела. В математике объекты в

данный момент доходят до пятого типа. Примеры утверждений с семью пе-

ременами кванторов по четвертому-пятому типу дают современные теория

динамических систем, алгебра, логика, топология. Примеры явно сформули-

рованных принципов высоких типов можно найти, например, в книге [54] и

в последующих книгах Матросова и Васильева.

Заметим, что типы традиционных языков программирования, например,

языков

Pascal

C++

, не поднимаются в классификации Рассела выше перво-

го, причем сущности первого типа реализованы некорректно.

§ B.6. ЧИСТЫЕ ТЕОРЕМЫ СУЩЕСТВОВАНИЯ

Развитие современных логических методов привело к новым логическим

парадоксам. Например, Брауэр подметил следующий парадокс классическо-

го существования:

B.6. ЧИСТЫЕ ТЕОРЕМЫ СУЩЕСТВОВАНИЯ

871

В любой достаточно сильной классической теории имеется дока-

зуемая формула вида

∃x A(x)

, для которой нельзя построить ни-

какого конкретного

, такого, что доказуемо

A(t)

В частности, нельзя построить в теории множеств ни одной нестандартной

модели действительных чисел, хотя можно доказать существование таких

моделей.

На самом деле чистые теоремы существования появляются уже в началь-

ном курсе математического анализа. Например, в принципе, при любом рас-

ширении понятия алгоритма, нельзя построить верхнюю грань любого огра-

ниченного множества действительных чисел, и даже найти наименьшее чи-

сло в любом непустом множестве натуральных чисел. Эти задачи могут ре-

шаться лишь в частных случаях.

Корни чистых теорем существования лежат в классической логике. Если

классическая теория неполна, то в ней обязательно есть чистые теоремы су-

ществования. А любая теория, содержащая натуральные числа, сложение и

умножение, неполна.

Если есть чистые теоремы существования, то теория неконструктивна.

Практически важными примерами теорий,где классическая логика конструк-

тивна —элементарная геометрия и элементарная алгебраическая теория дей-

ствительных чисел, в которой нет понятия натурального числа.

Для того, чтобы избавиться от неконструктивности, Брауэр предложил

модифицировать логику. Предложенная им модификация классической ло-

гики (удаление закона исключенного третьего и эквивалентного ему прин-

ципа снятия двойного отрицания) привела к логике, которая сохраняет кон-

структивность для теорий с числами — интуиционистской логике. Это была

первая из построенных конструктивных логик.

В конструктивных логиках формулы интерпретируются не через логиче-

ские значения, а через решения связанных с ними задач. Например, формула

A ∨ ¬A означает наличие ответа на вопрос, истинна A или ложна. Поэтому

обычно в них говорят не об истинности формул, а об их реализуемости.

В настоящее время известны следующие классы конструктивных логик.

1. Интуиционистская логика, которая адекватна вычислениям, где огра-

ничения на время и память несущественны (логика принципиальной

вычислимости). Интуиционистская логика максимально близка к клас-

сической, отличаясь от нее отсутствием закона исключенного третьего

(этого закона нет и в других конструктивных логиках). Ее модифика-

ция: интуиционистская логика с сильным отрицанием, или симметрич-

872

ПРИЛОЖЕНИЕ B. МЕТОДОЛОГИЧЕСКИЕ РЕЗУЛЬТАТЫ

ная интуиционистская логика, вводит в рассмотрение еще и процесс

анализа ошибок. Сильное отрицание сохраняет правило снятия двой-

ного отрицания и законы формулировки отрицаний, но полностью от-

казывается от правила приведения к абсурду. Соджержательно оно мо-

жет истолковываться как явное построение контрпримера.

2. Линейные логики, в которых рассматриваются вычисления, произво-

димые при ограничениии на ‘денежный’ ресурс. Тем самым мы мо-

жем иметь возможность реализовать A и B, но не оба вместе. Харак-

теристическим признаком для таких логик является отсутствие закона

A ⇒ A&A.

3. Нильпотентные логики, в которых вычисления производятся при огра-

ниченном времени. Таким образом, мы не можем не тратить выделен-

ный нам ресурс,даже если ничего не делаем. Характеристическим при-

знаком для них является правило исключенного застоя

A ⇒

¬A

Эти логики лучше всего описывают программирование от состояний.

4. Реверсивные логики, когда, наоборот, рассматриваются лишь обрати-

мые действия. Они описывают, например, вычисления в компьютере

на сверхпроводниках.

5. Когерентные логики, (часто называемые также категорными), когда

рассматриваются вопросы согласования данных. Они описывают про-

цессы приведения данных от одного типа к другому.

§ B.7. ДОКАЗАТЕЛЬСТВА И ПРОГРАММЫ

В конструктивных логиках доказательство не просто дает принципиаль-

ную возможность построить требуемый объект.При правильно подобранном

логическом инструментарии оно дает структуру алгоритма решения задачи.

При этом обычно выполняются следующие соотношения:

• Кванторы существования соответствуют значениям нулевого типа (зна-

чениям исходных типов). В целевой формуле они соответствуют ре-

зультатам создаваемой программы, в аксиомах — выходным данным

имеющихся методов либо подпрограмм.

B.7. ДОКАЗАТЕЛЬСТВА И ПРОГРАММЫ

873

• Конъюнкции соответствуют записям. Во многих конструктивных логи-

ках они естественно объединяются в промежуточных формулах с кван-

торами существования,образуя формулу,описывающую задачу постро-

ения структуры данных:

∃x

, . . . , x

& ···&A

В этой структуре x

представляют собой данные, а A

— структуры

данных либо методы.

• Импликации соответствуют преобразованиям. A ⇒ B означает по-

строение преобразования решений A в решения B.

• Кванторы всеобщности соответствуют параметрам создаваемых про-

цедур. Часто они объединяются с импликацией в группу:

∀x

, . . . , x

& ···&A

⇒ B),

выражающую задачу построения функционала с параметрами-данны-

ми x

и параметрами высших типов A

• Дизъюнкция соответствует в разных контекстах условному оператору

или структуре с альтернативными полями и дескриптором.

• Обычное отрицание порождает призраков. Оно доказывается приведе-

нием к абсурду, и успешность его доказательства показывает, что все

использованное при выводе отрицания не может выполняться при пра-

вильной работе программы,и поэтому может попасть разве лишь в ком-

ментарии.

• Сильное отрицание соответствует явно пойманной ошибке, которую

предстоит проанализировать.

Эти соотношения можно рассматривать как эвристики достаточно высоко-

го уровня и общности, применимые для получения плодотворных аналогий

и нетривиальных предупреждений при анализе понятий программирования.

Точное их применение требует серьезного теоретического анализа и практи-

ческого чутья в каждом отдельном случае.

Не только отрицания порождают призраков. Безобиднейшая с виду фор-

мула, подобная

∀x, y, z(A(x, y)&B(y, z) ⇒ C(x, z))

874

ПРИЛОЖЕНИЕ B. МЕТОДОЛОГИЧЕСКИЕ РЕЗУЛЬТАТЫ

может превратить в призраки все построения y. Поэтому в доказательстве

имеются большие бездействующие блоки, которые служат для обоснования

строящегося алгоритма.

В принципе, если у нас есть адекватная конструктивная формализация,

программа может быть чисто механически извлечена из конструктивного до-

казательства. Получающиеся конструкции часто требуют дальнейшего пре-

образования,поскольку они сплошь и рядом пользуются функционалами выс-

ших типов и порою недостаточно эффективны (второе гораздо реже).

Более того, такой подход единственно разумный в задаче обоснования

программ. Это обосновано теоремой о верификации, упорно замалчиваемой

научным сообществом уже 20 лет

Доказательство правильности программы может быть без существенного

увеличения длины перестроено в доказательство, синтезирующее програм-

му, удовлетворяющую заданным спецификациям.

Если в теории происходит увеличение длины в малое количество раз, на

практике это означает, что результат короче и проще. Отсюда следует вывод

Внимание!

Если вам необходимо построить доказательно правильную про-

грамму, делайте это с самого начала. Не пытайтесь сначала напи-

сать ее, а затем доказывать ее правильность!

§ B.8. ОСНОВНЫЕ ПОНЯТИЯ НЕФОРМАЛИЗУЕМОСТИ

И, наконец, последний класс логических парадоксов возникает на гра-

ницах между формализованными и неформализуемыми понятиями. Рассмо-

трим два из них.

Витгенштейн утверждает, что

«Все, что может быть сказано, мо-

жет быть сказано ясно. А о чем не следует говорить, о том нужно

молчать.»

Поскольку

“сказано ясно”

означает

“быть формализо-

ванным,”

а ни одно сложное понятие не может быть полностью

формализовано, нужно молчать обо всем, что выходит за рамки

чистой логики предикатов.

Ну, это в десять раз меньше, чем замалчивались открытия кн. Белосельского-Белозерско-

го.