?

Log in

No account? Create an account

[icon] /^.in$/
View:Recent Entries.
View:Archive.
View:Friends.
View:Profile.
View:Website (/me (домен, хотящийся в углу комнаты)).
Missed some entries? Then simply jump to the previous day or the next day.

Tags:
Security:
Subject:О какой-то лямбда-фигне и недостатке формализма
Time:06:41 pm
Current Mood:горячее желе вместо мозга
Сегодняшнюю ночь-день закопал в чтении умных книжек по теории типов и всяких статей и блогопостов умных дядек, которые этими вещами занимаются. Меня теперь не покидает ощущение, что я последние полтора года занимался фигнёй.
Просто вот оказывается дофига идей, которые приходили мне в голову случайным образом в разное время (например о вычислении функций от «числовых» аргументов результатами которых является тип, или о внесении в тип функции представлений об её алгоритмической сложности вычисления, потребляемой памяти и тому подобного) уже кое-где нашли своих исследователей и даже какие-то результаты.

Например, меня впечатляет тот факт, что можно строго описать язык вычислений в логарифмической памяти.
Или вот отношение свойств систем типов в лямбда-кубе. И вообще сама идея лямбда-куба мне кажется ужасно красивой. Я уже и не помню когда в последний раз меня так радовала какая-то математическая конструкция.

Ещё можно пооблизываться на всякие сильные (strong) подмножества языков, в которых есть рекурсия, но доказуема достижимость нормальной формы. И кстати, а вдруг кто-нибудь умный подскажет где почитать о соотношениях фактов отсутствия у модели вычислений Тьюринг-полноты и вычислимости любой программы в такой модели за конечное время? Т.е. правда ли, что машина Тьюринга это самый простой формализм, для которого можно придумать не завершающуюся программу, и наоборот: не завершающаяся программа всегда эквивалентна какой-нибудь программе машины Тьюринга? Не очевидно.
Ещё реквестирую какой-нибудь учебник, чтобы всё от теории множеств и её парадоксов и до теорий типов и категорий было разжёвано понятным языком, а то из этой книжки надо прочитать вторую главу, для того, чтобы там что-то понять следует из другой книжки прочитать пятую главу, а для того, чтобы там что-то понять надо из третьей книжки прочесть десятую главу, которая ссылается ещё на девять тысяч источников, и всё написано такими страшными незнакомыми английскими словами.... Не то, чтобы я был против литературы на английском, но просто если есть какой-то термин, то хоть пускай объяснят мне-дураку что это такое.

Короче, в то время как люди занимаются интересными вещами, я занимаюсь тупой бумажной работой, связанной с работой, содержание которой мне кажется абсолютно элементарным, но, тем не менее, требует много писанины для того, чтобы потенциальный читатель без базовых знаний там что-то понял. А учитывая, что потенциальных читателей у этой работы — эпсилон-малое, то сия работа нарекается фигнёй.

А ещё у меня возникает когнитивный диссонанс, когда после трёх часов чтения о рекурсии в зависимых системах типов и теории элиминаторов я переключаю свой лоскут внимания на ленту жж или ирку, где мирно общаются беззаботные люди, не обременённые мыслями об алгоритмах оценки структур логических выражений, на основе алгебраических типов данных, в языке Epigram.
withComments $ arr (take 2) >>> delay new

[icon] /^.in$/
View:Recent Entries.
View:Archive.
View:Friends.
View:Profile.
View:Website (/me (домен, хотящийся в углу комнаты)).
Missed some entries? Then simply jump to the previous day or the next day.