840 mokum avatar large
горячая сучка, на пенсии

доступно о завтипах, буддизме, лытдыбр и репосты инстика, характер пиздоватый, иронизировать не советую. Twitter, Github, Instagram: @5HT

Avatar for 5ht
The place I was born
Avatar for 5ht
Подошло к концу доказательство того факта, что тривиальное расслоение равно зависимой функции. Это конечно не топчик, но хорошее основание не только для алгебраической топологии, но и для теории типов, потому как тесно связан с квантором Пи и является по-сути еще одной его теоремой. Особенно хорошо этот пример показывает прямые пруфы в кубической теории, которые заметно отличаются от агдовских пруфов. Если взять доказательство этого же факта у Феликса Веллена на Агде, то заподозрить нас в плагиате будет невозможно, потому в кубике доказательство выглядет совершенно по-другому чем у Агды. С другой стороны, без PhD Феликса я вообще не уверен, что я бы взялся за эту задачу, настолько было полезным для меня ее прочтение. Книги: Хьюзмоллер "Расслоенные пространства", Стинрод "Косые произведения", Бурбаки "Дифференциируемые и аналитические многообразия", Ху Cы Цьзян "Теория Гомотопий".
Подошло к концу доказательство того факта, что тривиальное расслоение равно зависимой функции. Это конечно не топчик, но хорошее основание не только для алгебраической топологии, но и для теории типов, потому как тесно связан с квантором Пи и является по-сути еще одной его теоремой. Особенно хорошо этот пример показывает прямые пруфы в кубической теории, которые заметно отличаются от агдовских пруфов. Если взять доказательство этого же факта у Феликса Веллена на Агде, то заподозрить нас в плагиате будет невозможно, потому в кубике доказательство выглядет совершенно по-другому чем у Агды. С другой стороны, без PhD Феликса я вообще не уверен, что я бы взялся за эту задачу, настолько было полезным для меня ее прочтение. Книги: Хьюзмоллер "Расслоенные пространства", Стинрод "Косые произведения", Бурбаки "Дифференциируемые и аналитические многообразия", Ху Cы Цьзян "Теория Гомотопий".
Avatar for 5ht
Все вы знаете уже, что с августа 2017 года конструктивную интерпретация аксиомы унивалентности можно доказать не только на бумаге, но и используя тайпчекер cubicaltt. Но мало кто знает, что этот тайпчекер является устаревшим! Да да, начиная с марта 2018 года появилась новая конструктивная кубическая теория и ее тайпчекер yacctt, основанная не на примитивах композишина и склеек comp Glue glue, а на коершинах и гомогенных композициях coe, hcom, box, cap, а вместо glue — V-типы (в yacct две иерархии вселенных: претипы и типы Кана). Хотя и то и другое — операции Кана, последняя модель позволяет получить более компактные доказательства и более компактный тайпчекер. Основная мотивация такого пайвота в том, что на кубике не считается число Брунери n=2 в π_4(S^3) ≃ Z/nZ (канонический тест для гомотопического тайпчекера). Для этого оказывается 64ГБ памяти маловато! Правда на yacctt еще пока не написано, но уже видно, что основные унивалентные теоремы гораздо компактнее.
Comment
Если первая теория базировалась на ССHM-расслоениях (Кирилл Коен, Терри Кокан, Саймон Губер, Андерс Мортберг), то вторая называется Cartesian Cubical Type Theory (от чего и название репозитория). Для yacct есть формальная модель на Agda и NuPRL, основной вклад в это сделали Йан Ортон, Андрю Питц, Карло Анджиули, Роберт Харпер, Дэн Ликата, Гуилям Брунери, а авторов Карло Анжули, Фавонии (Ку Бан Хо) и Андерса Мортберга. Репа по сути клон cubicaltt, поэтому Мортберг всем заведует! ‎· горячая сучка, на пенсии
Avatar for 5ht
На выходных читал про расслоения пространств aka Fiber Bundles. FB — это сигнатура F -> E -> B с морфизмами, где F — расслоение (индексированный зависимый тип) [kernel], E — многообразие или топологическое тотальное пространство расслоения, B — база расслоения [image], на которой происходит расслоение. f: E -> B — это проекция или ретракт, s: B -> E — это секция (не всегда существует, так как должно быть f . s = id). Если E = B * F — такое расслоение называется тривиальным. Так вот если F взять Pi или Sigma вы получите сопряжения кванторов. Если взять вместо F — R^n вы получите расслоение векторных пространств. Факторпространства и расслоение сфер — другие примеры расслоений. Лента Мебиуса — это расслоение линии сегмента по окружности, секция такого расслоения перекручена. Бутылка Клейна — это расслоение окружности по окружности, когда сецкия такого расслоение перекручена. Пока писал пост, успел купить книгу и сформулировать определения на кубике.
Avatar for 5ht
Вчера весь вечер рисовал страницу про категории и крутил расширения Кана. Так и не смог построить даже сигнатуру универсальности расширений Кана, вот лох! Но обо всем по порядку. Расширение Кана двух функторов К: А -> B, G: A -> C — это такой функтор F: B -> C, для которого существует естественное преобразование композиции функоторов F o K и функтора G. Конус функтора D: J -> C — это расширение кана, где функтор К: J -> 1 действует в кодомен единичной категории. Свойство универсальности расширений Кана — это их единственность при фиксации К и G для любых двух расширений Кана. Правое расширение Кана функторов К и G, это по-сути определение расширения Кана вместе со свойством универсальности, т.е. ∑ (x: extension K G) ∏ (y: extension K G) isContr(universality K G x y). Категорный предел по функтору D: J -> C (диаграмме) — есть правое раширение Кана, где К: J -> 1 действует в единичную категорию. Вот и все.
Comment
Уровень бакалаврата в Гарварде: http://www.math.harvard.edu/theses/senior/lehner/lehner.pdf ‎· горячая сучка, на пенсии ‎· 2
Comment
Интересен был бы фидбек какие из этих источников тебе более понятные чем остальные. ‎· горячая сучка, на пенсии
Avatar for 5ht
Завтра Доклад
Comment
Красивые картинки, но все ч-б! ‎· 9000
Comment
Классика йопта! ‎· горячая сучка, на пенсии ‎· 2
Comment
Для тех, кто воспринимает эту хуйню не как ASCII арт: https://github.com/groupoid/groupoid.space/blob/master/tex/sl... ‎· горячая сучка, на пенсии
Avatar for 5ht
Из серии давно забытых срачей. Когда-то Жорж, автор учебника по Теории Категорий https://github.com/George66/Textbook/blob/master/Учебник верс... решительно громко хлопнул дверью и ушел из "всем похуй" камюнити в ЖЖ про теоркат, с которого начался теоркат в ЖЖ (ну пиздежь конечно) https://category-theory.livejournal.com/34284.html Спустя годы в условиях жесткой изоляции коммуникаций по предмету решил зайти на https://dxdy.ru/topic127434.html и задать вопрос про 2-категории и бикатегории, вопрос их изоморфизма произведению категорий. И что вы думаете — мне ответил Жорж! Посмотрим как будет разворачиваться борьба. Включайте подписку HBO!
Из серии давно забытых срачей. Когда-то Жорж, автор учебника по Теории Категорий https://github.com/George66/Textbook/blob/master/Учебник верс... решительно громко хлопнул дверью и ушел из "всем похуй" камюнити в ЖЖ про теоркат, с которого начался теоркат в ЖЖ (ну пиздежь конечно) https://category-theory.livejournal.com/34284.html Спустя годы в условиях жесткой изоляции коммуникаций по предмету решил зайти на https://dxdy.ru/topic127434.html и задать вопрос про 2-категории и бикатегории, вопрос их изоморфизма произведению категорий. И что вы думаете — мне ответил Жорж! Посмотрим как будет разворачиваться борьба. Включайте подписку HBO!
Avatar for 5ht
Урок Второй. Построение категорий от Set до Инфинити!

