Я имел ввиду
foreach(int l in candidates.Keys)
if (candidates[l]-- == 0)
candidates.Remove(l);
Правда я только что осознал что амортизированно там будет O(1) декрементов :)
Я рассматриваю случай когда реализации sort и sorted действительно соответствуют своим названиям — и утверждаю что в этом случае для доказательства их корректности обязательно потребуется еще один аргумент.
Без доказательства что cmp образует линейный порядок тоже ничего не получится — иначе отсортированная последовательность может не существовать (например если cmp всегда возвращает false)
Начинать никогда не поздно :)
В качестве смысла могу предложить следующие варианты:
а) Just for fun — многие (включая меня) считают олимпиады веселым и интересным времяпрепровождением
б) Помогает поддерживать мозги в тонусе
в) При определенном уровне можно объездить кучу разных мест благодаря онсайтам соревнований ;)
г) Помогает при подготовке к собеседованиям в стиле «Как сдвинуть гору Фудзи»
Очень даже помогает :)
Строчки в резюме о хороших результатах в крупных соревнованиях резко повышают шанс что его заметят, а олимпиадный опыт помогает сконцентрироваться на собеседовании, да и задачи обычно задают несложные с точки зрения олимпиадника.
Статистика среди моих знакомых показывает что у людей, занимающихся спортивным программированием, большой шанс съездить на стажировку и/или устроиться работать в Google/Facebook/Microsoft/etc.
Для agda есть замечательный emacs agda-mode, в нем есть сочетания для набора математических символов и goals, существенно облегчающие разработку/доказательства.
Goal, грубо говоря, «дырка» в программе, для которой agda показывает необходимый тип выражения и все выражения которые есть в контексте с их типами.
foreach(int l in candidates.Keys) if (candidates[l]-- == 0) candidates.Remove(l);Правда я только что осознал что амортизированно там будет O(1) декрементов :)
А то что без определений никак это очевидно)
В качестве смысла могу предложить следующие варианты:
а) Just for fun — многие (включая меня) считают олимпиады веселым и интересным времяпрепровождением
б) Помогает поддерживать мозги в тонусе
в) При определенном уровне можно объездить кучу разных мест благодаря онсайтам соревнований ;)
г) Помогает при подготовке к собеседованиям в стиле «Как сдвинуть гору Фудзи»
Строчки в резюме о хороших результатах в крупных соревнованиях резко повышают шанс что его заметят, а олимпиадный опыт помогает сконцентрироваться на собеседовании, да и задачи обычно задают несложные с точки зрения олимпиадника.
Статистика среди моих знакомых показывает что у людей, занимающихся спортивным программированием, большой шанс съездить на стажировку и/или устроиться работать в Google/Facebook/Microsoft/etc.
Goal, грубо говоря, «дырка» в программе, для которой agda показывает необходимый тип выражения и все выражения которые есть в контексте с их типами.
Спортивное программирование: ACM, topcoder, codeforces etc.