Comments 42
В компьютерах сливаются надежды на решение всех мыслимых и немыслимых проблем. Поэтому так манит мечта о том, чтобы найти универсальную концепцию - этакую теорию всего на свете, священный Грааль нашего времени. Но мы умеем только частные решения, и можем довольствоваться лишь тем, чтобы смотреть на проблему с разных сторон, а не внутрь, не в самую суть как бы хотелось.
У меня есть ощущение, что в компьютерах сливаются три разные дисциплины:
Формальная теория вычислений (одним концом утыкающаяся в Гёделя, вторым - в алгебру, им же в теорию категорий, третьим - в ещё какую-то математику)
Наука об понятиях (онтология); вторая сложная проблема в IT
Наука о сайд-эффектах
И когда представители первой школы говорят про "формошлёпство", они игнорируют две другие науки.
Потому что форма для ввода, какой бы тупой она не была, построена на модели, а модель построена из понятий, а эти понятия либо хороши, либо ужасны.
А наука о сайд-эффектах, она же, вообще, королева бала. Потому что как вы проверяете свой код? assert foo() == "что ожидали". А что ассерт делает? Вывод на экран.
И пока вам зелёненькие пикселы не сложат правильным образом, вы не знаете, работает оно или нет. Или красненькие. Или ещё какие-то. Но пикселы. Или буквы на принтере. Или даже мигающие лампочки и крутящиеся колёсики.
И вот с точки зрения этих вторых двух наук, названия в первой - катастрофа. Потому что они ничего не означают, они не дают никаких свойств. Группа/сложение/умножение - хорошо. Коммутация - уже плохо.
Потому что для математика коммутация - это слева на право переставить, а для всех остальных - протащить провод от одной дырки до другой. Про семигрупоиды даже говорить нечего, бытовой смысл семигрупоидов - быть изгоняемым батюшкой и святой водой.
Вы ошибатесь. Например, если я буду использовать вот такие, овеянные Гёделем, имена и формат записи, то как быстро ваша теория превратится в hexdump?
a 3
⚬ 5
x 7
= 11
, 13
∈ 17
G 19
? 23
И сразу становится видна проблема.
Поскольку 22846712859873746480447821666592346426694132333435558998983412854961114186622574870902442510049863025667206258127311451949520409822391138243055993672121915936570990365106665813437806284123385754752042992343, то
16864769537079009997552735623638851294210569891296956302019170815834250256093163457765206733996399414907576487787707854820563866134619804007689180058068808331904868741265704234181927702708284467667832782660642938045599860219748456547248516210575066967097702299635512897491732336497005063748600046522312097496491694130608325459036760407156214054244846963697027153596051357505117318705769068754707899307118108997799287559164292425986685558352710077107017962384001514570672285534154000146466930008347654728605402731492892610023306706815132862561594276335994491639491887879295602662162086985346695599058097061314205399549913988110276011211730852012745531603029064222726680211469288928708304819850613604929896662400170885448506493575929255134911646702551939491801562300744707316743031447269993464104392958730415248232758268566636347211848084900604469889334162302421600421868648023681084089562547594193300795035404459145132786570892003452683517834585410241030076873154281946148937016180452086956447477178192366083209274513455629974950299100904034689602370989704704375671768873175812581316078620556869742898574981983017235200394615844946414550918529870412138357767989055616952218056719280243053159515418718379184056457266529970850783918189620606567631342399381831504710266751145256437083940046253697705638202861777694804136273853865749513600617448614664819093509319647108342869634392479729702455189292034633816933762713798410775097456435701858667220687776578221203843222894167247018488427812426066472154302811719094539136969415402635548284885825389963092684180830424347684670894118412127692113703908128435155987327655947544759117761288055514713908611401649295657989569008350372314453125
моего компьютера не хватает на генерацию правильной записи дальше, а мой тезис становится куда более ярким, что произвольное переименование (на ординалы Гёделя, например), явно делает проблему нерешаемой.
Подозреваю, что с точки зрения той же Agda любое написанное в этой системе доказательство примерно так и выглядит.
Может быть. Но нужно понимать, что agda - это такая программа с сайд-эффектами. Если бы у agda не было сайд-эффектов, то вы бы ей не пользовались. Впрочем, как и любой другой программой без сайд-эффектов.
Вот запустили вы доказательство P!=NP. Оно завершилось. Доказало или нет?
Нет, не всё. Есть какой-то процесс вычислений (у которого тоже есть side effects, типа нагрева, но которыми мы пренебрегаем), он приводит к возврату результата в код, который делает сайд-эффект.
Правильная организация этого процесса - make it or break it. Например, если м возьмём любой алгоритм и аннотируем каждую операцию, выполняемую машиной на устройство вывода, то мы просто не сможем прочитать результат. Формально - он там, он какая тысяча из миллиардов строк искомая - мы не знаем. Получается, алгоритм формально задачу решил, но переложил на кожанных мешков задачу pattern matching'а. Это было бы глупо и теоретически, если бы иногда не оказывалось, что самая ценная строка с осмысленной ошибкой зарыта в мегабайтах трейсов, красных простынях вывода (которые не ошибки, но по сложным причинам должны быть красными). Я не могу сказать, что есть "теория сайд-эффектов", но точно есть искусство сайд-эффектов.
Имеет, имеет. Если вы его видите - это сайд-эффект. Особенность сайд-эффектов состоит в том, что их невозможно описать с помощью системы типов (потому что в финале у вас пин процессора, про который вы верите, что он зажигает зелёную лампочку а не выключает питание, и что он делает вы узнаёте только после того, как этот пин включите).
Чистая программа им. Чёрча представляет собой набор лябмд, результат применения которых (без сайд-эффектов) вы увидеть не может никаким образом.
Более того, ваша программа на агде - это всего лишь side cause для /usr/bin/agda (или куда она там ставится).
В вашей теории сайд-эффектов все оказывается сайд-эффектом, а такие теории не очень интересны.
Вас не смущает, что в отсутствии сайд-эффектов в вашей территории всё оказывается чистыми функциями?)
Как вы думаете, зачем такое деление понадобилось и в чем была их ошибка?
В итоге это деление упрощает рассуждения?
Сайд эффект это чтение или изменение состояния, которое не является локальными. Поэтому все зависит от того, как вы определяете локальность. IO выпихивает все такое за/в скобки (в рантайм) и все довольны. Хаскель подталкивает программировать в чистых функциях. Но это не решение проблемы, а заметание мусора под коврик. Коврик помогает не замечать проблем (отобенно если не тестить программу ;)), но бывает и так https://github.com/ndmitchell/ghcid/issues/274
Вот вот вот мы начинаем погружаться в современную философию. В какой момент мы можем сказать, что решение для задачи найдено?
https://link.springer.com/chapter/10.1007/978-3-0348-0862-0_4
Вот я утверждаю, что в отсутствие возможности сформулировать результат в терминах весьма ограниченной онтологической модели практически не отличимо от отсутствия результата.
Грубо говоря, если вы меня попросите написать приблизительное значение числа (например, корня из 3), я могу записать его в форме данных для алгоритма декодирования десятчных чисел (общепринятый), в форме данных для алгоритма декодирования дробей (чуть сложнее, хотя интересно), либо в форме данных для алгоритма вычисления приблизительного корня с помощью метода Ньютона.
Почему данные для метода Ньютона не считаются за решённую задачу, а данные для алгоритма декодирования соотношения двух чисел в десятичной нотации - считается?
Не проверяю свой код ассертами или вообще какими-либо тестами :]
О вот это интересно. А как без тестов-то сразу в продакшн?
Обычно в программе важно не только "что" она делает (то есть удовлетворяет-ли functional requirements), но и то "как" она это делает (non-functional requirements). Иначе для всех приложений было бы достаточно одной архитекторы и мы бы спокойно продолжали лепить монолиты. Взять пресловутый performance. Неужели ни когда не было желания сравнить пару альтернатив? Лично у меня глядя на примеры в статье сразу возникает вопрос - а нет ли более простого способа сконкатинировать пару строк безо всяких этих вот наворотов?)
Тайпчекер показывает лишь то, что написанное в коде удовлетворяет правилам тайпчекинга). Но какие гарантии, что программа вообще запустится в нужном окружении? Иными словами, вы допускаете возможность существования существенных требований к программе, которые невозможно выразить в терминах вашего тайпчекера?
А что за область, если не секрет?
В компьютерах сливаются надежды на решение всех мыслимых и немыслимых проблем. Поэтому так манит мечта о том, чтобы найти универсальную концепцию - этакую теорию всего на свете, священный Грааль нашего времени. Но мы умеем только частные решения, и можем довольствоваться лишь тем, чтобы смотреть на проблему с разных сторон, а не внутрь, не в самую суть как бы хотелось.
Группа/сложение/умножение - хорошо. Коммутация - уже плохо.
Не нашёл в статье этого слова и сегодня вижу впервые применительно к алгебраическим структурам. Всегда использовался термин "коммутативность", который обозначает свойство структуры. Напр. кольцо без уточнений имеет структуру коммутативной группы хотя бы по одной операции, векторное пространство по определению - коммутативная группа. При этом аналитические выкладки могут сопровождать словами "в силу коммутативности", "по свойству коммутативности". Часто используют оператор коммутатор: [a, b] = a*b - b*a.
Видимо, из-за того что эти термины обозначают именно свойства алгебраических структур, в программировании в чистом виде мне не попадались, но найдется немало основанных на них алгоритмов. Напр. алгоритм динамического программирования решения "matrix-chain multiplication problem" основан на свойстве ассоциативности умножения матриц.
Оказывается, что если мы будем отдельно вести учёт включений и исключений, то и вовсе добьёмся желаемого поведения.
Интересно, бухгалтерский метод с независимым подсчётом дебета и кредита появился как адаптация этой математики или был изобретён отдельно?
Сдаётся, что про PairedHashSet как группу вы напутали. И вот почему.
Множество изоморфно булеву вектору (существования каждого элемента) с операцией max (or) вместо плюса. А max - не обратим (в отличие от плюса, где есть минус). Когда мы используем симметричную разность - это мы используем xor, который сам себе обратим.
Пара множеств - изоморфна троичному вектору. Смекаете, к чему это я?
Давайте рассмотрим множества в универсуме из единственного элемента. И будем кодировать их числом: 0 - пусто, 1 - есть элемент. -1 - элемент надо удалить.
Поехали!
1 + 1 = 1
1 + 1 + 1 = 1
(1 + 1 + 1) - 1 = (1 + 1) = 1, но 1 - 1 = 0
Что-то как-то на группу не тянет, да? И ведь мы даже не добрались до -1.
---
А в чём же выход? А выход - в мультимножествах.
Мультимножество изоморфно вектору над Z+, и если его обобщить до вектора над Z, то получим группу - векторов целых чисел (со знаком) по сложению.
Извращенцы могут представить целое знаковое число как пару двух целых беззнаковых, одно из которых ноль, и написать изоморфную операцию сложения-вычитания для такой структуры.
---
Так что выкиньте ваш инженерный подход про два множества. Возьмите уж словарь - отображение T на int. (Не силён в шарпе, что там - HashMap<T,int>, наверное) и пишите складывалку-вычиталку, которая будет удалять ключи со значением 0, чтобы память экономить.
И потом сделайте проекцию этого словаря счётчиков на обычное множество - просто ключи с положительными значениями.
Властелин структур