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

Да нет, в качестве D подходит множество перечислимых множеств.

Очевидно, что какое-то множество подходит — множество всех термов. Вообще, в ULC может речь идти только о счётных бесконечностях — термов, кодируемых кортежей, кодируемых вычислимых функций, отсюда эти уравнения, а дальше на вопрос о модели твой ответ — назовём искомое решение объектом Set_ и можно забить на теорию доменов и расходиться.

Хотя речь о том, что искомое решение не есть объект изучения теории множеств, то есть категории Set, а что-то другое — в ULC и всех распостранённых ЯП всякому типу можно сопоставить множество (термов), но не всякому множеству — тип (пустому нельзя, например), так что категория другая, она и искомый модельный объект(ы) требуют построения.

Что-то у тебя вместе смешались кони, люди, ULC, SML, сишка какая-то откуда-то вылезла.

Теория доменов изначально задумывалась для типизированного LC, но потом оказалось, что одинаково хорошо подходит для моделей разных ЯП безотносительно типизации. Так что не то что смешались, просто картина общая.

По-этому - пустое множество, как подмножество D*D, где D - множество перечислимых множеств.

Функция частичная, то есть ты отменил требование «для всех элементов домена» для отношения (иначе существование в языке аппликаций bot к чему угодно и пустой домен её модельной функции входили бы в противоречие). Расскажи лучше как делать эти частичные функции, то есть как конкретно выглядит категория множеств (пусть любых) и частичных функций — я знаю только про эквивалентные Set* и Par (есть у Awodey), в которых как раз частичные функции моделируются как тотальные с добавлением ⊥ к множествам.

В CPO для них есть один единственный морфизм - жопа.

Опять false. Это не морфизм, ⊥ это элемент домена, то есть, можно сказать, модель виснущих термов которая добавляется к типам, расширяя их (вместе с заданием порядка) до доменов, а потом морфизмы-функции как-то работают с этим элементом — сохраняют (строгость) или могут игнорировать (лень).

Вот если бы мы могли различать эти ф-и - тогда да, семантика бы была. Но мы не можем. Потому что они все - жопа.

И вот как раз различать их можно — bot, строгая f и ленивая g, о которых шла речь, частичны на bool, но тотальны в модели на домене bool⊥ = bool ∪ {⊥} — можно прекрасно видеть как они работают там где работают тотально и как они виснут (или не виснут) в остальных случаях.

Да нет, в качестве D подходит множество перечислимых множеств.

Очевидно, что какое-то множество подходит — множество всех термов. Вообще, в ULC может речь идти только о счётных бесконечностях — термов, кодируемых кортежей, кодируемых вычислимых функций, отсюда эти уравнения, а дальше на вопрос о модели твой ответ — назовём искомое решение объектом Set_ и можно забить на теорию доменов и расходиться.

Хотя речь о том, что искомое решение не есть объект изучения теории множеств, то есть категории Set, а что-то другое — в ULC и всех распостранённых ЯП всякому типу можно сопоставить множество (термов), но не всякому множеству — тип (пустому нельзя, например), так что категория другая, она и искомый модельный объект(ы) требуют построения.

Что-то у тебя вместе смешались кони, люди, ULC, SML, сишка какая-то откуда-то вылезла.

Теория доменов изначально задумывалась для типизированного LC, но потом оказалось, что одинаково хорошо подходит для любых моделей разных ЯП безотносительно типизации. Так что не то что смешались, просто картина общая.

По-этому - пустое множество, как подмножество D*D, где D - множество перечислимых множеств.

Функция частичная, то есть ты отменил требование «для всех элементов домена» для отношения (иначе существование в языке аппликаций bot к чему угодно и пустой домен её модельной функции входили бы в противоречие). Расскажи лучше как делать эти частичные функции, то есть как конкретно выглядит категория множеств (пусть любых) и частичных функций — я знаю только про эквивалентные Set* и Par (есть у Awodey), в которых как раз частичные функции моделируются как тотальные с добавлением ⊥ к множествам.

В CPO для них есть один единственный морфизм - жопа.

Опять false. Это не морфизм, ⊥ это элемент домена, то есть, можно сказать, модель виснущих термов которая добавляется к типам, расширяя их (вместе с заданием порядка) до доменов, а потом морфизмы-функции как-то работают с этим элементом — сохраняют (строгость) или могут игнорировать (лень).

Вот если бы мы могли различать эти ф-и - тогда да, семантика бы была. Но мы не можем. Потому что они все - жопа.

И вот как раз различать их можно — bot, строгая f и ленивая g, о которых шла речь, частичны на bool, но тотальны в модели на домене bool⊥ = bool ∪ {⊥} — можно прекрасно видеть как они работают там где работают тотально и как они виснут (или не виснут) в остальных случаях.