These are chat archives for groupoid/exe

11th
Feb 2016
Zeit Raffer
@zraffer
Feb 11 2016 06:56
нормально - первый вариант (тип с лямбдой - это не тип, а зав.тип, его непосредственно в типизации использовать нельзя)
только это еще не группоид, а его носительно - инфинити-граф, оно же глобулярное множество
а про группоиды мы начали с НИванычем в последнем посте в комьюнити обсуждать
Namdak Tonpa
@5HT
Feb 11 2016 06:56
а запиши плиз групоид )
Zeit Raffer
@zraffer
Feb 11 2016 06:57
"реши мне теорему ферма" ))
Namdak Tonpa
@5HT
Feb 11 2016 06:57
а что в Lean нет?
это же должно быть в HoTT библиотеке вроде
Zeit Raffer
@zraffer
Feb 11 2016 06:57
www.cs.nott.ac.uk/~psztxa/publ/omega.pdf
я не смотрел всю НоТТ библиотеку, но вообще в НоТТ группоид описывать нет необходимости, там каждый объект бесплатно является группоидом
Namdak Tonpa
@5HT
Feb 11 2016 06:58
ну тех версиях которая на групоидах строится, а не на симплициальных множествах
ага, ну я счас такое читал как раз
Zeit Raffer
@zraffer
Feb 11 2016 07:00
ну то есть эту тему сейчас копают, но простых решений нету
Namdak Tonpa
@5HT
Feb 11 2016 07:00
ну групоид в любом случае будет зависимым рекурсивным коиндуктивным типом
Zeit Raffer
@zraffer
Feb 11 2016 07:01
да, еще один слой поверх существующих (ко)индуктивных типов - т.е. сложность повышается
а эти люди из традиционных подходов просто добавляют аксиомы Воеводского и получают НоТТ
им не надо описывать группоид
Namdak Tonpa
@5HT
Feb 11 2016 07:02
ну мы же отказались от всех аксиом )
Zeit Raffer
@zraffer
Feb 11 2016 07:03
каждый выбор дает свои последствия
Namdak Tonpa
@5HT
Feb 11 2016 07:03
я эту версию групоида из Lean украл кстати
я просто попробовал переписал в EXE по аналогии с Infinity Graph и Setoid
Zeit Raffer
@zraffer
Feb 11 2016 07:06
ааа! а я искал по *.lean и не нашел
Namdak Tonpa
@5HT
Feb 11 2016 07:06
надо просто поправить, чтобы было похоже на правду в EXE
я читал что Воеводский сначала сделал теорию на групоидах
а потом типа сложно выходило и он показал как HoTT можно на симплициальных множествах сделать
Zeit Raffer
@zraffer
Feb 11 2016 07:08
ну это самый классический подход, но у него тоже лейтмотив - все упрощать
Namdak Tonpa
@5HT
Feb 11 2016 07:08
но "сложно выходило" — это я так понимаю слабая поддержка зависимых рекурсивных коиндуктивных в пруверах :-)
Zeit Raffer
@zraffer
Feb 11 2016 07:08
мы же это с НИванычем как раз обсуждали
"сложно" даже в том смысле, что сложно укладывается в голову техническая часть (при простой идеологической)
Namdak Tonpa
@5HT
Feb 11 2016 07:09
групоиды это типа стримов, только вместо вычислений пути
Zeit Raffer
@zraffer
Feb 11 2016 07:09
равенства на равенствах
ну вобщем да
Namdak Tonpa
@5HT
Feb 11 2016 07:10
вообще я смотрю на космический куб и понимаю что действительнось состоит из моноидов (категорий, для вычислений) и групоидов (для ризонинга).
надо разобраться только с осями :-)
Zeit Raffer
@zraffer
Feb 11 2016 07:12
там еще есть работы мистера Lurie (Лури, Лурье) - книжки по тысяче страниц, все про (инф,1)-топосы (т.е. очень близкая тема) - он использовал сначала квазикатегории (как раз на симплициальных множествах основанный подход), потом не знаю, не читал уже, слишком много страниц; он сейчас главный классик, и ему пару лет назад дали премию на миллион денег (но не дали Филдса, из-за чего были бурления); так что если идти через симл.множ, то можно еще глянуть его.
Namdak Tonpa
@5HT
Feb 11 2016 07:14
я думаю что ничего технически сложного в групоидах нет
Zeit Raffer
@zraffer
Feb 11 2016 07:14
"действительнось состоит..." - Гротендик гордился тем, что по его мнению, его математика никакого отношения к действительности не имеет и применения никогда не найдет :)
Namdak Tonpa
@5HT
Feb 11 2016 07:14
по крайнер мере читая groupoid.hlean :-)
хочется идти через групоиды, а не через симл.множ
у нас же Groupoid Infinity :-)
тем более что в космическом кубе именно они )
надо cosmic-cube.com тоже зарегать )
Zeit Raffer
@zraffer
Feb 11 2016 07:16
пока что простых инф-группоидов никто не видел, самое простое - это аксиоматический подход НоТТ; в Леан описан 1-группоид, потому он и простой )))
Namdak Tonpa
@5HT
Feb 11 2016 07:17
ну так еще зациклить как инфинити граф да и все
Zeit Raffer
@zraffer
Feb 11 2016 07:17
вот последняя статья Тома Лейнстера и Евгении Чень очень интересная, надо реализовать и сравнить по сложности с тем, что у Альтенкирка
т.е. все копают в сторону упрощения этой науки, а начал все опять же Гротендик: https://ncatlab.org/nlab/show/tame+topology
Zeit Raffer
@zraffer
Feb 11 2016 07:21
не ну это "высокая наука", но с точки зрения топологии они и "группоидисты" заняты примерно одинаковым упрощением, переходу от пространства из точек к более "ручным" структурам (tame)
Namdak Tonpa
@5HT
Feb 11 2016 07:24
нашел вашу ветку с ниванычем
я ж как раз на лыжах был
Насчёт огромной инженерной сложности, ну это точно не так.
Zeit Raffer
@zraffer
Feb 11 2016 07:25
кстати про " quantifier elimination", который в википедии упоминается, это надо зафиксировать в уме как еще один идеологический момент, близкий ТК, - в идеале ТК-утверждения не должны требовать кванторов вообще, все должно выражаться функторами и морфизмами, все кванторы должны убираться в их аргументы (чего-то меня с утра прёт :) )
Namdak Tonpa
@5HT
Feb 11 2016 07:25
тут я соггласен, инфинити групоид без теорем будет компактным как и сетоид
Zeit Raffer
@zraffer
Feb 11 2016 07:25
"ну это точно не так" сказал, а потом ничего простого не предложил, ага )
Namdak Tonpa
@5HT
Feb 11 2016 07:26
ну он просто об этом не думает
хорошо вот у нас скажем есть 1-групоид
record Groupoid :=
         (ob: *)
         (hom: λ (a,b: ob) → Hom (a,b) → Groupoid)
