← All posts tagged math

anton0xf
Java math dev fp tl:dr: Монада — это враппер с возможностью оперировать над завёрнутым значением. Если вы пишете на Java то уже наверняка знаете, что это. Никакой магии или скрытых смыслов.

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

java.util.Optional — это натурально монада. Как стримы и любой другой враппер, если к нему прицепить метод flatMap() с поведением, как у соответствующих методов Optional или Stream.

Раскрою на примере того самого Optional. Как пишут в вики монада `M` над типом `T` (пишут `M T`) — это тройка, состоящая из
1. конструктора типа (`M T`), т.е. например `Optional<T>`
2. конвертера `unit: T -> M T`. Напомню, что в стандартной математической нотации `f: X -> Y` — это функция из `X` в `Y`. Для моего примера это будет создание Optional из значения, т.е. в той же нотации: `Optional::<T>of : T -> Optional<T>`
3. и комбинатора `(>>=): (M T, T → M U) → M U`, т.е. функа, который употребляет монаду и другой функ, который из значения, в неё завернутого, делает другое значение, завёрнутое в эту же монаду, и применяет второе к содержимому первой. Т.е. в точности то, что делает Optional::flatMap, если понимать объект, у которого этот метод вызывается, как неявный первый аргумент. Точнее если у нас есть `x : Optional<T>` (переменная `x` типа `Optional<T>`), то `x::<U>flatMap : (T -> Optional<U>) -> Optional<U>` (или как пишут в javadoc: `Optional<U> flatMap​(Function<? super T,​? extends Optional<? extends U>> mapper)`), что отличается от сигнатуры в определении только тем, что `x` — это неявный параметр, поэтому его тип e у меня написан отдельно, но это исключительно синтаксическая особенность — в том же Python этот аргумент пишется в сигнатуре методов явно.

Ну а "законы" — это абсолютно тривиальные ожидаемые от врапера свойства:
+ `unit(x) >>= f <-> f(x)` — означает что flatMap() применяет свой аргумент с завёрнутому значению, а не делает что-то более хитрое: `Optional.of(x).flatMap(f) == f(x)`
+ `ma >>= unit <-> ma` — если есть переменная `x : Optional<T>`, то примерение `flatMap()` к `Optional::of` ничего не поменяет: `x.flatMap(Optional::of) == x`
+ `ma >>= λx → (f(x) >>= g) <-> (ma >>= f) >>= g` — некое правило ассоциативности применения `flatMap()`, т.е. если `x : Optional<T>`, и `f: T -> Optional<U>`, а `g: U -> Optional<V>`, то `x.flatMap(x -> f(x).flatMap(g)) == x.flatMap(f).flatMap(g)`
anton0xf
math Coq Читаю Coq'Art. Доказал только что очередной (достаточно очевидный) факт, и внезапно захотелось поделиться и успехом (это было не очень просто), и мыслями на тему. А за одно решил обновить бложек на blogger. А чтобы не править по 10 раз для разных мест то тут просто оставлю ссылку. Поэтому под кат — это сюда
anton0xf
math ? Хочу "mathematical logic done right", так сказать.
Посоветуйте, что бы такого почитать по математической логике с максимально последовательным изложением (не было зависимостей от того, что будет дальше) и минимальным бутстрапом от интуиции к формальным или формализуемым доказательствам и строгим определениям. Лучше по-русски, но по-английски тоже можно.
А то порекомендовали почитать для начала это, а там изложение начинается с наивного (канторовского) определения множества (которое, и не определение вовсе), и на его основе определяются бинарные отношения, функции и их свойств, а второе же упражнение в книге (после описанных выше 3х страниц текста): "образуют ли бинарные отношения на множестве А группу относительно операций композиции и взятия обратного?", что, имхо, не дело. Мало того, что понятие "группа" не определено (ну да и чёрт бы с ним), так не описано ни как правильно строить рассуждения, ни что такое множество и пр..
У меня пока нагуглились только монографии Клини, Чёрча и Гильберта + книга Хаскелла Карри (того самого, да) 1969го года издания (в ужасном качестве и без возможности купить бумажную).
anton0xf
math ? во. я таки придумал годную формулировку для задачи, которую решаю (вроде-как придумал алгоритм, но доказательства нет):
есть "револьвер" с m-патронным барабаном. как зарядить его n пулями так, чтобы минимизировать максимальное число нажатий на курок между выстрелами, независимо от начального положения барабана?
т.е. максимальное число нажатий вычисляется среди всех (m) возможных начальных положений барабана.
anton0xf
math ? делим m на n на цело: m = k*n + r, r<n (все числа целые неотрицательные m >= n)
вопрос: соответствует ли вычисление h:
h = (n-k < r) ? k+1 : k
какому либо из известных способов округления?
собственно, похоже, что нет.
но может кто-то встречал что-то похожее раньше? ничего не напоминает?
anton0xf
math dev work ? programming есть датчик, выдает вещественные значения. выдает он их часто и значения меняются (как правило) мало, но собирается их много. изредка происходят (услоно мгновенные) скачки, после которых все тоже довольно гладко (в пределах погрешности измерения и всяких шумов).
anton0xf
quiz math programming в очень длинном тексте требуется заменить все буквы "a" на буквы "b", а все "b" — на "a", используя текстовый редактор, который позволяет заменить все вхождения одного произвольного набора символов на другой. Например, замена "bb"->"aCbb" переведёт строку "bbbbbD" в "aCbbaCbbbD". Как ему выполнить задачу с минимальным числом последовательных замен?
anton0xf
graphs math ? programming а как правильно искать все минимальные s-t пути во взвешенном орграфе с неотрицательными весами?
я, правда, изобрел что-то сложное: поиск в ширину в обратном направлении (от t) с переходами (против направления дуги соотв.) только по дугам с весом равным разности между длинами кратчайших путей (от s) до текущей и следующей (которая на другом конце дуги) вершин. но конечно же ничего об этом методе доказывать даже не пытался.
anton0xf
graphs math ? programming есть реализация алгоритма Форда-Фалкерсона. внезапно оказалось, что нужен еще и минимальный разрез. как его лучше искать?
(знание максимального потока, вроде как должно бы помочь, только не соображу как)