> Для конструирования моделей используется теория множеств, точнее два семейства теорий множеств
Любопытно, а почему не теоркат или какой-то из вариантов теории типов? И почему именно эта аксиоматика, а не NBD например? Так просто привычнее или ZFC(n)/CZF(n) позволяют получить результаты, принципиально недостижимые с помощью теории типов и проч.?
1) Потому что для конструирования моделей сперва используются теории, в которых все уверены и сила которых откалибрована за многие десятилетия. И уже потом можно для других целей использовать другие теории.
2) Почему NBG, а не ZFC? На самом деле NBG консервативна относительно ZFC, так что это “та же” аксиоматика.
3) Конструирование моделей внутри самих теорий типов - отдельная отросль, и собственно модель кубической теории типов BCH была (на языке NuPRL) построена в экстенциональной теории типов. Ну и сейчас несколько групп независимо ведёт работу по такому общему фреймворку, чтобы было удобно строить модели самых разных теорий типов в рамках некоторой удобной фиксированной теории типов (по выразительности между HoTTMin и HoTTMax(1)), и доказывать с комфортом всякие их свойства. Вот самый сок: http://www.cs.cmu.edu/~cangiuli/papers/xtt.pdf... )
Большой спасибо за ссылки. А есть некий обзор/ликбез современного состояния теорий типов (зависимые, экстенсиональные, кубические, интенсиональные...) и того, как они применяются (Coq, Agda, NuPRL, RedPRL...)?
В стародавние времена у нас матан начинался как раз с теории множеств и ZFC. Интересно, будет-ли в будущем использоваться та же XTT в качестве базиса. А может где-то уже так преподают?
1) Область настолько динамично развивается, что up-to-date обзора в целом нет.
2) Я думаю, рано или поздно теория типов войдёт в стандартную математическую программу, но сейчас до этого далеко. Для начала там должно всё стабилизироваться и должны выйти реально удобные и обкатанные инструменты (мы в JetBrains вот работаем над языком https://github.com/JetBrains/Arend, майкрософт на Lean, люди развивают Cubical Agda и Coq, RedPRL, но все они пока не идеал).
Теорий типов и вправду так много, что не знаешь, за что хвататься на почитать в первую очередь :) Поищу статьи аспирантов, работающих в этой теме - должны же они обзор литературы и публикаций делать.
> должно всё стабилизироваться и должны выйти реально удобные и обкатанные инструменты К сожалению далёк от автоматического доказательства теорем- что именно (для ZFC или NBD) считается обкатанным инструментом? В смысле "когда RedPRL станет столь же удобен как ХХХ, то можно считать, что лежащае в основе RedPRL теория типов применима в учебном процессе" - что здесь будет ХХХ?
И ещё про формальные методы - model checking типа TLA+ как-то связан с теориями типов или это совершенно ортогональные вещи?
Кстати, расскажи коллегам про spdx дот org - репозитарий без лицензии сейчас смотрится несколько непрофессионально.
> К сожалению далёк от автоматического доказательства теорем- что именно (для ZFC или NBD) считается обкатанным инструментом?
Бумажка с ручкой. Шучу. Нет, на самом деле для них есть Mizar, но в целом там всё чудовищно неудобно. Основной плюс теорий типов (причём именно HoTT, т.е. теории типов, где утверждения тривиально переносятся вдоль изоморфизма объектов) в том, что начинает быть удобно, и только этим и можно привлечь людей к тому, чтобы овладеть теориями типов.
> ещё про формальные методы - model checking типа TLA+ как-то связан с теориями типов или это совершенно ортогональные вещи?
Пока ортогональные, но над удобным конструктивным аналогом TLA+ работают.
Работы ведутся главным образом людьми по имени D. Spivak и P. Schultz с одной стороны (разные варианты Temporal Type Theory) и Stephan Merz с другой стороны (развитие и модификация TLA+ в сторону большего удобства). Вообще TLA+ это же просто комбинирование стандартной теории множеств с логикой TLA, чтобы получился язык спецификаций. Но TLA можно попробовать скомбинировать не с теорией множеств, а теорией типов (потому что ZFC во-первых нетипизирована, во-вторых overkill, в третьих доказывать там что-то компьютерно-проверябельно жесть как неудобно), той же HoTT. Stephan Merz некогда развил логику TLA, обобщение получилось удобным и аксиоматизируется поэлегантнее чем исходная TLA - называется TLA*. А потом он занимался проектами Isabelle/TLA* и Isabelle/TLA+ - реализацией этих штук поверх провера Isabelle. Чтобы практически удобно было применять, хочется помощи со стороны SAT/SMT-солверов и арифметических солверов, с этой целью он разработал полутипизированный вариант Isabelle/TLA+ и провёл ещё много всякой такой работы
( ... )
Любопытно, а почему не теоркат или какой-то из вариантов теории типов? И почему именно эта аксиоматика, а не NBD например?
Так просто привычнее или ZFC(n)/CZF(n) позволяют получить результаты, принципиально недостижимые с помощью теории типов и проч.?
Reply
2) Почему NBG, а не ZFC? На самом деле NBG консервативна относительно ZFC, так что это “та же” аксиоматика.
3) Конструирование моделей внутри самих теорий типов - отдельная отросль, и собственно модель кубической теории типов BCH была (на языке NuPRL) построена в экстенциональной теории типов. Ну и сейчас несколько групп независимо ведёт работу по такому общему фреймворку, чтобы было удобно строить модели самых разных теорий типов в рамках некоторой удобной фиксированной теории типов (по выразительности между HoTTMin и HoTTMax(1)), и доказывать с комфортом всякие их свойства. Вот самый сок: http://www.cs.cmu.edu/~cangiuli/papers/xtt.pdf... )
Reply
В стародавние времена у нас матан начинался как раз с теории множеств и ZFC. Интересно, будет-ли в будущем использоваться та же XTT в качестве базиса. А может где-то уже так преподают?
Reply
2) Я думаю, рано или поздно теория типов войдёт в стандартную математическую программу, но сейчас до этого далеко. Для начала там должно всё стабилизироваться и должны выйти реально удобные и обкатанные инструменты (мы в JetBrains вот работаем над языком https://github.com/JetBrains/Arend, майкрософт на Lean, люди развивают Cubical Agda и Coq, RedPRL, но все они пока не идеал).
Reply
Поищу статьи аспирантов, работающих в этой теме - должны же они обзор литературы и публикаций делать.
> должно всё стабилизироваться и должны выйти реально удобные и обкатанные инструменты
К сожалению далёк от автоматического доказательства теорем- что именно (для ZFC или NBD) считается обкатанным инструментом? В смысле "когда RedPRL станет столь же удобен как ХХХ, то можно считать, что лежащае в основе RedPRL теория типов применима в учебном процессе" - что здесь будет ХХХ?
И ещё про формальные методы - model checking типа TLA+ как-то связан с теориями типов или это совершенно ортогональные вещи?
Кстати, расскажи коллегам про spdx дот org - репозитарий без лицензии сейчас смотрится несколько непрофессионально.
Reply
Бумажка с ручкой. Шучу. Нет, на самом деле для них есть Mizar, но в целом там всё чудовищно неудобно. Основной плюс теорий типов (причём именно HoTT, т.е. теории типов, где утверждения тривиально переносятся вдоль изоморфизма объектов) в том, что начинает быть удобно, и только этим и можно привлечь людей к тому, чтобы овладеть теориями типов.
> ещё про формальные методы - model checking типа TLA+ как-то связан с теориями типов или это совершенно ортогональные вещи?
Пока ортогональные, но над удобным конструктивным аналогом TLA+ работают.
Reply
Очень интересно. Александр, не знаете ли вы название "удобного конструктивного аналога TLA+" над которым ведется работа?
Reply
Reply
Leave a comment