Category: наука

Category was added automatically. Read all entries about "наука".

moose, transparent

хочу все знать: велосипед

С этим велосипедом что-то не так. Есть некий серьезный дефект, который помешает на нем ехать. Видите ли вы, что?

(я увидел далеко не сразу)



Не читайте дальше, если хотите сами догадаться.

...
...
...
...
[Не хватает вот чего]
Не хватает части рамы: параллельных труб, которые идут от оси педалей к заднему колесу. Эти трубы называют по-русски "нижние перья" а по-английски "chain stays".


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

Теперь у меня есть вопрос: а что действительно будет, если сесть на велосипед, как он изображен здесь, и попробовать поехать?

Мое предположение - это что рама сломается, в том месте, где "верхние перья" ("seat stays") соединяются с трубой, на которой расположено сиденье. Я прав или нет? И если я прав: это случится обязательно при первой же попытке поехать, или скажем можно сделать трубы из такого прочного сплава, что даже без этой части можно ехать нормально?

Верно ли, что давление/напряжение в месте соединений труб можно с высокой точностью рассчитать аналитически как для такой странной конфигурации, так и для "нормальной" рамы, и сравнив с известными свойствами сплавов, ответить на мой предыдущий вопрос? Верно ли, что "сопромат" это та область инженерной науки, которая занимается всем этим делом? Можно ли просто, на пальцах объяснить, почему именно отсутствие этой части делает конструкцию нестабильной (интуитивно это "понятно", но что именно надо сказать на уровне сила-растяжение-сжатие, мне не вполне ясно)?

Спасибо!
moose, transparent

писатели-эмигранты

О знании писателями-эмигрантами языков стран проживания.

"Мария Васильевна [Розанова] французского не знает, и Синявский тоже не знал. При этом как-то мы с ней зашли в магазин, в отдел, где кастрюльки продают, и продавщица ее что-то спрашивает, она отвечает, мы выходим оттуда, я говорю: «Как же вы говорите, что не знаете язык, вы же сейчас разговаривали!». Она отвечает: «Нет, я просто понимаю, о чем она меня спрашивает, я у нее кастрюльку купила в прошлый раз». Но надо было видеть, как она там на рынке покупает мясо, как ее уважают мясники! (А французские мясники на рынке — это отдельная статья! Такие специалисты! Как они советуют, отрезают, заворачивают!) Но французского она не знает…
— То есть внутренне они себя чувствовали живущими в России?
— Ну конечно! Там все просто завалено, заставлено русскими книжками".

Далее из обсуждения у Светланы Мироновой.

Александр Бондарев: "Подтверждаю: не знали и не пытались. Кстати, точно так же вёл себя и основной идеологический противник четы Синявских в русской эмиграции — В.Е.Максимов, гл.ред. «Континента». Он считал, что знание иностранного языка русскоязычному писателю только мешает."

Наталия Рубинштейн: "Французского она [Розанова] действительно не знала, но очень лихо справлялась в кафе, в магазине, на рынке. Это называлось "Марья-полиглотка": " дё кафе, анкор дё кафе" и т.п. Раз в ворота постучали, француз что-то предлагал ей, она взяла его за руку и отвела в сад. Он посмотрел, принес лестницу, гигантские ножницы, некую электрическую машину и стал подстригать деревья. Я спросила, как она поняла его. - "А так. Я же видела, как он у соседей деревья стриг." Синявский же, вернувшись из Сорбонны, подробно пересказывал за столом весь ход Учёного совета, кто что сказал, какие перемены и что из чего следует. Держу пари, что Учёный совет не переходил для него на русский язык. Он учил французский и в школе, и в университете, сдавал кандидатский минимум. Читал все университетские бумаги. Но ему нестерпимо было при его перфекционизме мириться с несовершенством собственной французской речи. И он делал вид, что и трёх слов связать не может по-французски."

Знал ли Солженицын английский язык, вдруг стало интересно?

Были ли писатели-эмигранты, прожившие в Израиле много лет с нулевым знанием иврита?

Есть ли еще интересные примеры такого?
moose, transparent

теорема геделя по-английски

В продолжение записи "Теорема Геделя на коленке".

Для тех, кого интересует эта тема: я написал это доказательство также по-английски, и добавил к нему длинное предисловие о том, чем это доказательство интересно (ведь можно доказать неполноту через проблему остановки еще быстрее и проще). Если вкратце, то оно интересно тем, что в отличие от обычных "алгоритмических" доказательств теоремы Геделя, сохраняет лучшие свойства подхода Россера: минимальные требования к теории T, всего лишь непротиворечимость, и конструктивное построение утверждения, которое T не доказывает и не опровергает. При этом оно намного проще технически и понятнее концептуально, чем традиционное доказательство, с его "диагональной леммой" и "трюком Россера".

