Untying the knot

Больше года у меня в голове бурлили мысли по поводу связи проблемы внутренней интерпретации HoTT и открытой рекурсии в комплекте с индукцией-рекурсией. Вчера паззл сложился.

До формализации далеко и я совершенно не уверен, что на пути у этого подхода не встанет непреодалимых проблем, что откуда-нибудь не вылезет гидра арифметической иерархии. Однако, даже если это не работает, это именно то, что крутилось в голове год и искало выхода. Какое-ж это удовольствие, когда ты месяцами ловишь интуицию, что есть, вот уже прямо чувствуется, что должна быть связь между открытой индукцией, сверхзависимыми типами и представлением омега-когерентных объектов, а потом наконец вылавливаешь, что же твоё подсознание имело в виду. :-)

См. обновлённый пост http://akuklev.livejournal.com/1194596.html.

HoTT новости

Как попёрло-то!
Вчера Кокванд сотоварищи выкатили имплементацию языка на базе кубической теории типов. Это в общем вычислительная имплементация HoTT, единственное что унивалентных вселенных пока не сконструировали, зато canonicity в сильном смысле, более удобный синтаксис для синтетической гомотопической теории и изофорфизмы трансформируются в равенства клёво.

И позавчера (как я выяснил минуту назад), была решена проблема коданных в HoTT: http://arxiv.org/pdf/1504.02949v1.pdf

(no subject)

Согласно наиболее распространённой версии, Дарволдай был английским изобретателем, собратом Фарадея. Изобретенное им навигационно-хронометрическое устройство широко известно в узких кругах, близких к Геофаку, и названо в честь него, образуя забавную историческую параллель с клеткой Фарадея.

Другая версия гласит, что Дарволдай (François-Nicolas comte de Dairhoilais-Dállie) был ювелиром, художником и фабрикантом, родственником Фаберже. Он знаменит своими сериями миниатюрных керамических изделий с уникальной росписью.

Наконец, согласно третьей версии братья Дарволдаи были швейцарскими математиками, в честь одного из них называется характерная кривая третьего порядка в форме колокольчика.

Какие ещё версии известны всезнающему All'у? :-)