NK
Size: a a a
2017 December 11
NK
.Almost every SMT solver is known to contain bugs [10]
2017 December 13
2017 December 15
KR
🙂 Будь ласка! Цікава робота, виписав собі різні штуки на прочитання, потім якось повернусь.
2017 December 16
NK
Dmitry надо выяснить сначала, что интересует. Можно HoTT бук попередоказывать, можно списки сделать (библиотеку), можно подоказывать для неё равенства-изоморфизмы-фьюжен рулз. Можно эффекты запилить (хотя бы в свободномонадической кодировке)
NK
Помимо этого есть "глобальная" программа по будущему рантайму-чекеру-кодогену, для которой можно попилить куски на хаскеле, эрланге и расте. На хаскеле хачить апстримный cubicaltt
2017 December 18
NK
я пока вперемешку читаю *.ctt и перечитываю Барендрехта, и ничего не пишу. И что-то мне подсказывает, что 1)надо что-то писать для закрепления прочитанного, 2)возможно читать что-то другое. Если прокомментируете мой ход мыслей - буду благодарен.
TN
Прежде всего кубик — это просто язык. Поэтому то что нравится, то и нужно на нем писать. Если хочется гомотопий, тогда надо с HoTT учебника начинать. Если обычные завтипы, тогда можно компаративистикой с Агды и Кока заниматься.
NK
Вопрос в том, получится ли читать hott как самодостаточную вещь. Я почему-то думал, что нет. Но надо наверное просто попробовать :)
TN
получится
TN
начинай с HoTT, поймешь тогда для чего кубик и почему на Агде и Коке не получится. Будет понятна мотивация.
NK
Ack
NK
А по cubical я так понимаю надо почитать тезис Мортберга?
TN
ну в самом кубике лекции лучше
NK
папка lectures в репе
NK
ну а для мотивации можно посмотреть и в других местах
NK
В принципе я вообще ничего не читал (кроме лекций). Для меня вся эта кубическая муть только трюк чтобы были выводимы экстенсиональное равенство функций и равенство изоморфных типов
NK
Т.е. "что читать" зависит от запросов и любопытства. Можно и с кубических множеств Кана начать😀
NK
Общая идея что HoTT это единственная пока существующая формализация равенства эквивалентных объектов. У неё есть модель в Kan cubical sets, а CTT это формализация этой модели с карри-говардом, в виде экстенсиональной MLTT с хитрым равенством