мимоходом, ночное чтение

Я купил Stoner Джона Уильямса два года назад, и только сейчас начал читать. Потрясающая книга, раскрывающая скучную жизнь человека с неудачной судьбой так, что невозможно оторваться. Очень, очень хорошо написана. Несколько раз, читая ее, вспоминал "Защиту Лужина", похожую на нее, кажется, книгу (mutatis mutandis) - не столько структурой и некоторыми обстоятельствами сюжета, сколько ощущением одновременно радости и глубокой печали при ее чтении.

Вот статья о том, как эта книга после 40-летнего полузабытого существования, возвращается в новых изданиях и даже стала неожиданным бестселлером в Голландии.

Вот длинный отрывок, который дает представление о стиле романа. Это в самом начале книги; главный герой, выросший на ферме в Миссури, и ничего, кроме этой фермы и работы на ней, не знавший, учится на сельскохозяйственном факультете небольшого университета. Обязательный обзорный курс художественной литературы на втором году обучения одновременно пугает и притягивает его.

The class had read two plays by Shakespeare and was ending the week with a study of the sonnets. The students were edgy and puzzled, half frightened at the tension growing between themselves and the slouching figure that regarded them from behind the lectern. Sloane had read aloud to them the seventy-third sonnet; his eyes roved about the room and his lips tightened in a humorless smile.

“What does the sonnet mean?” he asked abruptly, and paused, his eyes searching the room with a grim and almost pleased hopelessness. “Mr. Wilbur?” There was no answer. “Mr. Schmidt?” Someone coughed. Sloane turned his dark bright eyes upon Stoner. “Mr. Stoner, what does the sonnet mean?”

Stoner swallowed and tried to open his mouth.

“It is a sonnet, Mr. Stoner,” Sloane said dryly, “a poetical composition of fourteen lines, with a certain pattern I am sure you have memorized. It is written in the English language, which I believe you have been speaking for some years. Its author is William Shakespeare, a poet who is dead, but who nevertheless occupies a position of some importance in the minds of a few.” He looked at Stoner for a moment more, and then his eyes went blank as they fixed unseeingly beyond the class. Without looking at his book he spoke the poem again; and his voice deepened and softened, as if the words and sounds and rhythms had for a moment become himself:

“That time of year thou mayst in me behold
When yellow leaves, or none, or few, do hang
Upon those boughs which shake against the cold,
Bare ruin’d choirs where late the sweet birds sang.
In me thou see’st the twilight of such day
As after sunset fadeth in the west;
Which by and by black night doth take away,
Death’s second self, that seals up all in rest.
In me thou see’st the glowing of such fire,
That on the ashes of his youth doth lie,
As the death-bed whereon it must expire,
Consumed with that which it was nourisht by.
This thou perceivest, which makes thy love more strong,
To love that well which thou must leave ere long.”

In a moment of silence, someone cleared his throat. Sloane repeated the lines, his voice becoming flat, his own again.

“This thou perceivest, which makes thy love more strong,
To love that well which thou must leave ere long.”

Sloane’s eyes came back to William Stoner, and he said dryly, “Mr. Shakespeare speaks to you across three hundred years, Mr. Stoner; do you hear him?” ( Read more... )

теорема о неполноте через машины тьюринга

(эта запись может быть интересна тем, кто интересуется логикой и компьютерными науками)

В книге Скотта Ааронсона, которую я продолжаю читать, мне понравилось описание хорошего доказательства теоремы Геделя о неполноте с помощью машин Тьюринга. Подробно это доказательство описывалось в блоге Ааронсона пару лет назад, но тогда, я видимо, упустил его или не обратил внимания.

Теорема о неполноте утверждает, как известно, что любая непротиворечивая формальная система аксиом T, способная выражать утверждения о натуральных числах, и достаточно мощная, чтобы доказать определенные простые арифметические факты, обязательно неполна - есть такие утверждения о натуральных числах, которые она не может доказать, ни опровергнуть.

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

Предположим, что формальная система T, кроме указанных выше условий, еще и корректна - т.е. она доказывает только истинные утверждения о натуральных числах. Тогда мы можем доказать, что T неполна, с помощью проблемы остановки. Действительно, предположим, что T полна, т.е. любое утверждение она либо доказывает, либо опровергает (доказывает его отрицание). Построим алгоритм решения проблемы остановки следующим образом. Если нам дана машина M и входные данные X, мы можем сформулировать и записать на языке арифметики утверждение P = "машина M рано или поздно остановится, если запустить ее с данными X" (нам для этого нужно придумать способ представлять описание машины M и данных X в виде натуральных чисел, но это легко - и в курсе теории вычислимости, когда изучают машины Тьюринга, и так делается). Будем перебирать все возможные доказательства в системе T, по возрастанию длины, ища доказательство или опровержение P. Согласно предположению о полноте, рано или поздно мы одно из них найдем. Но поскольку T доказывает только истинные факты, то ее доказательство (или опровержение) P означает, что M действительно останавливается (или не останавливается) на X, т.е. наш алгоритм решил проблему остановки.