После первой 2-часовой лекции по MLTT, где детально разбираются Пи, Сигма, Путь и все их компоненты Formation/Inro/Elim/Rec/Case/Induction/Eta/Beta (а у Пути еще дополнительных куча subst, trans, все конечно через J выражаются, но через J реально никто не пишет, поэтому надо учить сразу культурке). У Пи типа есть еще funExt аксиома без которой не доказывается, что тип морфизмов является множеством, поэтому конструктивное построение инфинити категорий было невозможно до agda --cubical. Если морфизмы образуют не множество, а групоид, то это уже будет другая категория и так дальше до инфинити групоида. Кроме этого категории еще вкладываются друг в друга, например 0-категория — это множества или сетоид, где отношение Hom A B — это отношение эквивалентности на множествах, 1-категория, это категория где объекты — это 0-категории, множества или топологические пространства, а морфизмы — это отображения, в 2-категориях объекты — это 1-категории или просто категории, 1-морфизмы — это функторы, а 2-морфизмы — это естественные преобразования. На втором уроке можно уже строить категорию Множеств. Ну а категорию функторов можно давать уже после полного введения в теорию категори с лимитами. И уже только после теорката и категории функторов можно прееходить к семантике зависимой теории, категории контекстов, где морфизмы — это подстановки и категориям с семействами. Только сейчас решил написать это.
Урок Второй. Построение категорий от Set до Инфинити!

