функция маккарти (немного математики)

Мне раньше не встречалась эта забавная функция.

Определение (рекурсивное):

• g(x) = x-10 если x > 100
• g(x) = g(g(x+11)) если x <= 100

g(x) называется 91-функцией Маккарти. Поведение g(x) для x>100 тривиально, как следует из первой строки определения; поведение для x<=100 на первый взгляд неочевидно.

Доказать: g(x)=91 для x<=101.

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

к происхождению версипеля

В рассылке набоковедов в очередной раз обсуждают сочиненное им слово versipel. Это из Бледного пламени (Pale Fire):

You drive me to the library. We dine
At half past six. And that odd muse of mine,
My versipel, is with me everywhere,
In carrel and in car, and in my chair.

Что можно добавить к их ученому спору? Только то, что versipel, муза Набокова - сурок, как свидетельствует Лев Рубинштейн:

А это я.
А это я в трусах и в майке.
А это я в трусах и в майке под одеялом с головой.
А это я в трусах и в майке под одеялом с головой бегу по солнечной лужайке.
А это я в трусах и в майке под одеялом с головой бегу по солнечной лужайке, и мой сурок со мной.
И мой сурок со мной.
Уходит.

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

По разным странам я бродил
И мой сурок со мною,
И весел я, и счастлив был,
И мой сурок со мною!

И мой всегда, и мой везде,
И мой сурок со мною.
И мой всегда, и мой везде,
И мой сурок со мною.

Песенка эта - перевод стихов Гете - пелась под ту же музыку, на которую эти стихи положил Бетховен. В стишке Гете немецкие строки чередуются с французским рефреном. Я цитирую только первый куплет с припевом, есть еще несколько.

Ich komme schon durch manche Land,
avecque la marmotte.
Und immer was zu essen fand,
avecque la marmotte.

Avecque si, avecque la,
avecque la marmotte.
Avecque si, avecque la,
avecque la marmotte.

Иногда пишут "avec que la marmotte", но это искажение - на самом деле это именно avecque, оно же avec, просто когда-то его так писали.

мимоходом

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

Пришелец номер раз: Ну что, как еще мы можем над ними поиздеваться?

Пришелец номер два: Давай старое-доброе - заставим их пить какую-то невероятную дрянь и нахваливать.

Номер 1: Я думал, что тут все возможности уже исчерпаны. Как мы можем надеяться превзойти такие триумфы, как Diet Pepsi и 7-Up?

Номер 2: У меня есть идея... только не смейся. Не, серьезно, пообещай, что не будешь смеяться. Короче, такая мысль... Кофе. без. кофеина.

опять только программистам будет интересно

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

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

Изучение Лиспа очень хорошо продвигается, по главе в день - знаю теперь, например, зачем нужны макросы и как они работают. На днях попробую что-нибудь написать.

Листая наугад старые заметки Дейкстры, обнаружил алгоритмическую задачку, которая помогла размять мозги немного. Для тех, кому интересно, перескажу условие под катом. ( Read more... )

вам, израильтяне

Большая иерусалимская развиртуализация через полторы недели. Отмечайтесь там, приезжайте и приходите. Насчет нас еще не знаю, если сможем - придем.

о доказательствах

В одной из своих замечательных заметок (англ., PDF) Дейкстра протестует против, по его мнению, вредного и приводящего к путанице понятия косвенного доказательства. Если, желая доказать A--->B (из A следует B), мы начинаем с предположения "не-B", и доказываем исходя из этого "не-A", это называется косвенным доказательством (в отличие от прямого доказательства, когда мы предполагаем A и доказываем B напрямую).

Дейкстра считает, что разделять эти два метода - нелепо, и они есть одно и то же. Действительно, с точки зрения чистой логики утверждения A--->B и (не-B)--->(не-A) совершенно эквивалентны, и доказать одно означает доказать другое. Собственно, они оба тождественно утверждению "не-A или B", которое Дейкстра предлагает считать более фундаментальным, чем обе эти версии.

Дейкстра неправ. Математики не просто так и не из соображений устаревшей терминологии называют некоторые доказательства прямыми, а другие - косвенными. Несмотря на формальную тождественность, между ними есть существенная разница с точки зрения математической практики. Но как это продемонстрировать?

Обратимся к еще одному примеру вредной терминологии с точки зрения Дейкстры, тесно связанному с только что упомянутым. Принцип математической индукции можно сформулировать следующим образом: если мы хотим доказать какой-то предикат (какое-то свойство) P(x) для любого натурального числа x (x = 0, 1, 2, ...), то нам достаточно доказать следующее: из того, что P выполняется для всех y меньше x, следует, что P выполняется для x. В символьном виде (∀x читается "для каждого икс...", а ∃x - "существует икс такой, что...", и эти два символа называются кванторами общности и существования): (∀y)(y<x ---> P(y)) ---> P(x). Еще раз словами: если для любого y верно, что из того, что y меньше x следует истинность P(y), тогда верно и P(x). Если мы докажем это, то принцип математической индукции гласит, что мы доказали P(x) для любого x.

(более привычная формулировка индукции, когда переходят от P(n) к P(n+1), является частным и несколько более слабым вариантом. В более общей формулировке, приведенной выше, для доказательства P(n+1) нам разрешено пользоваться не только доказанностью для предыдущего числа, P(n), но и для всех чисел, уже доказанных до сих пор, начиная с 0 - переменная y как раз и пробегает весь их список).

С другой стороны, принцип бесконечного спуска - приоритет сознательного и плодотворного его использования принадлежит Ферма - является вариантом принципа математической индукции, хоть это может и не быть очевидным заранее. ( как это увидеть? )

Таким образом, с точки зрения чистой логики два этих принципа совершенно тождественны, подобно тому, как тождественны "прямое" доказательство A → B и "косвенное" ¬B → ¬A. Исходя из этого факта, Дейкстра протестует против того, чтобы вообще считать принцип бесконечного спуска отдельным принципом, и хвалить того же Ферма за блестящее его применение. Ведь он совершенно эквивалентен индукции, и ничего нового или интересного в нем нет; любое доказательство, использующее его, можно представить в виде доказательства, использующего индукцию.

Дейкстра неправ. Математики не просто так используют разные названия, когда говорят об этих двух принципах. Хотя с точки зрения формальной логики они и тождественны, есть доказательства, "естественным" образом использующие индукцию, а есть доказательства, "естественным" образом использующие принцип бесконечного спуска. Но что это значит - "естественным образом", и как это продемонстрировать?

Об этом - через час-два в следующей записи :)