как его превратить в infinity ?
я так чисто исхожу из комбинаторного синтаксиса )
Zeit Raffer
@zraffer
Feb 11 2016 07:29
ну на мой взгляд это еще не 1-группоид, это инф-граф - у него есть морфизмы всех размерностей, но не заданы никакие операции; нужно добавить операции и операции на операциях.
а где ты говоришь, что писал на основе Леан, я там такого как утебя не вижу
hott/algebra/category/groupoid.hlean
Zeit Raffer
@zraffer
Feb 11 2016 07:32
ну так там прекатегория это ((hom : ob → ob → Type)) плюс операция обращения морфизма (@is_iso ob parent a b f)
не, там просто 1-группоид
а у тебя инф-граф, глобулярное множество
вот если их скрестить
то получится то, что нам надо
Namdak Tonpa
@5HT
Feb 11 2016 07:33
ну первые два параметра такие как у сетоида
я думал что их скрестил :-)
инфинити граф и сетоид
Zeit Raffer
@zraffer
Feb 11 2016 07:34
умножение, обращение, ассоциативность, когеррентность
это операции
Namdak Tonpa
@5HT
Feb 11 2016 07:34
ну надо добавить, но структура же в ob и hom хранится
Т.е. технически никаких проблем
Zeit Raffer
@zraffer
Feb 11 2016 07:35
ну вот можешь посмотреть в процитированных статьях, как добавляют; проблем, кроме того, что это надо делать поверх индуктивных типов, и это немного громоздко, никаких
я просто помню, что у нас был вначале принцип - все сервера на 20-30 строчек :)
а тут...
Namdak Tonpa
@5HT
Feb 11 2016 07:36
я просто сетоид тоже цитирую без операций, это тоже неверно ))
record Setoid :=
         (ob: *)
         (hom: ∀ (X,Y: ob) → Hom (X,Y))
