На днях оповещения от ЖЖ перестали приходить мне на почту (у кого-нибудь еще такое наблюдается? Upd: разобрался, проблема была в настройках моего сервера), заглянул в список сообщений тут на сайте, внезапно увидел персональное сообщение, которое было отправлено 2 месяца назад, но ЖЖ счел его подозрительным и на почту не продублировал.

Чтобы такого впредь не случалось, всем, кому это может понадобиться, сообщаю: мне можно (и лучше) писать на info@ мой ник тут .com.

(написано в марте 2015, пост поднят вверх для заметности)

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



Это Хокинг расстарался в свое время.

Давно хотел сам пронаблюдать. А тут попалась в руки лазерная указка. Берем такую указку, берем один волос со своей головы, светим на стену в полуметре-метре от себя, ставим перед указкой волосок. До/после:

Вот они, обещанные волновой природой света пятнышки!

Еще интересный эффект на камере, когда пятно от лазера близко к центру кадра:

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

Обнаружил вдруг самый лучший ТВ-канал, ради которого можно прям и плазму купить, на стену повесить и крутить там круглосуточно, вместо окна. Live feed from ISS:
https://www.youtube.com/watch?v=RtU_mdL2vBM
Не знаю, сколько там действительно live, а сколько записи, как ни загляну, там все кто-то на морозе шастает, вышел вакуумом подышать. Но зрелище завораживает.

А вот еще случай был. Программа генерит длинную последовательность неких значений (phase_1), и поблочно эти значения потом как-то дальше обрабатываются (phase_2), производя добро (PROFIT!). И надо бы это делать побыстрее. Пришла очевидная мысль это дело распараллелить: пока phase_2 обрабатывает первый блок данных от phase_1, в это время phase_1 может уже параллельно создавать следующий блок, и так далее, блок N обрабатывается параллельно созданию блока N+1. В каждый момент времени в памяти лишь два блока - генерируемый и обрабатываемый. Завел для них два массива: то пишем в первый, читаем из второго, то наоборот.

std::vector<Freq> ranges[2];

При этом phase_1 что-то пишет в один из массивов через push_back, а обработка блока в phase_2 выглядела как-то так:

BYTE* writeBlock(const std::vector<Freq> &ranges, BYTE *dst) {
    ...
    for(int i=ranges.size()-1; i>=0; i--) {
        ... // use ranges[i]
    }    
    ...
}

До распараллеливания phase_1 занимал по времени 12 попугаев, phase_2 - 13 попугаев, всего 25. Запускаю новый распараллеленный вариант и вдруг вижу, что общее время стало аж 41 попугай. Вместо ускорения получил замедление!
А теперь беру и меняю пару строк:

BYTE* writeBlockV(const std::vector<Freq> &rangesV, BYTE *dst) {
    ...
    const Freq * ranges = &rangesV[0];
    for(int i=rangesV.size()-1; i>=0; i--) {
        ... // use ranges[i]
    }
    ...
}

И общее время становится менее 15 попугаев, почти втрое быстрее! Т.е. в первом случае код в цикле каждый раз загружал указатель на данные в векторе, а этот указатель лежал в памяти рядом с длиной другого массива, которая менялась в другом потоке, так что два ядра тягали этот кусочек памяти туда-сюда: одно ядро туда пишет новую длину, второе ядро копирует изменившуюся кэш-линию, чтобы прочитать указатель по соседству. Из-за этих тяганий туда-сюда получается медленнее, чем если все делать в один поток. А стоило указатель на данные вектора унести в стек и перестать читать меняющуюся кэш-линию, как все заработало быстро, как и планировалось.
Причем безобразие такое только у интеловского компилятора. MSVC и GCC не перечитывают указатель и тяганий кэш-линий не устраивают, оба варианта кода работают с одинаковой скоростью. При этом с GCC время получается чуть менее 16 попугаев, а с MSVC - почти 33 (что все же быстрее непараллеленного варианта, где у MSVC 42 попугая).

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



