Category: наука

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

Book

SASE

Тут вопрос в том, что "нам", как новой геораспределённой cloud-first организации, нет смысла деплоить надёжное говно и палки из 2010. А вместо этого взять "свежие" предложения от "взрослых" вендоров (VMware и Cisco например). Которые будут созревать вместе с нами.

С кем можно об этом поговорить, и вообще, как о таких вещах надо начинать говорить? Потому что пока такой колоссальный разброс - либо у отвечающего слишком низкий уровень, рассуждает на совершенно начальном уровне, либо слишком высокий, и меня, как дурачьё посылают нахуй, "вот станешь таким большим, как я, тогда и поговорим". Ну или не слишком высокий, а просто дури и гонора очень много. В любом случае проблема коммуникации. Если в ЖЖ все умерли, то где они теперь? Или прямо вот на сайте vmware и писать?

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

Book

День прошёл в обновлениях

Как-то достался мне бесхозный роутер, на который добрый человек накатил DD-WRT, ну и я его приспособил раздавать мне в спальню вайфай, поскольку роутер из зала не достаёт. (Раздавать на телефон — рабочий комп подключен по меди, ну его нахуй — я как чувствительный к потерям и задержкам ещё не видел работоспособного вайфая на самом деле, какая-то нерабочая технология, я даже не требую там больше 10 мбит или менее 50 мс; но мы отвлеклись)

Вот этот роутер как-то упорно не хотел обновляться с одного билда дд-врт на другой. Ну я терпел-терпел, а сегодня терпение лопнуло (а точнее, не было настроения работать — но было настроение пострадать хуйнёй), и я таки пострадал.

Включил на роутере телнет, обновился через mtd write но с ошибкой, и роутер превратился в полукирпич. Нашёл в вики как его восстановить, но там как-то по-дебильному всё описано. В результате нашёл несколько видео на етубе, третье оказалось приемлемым, ну и вернул родную прошивку, а потом накатил дд-врт последний в надежде на то, что он чуть менее дырявый (родная прошивка от 2015 года, а ддврт на ядре 3.18, которое в EOL ушёл всего лишь год назад).

Человечьим языком процедура такова:

— Роутер включаем с зажатой кнопкой резета, после чего он переходит в режим восстановления

— В этом режиме он хочет вытянуть файлик по TFTP c 192.168.0.66

 — Ставим на этот адрес тфтп-сервак, смотрим в логе, какое имя файла роутер пытается вытянуть

— Переименовываем родную прошивку в это имя и кладём на TFTP

— Профит!!!111

Collapse )
Book

Новости перловодства-3

Вчера методом научного тыка обнаружил, что в рантайме нужны всего 6 из 17 созданных зависимостей.

Сегодня с утра при попытке найти что-то, что бы позволило мне отфильтровать зависимости автоматически, попробовал проинсталлировать Module-Depends и наткннулся на баг годичной давности, с патчем: https://rt.cpan.org/Public/Bug/Display.html?id=119324 Тьфу!

Но в результате использовал не его, а MetaCPAN-Client, который аж третья попытка написать эту либу, две прошлые задепрекейчены.

Применив скрипт к другим используемым мной либам, обнаружил и зарепортил баг в метаданных у Event-RPC: https://rt.cpan.org/Ticket/Display.html?id=125770

Добавляет педерастии то, что есть distributions, modules and packages. Packages это вообще невероятная хуета, не хочу даже начинать о неограниченных возможностях пидарасов по помещению более одного пакаджа в модуль и прочем говне. Если считать, что модули с пакаджами (которые выглядят одинаково, но есть контексты в которых это не одно и то же) мы не путаем - то остается возможность спутать модули с дистрибьюшенами. В результате "cpanp o" выдает список устаревших дистров, но делает вид, что выдает список устаревших модулей. То есть, для каждого дистра вместо имени пакаджа дистра он пишет имя "главного" модуля в нём. Ну и чтобы обновить модуль, надо делать обратный лукап из модуля в дистр. Тьфу!

Список установленных дистров получить не представляется возможным, на SO советуют использовать cpan -a (не путать с cpanp), внутри которого такое говно и палки, которое можно вывесить (выложить?) в палате мер и весов как пример вылизанного за годы говна на перле. Короче, тот способ энумерации дистров, который делает CPAN, применять нельзя просто потому что это кал. В-общем решил пока не энумерировать установленные дистры :)

