История изменений

С чего это вдруг?

Ну формально теория множеств изучает произвольные множества, если добавить немного структуры/ограничений, то это уже может быть «теория порядка», «теория групп», «теория доменов», «теория вычислимости» и т.п. Понятно, что в теории множеств соответствующие вещи моделируются как множества, но не всякое множество будет в модели, то есть обратно не всякому множеству будет соответствовать вещь теории — нужна другая категория со своим языком (в т.ч. косвенно).

Ты же сам прекрасно знаешь, как она выглядит.

Set_? Нет. Конструктивно я её представить не могу, хотя понятно, что она «существует».

Помимо моделей в духе теории доменов есть ещё подход при котором Set заменяется «эффективным топосом» (http://math.andrej.com/data/synthetic.pdf) с помощью выбора подходящего внутреннего языка для него.

У тебя в СРО нету элементов домена.

У доменов есть элементы (у bool⊥ — ⊥, false и true, плюс ещё есть порядок), домены это объекты CPO и подобных. Ну и как обычно — в любой категории есть понятие обобщённого элемента, в CPO есть терминальный объект (так как она CCC), поэтому есть теоретико-категорное представление для элементов доменов.

Ну так и в Set_ все также - мы прекрасно видим, как функция работает на своей области определения. А вне области определения - жопа.

Не вполне так. Потому что в доменах есть ещё варианты ⊥ -> * (* обозначает «нормальные» значения из области определения), то есть ленивые функции могут их делать, строгие — нет, только * -> ⊥ и ⊥ -> ⊥, это я имел в виду — различение не только по в/вне области определения (работает/виснет), но и по тому как стратегия вычисления обращается с ⊥. А ещё в более сложной ситуации разумно добавить в домен разные элементы как для non-termination, так и для разных исключений — опять будет различие видно в модели.

Например, множество всех нормализуемых термов перечислимо, а множество соответствующих классов эквивалентности - уже нет.

Множество всех синтаксических термов перечислимо (Godel numbering), нет? А эквивалентность по какому признаку? Внешнему равенству? Тогда ок. Но я не говорил «перечислимо», я сказал «счётная бесконечность» — классов всё равно столько же, это к тому, почему уравнения именно такие (помимо кодирования кортежей и функций, тезиса Чёрча-Тьюринга, Godel numbering и Cantor pairing тут важна счётность функциональных пространств в случае вычислимости).

С чего это вдруг?

Ну формально теория множеств изучает произвольные множества, если добавить немного структуры/ограничений, то это уже может быть «теория порядка», «теория групп», «теория доменов», «теория вычислимости» и т.п. Понятно, что в теории множеств соответствующие вещи моделируются как множества, но не всякое множество будет в модели, то есть обратно не всякому множеству будет соответствовать вещь теории — нужна другая категория со своим языком (в т.ч. косвенно).

Ты же сам прекрасно знаешь, как она выглядит.

Set_? Нет. Конструктивно я её представить не могу, хотя понятно, что она «существует».

Помимо моделей в духе теории доменов есть ещё подход при котором Set заменяется «эффективным топосом» (http://math.andrej.com/data/synthetic.pdf) с помощью выбора подходящего внутреннего языка для него.

У тебя в СРО нету элементов домена.

У доменов есть элементы (у bool⊥ — ⊥, false и true, плюс ещё есть порядок), домены это объекты CPO и подобных. Ну и как обычно — в любой категории есть понятие обобщённого элемента, в CPO есть терминальный объект (так как она CCC), поэтому есть теоретико-категорное представление для элементов доменов.

Ну так и в Set_ все также - мы прекрасно видим, как функция работает на своей области определения. А вне области определения - жопа.

Не вполне так. Потому что в доменах есть ещё варианты ⊥ -> * (* обозначает «нормальные» значения из области определения), то есть ленивая функция может их делать, строгая — нет, только * -> ⊥ и ⊥ -> ⊥, это я имел в виду — различение не только по в/вне области определения (работает/виснет), но и по тому как стратегия вычисления обращается с ⊥. А ещё в более сложной ситуации разумно добавить в домен разные элементы как для non-termination, так и для разных исключений — опять будет различие видно в модели.

Например, множество всех нормализуемых термов перечислимо, а множество соответствующих классов эквивалентности - уже нет.

Множество всех синтаксических термов перечислимо (Godel numbering), нет? А эквивалентность по какому признаку? Внешнему равенству? Тогда ок. Но я не говорил «перечислимо», я сказал «счётная бесконечность» — классов всё равно столько же, это к тому, почему уравнения именно такие (помимо кодирования кортежей и функций, тезиса Чёрча-Тьюринга, Godel numbering и Cantor pairing тут важна счётность функциональных пространств в случае вычислимости).

С чего это вдруг?

Ну формально теория множеств изучает произвольные множества, если добавить немного структуры/ограничений, то это уже может быть «теория порядка», «теория групп», «теория доменов», «теория вычислимости» и т.п. Понятно, что в теории множеств соответствующие вещи моделируются как множества, но не всякое множество будет в модели, то есть обратно не всякому множеству будет соответствовать вещь теории — нужна другая категория со своим языком (в т.ч. косвенно).

Ты же сам прекрасно знаешь, как она выглядит.

Set_? Нет. Конструктивно я её представить не могу, хотя понятно, что она «существует».

Помимо моделей в духе теории доменов есть ещё подход при котором Set заменяется «эффективным топосом» (http://math.andrej.com/data/synthetic.pdf) с помощью выбора подходящего внутреннего языка для него.

У тебя в СРО нету элементов домена.

У доменов есть элементы (у bool⊥ — ⊥, false и true, плюс ещё есть порядок), домены это объекты CPO и подобных. Ну и как обычно — в любой категории есть понятие обобщённого элемента, в CPO есть терминальный объект (так как она CCC), поэтому есть теоретико-категорное представление для элементов доменов.

Ну так и в Set_ все также - мы прекрасно видим, как функция работает на своей области определения. А вне области определения - жопа.

Не вполне так. Потому что в доменах есть ещё варианты ⊥ -> * (* обозначает «нормальные» значения из области определения), то есть ленивая функция может его делать, строгая — нет, только * -> ⊥ и ⊥ -> ⊥, это я имел в виду — то есть различение не только по в/вне области определения (работает/виснет), но и по тому как стратегия вычисления обращается с ⊥. А ещё в более сложной ситуации разумно добавить в домен разные элементы как для non-termination, так и для разных исключений — опять будет различие видно в модели.

Например, множество всех нормализуемых термов перечислимо, а множество соответствующих классов эквивалентности - уже нет.

Множество всех синтаксических термов перечислимо (Godel numbering), нет? А эквивалентность по какому признаку? Внешнему равенству? Тогда ок. Но я не говорил «перечислимо», я сказал «счётная бесконечность» — классов всё равно столько же, это к тому, почему уравнения именно такие (помимо кодирования кортежей и функций, тезиса Чёрча-Тьюринга, Godel numbering и Cantor pairing тут важна счётность функциональных пространств в случае вычислимости).