AG
вот quotient типы/коуравнители, которые выше упоминали, это в точности про решение проблемы удобного определения класса эквивалентности
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 23
NR
Да я уже вижу все эти слова в статье. Может даже разберусь.
AG
посмотрите магистерскую работу кидни, там вроде неплохо расписана теория и практика нетривиальная
NR
Посмотрю. Спасибо.
SF
Ну квошенты и без HoTT можно ворочать
SF
В Lean вот есть, только с вычислимостью проблемы
AG
я поэтому и написал "удобного"
NR
Но день уже прошёл не зря)
SF
Ну в Lean с квошентами весьма удобно работать, особенно если не думать о вычислимости
SF
И если вспомнить про setoid hell
SF
Так-то целое CTT надо, чтобы всё считалось нормально
AG
ок, "удобно и без хаков"
SF
Ну это не хак там
SF
Просто свойства плохие
AG
насколько я знаю в лине сломали subject reduction чтобы квошенты работали
SF
Да, сломали
AG
ТК в смысле инфинити-категории?
MT
В смысле поиска решений в других доменных областях для применения в интересующей. Как средство описания и манипулирования "знаниями". Но "я не настоящий сварщик"...
DK
отмену по HoTT необходимости всяких аксим как оценить? мне кажется именно то важное, чего не хватало остальным основаниям.
NR
Не очень понял. В чем преимущество отсутствия аксиом?