После первой 2-часовой лекции по MLTT, где детально разбираются Пи, Сигма, Путь и все их компоненты Formation/Inro/Elim/Rec/Case/Induction/Eta/Beta (а у Пути еще дополнительных куча subst, trans, все конечно через J выражаются, но через J реально никто не пишет, поэтому надо учить сразу культурке). У Пи типа есть еще funExt аксиома без которой не доказывается, что тип морфизмов является множеством, поэтому конструктивное построение инфинити категорий было невозможно до agda --cubical. Если морфизмы образуют не множество, а групоид, то это уже будет другая категория и так дальше до инфинити групоида. Кроме этого категории еще вкладываются друг в друга, например 0-категория — это множества или сетоид, где отношение Hom A B — это отношение эквивалентности на множествах, 1-категория, это категория где объекты — это 0-категории, множества или топологические пространства, а морфизмы — это отображения, в 2-категориях объекты — это 1-категории или просто категории, 1-морфизмы — это функторы, а 2-морфизмы — это естественные преобразования. На втором уроке можно уже строить категорию Множеств. Ну а категорию функторов можно давать уже после полного введения в теорию категори с лимитами. И уже только после теорката и категории функторов можно прееходить к семантике зависимой теории, категории контекстов, где морфизмы — это подстановки и категориям с семействами. Только сейчас решил написать это.
Comment
Почему категорию множеств можно давать сразу на втором уроке без теорката? Потому, что в доказательствах свойств категории испольется только refl, такой же фокус как и с инференс правилами встроенной теории типов (самодоказательство, пруф чекинг тайп чекера по сути). Остается только детально разбрать доказательствао setFun которое говорит, что если кодомен множество, то стрелка тоже множество, ну а у нас не только кодомен множество, но и домен, так что доказательство тоже тривиальное, и как раз оно требует funExt. ‎· горячая сучка, на пенсии
Comment
@5ht: Мне скорее становится понятно, что "о как бывает-то" и "вот список на почитать". Т.е. понятно, что узко знакомые мне понятия функторов / категорий / гомологий / проверки типов можно рассмотреть сильно более общим образом, и тогда можно рассуждать вот так. Но мне пока не хватает 5-6 концептуальных ступеней, я чувствую. (Вообще всё, что я знаю про более-менее абстрактную алгебру, я узнал сам; в институте моей специальностью были встроенные системы, схемотехника всякая, а из математики — минимальные анализ и линейная алгебра.) ‎· 9000
Avatar for 5ht
Ха-ха, у меня первый анфолов! Трепещите!
Comment
Гаммельнский анфолов. ‎· псы в рапиде ‎· 13
Comment
^^^^^^ вообще, надо сказать, эстетику ЖЖ воссоздать получилось! ‎· горячая сучка, на пенсии ‎· 3
Avatar for 5ht
Как известно понять теорию категорий можно только если научился строить лимиты, а понять теорию гомотопий можно, если научился строить гомотопические лимиты! Гомотопический лимит в общем случае не равен категорному. Определение лимита простое — для любых f: A -> C и g: B -> C это ∑ (a: A) ∑ (b: B) f(a) =_C f(b) . Т.е. гомотопический лимит это обобщение расслоения. Кроме Кубической Теории Типов есть еще и Кубическая Гомотопическая теория, в которй 0-клетки — это пространства, 1-клетки — это расслоения, 2-клетки — это лимиты и колимиты, и т.д. В учебнике HoTT троллят читателя и вместо того, чтобы дать пулбеки и пушауты главами, пулбек предлагают решить как упражнение 2.11 ко второй главе.
Avatar for 5ht
Слева направо: Тамар (Гонконг), Долина Дзогчен (Китай), Лайор (Тибет)
Comment
Долина в натуральных цветах? ‎· 9000
Comment
@9000: все после инстаграмма :-( ‎· горячая сучка, на пенсии ‎· 1
Avatar for 5ht
Первая лекция. Формальная модель MLTT путем прямого встраивания в теорию типов

Стрим на мокуме начинается с "Конструктивного доказательства унивалентности", теоремы которая стала возможной только в августе 2017 года! Я думаю надо понижать планку и рассказать вам о первой лекции, которую я всегда даю по завтиповой теории. В этой лекции мы формально выписываем все формейшин рулы, интродакшин рулы, элиминейшин рулы и бета и эта равенства для трех типов, из которых состоит MLTT: Пи, Сигма и Равенство. И что интересно, если записать MLTT на самой MLTT то, получится, что доказательство большинства равенств будет состоять из reflection интродакшин рула от типа равенства. Таким образом показывается, что NBE настолько мощная штука, что может доказать почти все теоремы MLTT, кроме компютейшинал правила (эта-правило) для равенства. Я засекал на видосе live-кодинг и формального доказательства всей MLTT в кубике у меня уместилось в пару часов. В качестве пейпера который можно взять как основу для данной демонстрации я беру Мартина Хоффмана и Томаса Страйхера "Групоидная интерпретация теории типов", работы, с которой начался путь в унивалентные основания. Но вообще можно брать любой пейпер по MLTT начиная с Мартина-Лёфа 1984.
Первая лекция. Формальная модель MLTT путем прямого встраивания в теорию типов

Стрим на мокуме начинается с "Конструктивного доказательства унивалентности", теоремы которая стала возможной только в августе 2017 года! Я думаю надо понижать планку и рассказать вам о первой лекции, которую я всегда даю по завтиповой теории. В этой лекции мы формально выписываем все формейшин рулы, интродакшин рулы, элиминейшин рулы и бета и эта равенства для трех типов, из которых состоит MLTT: Пи, Сигма и Равенство. И что интересно, если записать MLTT на самой MLTT то, получится, что доказательство большинства равенств будет состоять из reflection интродакшин рула от типа равенства. Таким образом показывается, что NBE настолько мощная штука, что может доказать почти все теоремы MLTT, кроме компютейшинал правила (эта-правило) для равенства. Я засекал на видосе live-кодинг и формального доказательства всей MLTT в кубике у меня уместилось в пару часов. В качестве пейпера который можно взять как основу для данной демонстрации я беру Мартина Хоффмана и Томаса Страйхера "Групоидная интерпретация теории типов", работы, с которой начался путь в унивалентные основания. Но вообще можно брать любой пейпер по MLTT начиная с Мартина-Лёфа 1984.
Comment
NOTE: На самом деле в MLTT формально еще присутствуют Nat, List и W-типы, но поскольку мы знаем, что такое черч-кодировка, то мы можем закодировать эти типы через пи и сигму, так что вообщем-то они для нас всего-лишь аксиомы, а не примитивы тайп чекера. С другой стороны Nat, List и W никто в тайпчекер не включает, а сразу уже индуктивные семейства типов, привычые нам data и codata. Способов кодировок я знаю минимум шесть! ‎· горячая сучка, на пенсии
Avatar for 5ht
Молоді Карпати. Зліва направо: Синевір, Говерла, Пилипець.
Avatar for 5ht
Чтобы определить гомотопический колимит или пушаут, уже недостаточно пи и сигмы даже чтобы записать сигнатуру, нужны либо высшие индуктивные типы, либо, если вы умеете (а я вам рассказывал), ипредикативную кодировку. Проще говоря, нужно умножение в лимите заменить на сумму. Покажем как выглядит гомотопический колимит, это для функций f: C -> A, g: C -> B по сути сумма типов po1: A -> colim, po2: B -> colim и их равенства po3: (c: C) -> po1 (f c) = po2 (g c). Нужно построить для этого типа рекурсор и индукцию, кто возьмется?
Comment
(гомотопический колимит звучит как название болезни ЖКТ) #извините ‎· peiſda pomeleis ‎· 5
Avatar for 5ht
Модальная теория типов. Загнали акиомы и погнали. Невозможно же посчитать бесконечно малые. Можно сюда алгоритмы вставить которые будут комонадично считать до определенной точности или в тайпчекер зашить! Тут записано https://ncatlab.org/nlab/show/infinitesimal+shape+modality коредуцированные объекты.
Comment
А можно на пальцах (или даже метафрически), где в теории типовы выезают бесконечно *малые*? (Мне оно всё представляется поисходящим в дискретных, хотя и бесконечных, пространствах.) ‎· 9000
Comment
Просто, чтобы не городить R^n топологию на Коши, договорились использовать вот этот кусок кода. Траст ми, я математик :-) ‎· горячая сучка, на пенсии ‎· 1
Avatar for 5ht
Для любителей монад у меня есть хорошая новость, самое последнее расширение HoTT, cohesivett, или модальная теория типов, которая синтаксически хачит такие штуки как линейность, окресности, связность, бесконечно малые и шейпы как фундаментальные инфинити групоиды. Там три вида контекстов Γ | ∆ | Ξ. И 6 операций — cohesive модалити ʃ (групоид, комонада) ⊣ ♭ (комонада, дискретность) ⊣ ♯ (монада, кодискр.) и дифференциальные модалити ℜ (редукции, комонада, гладкость) ⊣ ℑ (бесконечно малые фиг. модальности, монада) ⊣ & (étale морфизмы, комонада).
Comment
Использование музыкальной нотации прекрасно. Особенно рядом с bosonic / fermionic. ‎· 9000 ‎· 1
Avatar for 5ht
Море новостей. Во-первых чтобы конструтивно бандлы смоделировать и что-то "посчитать", то посчитать можно только Структурные группы aka Covering Spaces и G-structures, на смоделированых через фломальные étale мапы многообразиях. Так можно смоделировать векторные бандлы и посчитать ихние группы автоморфизмов. Бывает так, что и сам слой F является группой афтоморфизмов. Так вот étale мапы моделируется через интересную штуку — модалити, она есть в конце первой части HoTT, но не испольузется дальше в книге нигде. Бандлы — это вообще самая главная часть алг. топологии, есть в каждом учебнике, можно сравнить определения, но самое интересное — это PhD Феликса Веллена http://www.math.kit.edu/iag3/~wellen/media/diss.pdf где формализируется на Агде то, про что я сейчас рассказал. Чтобы вы не рылысь в его исходниках я выдер только эти определения, еще там есть 4 равнозначных определения расслоеных пространств, определение модальностей, étale морфизмов на них, многообразий на этале морфизмах, определение G-структуры на Автоморфизмах и фундаментальный инфинити групоид в виде индуктивного типа Майкла Шульмана. Вес это я занимает 500 строчек на Агде https://github.com/groupoid/infinity/blob/master/priv/bundle..... Нашел еще классные слайды Favonia (к которому обращается Роберт Харпер в своих лекциях 15-819) https://www.math.ias.edu/~favonia/files/cover-crm2013-slides.pdf которые показывают, что G-структыры эквивалентны Накрывающим Пространствам.
Avatar for 5ht
Больше файбер бандлов! Целый день доказывал простейшую теорему о том, что слоение — это квантор всеобщности, но не сходятся условия ретракта и секции f . g = id_A, g . f = id_B. В беспомощности отправил письмо с просьбой подсказки. Пытался починить фибрации Хопфа, но они не чинятся никак. Инвертирование S1 не дает S1, говорит S1 /= S1 и все. Надо будет попробовать на днях новую ветку hcomptrans. Нарисовал страничку, куда со временем должны попасть фибрации Хопфа. Оказывается то, как я придумал создавать индуктивно сферы называется иерархия суспензий. Сфера S^0 — это булевый тип, две точки. Сфера S^(n+1) — это суспензия сферы S^n, n=0... Cуспензии к счастью в кубике работают. Посмотрел у Спеньера, что для того, чтобы определять всякие разные виды расслоений мне нужна структурная группа.
Больше файбер бандлов! Целый день доказывал простейшую теорему о том, что слоение — это квантор всеобщности, но не сходятся условия ретракта и секции f . g = id_A, g . f = id_B. В беспомощности отправил письмо с просьбой подсказки. Пытался починить фибрации Хопфа, но они не чинятся никак. Инвертирование S1 не дает S1, говорит S1 /= S1 и все. Надо будет попробовать на днях новую ветку hcomptrans. Нарисовал страничку, куда со временем должны попасть фибрации Хопфа. Оказывается то, как я придумал создавать индуктивно сферы называется иерархия суспензий. Сфера S^0 — это булевый тип, две точки. Сфера S^(n+1) — это суспензия сферы S^n, n=0... Cуспензии к счастью в кубике работают. Посмотрел у Спеньера, что для того, чтобы определять всякие разные виды расслоений мне нужна структурная группа.
Avatar for 5ht
Уже давно посыпался веник на http://ns.synrc.com, день назад пошел в ЭПОС, восстановил книги по теоркату и математике, которые лежали на нем, купил самую дешевую 120-ку кингстон и воткнул уже на VPC-S в магниевом корпусе, докинул 2Г планочку до 6Г и как новенький? Предыдущий пластмассовый SZ уже не выдерживает критики, поэтому я его разобрал и законсервировал (я в качестве серверов использую старые ноуты), запчасти к нему еще через Валкина покупал! Поставил xubuntu. НО! Пробовал подключить веник к своему https://5ht.co/tristellar/ и нихуя не заработало! Все порта! Кабели хуябели, CMOS клок резет, перешивка UEFI, ни к чему не привело. Мечта про 8ТБ рейд SSD отодвинулась на неопределенное время. Хорошо, что я сразу 4 веника не купил :-) Вообщем есть последняя надежда, что M.2 веник SATA интерфейса захватывает шину и отключает SATA порта, вряд ли конечно такой ебанизм может быть на ASUS. В то, что они сгорели тоже не верится. Придется раскручивать, снимать систему охлаждения и вытаскивать мамку. Ах.
Comment
Ах как это все не вовремя, как раз микрофончик с усилком TASCAM едет. Думал подкастики пописать, пригласить мокумовцев в гости! Пока думаю отложить решение это проблемы. ‎· горячая сучка, на пенсии
Comment
Слева направо: Happy Hacking Keyboard Pro 2, STRIX Z370-I, STRIX 1080 Ti ‎· горячая сучка, на пенсии
Comment
Сегодня на мониторе, который я взял поганять появились две вертикальные полоски :-( ‎· горячая сучка, на пенсии ‎· 1
Comment
^ Когда что-то ведёт себя нестабильно и склонно гореть, я бы пошёл проверять питание. Surge protector, вот это всё. ‎· 9000 ‎· 2
Comment
@9000: дак у меня Premium Fanless Titanium 600W (правда без фильтра), а SATA вообще хот плаг. Монитор был в фильтре кстати сяомишном. ‎· горячая сучка, на пенсии
Avatar for 5ht
На прошлом уроке мы познакомились с расслоениями пространств, как ближайшими изоморфизмами для пи и сигма типов. В MLTT вообще много изоморфизмов, поэтому, когда дают определение чему-то, всегда говорят up to isomorphism, именно так родилось определение Категории в учебнике HoTT, с помощью пополнения Rezk. В нашей базовой библиотеке именно такое определение. У равенства в MLTT есть три изоморфизма которые учавствуют в описании унивалентности: 1) это встроенный в тайпчекер Path, 2) это эквивалентность которая определяется через расслоения и 3) изоморфизм который опрделеяется как пара морфизмов A -> B, B -> A, левая и правая композиция которых это тождественная функция А или B типа. Так вот iso уже посложнее выглядит как терм, а эквивалентность еще не такая сложная. Всего при трех равенствах получается 18 унивалентных теорем о равенствах: Iso(Path,Equiv), Equiv(Path,Iso), ...т.е. флипы аргументов, в разные стороны стрелки, и в разном порядке все равенства.
Comment
Вообще поиск нетривиальных изоморфизмов -- это благородная судя по всему деятельность в математике. Если у нас есть три изоморфизма и термы одного из них гораздо меньше и элиминаторы которого работают быстрее, то очевидно, что надо везде использовать на практике его, а не более громоздких братьев. ‎· горячая сучка, на пенсии
Comment
Андреа запилил порт кубиковской либы на Агду: https://github.com/Saizan/cubical-demo В принципе совместима с нашей либой, если вы это прочитаете, вы будете в либе Групоид Инфинити как рыба в воде. Работает в режиме agda --cubical ‎· горячая сучка, на пенсии
Avatar for 5ht
Как ни крути инстанс любой мало-мальски нетривиальной модели — это категория. Вот так и система доказательства теорем, будь-то с экстрактами или без, или вообще система языков. как например F*, где и SMT солверы и Coq и где нада С и другие языки присутствуют. В ней объекты — это виды лямбда калкулусов, но не простые а со своими моделями во второй части сигмы закодированные (сами модели это тоже категории), а морфизмы — это AST трансформации между языками, например, это можеть быть: компляция, экстракция, тайп чекинг, удаление типов, оптимизация, дешугаринг, и т.д. Элементы объектов — это программы или базовые библиотеки, которые могут учавствовать в уравнениях на предмет валидности и соотвествия сертификации.
Как ни крути инстанс любой мало-мальски нетривиальной модели — это категория. Вот так и система доказательства теорем, будь-то с экстрактами или без, или вообще система языков. как например F*, где и SMT солверы и Coq и где нада С и другие языки присутствуют. В ней объекты — это виды лямбда калкулусов, но не простые а со своими моделями во второй части сигмы закодированные (сами модели это тоже категории), а морфизмы — это AST трансформации между языками, например, это можеть быть: компляция, экстракция, тайп чекинг, удаление типов, оптимизация, дешугаринг, и т.д. Элементы объектов — это программы или базовые библиотеки, которые могут учавствовать в уравнениях на предмет валидности и соотвествия сертификации.
Comment
Я себе представил как люди это в UML диаграммах (Диаграмма Компонент?) для Java какой нибудь рисуют сейчас и вздрагиваю. ‎· горячая сучка, на пенсии ‎· 1
Comment
@9000: ну сойдется ли построение категории монад, или что мы там моделируем. ‎· горячая сучка, на пенсии
Avatar for 5ht
Если кому-то инетерсна буддийская темка и он хочет немного погрузить себя в контекст того, что я пишу, я советую обратиться к стриму Безумного Монаха http://t.me/madmonk, который я создал специально по запросу для @sorhed, где я в двух словах попытался объяснить за буддизм своему другу, в полном соответствии с буддийским каноном. Стрим оканчивается презентацией сайта http://longchenpa.guru Это все было сделано в рамках движения KEEP YOUR SHIT TOGETHER, на основе постов в ЖЖ под тегом dharma (теперь их там нет, а вся полезная и качественная информация разложилась на последовательность постов в стриме). Все записи на мокуме про буддизм консидерятся как продолжение стрима Безумного Монаха (возможно будет бекпорт). Поэтому те, кто желает смотреть фильмы Марвел в правильной последовательности, читайте стрим Безумного Монаха.
Avatar for 5ht
Простираюсь перед Ваджрасаттвой