Основная идея энумерации - посмотреть на то, какие зависимости устанавливаемого дистра стоят, но устарели. Чтобы можно было выбрать, обновлять их или нет.
Book

Унивалентность на кубических типах

https://github.com/mortberg/cubicaltt/tree/master/lectures (там же чекер на х-е) позволяет понять, как примерно будет выглядеть обещанное Воеводским счастье ("his vision of a foundational system for mathematics in which the basic objects are homotopy types, based on a type theory satisfying the univalence axiom, and formalized in a computer proof assistant")

Идея заключается в том, чтобы усилить identity type так, чтобы больше вещей можно было доказать "в одно действие" через аналог идрисовского replace (названный в лекциях subst):

replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

Для этого из гомосексуальных гомологических примитивов собирается тип Path X a b, играющий роль {X} -> (a: X) = (b: X), который можно населить:

- "рефлом", т.е. definitionally equal terms

refl (A : U) (a : A) : Path A a a

- экстенсионально равными функциями (версия для dependent product тоже есть)

funExtNonDep (A B: U) (f g : A -> B) (p : (x : A) -> Path B (f x) (g x)) : Path (A -> B) f g

- изоморфными типами (т.е. если у нас есть функция между значениями типов A и B с левой и правой обратной - то типы "равны"):

isoPath (A B : U) (f : A -> B) (g : B -> A)
      (s : (y : B) -> Path B (f (g y)) y)
      (t : (x : A) -> Path A (g (f x)) x) : Path U A B
Интересно, что всё это работает и с функциями уровня типов.

В результате можно написать такую функцию:
functor_transport (F G: U -> U) (p: Path (U -> U) F G) (f: functor F): functor G
  = subst (U -> U) functor F G p f
То есть, для изоморфных типов F и G (с кайндами * -> * в терминах х-я) по инстансу функтора для F можно родить инстанс для G, при этом тело и сигнатуры fmap и теоремы о соблюдении законов функтора переписываются "автомагически".

Ну а дальше оказывается, что изоморфизмы у нас повсеместно. Скажем, таплы у самоизоморфны - т.е. есть Path U (A, B) (B, A), ну и из (first, fst, functorForA) "в одно действие" получаются (second, snd, functorForB). А дальше из (first, fst, functorForA, second, snd, functorForB) "в одно действие" получается реализация 6 функций и док-во 4 теорем (1 ф-ция и 2 теоремы внутри functorA/B сидят) для пар в кодировках чёрча и остальных over 9000 возможных представлений пар.

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

Кроме того, есть техника метапрограммирования: есть изоморфизм bool самого с собой (через not). И мы можем написать функцию, автомагически заменяющую все булы в любом терме вида F bool на их отрицания (и функции что самое смешное тоже переписываются). Типа

data food = cheese | beef | chicken

-- Predicate encoding which food someone eats
eats (X : U) : U = list (and food X)

anders : eats bool = cons (cheese,true)
                    (cons (beef,false)
                    (cons (chicken,false) nil))

-- Cyril eats the complement of Anders
cyril : eats bool = substEquiv eats bool bool notEquiv anders
notEquiv тут как раз доказательство изоморфизма. Ну и понятно что заменяются не все вхождения Bool, а "все вхождения в позициях, отмеченных Х". Любопытно, что код ничего не знает о том как обходить списки - у нас нету fmap для eats :)

Дебильные комментарии, комментарии "практиков" и школьников - как обычно, скринятся. RTFM, do you homework, пиши развёрнуто и конструктивно! https://t.me/groupoid (но там банхаммер, так что лучше сюда)
Book

Contracts first

Тут из альтернативной вселенной сообщают, что завтипы говно и не нужны.

Вместо этого берете язык с простыми типами и контрактами в стиле Eiffel https://www.eiffel.com/values/design-by-contract/introduction/ и скармливаете статик ассерты в http://why3.lri.fr/#users которая дальше их скармливает пруверам из списка http://why3.lri.fr/#provers

Оно и в кок конечно умеет скармливать, но пруверы для конечных теорий (типа SMT FixedSizeBitVectors) по понятным причинам и работают лучше, и точнее моделируют машинное представление.
Book

Владимир Михайлович Бондарев | Официальный сайт ХНУРЭ

Владимир Михайлович Бондарев | Официальный сайт ХНУРЭ

Кандидат технических наук, профессор кафедры программной инженерии (ПИ) Харьковского национального университета радиоэлектроники (ХНУРЭ).

Posted by Andy Melnikov on 7 Mar 2017, 00:08

