Как стать автором
Обновить

Комментарии 13

Даже с простейшими градусами уже возникают проблемы: они не обязательно являются типом, возможно это просто другая форма представления, ведь 30° это тоже самое, что pi/6
В свое время увлекался темой типизации фундаментальной математики. Вот эта штука мне особенно приглянулась.
Говорить о типах в математике и не упомянуть изоморфизм Карри-Говарда и тем паче гомотопическую теорию типов это как-то… странно.

Тем более непонятен посыл статьи. Даже у меня, вроде бы знакомого с предметной областью, возникает только один вопрос: «и чо?».

В целом я нахожу привлекательной идею запилить для математиков относительно (но не полностью) формальный язык, на котором можно будет писать статьи или просто рассуждения, который не будет позволять верифицировать доказательство, но при этом позволит сколь-нибудь часто выявлять популярные виды лажи или явно сомнительные места в доказательствах.

или даже топографическое пространство

Э-э, хм-хм.

Кажется, перегрузка сбивает студентов с толку (...) иногда математические концепции перегружаются без всяких причин, кроме исторических

А если разные объекты в разных контекстах обозначаются одной и той же буквой — это перегрузка?

Говорить что объект Z имеет тип группа тоже не совсем правильно. Группа это не только множество, но и три операции (умножение, единичный элемент и обращение), и на одном и том же множестве могут быть заданы поразному. То есть тип группа имеет четверка (Z, _+_, 0, -_). А для систем, вроде Coq, в тип надо еще и доказателства свойств этих операций поместить.
Группа это не только множество, но и три операции (умножение, единичный элемент и обращение)

Зачем множить сущности? Операция одна — умножение.

Неконструктивное задание нейтрального элемента и обратного может усложнить доказательства.
Неконструктивное задание нейтрального элемента и обратного может усложнить доказательства.

Допустим, мы уже задали множество и операцию умножения. Например, я беру {0, 1, 2, 3, 4} и сложение по модулю 5 в роли *.
Как вы будете "неконструктивно" задавать нейтральный элемент? Операция * не даст выбрать что-то, отличное от 0.

В Coq мы можем описать в типе условия существования вроде (exists a: Element. b: Element -> a * b = b), но если мы попытаемся использовать конкретные свойства существующего a, кроме явно тут описанного, у нас будут проблемы. Проще указывать конкретный элемент.
Не знаю, почти все люди, что я знаю, используют термины интервал и промежуток как взаимозаменяемые. Раз 10 перечитал объяснение, пока понял, в чем дело. Тут скорее всего дело не в типах, а просто в разной терминологии, неправильной в одном случае, но тем не менее.
Дело не только в терминологии, а в принятых неявных допущениях.

[0, 1] — это замкнутый отрезок в R со стандартной метрикой. Но если брать его не в R, а в [0, 1] — он будет не только замкнутым, но еще и открытым (универсальное множество всегда открытое). То же самое будет если рассматривать его как отрезок в R, но с дискретной метрикой (в дискретных пространствах любые подмножества одновременно замкнуты и открыты).
Зарегистрируйтесь на Хабре , чтобы оставить комментарий

Публикации

Истории