Поправки, замечания и вопросы принимаются, конечно же.
moose, transparent

теорема геделя на коленке

Вот набросок простого и элегантного, на мой взгляд, подхода к доказательству знаменитой теоремы Гёделя о неполноте. Мы стремимся доказать, что любая достаточно мощная непротиворечивая формальная теория T (т.е. набор аксиом, из которых мы, пользуясь логикой, доказываем теоремы), неизбежно неполна: есть такое утверждение S, что T не доказывает ни S, ни его отрицание not-S.

Сначала небольшое вступление. Представим все возможные утверждения о чем угодно - о числах, о геометрии, о любых объектах, о которых можно рассуждать логически. Если мы хотим найти доказательства многих из них, нам нужно начать с каких-то аксиом (скажем, "2+2=4" и другие в том же духе, если мы хотим доказывать что-то про числа, ту же теорему Ферма). Представьте, что мы строим теорию T, добавляя к ней аксиому за аксиомой. Каждый раз, когда мы добавили новую аксиому, сразу много новых утверждений S, которые до этого были вне досягаемости, становятся внезапно доказуемыми. Но нам недостаточно, мы добавляем еще и еще аксиомы, и каждый раз "захватываем" много новых теорем S. Однако, если мы слишком пожадничаем, в какой-то момент мы сможем доказать слишком много - и какое-то S, и его отрицание not-S. Это будет означать, что мы дошли до противоречия: наша теория Т стала противоречивой (или "неконсистентной"). Противоречивая теория доказывает вообще все, что угодно - любую истину и любую ложь - и поэтому ни на что не годна. Этого мы не хотим. Однако можно надеяться, что если мы подберем, умно и тщательно, правильные аксиомы, то мы сможем "захватить" максимум: для любого утверждения S мы докажем либо S, либо not-S. По каждому возможному вопросу S наша теория T будет "иметь свое мнение": либо согласна - доказала S - либо не согласна - "опровергла" S, то есть доказала его отрицание.

Гедель в 1931 году доказал, что этот идеал в принципе недостижим. По мере того, как мы добавляем аксиомы в T, после того, как мы переходим определенный порог способности T доказывать интересные утверждения, она становится неизбежно неполной: всегда будут такие S, что мы не сможем доказать ни S, ни not-S, сколько бы мы ни гнались и не добавляли новых аксиом.

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

Теперь набросок доказательства, которое использует понятие алгоритма или программы (но уметь программировать не нужно, чтобы его понять). Сначала надо сформулировать, что значит "переходим определенный порог способности T", туманно написанное выше. Возьмем любую программу P, которая запускается с входными данными I, работает какое-то время, заканчивает работу и выдает выходные данные O. В такой ситуации мы требуем от нашей теории T способность доказать два вида утверждений:

- "P, запущенная на I, останавливается и выдает O"
- "неверно, что P, запущенная на I, останавливается и выдает O' ", для любого неправильного варианта выходных данных O', отличающегося от настоящего O.

Это не очень строгие требования, и очень легко построить формальные теории T, способные их выполнить. Тут есть всякие технические детали, которые мы опустим; например, если наша формальная теории T говорит "на языке" натуральных чисел, то нужно сначала придумать, как "кодировать" программы P и данные I или O с помощью чисел; и как именно определить на формальном языке утверждения, написанные выше. Но в целом это просто. Главная причина, если в двух словах, того, что это просто - это что если P действительно отработала на I и выдала O, можно представить доказательство этого факта, состоящее из подробного описания работы программы, шаг за шагом, от начала до конца. Тогда теория T всего лишь должна доказать, что это описание действительно отвечает всем правилам и заканчивается на O, и что не может быть другого описания, заканчивающегося на O', потому что оно должно будет разойтись на каком-то шаге от правильного описания, а как ему разойтись, если программа все та же P, данные все те же I, и программа делает строго свою работу шаг за шагом?

Итак, предположим, что формальная теория T умеет доказывать такие утверждения, и предположим, что она непротиворечива. Напишем программу P, которая делает следующую работу:

Получив входные данные I, программа P перебирает все возможные строки текста, начиная от пустой строки или одной буквы/одного символа, потом все строки из двух символов и так далее до бесконечности. Каждую строку она проверяет: является ли эта строка доказательством в теории T одного из двух утверждений:

- "программа I, запущенная на входных данных I, останавливается и выдает 1". Если программа P находит доказательство этого утверждения, она останавливается и выдает 0.

- not-"программа I, запущенная на входных данных I, останавливается и выдает 1", то есть отрицание предыдущего. Если P находит доказательство этого утверждения, она останавливается и выдает 1.

P ищет с помощью T ответ на вопрос "что будет, если программу I запустить и дать ей собственный исходный код, верно ли, что I тогда остановится и скажет "1"? Если T доказывает, что такое случится, то P выдает 0, если T доказывает обратное, то P выдает 1.

Теперь следите за руками. Что будет, если запустить программу P и дать ей как входные данные собственный код P? Тогда программа P будет искать доказательство утверждения "P, запущенная на P, останавливается и выдает 1", или его отрицания. Назовем это утверждение W. Программа P ищет доказательство W или not-W. Найдет ли она их?

- предположим, P найдет доказательство W. Тогда по определению P, она должна остановиться и выдать 0. Но мы знаем, что в таком случае - раз P в реальности выдает 0 - теория T должна доказывать "неверно, что P запущенная на P, выдает 1", а это как раз not-W. Выходит, что T противоречива, она доказывает и W и not-W, а мы предположили, что это не так. Значит, не может быть.
- предположим, P найдет доказательство not-W. Тогда по определению P, она должна остановиться и выдать 1, но тогда мы требуем от T уметь доказать "P, запущенная на P, выдает 1", а это W. Опять выходит, что T доказывает и W, и not-W, а этого не может быть.

Вывод: P не найдет ни доказательство W, ни доказательство not-W, и поэтому вообще не остановится (так и будет перебирать до бесконечности все более длинные строки текста). Это единственная возможность, исходя из того, что T непротиворечива. Но тогда T не доказывает ни W, ни not-W: если бы такое доказательство было, P бы наткнулась на него рано или поздно. Значит, мы доказали, что хотели: Т неполная теория, причем мы нашли конкретное утверждение W - его в принципе можно выписать, если захотеть, хотя оно будет очень длинное - которое T не может ни доказать, ни опровергнуть. Это значит, что наше доказательство "конструктивное", так говорят в математике, когда могут не просто доказать существование чего-то, но даже привести конкретный пример.

Всё.
moose, transparent

омерзительное доказательство

В теории чисел есть важная теорема под названием "Квадратичный закон взаимности". Как и многое другое в математике, его открыл Эйлер; как и многое другое в теории чисел, его доказал Гаусс, в 1801 году.

(если у вас есть два простых числа p и q, этот закон объясняет связь между "найдется целый квадрат, который дает p в остатке при делении на q" и "найдется целый квадрат, который дает q в остатке при делении на p", поэтому "взаимность")

Гаусс так полюбил этот закон, что придумал шесть разных его доказательств. То, которое он нашел первым - самое сложное и запутанное. Оно занимает пять страниц текста, в зависимости от чисел p и q рассматриваются восемь разных случаев, у многих из этих случаев есть под-случаи, а в одном особенно коварном случае один из под-случаев разбивается на четыре под-под-случая.

Кто-то пошутил и назвал его "доказательством методом математического омерзения".
moose, transparent

теорема о неполноте и проблема остановки

Наткнулся пару дней назад на интересную страницу на математическом stackexchange:

Computability viewpoint of Godel/Rosser's incompleteness theorem

Хорошо известно, что можно доказать теорему о неполноте Гёделя с помощью неразрешимости проблемы остановки, доказанной Тьюрингом (исторически это было в обратном порядке: теорема о неполноте в 1931-м, неразрешимость проблемы остановки в 1940-х).

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

Классическое доказательства Геделя накладывало дополнительное требование на формальную систему (так называемая омега-непротиворечивость); несколько лет спустя Россер нашел трюк, который позволил убрать его, и от системы кроме описанных выше условий требовалось только непротиворечивость. Я не знал, что есть естественный способ перевести трюк Россера на язык вычислимости. Стандартное доказательство Геделя использует предикат доказуемости, а его вычислительная версия использует проблему остановки. Доказательство Россера немного изменяет предикат доказуемости, а его вычислительная версия использует проблему угадывания, в которой требуется, при наличии программы P и входных данных X, угадать, какой ответ выводит P на X, если останавливается, но зато если не останавливается, можно ответить что угодно. Проблема угадывания тоже неразрешима. Это все подробно объясняется по ссылке выше.

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

