AB
Бренор пройди на dxdy.ru со своими сентенциями, там тебе математики пояснят и по понятиям и по определениям.
Size: a a a
2021 April 27
B
Ну ты сам пройди и напиши про противоречия и аксиому пустого множества. Гарантирую, что в пургаторий улетит сразу, как будет написано.
s
Самое забавное, что он даже в каком-то смысле прав: пустое множество это аналог ⊥. Но противоречие это не само ⊥, а значение типа ⊥.
B
Это работает только при введении соответствия между теорией множеств и теорией типов, но очевидно, что аксиома пустого множества никак не связана с противоречиями даже при введении.
s
Это соответствие называется теорией категорий.
B
Теория категорий — это просто одна из теорий
B
С тем же успехом можно проводить соответствие между теорией категорий и теорией множеств в терминах теории типов и так далее
s
Переизобретая в процессе категорные понятия?
B
Или можно сразу взять классическую теорию категорий, где категории определяются в терминах множеств
B
(неклассическим в этом смысле будет подход Ловера и его категориальная логика)
B
Хотя, наверное, в более широком понимании классики и то, и то — классика, только одна более классика, чем другая
s
В ещё более широком понимании, смысл математики важнее, чем её основания.
AK
Коллеги, я еще раз напоминаю, что теоркат и прочие математические дисциплины без конкретного применения к компиляторостноению являются оффтопом
s
В качестве оснований можно брать хоть множества, хоть HoTT, хоть вообще какую-нибудь дикую экзотику.
B
Да
Просто оказалось в ходе актуальных разработок, что нужно ещё механизировать, ведь верификация в том числе математических теорем должна быть удобной, а это научились делать типами (но это не говорит о том, что принципиально можно только типами).
Просто оказалось в ходе актуальных разработок, что нужно ещё механизировать, ведь верификация в том числе математических теорем должна быть удобной, а это научились делать типами (но это не говорит о том, что принципиально можно только типами).
B
Ладно, сворачиваем.
МБ
Metamath, minlog, PX, ACL2 механизируют без типов. Но типы популярнее. Я так понимаю, потому что технически проще.
B
Тут кое-кто (некоторый Алексей или Александр) скажет, что metamath — это ад
B
И что механизация — это, я думаю, он так скажет, не просто про то, что проверяется на компьютере, а то, что также, дополнительно, в нужной степени автоматизируется.
AT
Compositionality и всякое такое. Теории типов обычно сразу так строятся, а остальные — нет.