Если верить буддистам, то наше бытие определяется нашим мышлением (впрочем не только буддисты так считали), а мышление оно ж поразному может быть от точки до пространства, зависит от медитации. Вот представьте себе пустое пространство, где сила вашего мышления удерживает образы настолько ясно и четко, что вы можете представить от одной светящейся точки в пустоте, до целого иллюзорного мира наподобии (или нет) нашему. Другими словами нарисовать и осознать любую ткань реальности. А теперь сравните это с той медитацией, которую вы выполняете на подушке, или, прости господи, намаливаете с четками рогатым богам. Сравнили? Приблизительно такая же разница между буддизмом и тем, что вы о нем думаете.
Простираюсь перед Ваджрасаттвой

Если верить буддистам, то наше бытие определяется нашим мышлением (впрочем не только буддисты так считали), а мышление оно ж поразному может быть от точки до пространства, зависит от медитации. Вот представьте себе пустое пространство, где сила вашего мышления удерживает образы настолько ясно и четко, что вы можете представить от одной светящейся точки в пустоте, до целого иллюзорного мира наподобии (или нет) нашему. Другими словами нарисовать и осознать любую ткань реальности. А теперь сравните это с той медитацией, которую вы выполняете на подушке, или, прости господи, намаливаете с четками рогатым богам. Сравнили? Приблизительно такая же разница между буддизмом и тем, что вы о нем думаете.
Comment
Когда люди закрывают глаза и садятся с этого начинается дорога медитации. А там дальше от типа зависит: одни просто попадают в спокойное место, другие рисуют себе свободные места или фантазии, третьи, только закрывают глаза сразу начинают уносить картинки, некоторые сразу засыпают и клонит в сон, некоторых сразу выбешивает. Это нулевой уровень медитации. ‎· горячая сучка, на пенсии
Comment
@5ht: спасибо, так понятно ‎· ору ‎· 1
Avatar for 5ht
Синтаксис Кубика