Не уверен, что я вполне с этим согласен. Попробую немного развернуть эту мысль. В традиционном доказательств теоремы Геделя у нас есть формальная система, которая умеет доказывать утверждения о натуральных числах. Мы вводим "арифметизацию синтаксиса": кодирование числами переменных, логических символов, формул и наконец доказательств - и в результате этого технического процесса мы научили нашу формальную систему доказывать в некотором смысле "утверждения об утверждениях", и отсюда прямая дорога к автоферерентности.

Что происходит в доказательстве через вычислимость? Мы переходим из области логических утверждений в область алгоритмов. Вместо того, чтобы научить утверждения "говорить" об утверждениях, и найти автореферентное противоречие в виде логического утверждения (говорящего о себе), мы идем в обход:

1. учим утверждения говорить об алгоритмах (это та часть, что по ссылке называется "can reason about programs")
2. учим алгоритмы говорить об алгоритмах (это универсальная машина Тьюринга, например)
3. учим алгоритмы говорить об утверждениях (это та часть доказательства, где мы строим программу, перебирающую все возможные формальные доказательства).

Вместо одного обучения у нас три! Почему же это кажется более легким и естественным? Потому что 2 и 3 интуитивно верны для людей, знакомых с алгоритмами и интерпретаторами, и хотя формально говоря они требуют технических решений - как именно кодировать программу в виде последовательности символов? как именно кодировать утверждение в виде последовательности символов? - это ощущается (возможно, что справедливо) как мелкие и не очень важные подробности. А главная часть доказательства - автореферентное утверждение - полностью относится к алгоритмам, и там оно выглядит проще и понятнее, чем в применении к утверждениям (диагональная лемма Геделя итп.).

С другой стороны, все же надо отметить, что остается первое обучение - формальную систему надо научить доказывать и опровергать утверждения типа "вот вычисление, показывающее, что данный алгоритм останавливается при таких-то входных данных и дает такой-то результат". По ссылке выше это спрятано под невинно выглядящее название "can reason about programs", но по сути для любой конкретной формальной системы это не тяжелее и не проще, полагаю, чем научить ее арифметизации синтаксиса в первоначальной версии доказательства Геделя. По сути это одно и то же, только вместо "доказательства" мы рассматриваем "вычисление" итд. Так действительно ли это проще, доказывать через алгоритмы? Наверное, нет, если настаивать на полном строгом доказательстве, то то же самое или даже больше работы. Действительно ли это естественнее? Возможно, да - главный аргумент изолирован в области алгоритмов, где он кажется особенно простым и естественным. Но я не знаю, насколько верно, и даже осмысленно, говорить о том, что там его "настоящее место".
moose, transparent

рациональная геометрия

В аксиомах Эвклида нет ничего о непрерывности линий или кривых. Это значит, что можно представить "рациональную плоскость", состоящую только из точек с рациональными координатами, и все аксиомы на ней будут выполняться.

Казалось бы, на такой плоскости вообще не будет окружностей, но это обманчивое впечатление. Окружности вполне себе существуют, просто они часто проходят друг "сквозь" друга, не пересекаясь.

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

Их просто нет.
moose, transparent

наука рвется вперед

В 2011-м году я написал о потрясающей научной новости: математики научились умножать две матрицы размером n x n за время O(n2.373) вместо предыдущего рекорда O(n2.376). Этот результат был достигнут Вирджиней Вассилевская-Уильямс из Стэнфорда.

С тех пор я не возвращался к этой теме, а прогресс не стоял на месте! В 2012-м году Вассилевская-Уильямс улучшила свой результат до экспоненты 2.37288. В 2014-м гoду неожиданно ее обогнал француз Франсуа Ле Гал, доказав, что можно умножить за время n в степени 2.37287. И вот сейчас, буквально вчера!! - Вассилевская-Уильямс (теперь уже в МИТ, и с соавтором Джошом Альманом) опять вырвалась вперед, снизив экспоненту до рекордного и невероятного значения 2.37286.

А вы говорите - выборы, коронавирус... тут такое происходит. Страшно даже подумать, что будет дальше.
moose, transparent

анаграммы

"А. Шень искал два самых длинных слова в русском
языке, таких, чтобы одно было анаграммой другого.
Нашел слова австралопитек и ватерполистка
и с гордостью об этом рассказывал. Матфизик О., услышав
об этом, задумался. На другой день он позвонил Шеню
и сказал, что нашел пару еще длинней:
обезьяноводство и световодобоязнь.

Легенда гласит, что Шень написал программу, а его друг нашёл прямо в голове."

(из рассказа К.Америк в пересказе Ю.Фридман)