These are chat archives for groupoid/exe

9th
Aug 2016
Namdak Tonpa
@5HT
Aug 09 2016 09:03
классная статья, жалко раньше не видел
NuPRL, 1988
Namdak Tonpa
@5HT
Aug 09 2016 09:09
все таки склоняюсь к тому, что в статье надо сначал ТТ главу давать, а потом уже семантику CT
Zeit Raffer
@zraffer
Aug 09 2016 09:28
нормально
ты просто различай
Namdak Tonpa
@5HT
Aug 09 2016 09:29
нормально NuPRL или моя идея начинать с TT ?
Zeit Raffer
@zraffer
Aug 09 2016 09:29
аксиоматику ТК и семантику ее в ТТ
твоя
Namdak Tonpa
@5HT
Aug 09 2016 09:29
я хочу начать с Natural Deduction потом зависимая теореия потом теория категория потом кодировка
и для каждого этапа три варианта картинок 1) правилы вывода 2) комутативные диаграми 3) код на EXE
Zeit Raffer
@zraffer
Aug 09 2016 09:30
не заебешся? ))
Namdak Tonpa
@5HT
Aug 09 2016 09:30
тогда все выстраивается в цельную картину
Zeit Raffer
@zraffer
Aug 09 2016 09:31
рисуй, конечно, но тебе же работы больше будет
Namdak Tonpa
@5HT
Aug 09 2016 09:31
ну я уже заебался на этапе подачи документов :-)
уже хочу бросить аспирантуру )
Zeit Raffer
@zraffer
Aug 09 2016 09:31
ого
Namdak Tonpa
@5HT
Aug 09 2016 09:31
гг
но когда дышат в спину и требуют, лучше работается
Zeit Raffer
@zraffer
Aug 09 2016 09:31
тяжело снаружи поступать наверное
я типа просто "остался" на кафедре
я в магистратуре на полставки инженером работал
там же
Namdak Tonpa
@5HT
Aug 09 2016 09:32
но главное что за эти 9 месяцев вера в нашу работу и дозировки счастья только усилились
Zeit Raffer
@zraffer
Aug 09 2016 09:32
чья вера? твоя?
Namdak Tonpa
@5HT
Aug 09 2016 09:32
ага
вера в Групоид Инфинити )
Zeit Raffer
@zraffer
Aug 09 2016 09:33
ну результата уже как бы нарисовывается, еще чуть-чуть...
Namdak Tonpa
@5HT
Aug 09 2016 09:33
ладно, раз ты одобряешь я тогда поменяю главы TT и CT местами
будет новый учебник по языку пространства
Zeit Raffer
@zraffer
Aug 09 2016 09:34
про ТК должно быть две главы. ее аксиомы как формальнйо системы и ее реализация в ТТ=ЕХЕ
Namdak Tonpa
@5HT
Aug 09 2016 09:34
а что паралельно нельзя ?
правила вывода и тут же код на EXE их повторяющий
Zeit Raffer
@zraffer
Aug 09 2016 09:35
надо чтобы читатель мог зафиксировать в сознании отдельно то и это
Namdak Tonpa
@5HT
Aug 09 2016 09:35
как вот в этой статье CTMLTT
ну параграф 1 пункт А и Б и С
Zeit Raffer
@zraffer
Aug 09 2016 09:35
та статья написана для людей которые уже понимают и про ТТ и про ТК ) а ты пишешь типа с нуля
Namdak Tonpa
@5HT
Aug 09 2016 09:35
комутативные диаграмы, правила вывода и код на EXE
ну вот с нуля чтобы писать надо сначала объяснить правила вывода, так как это самый простой способ бустрапа
Zeit Raffer
@zraffer
Aug 09 2016 09:36
ага
Namdak Tonpa
@5HT
Aug 09 2016 09:36
иначе не получается красиво забутсрапится
если с ТК начинать начинаются проблемы :-)
Zeit Raffer
@zraffer
Aug 09 2016 09:36
какие проблемы
Namdak Tonpa
@5HT
Aug 09 2016 09:37
что категорию два раза придется описывать, как НАЧАЛО и потом на категорном языке себя же
не очень красиво
Zeit Raffer
@zraffer
Aug 09 2016 09:38
мне кажется мы сейчас друг друга не понимаем
пиши как ты видишь )
Namdak Tonpa
@5HT
Aug 09 2016 09:38
ну мы согласны двоем что начинать с правил вывода проще для максимального покрытия для любого народа, в том числе математиков СССР и как пребываение в контексте логики и пруверов
Zeit Raffer
@zraffer
Aug 09 2016 09:38
да
Namdak Tonpa
@5HT
Aug 09 2016 09:39
ну вот это главная мысль
остальное технические детали
Namdak Tonpa
@5HT
Aug 09 2016 13:48
на реддите наш вброс минусуют, бляди :-)
Zeit Raffer
@zraffer
Aug 09 2016 13:50
z db;e nfv +10
я вижу там +10
Namdak Tonpa
@5HT
Aug 09 2016 13:50
оно прыгает, но точно вижу что минусуют!
я видел 15
Zeit Raffer
@zraffer
Aug 09 2016 13:51
это конкурренты
Namdak Tonpa
@5HT
Aug 09 2016 13:51
андромедане )
Zeit Raffer
@zraffer
Aug 09 2016 13:51
ага
Namdak Tonpa
@5HT
Aug 09 2016 13:52
заврапил твой пост ;-)
envelope )
Zeit Raffer
@zraffer
Aug 09 2016 13:52
в смысле своим постом?
Namdak Tonpa
@5HT
Aug 09 2016 13:52
ага, обрамил
Zeit Raffer
@zraffer
Aug 09 2016 13:53
я обратил внимание, что на прошлой неделе написал кучу термов с лямбдами и кванторами, а в течение недели они испарились, и остался код со скобочками
само получилось
Namdak Tonpa
@5HT
Aug 09 2016 13:54
ну квантор оставется только один в начале теоремы
все остальное в LISP превращается, да
Namdak Tonpa
@5HT
Aug 09 2016 14:59
AUTOMATH:
text ← | text item | text ‘;’
item ← ‘+’ IDENT | ‘+’ ‘*’ IDENT | ‘-’ IDENT | ‘--’
| STAR | sym STAR
| IDENT ASSIGN EB SEMI expr | IDENT SEMI expr ASSIGN EB
| ‘[’ IDENT COMMA expr ‘]’
| IDENT ASSIGN PN SEMI expr | IDENT SEMI expr ASSIGN PN | IDENT ASSIGN noexpand expr SEMI expr
| IDENT SEMI expr ASSIGN noexpand expr noexpand ← | ‘~’
expr ← ‘TYPE’ | ‘'type'’ | ‘PROP’ | ‘'prop'’
| sym | sym ‘(’ ‘)’ | sym ‘(’ exprlist ‘)’
| ‘<’ expr ‘>’ expr | ‘[’ IDENT COMMA expr ‘]’ expr
exprlist ← expr | exprlist ‘,’ expr
sym ← IDENT | IDENT ‘"’ identlist ‘"’
identlist ← | IDENT | identlist HYPHEN IDENT EB ← ‘EB’ | ‘'eb'’ | ‘---’
PN ← ‘PN’ | ‘'pn'’ | ‘PRIM’ | ‘'prim'’ | ‘???’ STAR ← ‘*’ | ‘@’
ASSIGN ← ‘:=’ | ‘=’
SEMI ← ‘'E'’ | ‘E’ | ‘;’ | ‘:’
COMMA ← ‘,’ | ‘:’
HYPHEN ← ‘-’ | ‘.’
компактненько
Zeit Raffer
@zraffer
Aug 09 2016 15:00
это ЕХЕ?
Namdak Tonpa
@5HT
Aug 09 2016 15:00
не, в AUTOMATH не было полиномиальных функторов
поэтому AUTOMATH — это OM скорее
Zeit Raffer
@zraffer
Aug 09 2016 15:01
а, АВТОМАТ
Namdak Tonpa
@5HT
Aug 09 2016 15:01
думаю может сделать фронтенд AUTOMATH к ОМ?
Zeit Raffer
@zraffer
Aug 09 2016 15:01
ха
интересно
Namdak Tonpa
@5HT
Aug 09 2016 15:01
и с этим подкатить к барендрехту
:-)
Zeit Raffer
@zraffer
Aug 09 2016 15:02
если будут руки и время ;)
Namdak Tonpa
@5HT
Aug 09 2016 15:02
ну взять студента
Zeit Raffer
@zraffer
Aug 09 2016 15:02
вообще много фронтэндов
с любых языков
Namdak Tonpa
@5HT
Aug 09 2016 15:02
вот этот язык назову A
Zeit Raffer
@zraffer
Aug 09 2016 15:03
А (в томате).
Namdak Tonpa
@5HT
Aug 09 2016 15:06
есть два синтаксиса AUT-68, AUT-QE, будет AUT-OM
AUT-OM-ATH