s
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 23
NR
Я не настоящий сварщик. Никак не определяю.
NR
Спасибо
AC
Тогда у Вас и проблемы такой нет! 😃
s
Вот ещё про целые числа: https://arxiv.org/abs/2007.00167
MT
Да, похоже это начало того что надо.
NR
Наверное в одиночку я это не пойму. С другой стороны могу же в этом чате спрашивать?
[
Обычно это
data Nat = Z | S Nat
data Int = Negative Nat | Pozitive Nat
data Nat = Z | S Nat
data Int = Negative Nat | Pozitive Nat
SF
Можно определить целые числа как петли на окружности, тогда ассоциативность сложения индукцией по путям тривиально докажется
SF
Обычно ассоциативность сложения целых чисел неприятно доказывать
NR
Такое я слышал, да.
AG
тут возникает проблема с двумя нулями
AG
пример нетривиального приложения хотта с программированием и пруфами можно глянуть например в https://doisinkidney.com/pdfs/masters-thesis.pdf
AG
там конструируется по шагам удобное определение конечности типа и потом поверх этого строится алгоритм перебора, которым можно решать комбинаторные задачи
NR
Кстати вот в статье что выше скинули приведён пример определения именно такой как я в детстве об этом думал. Более умными словами конечно. Целые числа как классы эквивалентности разностей натуральных.
SF
Там простой трюк для доказательства коммутативности сложения тоже есть, кстати
NR
Определение через петли в общем то тоже к этому сводится.
AC
Забавно, я "с детства" цетые понимал примерно так же как https://t.me/typeslife/14038 😊