to post messages and comments.

← All posts tagged CS

Буду и сюда постить "хорошие статьи/книги" по понедельникам.

При программировании в языках с неизменяемыми структурами данных, часто применяются методы работающие со структурой в-целом. Такие техники позволяют писать программу, как объединение более простых подпрограмм. Однако этот подход может ухудшать производительность, т.к. заставяет создавать огромные структуры данных, для решения это проблемы используется оптимизации deforestation (и fusion), основанная на правилах перезаписи выражений. При этой оптимизации удаляются промежуточные структуры и при компиляции код обрабатывающий сложную структуру превращается в настолько же эффективный, как код написанный на С, но при этом более поддерживаемый. В диссертации Дункана Котса рассматриваются различные такие правила (со ссылками на статьи о них), а так же дается доказательство корректности, и минимальные требования к языку, в котором эффективно принимать данные правила.

D. Coutts, “Stream Fusion: Practical shortcut fusion for coinductive sequence types,” 2010.

И в догонку, допустим у меня есть линейный вектор, и я его сортирую; достаточно ли привести доказательства, что результирующая линейный вектор имеет тот же размер и сортирован.
Т.Е. Можно ли фактом использования линейных структур заменить доказательство того что новый вектор это перестановка элементов исходного?

Вот есть люди, которые в Chalmers пилят всякие инетерсные штуки типа линейных типов.
А почему если заходить на сайт и смотреть какие есть программы для Post Doc то там какая-то туфта :(

чистил Downloads, нашёл кучу классных книжек, не могу правда вспомнить в каком контексте я их скачивал и зачем оно было надо.
Вот нафига мне было:
Naming and synchronization in a decentralized computer system, 78 года и стоит ли её читать.