(чуток подробностей от автора: https://youtu.be/-pqUbSvVhGQ?t=15m58s )

Замечательный диалог тут вышел с моим любимым Шоном Кэрроллом (14 минут видео):
https://www.closertotruth.com/series/physics-consciousness
Про сознание, корабль Тесея, его копирование, зомби и стоит ли мечтать об аплоаде сознания в сеть (спойлер: видимо, не стоит).
Кэрролл еще раньше высказывался, что в физике нет места сознанию, что вот мол есть уравнения стандартной модели и они отлично описывают все физические процессы, и если бы было что-то нематериальное/духовное, что могло бы как-то влиять на физический мир (шевелить вашими мускулами, например), то это бы прямо противоречило экспериментальным проверкам текущих физических теорий. А здесь рядом David Chalmers явно указывает, где именно сознание может в физике прятаться - грубо говоря, в редукции волновой функции. О том же говорил и Менский у Гордона, и многие другие вплоть до чуть ли не Шрёдингера. Хороших ответов ни у кого пока нет, но есть о чем поразмыслить.

Вот Идрис синтаксически очень похож на хаскель, однако не ленивый. В хаскеле ленивость-по-умолчанию сопровождается строгостью-по-запросу, добавшяешь перед полем значок ! и оно строгое. Оказывается, в Идрисе нынче есть симметричная штука: добавляешь перед типом поля волшебное слово Inf, и поле оказывается "ленивым": когда данные конструируются, выражение для вычисления этого поля не вычисляется сразу, а автоматически оборачивается в Delay (если явно поленился это сделать), а при паттерн-матчинге оно когда надо автоматически форсится через Force (т.е. механика практически как в окамле с ленивыми значениями, но вручную необязательно оборачивать и форсить, компилятор сам вставляет).
Например, через этот механизм сделан тип бесконечных последовательностей:

data Stream : Type -> Type where
(::) : (value : elem) -> Inf (Stream elem) -> Stream elem

Благодаря автоматическому расставлению делеев и форсов, код с такими коданными выглядит так же просто и чисто, как в хаскеле:

countFrom : Integer -> Stream Integer
countFrom x = x :: countFrom (x+1)

first : Nat -> Stream a -> List a
first Z xs = []
first (S k) (x :: xs) = x :: first k xs

prepend : List a -> Stream a -> Stream a
prepend [] ys = ys
prepend (x :: xs) ys = x :: prepend xs ys

Обратите внимание, что в функциях выше :: используется в паттерн-матчинге и в конструировании сразу и для списков и для стримов, компилятор сам по типу понимает где что, и для стримов вставляет delay/force.
Подобно Основной Теореме Арифметики и Основной Теореме Алгебры, есть Основная Теорема Функционального Программирования (это, по Карри-Говарду, конечно же тоже функция), ее можно записать так:

fibs : Stream Integer
fibs = 1 :: 1 :: zipWith (+) fibs (drop 1 fibs)

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

— Не пугайтесь, Екатерина Петровна, и не волнуйтесь. Только нет в мире никакого равновесия. И ошибка-то всего на какие-нибудь полтора килограмма на всю вселенную, а все же удивительно, Екатерина Петровна, совершенно удивительно!

This paper thoroughly analyzes three state-of-the-art, formally verified implementations of distributed systems: IronFleet (Dafny/C#), Verdi (Coq/OCaml), and Chapar (Coq/OCaml). Through code review and testing, we found a total of 16 bugs, many of which produce serious consequences, including crashing servers, returning incorrect results to clients, and invalidating verification guarantees.
https://homes.cs.washington.edu/~pfonseca/papers/eurosys2017-dsbugs.pdf
В протоколах и их доказанных реализациях багов не нашли, все баги были на границе взаимодействия верифицированного кода с жестоким внешним миром - неверифицированным окружением. Сложно описать формально все возможные косяки низкоуровневых библиотек и сторонних процессов. Смешной момент - Dafny для верификации использует Z3 солвер, если солвер невовремя прервать, Дафни считает, что все ок и считает недопроверенную программу годной.

А тут мужики нагенерили много тестовых программок для компиляторов:
In less than six months, our approach has led to 217 confirmed GCC/Clang bug reports, 119 of which have already been fixed ... In about three weeks, we have also found 29 CompCert crashing bugs, and 42 bugs in the production Scala compiler and the Dotty research compiler.
https://arxiv.org/pdf/1610.03148.pdf
GCC и Clang могут падать, а могут неправильный код генерить. CompCert (который на Coq'e верифицирован), как я понял, неправильный код не генерит, но вот сам падать может - ассерты срабатывают внутри, т.е. некоторая неконсистентность логическая там была.

Книжки перечитывать было лень, но внезапно посмотрел несколько публичных лекций Пенроуза на злосчастную тему (он там еще на вопросы отвечал). Краткий конспект, пока опять не забыл.

У него нет законченной, проработанной и/или доказанной теории или гипотезы. Есть лишь набор разрозненных мыслей разной степени строгости/оформленности, и он отлично это сознает и не скрывает.

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

В том, что касается ИИ, компьютеров и человеческого ума, на этом вобщем-то все. Только в этом состоит пенроузовская "невозможность" построения математического ума на тьюринговском вычислителе. Нейронные сети идут лесом, в том числе.

Дальше он уже начинает интересоваться, как это так человек умеет, и ( Read more...Collapse )

А, пользуясь случаем. Я лишь в прошлом году узнал, что у Пенроуза есть чудесная книжка The Road to Reality. Там нет ничего вот этого, а просто хороший обзор "вся физика в одной книжке" (у нее подзаголовок "A Complete Guide to the Laws of the Universe"). Рекомендую.