Это один из самых простых и элегантных способов доказать теорему Геделя о неполноте (особенно для студентов, уже знающих про машины Тьюринга), но у него есть один серьезный недостаток: он требует условия корректности T. Хотя обычные системы аксиом арифметики, как, например, аксиомы Пеано, несомненно корректны, теорема Геделя в общей ее формулировке требует лишь непротиворечивости T, гораздо более слабого условия, и это бывает весьма полезным. Я думал, что в таком подходе к доказательству теоремы Геделя - через машины Тьюринга - это ограничение неизбежно, а запись Ааронсона показывает, что это совсем не так, и что довольно просто перекроить доказательство так, чтобы оно не требовало корректности T. Вот краткое описание этого доказательства.

Мы будем рассматривать машины Тьюринга, которые, останавливаясь, дают результат "да" или "нет" (а также могут никогда не остановиться, конечно). Вместо корректности в доказательстве Ааронсона нам нужны от системы аксиом T лишь непротиворечивость, а также достаточная мощность, чтобы не просто иметь возможность формулировать утверждения о машинах Тьюринга, но и доказывать все истинные утверждения вида "машина M останавливается на входных данных X за Y шагов и говорит да", или "... и говорит нет". Это очень слабое требование, потому что если это утверждение истинно, т.е. это действительно так, она останавливается за Y шагов, то можно выписать последовательные состояния машины после каждого шага, и написать длинное утверждение, которое проверяет, что эта последовательность шагов действительно описывает запуск машины M, действительно останавливается в конце, действительно говорит да. Все это будут простые арифметические отношения между конкретными числами (кодами машин и состояний), поэтому достаточно мощная система T - такой мощи, какая обычно требуется для теоремы о неполноте в любом случае - сможет их доказать.

Из этого условия также следует, что T доказывает любое истинное утверждение вида "M останавливается на X и говорит да/нет", потому что если оно истинно, то есть какое-то число шагов Y, за которые она останавливается, и T доказывает утверждение про конкретное число шагов Y, а более общее сразу из него следует. Если P - истинное утверждение такого вида, то T доказывает P, и следовательно не может доказать не-P, потому что T непротиворечива (но заметим, что хотя не-P - пример ложного утверждения, которое T не доказывает, у нас нет общего ограничения корректности: T может доказывать всякие другие ложные утверждения других видов).

Теперь сформулируем проблему "угадай ответ", похожую на проблему остановки. Это следующая задача: пусть нам дают описание машины M, и входных данных X. Мы обязуемся всегда остановиться за конечное время, и если M на X отвечает да, то мы обязуемся ответить да; если М на X отвечает нет, то мы обязуемся ответить нет; а если M на X не останавливается, мы можем сказать хоть да, хоть нет (но остановиться и что-то сказать обязаны!).

Хотя эта проблема кажется менее полезной, чем проблема остановки, легко видеть, что она тоже не поддается решению; доказательство очень похоже на доказательство неразрешимости проблемы остановки, см. подробности в записи Ааронсона.

Осталось описать, как с помощью формальной системы T, если она полна, решить проблему "угадай ответ". Нам дают M и X; мы перебираем все возможные доказательства в T, ища доказательство или опровержение утверждения P = "М останавливается на X и говорит да". Если находит доказательство, отвечает "да", если опровержение, "нет". Поскольку T полна, либо доказательство, либо опровержение мы найдем, так что наш алгоритм всегда остановится. Если M на самом деле останавливается на X и говорит да, то T доказывает это истинное утверждение, согласно нашему условию, и не может его опровергать (ввиду непротиворечивости), поэтому мы остановимся и скажем "да". Если M на самом деле останавливается на X и говорит нет, то утверждение "М останаливается на X и говорит да" ложно, и T не может доказать ложное утверждение такого вида, поэтому наш алгоритм неизбежно ответит "нет". Ну а если M не останавливается, то я не знаю, что мы ответим, но мне неважно, главное, что сами точно остановимся из-за полноты T. Вот мы и решили проблему "угадай ответ", в точности по ее определению.

ночные стихи

Александр Пушкин

ВОСПОМИНАНИЕ

Когда для смертного умолкнет шумный день,
         И на немые стогны града
Полупрозрачная наляжет ночи тень
         И сон, дневных трудов награда,
В то время для меня влачатся в тишине
         Часы томительного бденья:
В бездействии ночном живей горят во мне
         Змеи сердечной угрызенья;
Мечты кипят; в уме, подавленном тоской,
         Теснится тяжких дум избыток;
Воспоминание безмолвно предо мной
         Свой длинный развивает свиток;
И с отвращением читая жизнь мою,
         Я трепещу и проклинаю,
И горько жалуюсь, и горько слезы лью,
         Но строк печальных не смываю.

1828

открытая запись

В комментах к этой Открытой Записи приветствуются любые темы, любые комменты, любые вопросы, любые ответы, любые дискуссии.

Давайте поговорим о чем-нибудь.