Нашли или выдавили из себя код, который нельзя назвать нормальным,
на который без улыбки не взглянешь?
Не торопитесь его удалять или рефакторить, — запостите его на
говнокод.ру, посмеёмся вместе!
(** Set of all possible interleaving of two traces is a trace
ensemble. As we later prove in [interleaving_to_permutation], this
definition is dual to [Permutation]. *)
Inductive Interleaving : list TE -> list TE -> TraceEnsemble :=
| ilv_cons_l : forall te t1 t2 t,
Interleaving t1 t2 t ->
Interleaving (te :: t1) t2 (te :: t)
| ilv_cons_r : forall te t1 t2 t,
Interleaving t1 t2 t ->
Interleaving t1 (te :: t2) (te :: t)
| ilv_nil : Interleaving [] [] [].
Попытка оптимизации:
(* Left-biased version of [Interleaving] that doesn't make
distinction between schedulings of commuting elements: *)
Inductive UniqueInterleaving : list TE -> list TE -> TraceEnsemble :=
| uilv_cons_l : forall l t1 t2 t,
UniqueInterleaving t1 t2 t ->
UniqueInterleaving (l :: t1) t2 (l :: t)
| uilv_cons_r1 : forall l r t1 t2 t,
~trace_elems_commute l r ->
UniqueInterleaving (l :: t1) t2 (l :: t) ->
UniqueInterleaving (l :: t1) (r :: t2) (r :: l :: t)
| uilv_cons_r2 : forall r1 r2 t1 t2 t,
UniqueInterleaving t1 (r1 :: t2) (r1 :: t) ->
UniqueInterleaving t1 (r2 :: r1 :: t2) (r2 :: r1 :: t)
| uilv_nil : forall t, UniqueInterleaving [] t t.
Сложный говнокод. Почему вторая "оптимизированная" версия работает хуже первой?
SEO: для того, чтобы доказать что-то про недетерминированную систему (любая система, которая совершает I/O такой является) мы используем трейсы. Если эта система ещё и параллельная/распределённая до кучи, то мы эти трейсы должны особым образом перемешать (см. первый пример). Количество таких перемешиваний растёт примерно по экспоненте, и это плохо. Однако, некоторые операции коммутируют, и это хорошо. Мы эти коммутирующие операции можем из рассмотрения выкинуть, и степень экспоненты уменьшается (см. второе пиздец изящное определение). Оно формально правильно, Снаутяша это доказала. Количество трейсов реально уменьшается. Однако, тактика, которая эти трейсы разворечивает имеет такую же асимтотику, что и тупая тактика, но с большим (!) множителем. Вопрос к залу, как так вышло.
А разгадка в бектрекинге: тактика должна размотать второй процесс, применяя третий конструктор до тех пор, пока либо не наткнётся на некоммутирующий вызов в первом процессе, тогда она может применить второй конструктор и вернуть полученный трейс. Либо же она доходит до конца второго треда, понимает, что собрать правильный трейс ей не удастся, и откатывает весь этот путь назад.
P.S. А всё потому, что мне было лень менять одно из ключевых определений, которое изначально было не очень удобным. Если бы пид процессов изначально жил отдельно от определения ио-псов, не пришлось бы городить этот хак. Такая вот техническая долговая яма вышла.
P.S. Дампик Точная формула сложности доказательства, если кому интересно:
Fixpoint num_interleavings (a b : nat) : nat :=
match a, b with
| 0, _ => 1
| _, 0 => 1
| _, S b => fold_left (fun acc i => acc + (num_interleavings i b)) (seq 0 (S a)) 0
end.
Мне вообще не нравится эта ML-нутая хрень с матчингом. Если смотришь на это в первый раз, тут есть явные неоднозначности
Вот допустим у меня есть такая хрень
Fixpoint someshit (a b : nat) : nat :=
match a, b with
| 0, _ => 0
| _, 0 => 1
| _, _ => 2
end.
И допустим в эту хуйню передается два нуля как аргумент. Что она вернет? По первому совпадению, т.е. 0? Или это вообще не "скомпилируется"?
Во всех ФП языках, кроме логических с бэктрекингом (Curry, Ltac), паттерн-матчинг работает сверху вниз до первого совпадения. Так что жалоба в духе джавамэнов, что "в сишке нужно free делать".
ну судя по наличию там бектрекинга, он работает до самого "полного" совпадения, как маленькая жадная регулярка
Это знечит, что опотный программист может написать такой паттерн-матчинг, который за экспоненциальное время будет работать, и повесит тебе машину нахуй
Лень было переименовывать что там inversion нагенерила. Поэтому я за ``Coq'': между Proof и Qed может быть любая дикая говнота, написаная левой лапкой, лишь бы coqchk её жрал.
Вот допустим у меня есть такая хрень
И допустим в эту хуйню передается два нуля как аргумент. Что она вернет? По первому совпадению, т.е. 0? Или это вообще не "скомпилируется"?
Это знечит, что опотный программист может написать такой паттерн-матчинг, который за экспоненциальное время будет работать, и повесит тебе машину нахуй
Подарил бы кто. Например, ты.
так вижу
https://youtu.be/rX8j3TAG1qY?t=66
sauto, sauto, sauto, sauto! firstorder. sauto!
Сразу видно ма-те-ма-ти-чес-кую школу.