Зачем коллаца? Рассмотрим какую-нибудь сортировку. Вот например такая реализация на Haskell:
bubbleSort :: Ord a => [a] -> [a]
bubbleSort = untilFixed bubblePass
where
bubblePass [] = []
bubblePass [x] = [x]
bubblePass (x:y:xs)
| x > y = y : bubblePass (x:xs)
| otherwise = x : bubblePass (y:xs)
untilFixed f x = let fx = f x
in if fx == x then x else untilFixed f fx
Такой код может быть переписан на STMLib относительно легко
(set-logic ALL)
(set-option :produce-models true)
; bubblePass :: [Int] -> [Int]
; Haskell:
; bubblePass [] = []
; bubblePass [x] = [x]
; bubblePass (x:y:xs)
; | x > y = y : bubblePass (x:xs)
; | otherwise = x : bubblePass (y:xs)
(define-fun-rec bubblePass ((s (Seq Int))) (Seq Int)
(ite (<= (seq.len s) 1)
; [] или [x]
s
; (x:y:xs)
(let ((x (seq.nth s 0))
(y (seq.nth s 1))
(len (seq.len s)))
(let ((xs (seq.extract s 2 (- len 2))))
; tailInput = if x > y then (x:xs) else (y:xs)
(let ((tailInput
(ite (> x y)
(seq.++ (seq.unit x) xs)
(seq.++ (seq.unit y) xs))))
; tailOutput = bubblePass tailInput
(let ((tailOutput (bubblePass tailInput)))
; head = if x > y then y else x
; результат: head : tailOutput
(seq.++ (seq.unit (ite (> x y) y x))
tailOutput)))))))
; untilFixed :: (a -> a) -> a -> a
; Haskell-специализация:
; bubbleSort = untilFixed bubblePass
(define-fun-rec untilFixed ((s (Seq Int))) (Seq Int)
(let ((fx (bubblePass s)))
(ite (= fx s)
s
(untilFixed fx))))
(define-fun bubbleSort ((s (Seq Int))) (Seq Int)
(untilFixed s))
(define-fun initialArray () (Seq Int)
(seq.++ (seq.unit 9)
(seq.++ (seq.unit 2)
(seq.++ (seq.unit 4)
(seq.++ (seq.unit 1)
(seq.++ (seq.unit 3)
(seq.++ (seq.unit 5)
(seq.++ (seq.unit 7)
(seq.++ (seq.unit 8)
(seq.++ (seq.unit 6)
(seq.unit 0)
))))))))))
(define-fun sortedArray () (Seq Int)
(bubbleSort initialArray))
(check-sat)
(get-value (initialArray sortedArray))
Вроде всё корректно. Тут я для примера сортирую список 9 2 4 1 3 5 7 8 6 0. Можно запустить это в Z3 и он действительно сортирует, только он не сможет доказать, что такая сортировка работает для общего случая. Для проверки сортировки тут требуется функция для проверки упорядоченности (для любых двух соседних элементов a, b должно быть верно, что a <= b) и что массив после сортировки является перестановкой изначального массива, и что для любых списков любой длины эти оба условия выполняются. Если так сделать, Z3 просто зависнет или отвалится по таймауту. Такое надо через Rocq, Idris, Agda и прочие proof assistant доказывать
И зачем завязываться на SMT-солверы? Может быть какие-то вещи они доказать не осилят, и придется доказывать на Coq Rocq или чем-то подобном? Насколько я помню, Frama-C переводит свои ASCL-контракты в WhyML, и там он может быть оттранслирован в кучу разных автоматических и интерактивных пруверов https://www.why3.org/#provers. Может быть вам тоже стоит использовать такой подход?
А до какого уровня авторы численных схем их оптимизируют, какие нюансы учитываются? Например, этот herbie "знает" о том, что в процессорах есть FMA инструкции (fused multiply-add) и может их использовать, в числовых схемах такое учитывают? Учитывается ли наличие SIMD инструкций (в подобных схемах могут явно указывать, что вот тут это уравнение должно считаться через SIMD?) ?
Но у вас ведь тоже на задачах газодинамики используется некий алгоритм разбиения пространства на некие куски, чтобы симуляцию этих кусков разбросать по отдельным вычислительным узлам. Каким образом вы решаете, на какие куски разделить пространство и как оптимальней его разбросать на разные ядра с учетом особенностей оперативной и кеш памяти? Этот LRnLA как раз об этом. Может тут еше подойдет полиэдральная модель оптимизации циклов https://xeno-by.livejournal.com/28122.htmlhttps://en.wikipedia.org/wiki/Frameworks_supporting_the_polyhedral_model
Может для вашей задачи получается, что некие области требуют более точного моделирования (с использованием более мелкой сетки) т.к. в них происходят более сложные процессы, и эту сетку можно динамически перестраивать, когда этот сложномоделируемый процесс (ударная волна или может турбулентность какая-то) будет смещаться в пространстве (т.е. придумать эвристику, которая отслеживала границы процесса и уплотняла под него сетку)? Применяется ли у вас что-то подобное?
Есть еще такой проект https://herbie.uwplse.org/ для оптимизации вычислений с плавающей запятой. Там можно находить некие компромиссные оптимизации (например теряем в точности 5% для такого-то диапазона входных значений, но зато считаем в 5 раз быстрее). Написан на Racket (диалект лиспа)
https://stackoverflow.com/questions/77846522/how-can-i-generalize-diamond-tiling-to-higher-dimensions вот тут например, в самом низу есть ссылки на ряд статей. Сразу скажу, я не специалист в этой области, так что напишу в рамках своего понимания. Насколько я понял, симулируются некие процессы в пространстве, пространство разбивается на некие кирпичики определенной формы, притом разбивается рекурсивно. Для симуляции некоей одной клетки нужно учитывать состояние соседних клеток вокруг нее, время в клетках вокруг допустим будет t, просимулировали процессы в клетке и получили ее состояние для времени t+n. И пространство можно каким-то хитрым образом разбивать на такие куски, чтобы простоя было меньше. Собственно, вот цитата из той ссылки:
The only hint I can find in the literature on how it may be done comes from a Russian research group at Keldysh Institute of Applied Mathematics. This group developed a series of different parallel spacetime decomposition algorithms in the last 20 years using a methodology called Locally-Recursive non-Locally Asynchronous (LRnLA) algorithms. LRnLa is not a single algorithm but a general guideline of how to design them. Basically: (1) The tessellation must should be a recursive process to utilize the entire memory hierarchy (it's not necessarily automatic, manual parameter tuning for different machines is allow as long as tiling algorithm itself can be generalized). (2) Parallelism should exist between different tiles, the dependency conflict problem should be solvable in some natural way. Using both requirements as starting point, researchers would manually examine the stencil dependencies and use their intuition in solid geometry to design custom algorithms to satisfy these goals. Unlike polyhedron compilers, these are custom solutions designed by human domain experts for human use, with geometric interpretations that ease implementations (but only from the perspective of mathematicians and physicists...).
Чтобы максимально избежать простоев железа необходимо запускать счет на каждом ядре и GPU сразу же, как только для него готовы входные данные. К моменту, когда ядро или GPU завершило обработку, для него должен уже быть готов новый входной массив, чтобы следующий цикл счета запускался без задержек.
Почитайте про LRnLA алгоритмы, вроде это как раз из этой области
Делать на уровне DSL то, что называется common subexpression elimination (CSE) чисто для того, чтобы компилятор быстрее компилировал - это еще имеет смысл, если куски подвыражений много раз повторяются и компилятор при оптимизации их долго сам находит и оптимизирует. А вот loop-invariant code motion это достаточно простая и понятная вещь, не думаю что компилятор будет сильно дольше компилировать (или хуже оптимизировать), если это не делать за него.
Я заметил, что некоторые выражения повторяются, но со смещением на 1 по одному из индексов (индексу самого внутреннего цикла). В принципе, это ожидаемо – мы вычисляем поток через правую грань ячейки, потом сдвигаемся на 1 вправо и снова вычисляем то же значение для уже левой грани текущей ячейки. Почему бы не вычислить его один раз и не сохранить для следующей итерации цикла?
Не знаю, есть ли специальное название для такой оптимизации, но некоторые компиляторы это делать умеют. Правда тут требуются некоторые моменты учесть, дать компилятору определенные гарантии https://godbolt.org/z/Eo4dxz3x5 Компилятор должен понимать, что вызываемая в теле цикла функция является функционально чистой, и что входной массив не изменяется. Clang эту оптимизацию сделать не осиливает
Дело в том, что кусочки выражений, которые подставляются в зависимости от условий, в численных схемах не такие уж и большие. В принципе, дешевле будет вычислять сразу обе ветки ветвления, а потом код вида ...
Проблема тут в том, что компилятор может на эти "подсказки" наплевать и всё равно сгенерировать бранч. Вот например https://godbolt.org/z/xx5vf3jrK тут branchless получился только для функции test4. Инструкция bltu это "branch if less than unsigned"
Лучше было бы для таких вещей специальные директивы для компилятора придумать, чтобы пометить конкретную область кода или функцию, в которой бранчи не использовать. Может быть такое уже есть где-то.
На вопрос про медианную сложность я там ответа не нашел. Или может я невнимательно читал? Временная сложность алгоритмов оценивается обычно по лучшему, среднему и худшему случаю. Лучший случай - число неких операций при самом лучшем случае входных данных. Средний - когда рассматриваем среднее арифметическое числа операций для всех возможных входных данных длины n. Худший - для худшего случая. А оцениваются ли алгоритмы по медианному критерию, т.е. когда есть такое число x, что в половине случаев алгоритм решает задачу за меньше чем x операций, в половине случаев решает задачу за более чем x операций? Или такая оценка не имеет смысла?
А делались ли медианные оценки временной сложности разных алгоритмов сортировки? Ну т.е. для размера массива n для всего множества входных данных, какой будет медианное значение сравнений (в половине случаев алгоритм будет делать меньше, в половине случаев больше сравнений)? И какая наименьшая медианная оценка из множества всех возможных алгоритмов?
Что-то я вообще запутался. Сначала вы пишете "в худшем случае", потом нижняя оценка. Big-omega это же про лучший случай. И "нижняя оценка" это тоже означает лучший случай. Т.е. такой случай, когда алгоритм выполняется быстрее всего.
Нижняя оценка для сортировки будет Ω(n). У пузырьковой она как раз такая, если на вход подать изначально сортированный массив. Он просто пробежится по всему массиву, попарно сравнивая соседние элементы.
Не существует универсального алгоритма .... находил бы перестановку элементов p такую, что .... используя меньше, чем O(n log n) попарных сравнений, т.е. сравнений двух конкретных элементов.
Что значит "универсального алгоритма"? O(n log n) это верхняя, нижняя или средняя оценка? Если предположить, что массив уже изначально сортирован, количество попарных сравнений для проверки этой гипотезы будет n-1.
Есть несколько заблуждений насчет e-mail-маркетинга, которые приобрели широкое распространение. e-mail-маркетинг — это СПАМ. Основное отличие e-mail-маркетинга от спам-рассылки состоит в том, что первый — это коммуникация с подписчиками собственной базы e-mail адресов по их предварительному согласию, а вторая — это массовая рассылка материалов рекламного характера по базам e-mail адресов из открытых источников, без согласия получателей, что в свою очередь нарушает закон в любой стране мира.
Как я понял из статьи, никакого предварительного согласия ни с какими подписчиками у вас не было, следовательно вы занимались т.н. спамом.
Довольно долго я никак не мог понять, как с подобным уровнем знаний все эти молодые люди сумели сдать БАК, задачи в котором, как правило, составлены на вполне приличном уровне и решить которые (как мне казалось) можно, лишь обладая вполне приличными знаниями. Теперь я знаю ответ на этот вопрос. Дело в том, что практически все задачи, предлагаемые на БАКе, можно решить с помощью хорошего калькулятора - они сейчас очень умные, эти современные калькуляторы: и любое алгебраическое преобразование сделают, и производную функции найдут, и график ее нарисуют. При этом пользоваться калькулятором при сдаче БАКа официально разрешено. А уж что-что, а быстро и в правильном порядке нажимать на кнопочки современные молодые люди учатся очень лихо. Одна беда - нет-нет да и ошибешься, в спешке не ту кнопочку нажмешь, и тогда получается конфуз. Впрочем, "конфуз" - это с моей, старомодной, точки зрения, а по их, современному, мнению - просто ошибка, ну что поделаешь, бывает. К примеру, один мой студент что-то там не так нажал, и у него получился радиус планеты Земля равным 10 миллиметрам. А, к несчастью, в школе его не научили (или он просто не запомнил), какого размера наша планета, поэтому полученные им 10 миллиметров его совершенно не смутили. И лишь когда я сказал, что его ответ неправильный, он стал искать ошибку. Точнее, он просто начал снова нажимать на кнопочки, но только теперь делал это более тщательно и в результате со второй попытки получил правильный ответ. Это был старательный студент, но ему было абсолютно "до лампочки", какой там радиус у Земли: 10 миллиметров или 6400 километров, - сколько скажут, столько и будет. Только не подумайте, что проблему можно решить, запретив калькуляторы: в этом случае БАК просто никто не сдаст, дети после школы вынуждены будут вместо учебы в университетах искать работу, и одновременно без работы останется целая армия университетских профессоров - в общем, получится страшный социальный взрыв. Так что калькуляторы трогать не стоит, тем более, что в большинстве случаев
Зачем коллаца? Рассмотрим какую-нибудь сортировку. Вот например такая реализация на Haskell:
Такой код может быть переписан на STMLib относительно легко
Вроде всё корректно. Тут я для примера сортирую список 9 2 4 1 3 5 7 8 6 0. Можно запустить это в Z3 и он действительно сортирует, только он не сможет доказать, что такая сортировка работает для общего случая. Для проверки сортировки тут требуется функция для проверки упорядоченности (для любых двух соседних элементов
a, bдолжно быть верно, чтоa <= b) и что массив после сортировки является перестановкой изначального массива, и что для любых списков любой длины эти оба условия выполняются. Если так сделать, Z3 просто зависнет или отвалится по таймауту. Такое надо через Rocq, Idris, Agda и прочие proof assistant доказыватьИ зачем завязываться на SMT-солверы? Может быть какие-то вещи они доказать не осилят, и придется доказывать на
CoqRocq или чем-то подобном? Насколько я помню, Frama-C переводит свои ASCL-контракты в WhyML, и там он может быть оттранслирован в кучу разных автоматических и интерактивных пруверов https://www.why3.org/#provers. Может быть вам тоже стоит использовать такой подход?Возможно я что-то путаю, но по-моему это называется refinement type (Как в Liquid Haskell) a не dependent type
А до какого уровня авторы численных схем их оптимизируют, какие нюансы учитываются? Например, этот herbie "знает" о том, что в процессорах есть FMA инструкции (fused multiply-add) и может их использовать, в числовых схемах такое учитывают? Учитывается ли наличие SIMD инструкций (в подобных схемах могут явно указывать, что вот тут это уравнение должно считаться через SIMD?) ?
Но у вас ведь тоже на задачах газодинамики используется некий алгоритм разбиения пространства на некие куски, чтобы симуляцию этих кусков разбросать по отдельным вычислительным узлам. Каким образом вы решаете, на какие куски разделить пространство и как оптимальней его разбросать на разные ядра с учетом особенностей оперативной и кеш памяти? Этот LRnLA как раз об этом. Может тут еше подойдет полиэдральная модель оптимизации циклов https://xeno-by.livejournal.com/28122.html https://en.wikipedia.org/wiki/Frameworks_supporting_the_polyhedral_model
Может для вашей задачи получается, что некие области требуют более точного моделирования (с использованием более мелкой сетки) т.к. в них происходят более сложные процессы, и эту сетку можно динамически перестраивать, когда этот сложномоделируемый процесс (ударная волна или может турбулентность какая-то) будет смещаться в пространстве (т.е. придумать эвристику, которая отслеживала границы процесса и уплотняла под него сетку)? Применяется ли у вас что-то подобное?
Есть еще такой проект https://herbie.uwplse.org/ для оптимизации вычислений с плавающей запятой. Там можно находить некие компромиссные оптимизации (например теряем в точности 5% для такого-то диапазона входных значений, но зато считаем в 5 раз быстрее). Написан на Racket (диалект лиспа)
https://stackoverflow.com/questions/77846522/how-can-i-generalize-diamond-tiling-to-higher-dimensions вот тут например, в самом низу есть ссылки на ряд статей. Сразу скажу, я не специалист в этой области, так что напишу в рамках своего понимания. Насколько я понял, симулируются некие процессы в пространстве, пространство разбивается на некие кирпичики определенной формы, притом разбивается рекурсивно. Для симуляции некоей одной клетки нужно учитывать состояние соседних клеток вокруг нее, время в клетках вокруг допустим будет t, просимулировали процессы в клетке и получили ее состояние для времени t+n. И пространство можно каким-то хитрым образом разбивать на такие куски, чтобы простоя было меньше. Собственно, вот цитата из той ссылки:
Почитайте про LRnLA алгоритмы, вроде это как раз из этой области
Делать на уровне DSL то, что называется common subexpression elimination (CSE) чисто для того, чтобы компилятор быстрее компилировал - это еще имеет смысл, если куски подвыражений много раз повторяются и компилятор при оптимизации их долго сам находит и оптимизирует. А вот loop-invariant code motion это достаточно простая и понятная вещь, не думаю что компилятор будет сильно дольше компилировать (или хуже оптимизировать), если это не делать за него.
Это должен уметь делать компилятор. https://en.wikipedia.org/wiki/Common_subexpression_elimination
А это https://en.wikipedia.org/wiki/Loop-invariant_code_motion
Не знаю, есть ли специальное название для такой оптимизации, но некоторые компиляторы это делать умеют. Правда тут требуются некоторые моменты учесть, дать компилятору определенные гарантии https://godbolt.org/z/Eo4dxz3x5
Компилятор должен понимать, что вызываемая в теле цикла функция является функционально чистой, и что входной массив не изменяется. Clang эту оптимизацию сделать не осиливает
Проблема тут в том, что компилятор может на эти "подсказки" наплевать и всё равно сгенерировать бранч. Вот например https://godbolt.org/z/xx5vf3jrK тут branchless получился только для функции test4. Инструкция bltu это "branch if less than unsigned"
Лучше было бы для таких вещей специальные директивы для компилятора придумать, чтобы пометить конкретную область кода или функцию, в которой бранчи не использовать. Может быть такое уже есть где-то.
На вопрос про медианную сложность я там ответа не нашел. Или может я невнимательно читал?
Временная сложность алгоритмов оценивается обычно по лучшему, среднему и худшему случаю. Лучший случай - число неких операций при самом лучшем случае входных данных. Средний - когда рассматриваем среднее арифметическое числа операций для всех возможных входных данных длины n. Худший - для худшего случая. А оцениваются ли алгоритмы по медианному критерию, т.е. когда есть такое число x, что в половине случаев алгоритм решает задачу за меньше чем x операций, в половине случаев решает задачу за более чем x операций? Или такая оценка не имеет смысла?
Да, теперь понятно.
А делались ли медианные оценки временной сложности разных алгоритмов сортировки? Ну т.е. для размера массива n для всего множества входных данных, какой будет медианное значение сравнений (в половине случаев алгоритм будет делать меньше, в половине случаев больше сравнений)? И какая наименьшая медианная оценка из множества всех возможных алгоритмов?
Что-то я вообще запутался. Сначала вы пишете "в худшем случае", потом нижняя оценка. Big-omega это же про лучший случай. И "нижняя оценка" это тоже означает лучший случай. Т.е. такой случай, когда алгоритм выполняется быстрее всего.
https://www.bigocheatsheet.com/ - тут у bubble sort в столбце Time Complexity указано Ω(n) для Time Complexity - Best
Нижняя оценка для сортировки будет Ω(n). У пузырьковой она как раз такая, если на вход подать изначально сортированный массив. Он просто пробежится по всему массиву, попарно сравнивая соседние элементы.
Что значит "универсального алгоритма"? O(n log n) это верхняя, нижняя или средняя оценка? Если предположить, что массив уже изначально сортирован, количество попарных сравнений для проверки этой гипотезы будет n-1.
Ну так зачем использовать термин "e-mail маркетинг", если то что вы сделали это именно что спам? Давайте я вам википедию процитирую
https://ru.wikipedia.org/wiki/Email-маркетинг#Заблуждения,_касающиеся_e-mail-маркетинга
Как я понял из статьи, никакого предварительного согласия ни с какими подписчиками у вас не было, следовательно вы занимались т.н. спамом.
Это так сейчас называют спам?
Эта статья напомнила мне одну статью с журнала "Наука и жизнь" https://www.nkj.ru/archive/articles/457/ :
В этом спинлоке
Количество итераций холостого цикла (в данном случае это 24 * 100) по каким критериям подбирать?
Скажите это квантовой физике