Разное про программирование

thesz — 12.09.2024 https://agda.readthedocs.io/en/v2.7.0/language/syntax-declarations.html

Оказывается, в Агде есть расширение языка своим синтаксисом. Мало им mixfix (if_then_else_ это функция, а не синтаксическая конструкция) , теперь ещё и синтаксис можно (ограничено) менять.

Надо приглядеться. Агдой управляют не самые глупые люди (они выбрали нормальный порядок вычислений, в отличии от Идриса), вполне возможно, они всё продумали.

http://meta2016.pereslavl.ru/papers/2016_Glueck_Klimov_Nepeivoda__Non-Linear_Configurations_for_Superlinear_Speedup_by_Supercompilation.pdf

Довольно интересная статья. В ней суперкомпиляция дополняется наиболее точным обобщением (most specific generalization) и появляется возможность получить сверхлинейное ускорение, то есть, перевести квадратичный алгоритм в линейный. До чтения этой статьи я думал, что для этого требуется возгонка (дистилляция, вот тут есть реализация этого алгоритма), но, похоже, наиболее точное обобщение имеет сходную силу преобразований.

Как минимум, надо проверить.

Оставить комментарий

Популярные посты:

• Ранее
• Архив