from Facebook
Book

Домики набигают

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

Людей и обычных роботов туда из-за нехватки размерности не пошлёшь, но удалось конструировать зонды прямо там. За годы исследований специалистам CERN и NASA удалось создать "там" путём квантовой телепортации состояния земных моноатомных плёнок 2д-нанозонды с 1д-камерой, примитивным интерпретатором и каналом связи.

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

Поскольку ресурсы Кольца всё же конечны, возникла необходимость придумать схему распределения ресурсов. Причём такую, чтобы с одной стороны, за мировой закулисой сохранялась значительная квота, а с другой стороны, использование этой квоты было неотлавливаемо через side channel attacks. Более того, даже само разглашение информации о Кольце должно быть оформлено как шутка и не то что не позволять вычислить местонахождение Кольца, но полностью слить реальность с вымыслом. В-общем, plausible (crypto)deniability all way down.

В следующем выпуске вы узнаете:
- какое отношение контроль мировой закулисы над GHC имеет к квантовой телепортации в двумерные многообразия
- какое отношение тот факт, что закрытие правительством SilkRoad якобы не выявило уязвимостей ни в Tor, ни в Bitcoin, имеет к стримингу 1d-видео

Следите за апдейтами.
Book

Фикспоинт всюду срёт

Посмотрел я на литературу по теме отказа от индукции.

При использовании индукции доказательства получаются короткими, но их нереально найти компьютером. Поэтому есть ACL2 (Boyer-Moore family), который почти в одиночку пытается искать индуктивные доказательства перебором, и все остальные.

Все остальные делятся на индуктивные MLTT-пруверы, неиндуктивные SMT-солверы и нетипизированные пруверы а ля Isabelle (LCF family). MLTT бывают полуавтоматические и ручные. SMT-солверов ручных я не видел.

При отказе от индукции и заодно от PA часто получается даже полная decision procedure в NP. Но доказательства становятся очень длинными и их часто даже не пытаются печатать, не то что составлять руками. Тем не менее попытки что-то достать из солвера и независимо проверить существуют.

Индустрия (aerospace, automotive, transportation, medical, telecom, business information) забила на MLTT, случаи верификации чего-то на Coq на фоне общих усилий по формализации разработки выглядят как "а давайте для смеху". Все пользуют модел-чекеры (которые архитектурно являются специализированными SMT-солверами). Кроме того сертификация идёт путём refinement - т.е. верифицируют не полные требования, а от фонаря дописывают инварианты в надежде что солвер их подтвердит. Ну и в процессе обнаруживают достаточное кол-во багов, разумеется. Короче, гарантии в результате получаются довольно смешными, сплошные звёздочки и мелкий шрифт.

Что в этой связи делать? А хез. Слабых типизированных теорий с короткими доказательствами, которые можно искать полуавтоматически, я не видел пока.

P.S. Идея, что типичный математический аппарат не годится для CS из-за того что разработан был для решения проблем с бесконечностями, и нужно что-то особое, является довольно распространённый. Хороших решений нет, но есть например finite model theory. Но там всё равно общие слова - по сути, если запретить бесконечные модели, пропадает много полезных (математикам, не в разрезе народного хозяйства) свойств.
Book

Автоподбор параметров

Пилим тут https://github.com/streamcode9/node-discrete-spsa

An implementation of the Discrete Simultaneous Perturbation Stochastic Aproximation algorithm.

See Stacy D. Hill, "Discrete Stochastic Approximation with Application to Resource Allocation", 2005 http://www.jhuapl.edu/SPSA/PDF-SPSA/Hill_TechDig05.pdf

Cам алгоритм на 5-й странице step1-5, прост как палка.

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

Это всё равно бесконечная игра с подбором learning rate, но наверное получше будет, чем наивный подход "просемплировать всё пространство состояний с заданным шагом, используя статистически значимые бенчмарки".

Трюк в том, что вместо рассчёта градиента через частные производные, которые приближаем конечными разностями, используем 1-мерную конечную разность в случайном направлении. Которая, о чудо, оказывается (несмещённой статистической) оценкой градиента. И при этом требует вычислить целевую функцию всего 2 раза на итерацию, вместо стольки раз, сколько у нас частных производных + 1.

Вдобавок, оно работает нормально для зашумлённых целевых функций. Т.е. рандомность бенчмарков устранять не надо. И даже в случае целочисленных параметров и пространства разрешённых состояний произвольной формы (ну может почти произвольной, я в детали не вникал).