Oℕ
А можно сурс, откуда такие определения?
Size: a a a
2019 October 30
Oℕ
Мне кажется, Михаил функциональную экстенсиональность спутал
IJ
Тут написано —
https://ru.wikipedia.org/wiki/Экспоненциал
Если экспоненциал zʸ существует для всех z в C, то функтор, отправляющий z в zʸ является правым сопряжённым к [_] × y.
https://ru.wikipedia.org/wiki/Экспоненциал
Если экспоненциал zʸ существует для всех z в C, то функтор, отправляющий z в zʸ является правым сопряжённым к [_] × y.
еще ссылка по теме:
https://bartoszmilewski.com/2016/04/18/adjunctions/
https://bartoszmilewski.com/2016/04/18/adjunctions/
МБ
Да, может, я вообще всё спутал. Пользуюсь тем, что extension предиката -- это множество объектов, на которых он истина. То есть, вроде как, это не определение через терм.
Oℕ
Интенциональное всегда рефлективно поэтому экстенсиональное влечёт интенсиональное
Oℕ
Обратное делается введением аксиомы К
Oℕ
Да, может, я вообще всё спутал. Пользуюсь тем, что extension предиката -- это множество объектов, на которых он истина. То есть, вроде как, это не определение через терм.
Extensional type theory denotes the flavor of type theory in which identity types are demanded to be propositions / of h-level 1. In other words, they are determined by their extensions — the collection of pairs of points which are equal.
МБ
Ну, так о том и речь, то есть, это определяется не конструкцией термов.
МБ
Или не о том?
Oℕ
Т.е. в экстенсиональной равенство между двумя элементами содержит не более одного элемента.
Об этом речь
Об этом речь
Oℕ
А в интенсиональной равенство может иметь дополнительную нетривиальную структуру
МБ
Но Вы говорите о теориях типов, экстенсиональной и интенсиональное. А мне интересны простые вычисленния. В бестиповом lambda-исчислении тоже экспоненциалы есть.
Oℕ
Я про равенства говорил
Oℕ
Я не знаю как безтиповую теорию расширить типом равенства
МБ
Но вот и получается. Что экстенсиональное -- это как равенство тех функций, которые закодированы термами (мы стираем всю структуру). А интенсиональное -- это равенство термов с учётом доказательства по их структуре.
Oℕ
Я не очень понимаю, из чего это получается.
Думаю, если нет типа равенства, то бессмысленно пытаться понять, интенсиональное оно или экстенсиональное
Думаю, если нет типа равенства, то бессмысленно пытаться понять, интенсиональное оно или экстенсиональное
МБ
Почему? Вот вопрос такой: есть у нас программа. Как мы понимаем равны программы или нет? Можно попробовать сравнить их, как функции. Иногда что-то из этого выходит. А можно доказать равенство, исходя из кода этих программ и каких-нибудь аксиом и правил вывода. Ну, типы -- это прям очень строгая форма этого всего, но лично мне не надо так строго в моих текущих рассуждениях.
МБ
Об экстенсиональности и интенсиональности философы задолго до типов говорили.
Oℕ
Я не говорю, что не нужно вводить равенства.
Но мы не имеем теорию, где есть типы, и равенство один из них.
Насколько я понимаю "интенсиональная" и "экстенсиональная" разделяют именно такие теории.
Но мы не имеем теорию, где есть типы, и равенство один из них.
Насколько я понимаю "интенсиональная" и "экстенсиональная" разделяют именно такие теории.