Если хочется взять завтиповый язык, (так, чтобы понять зачем вообще эти языки пишут), то надо брать не Идрис, а Агду, там по кодобазе становится понятно, что значительная часть полезного находится в *.Properties неймспейсе. В принципе в базовой либе много чего есть из Завтиповой Прелюдии, задачи и принципы которой не похожи на System F (хаскелевскую, например) библиотеку, но есть и много похожего, например ран-тайм части базовой библиотеки. Проблема Идриса в том, что там все ориентировано на рантайм, а Агды в том, что там все ориентировано на математику (кто ставил MAlonso тот понимает о чем я). Зачем же я занимаюсь кубиком, для которого и базовой либы нет, и экстракта нет? Потому, что он самый красивый, модный и охуенный! И раз на нем нет базовой библиотеки и своего ран-тайма, то это хорошая возможность сделать это, мы ж программисты! На рисунке синтаксис Кубика в BNF нотации, ну как можно такой язык не любить?
Синтаксис Кубика

Если хочется взять завтиповый язык, (так, чтобы понять зачем вообще эти языки пишут), то надо брать не Идрис, а Агду, там по кодобазе становится понятно, что значительная часть полезного находится в *.Properties неймспейсе. В принципе в базовой либе много чего есть из Завтиповой Прелюдии, задачи и принципы которой не похожи на System F (хаскелевскую, например) библиотеку, но есть и много похожего, например ран-тайм части базовой библиотеки. Проблема Идриса в том, что там все ориентировано на рантайм, а Агды в том, что там все ориентировано на математику (кто ставил MAlonso тот понимает о чем я). Зачем же я занимаюсь кубиком, для которого и базовой либы нет, и экстракта нет? Потому, что он самый красивый, модный и охуенный! И раз на нем нет базовой библиотеки и своего ран-тайма, то это хорошая возможность сделать это, мы ж программисты! На рисунке синтаксис Кубика в BNF нотации, ну как можно такой язык не любить?
Comment
Про базовую библиотеку расскажу немного в комментариях. Главное, что все библиотеки завтиповых языков похожи на блевотину, отчасти из-за того, что слишком много людей принимают участие в написании. А поскольку завтиповая теория в своем синтаксисе недалеко от лиспа ушла, то изоморфизмов много, и написать одно и то же можно миллионами способов, понятное дело, что большинство из них — говно. ‎· горячая сучка, на пенсии ‎· 1
Comment
Вообще такой коиндуктивный процесс есть у нас смоделированый на PTS с экстрактом в Erlang, но это другая базовая библиотека и другой язык, будет возможно отдельным постом. Это язык ОМ с которого началось мое путешествие в академию! В нем нет в основе ничего кроме Пи-типа и бесконечного количества вселенных, но при этом в нем дерайвабл бесконечный ввод-вывод, сигма типы и индуктивные типы, но без индукции (зачем она нужна в рантайме-то, но если нада, то можно добавить селф-типы одним уравнением). ‎· горячая сучка, на пенсии
Avatar for 5ht
В Олюдениз не поедем, хотя там хорошо (тем, что все пенсионеры, и это не ирония), но не топчик. Я вот 2 года в Стамбуле прожил и полюбил турков. Предлагайте варианты на лазурном берегу или в Италии, так чтобы домик на отшибе в виде старого отеля с хорошей кухней, желательно Мишлен. А пока фоточки прошлого Олюдениза.
В Олюдениз не поедем, хотя там хорошо (тем, что все пенсионеры, и это не ирония), но не топчик. Я вот 2 года в Стамбуле прожил и полюбил турков. Предлагайте варианты на лазурном берегу или в Италии, так чтобы домик на отшибе в виде старого отеля с хорошей кухней, желательно Мишлен. А пока фоточки прошлого Олюдениза.
Comment
//потирает ушибленное на бабадаге колено// Ну, далеко не все пенсионеры, особенно в это время года. ‎· ulidkovod ‎· 3
Comment
министерство здравоохранения предупреждает: спорт опасен для вашего здоровья! ‎· горячая сучка, на пенсии ‎· 1
1 2 3 4 5 6 7 8 9 10

2015-2018 Mokum.place