s
Для них нужны higher inductive types.
Size: a a a
2021 April 29
EL
Спасибо!
s
На самом деле, проблемы уже начинаются при попытке выразить целые числа как индуктивный тип.
AG
функция это базовый тип коданных, т.е. потребителей, список это базовый тип полиморфных индуктивных данных, т.е. производителей
AG
в идеале вам нужны в системе и потребители, и производители, чтобы запустить вычисление
AG
либо в явном виде, либо вшитые
AG
в этом изящество теории типов - там в основу кладется принцип что для каждого типа есть канонический набор производителей и потребителей
EL
Сахар с сигмой это в агде?
AG
на такой "фундаментальный набор" претендуют гомотопические теории типов
s
Вот, кстати, подробнее про целые числа.
AG
ну на практике проблемы с целыми числами не такие уже большие, настоящие проблемы начинаются при работе с конструкциями, требующими постоянной перенормализации, например рациональными числами :)
s
Ну целые числа это самое введение в боль, когда же рациональные это уже продвинутый уровень.
B
What
Вообще-то пишется так:
Qx:P(x)
либо
Qx.P(x)
либо
Qx(P(x))
где Q — это некоторый квантор
в простейшем случае (буквально как выше) можно опустить '(x)'
Вообще-то пишется так:
Qx:P(x)
либо
Qx.P(x)
либо
Qx(P(x))
где Q — это некоторый квантор
в простейшем случае (буквально как выше) можно опустить '(x)'
B
Вот здесь всё плохо с нотацией, так не пишут
B
Вот так пишут
EL
ага, только у тебя в нотации нет места для условия (их может быть и несколько)
B
Там, где не важна последовательность кванторов, можно записать так: Q¹x, Q²x, ...