МБ
Ай! Блин. Всё-равно бредово звучит. Если стрелки - это термы, то почему они равны, если термы разные? Значит, мы рассматриваем классы эквивалентности?
Size: a a a
2019 October 30
МБ
Вот если бы стрелка была функцией, которую задаёт терм... Тогда, было бы проще думать.
NI
Ай! Блин. Всё-равно бредово звучит. Если стрелки - это термы, то почему они равны, если термы разные? Значит, мы рассматриваем классы эквивалентности?
;-) Есть такая сложность в определении равенства.
Для языков с зависимыми типами, классическая.
А для гомотопических типов, два раза классическая ;-)
Для языков с зависимыми типами, классическая.
А для гомотопических типов, два раза классическая ;-)
NI
Вот если бы стрелка была функцией, которую задаёт терм... Тогда, было бы проще думать.
Можно экстенсионально определить ;-)
МБ
Можно экстенсионально определить ;-)
Можно ли считать, что это экстенсиональное определение и есть понятие "computation"? Ну, как преобразование входа к выходу алгоритма?
NI
Наверное, можно...
Но я не вижу, почему навроде "observational" тоже нельзя так назвать ;-)
Но я не вижу, почему навроде "observational" тоже нельзя так назвать ;-)
NI
Можно ли считать, что это экстенсиональное определение и есть понятие "computation"? Ну, как преобразование входа к выходу алгоритма?
Наверное, наиболее практичным будет сравнивать нормальные формы, если они существуют.
МБ
Наверное, можно...
Но я не вижу, почему навроде "observational" тоже нельзя так назвать ;-)
Но я не вижу, почему навроде "observational" тоже нельзя так назвать ;-)
Я пока хочу разобраться с computation, которое как-то связывают с этой самой
lambda. Видимо, наверное, можно и иначе это всё описывать. Вроде, стало чуть понятнее.МБ
Наверное, наиболее практичным будет сравнивать нормальные формы, если они существуют.
Для практики, наверное, можно использовать NbE-техники. Что, видимо, уже все делают для зав. типов. Но, семантически, ведь, установление равенства через нормальные формы означает и равенство экстенсиальное, как функций, которые эти нормальные формы задают, если их начать применять к аргументам.
NI
Для практики, наверное, можно использовать NbE-техники. Что, видимо, уже все делают для зав. типов. Но, семантически, ведь, установление равенства через нормальные формы означает и равенство экстенсиальное, как функций, которые эти нормальные формы задают, если их начать применять к аргументам.
Но мы не можем доказать экстенсиональное равенство.
МБ
Но оно же, видимо, должно следовать из интенсионального?
NI
Но оно же, видимо, должно следовать из интенсионального?
Мож туплю, но не вижу, как.
А вот если задать аксиомой, то не должно быть противоречия.
А вот если задать аксиомой, то не должно быть противоречия.
Oℕ
наоборот
МБ
Может, это я туплю. Интенсиональное - это (верно понимаю?), то, что определяется конструкцией терма? Если мы доказали, что два терма синтаксически имеют одну нормальну форму, то и как функции (экстенсионально) они должн быть равны. Не так?
Oℕ
нет
МБ
А как?
Oℕ
равенство термов по конструкции - это экстенсиональное
Oℕ
а когда равенство определяется через какой-то индуктивный тип или элиминатор, отдалённо напоминающий принцип Лейбница - интенсиональное
KV
а когда равенство определяется через какой-то индуктивный тип или элиминатор, отдалённо напоминающий принцип Лейбница - интенсиональное
А можно сурс, откуда такие определения?
Oℕ
есть функциональная экстенсиональность