Zeit Raffer
@zraffer
Feb 11 2016 07:36
вместо лямбды квантор
Namdak Tonpa
@5HT
Feb 11 2016 07:36
исправил на странице
ты туда иногда подглядывай )
чтобы открытой ахинеи небыло
Zeit Raffer
@zraffer
Feb 11 2016 07:37
значения будут с лямбдой, а тип с квантором )
Namdak Tonpa
@5HT
Feb 11 2016 07:46
Я хочу расположить типы на странице http://groupoid.co/exe.htm таким образом, чтобы если создать курс, который детально объясняет эти типы и их библиотеки полиморфных функций, то можно было бы создать непрерывный рассказ от чисел до геометрии.
В связи с чем у меня несколько вопросов. например когда мы размышляем о дискретных структурах — нам зависимые типы не нужны, они начинают нам быть нужны когда мы размышляем о континууме, например хотим извлечь корень n-й степени. Такие зависимые типы нам достаточно иметь индуктивные, они выкалывают точки на каком-то многообразии, в даном случае на кольце. Таким образом у меня вопрос: что "выкалывают" (или что они там делают) коиндуктивные зависимые типы?
Namdak Tonpa
@5HT
Feb 11 2016 08:31
или типа индуктивные для сингулярностей, а коиндуктивные для гладких многообразий?
Namdak Tonpa
@5HT
Feb 11 2016 08:58
    I := #identifier

    O := * | OO |
         □ | I : O |
         ∅ | O   O | λ O |
         I | ( O ) | ∀ O |

    E := ∅ | E <data|record> O := O
вроде компактней нельзя :-)
можно еще := убрать: E := ∅ | E <data|record> O просто
если параметры как в Lean группировать, то разделитель нада полюбому
Namdak Tonpa
@5HT
Feb 11 2016 09:04
ну это не синтаксис, а набор парсеров, но ними можно синтаксис распарсить
набор конструкторов
Namdak Tonpa
@5HT
Feb 11 2016 09:24
  data om: * := 
       (nil: () → om)
       (star: () → om)
       (box: () → om)
       (var: name → om)
       (app: om → om → om)
       (arrow: name → om → om → om)
       (pi: name → om → om → om)
       (scope: om → om)

  data exe: * := 
       (record: name → om → om → exe)
       (data:   name → om → om → exe)
Zeit Raffer
@zraffer
Feb 11 2016 09:25
сейчас вчитаюсь
Namdak Tonpa
@5HT
Feb 11 2016 09:25
можешь ревьюить прямо на гитхабе :-)
Zeit Raffer
@zraffer
Feb 11 2016 09:26
это на гитхаб-репе сайта?
Namdak Tonpa
@5HT
Feb 11 2016 09:26
ага, только в ветке gh-pages, а не master
там же на гитхабе можно коментить коммиты
но это обычно между командами
так то зачем :-)
Namdak Tonpa
@5HT
Feb 11 2016 09:36
при чем эти конструкторы можно облегчить, например достаточно чтобы у всех был только один параметр om: record: om → exe а остальное конструировать из var и app.
типа такого: Arrow (App (App Var Om) Om)
тогда app: om → om → om остается, а стрелки можно arrow: om → om
это если мы хотим суперминимализм, но я думаю после редукций оно может само сократится.
Zeit Raffer
@zraffer
Feb 11 2016 09:47

последовательно

"или типа индуктивные для сингулярностей, а коиндуктивные для гладких многообразий?"
вот это близко к правде - действительные числа (отрезок [0,1]) можно задать как коиндуктивный тип
зав.типы, если отвлечься от всяких векторов и необходимости нассмотрения зав.рекордов (сигма-тип) и квантора всеобщности (пи-тип) - которыми мы уже вовсю пользуемся - нужны для самой логики, как предикаты. например, черч дает нам прямое произведение (вроде гипер-параллелепипеда), а я в нем вырезаю предикатом предел (допустим, "круглую", вписанную в этот параллелепипед, точку). вот такие образы.
если мы хотим остановиться на коиндуктивных зависимых более подробно, то надо просто представить достаточно общий полиномиальный функтор на слайс-категории, и посмотреть, как меняется терминальная алгебра при смене функтора - такая медитация (у меня готовых образов для этого нет, надо подумать и "родить")

Zeit Raffer
@zraffer
Feb 11 2016 09:53
шото меня "суперминимализм" в конструкторах AST не прёт - в исходном виде у нас было однозначное соответствие с грамматикой, а так у нас деревья могут быть "лишние", недопустимые, и это как-то отдельно надо проверять при паттерн-метчинге. разве это минимализм? вобщем, если ты писал парсеры в таком же стиле раньше, то может оно как-то оправдано для этого стиля, но мне кажется концептуальным усложнением (то, что AST не соответствует грамматике)
Namdak Tonpa
@5HT
Feb 11 2016 10:33
Ну это только в BNF нотации надо пофиксать.
Zeit Raffer
@zraffer
Feb 11 2016 10:35
да ради бога, я просто ворчу )