История изменений
Исправление quasimoto, (текущая версия) :
Ну для теории множеств эти уравнения решаются в работах по теории множеств. То есть тебе нужны ссылки на теорию множеств таки?
В теории множеств они не решаются никак кроме D = 1 = {*}, что не годится как модель ULC. Ты говоришь, что они решаются нетривиально (и пригодно для модели) в какой-то Set_ — ссылки сюда.
Мы, видимо, про разные bot?
Я просто упрощаю задачу — пусть функция «без аргументов» будет функцией с одним аргументом типа unit, как в SML:
- ();
val it = () : unit
- fun bot() = bot() : bool;
val bot = fn : unit -> bool
- bot();
Interrupt
соответственно:
bool bot(const std::tuple<>&)
{
return bot({});
}
void test()
{
f(bot({}));
}
аналогично функции от многих аргументов суть функции из кортежей, многозначные — в кортежи. В итоге достаточно рассматривать только унарные функции. Как я понимаю, твоя модель такой bot это пустое множество как подмножество unit * bool.
А этой композиции не существует.
Ты уже «в домике» штоле? :) f(bot()), Sched::handlePossibleHalts(Sched(...).run(...)) и т.п. есть в работающем и осмысленном коде — им нужна семантика, то есть правильная модель, то есть приписывание смысла таким композициям.
В математике все ф-и strict by design
В математике функция это частный случай отношения — тройка из домена, кодомена и графа (подмножества произведения домена на кодомен) с условиями единственности значения и тотальности по домену. Вопрос реализации такого соответствия тут вообще ортогонален (рекурсивные это функции, термы какого-то языка с какой-то стратегией вычисления, единожды полученные данные выписанные в таблицу — не важно).
если хочешь лени - добавляй руками через санки
Не хочу — 1) есть нормальные ленивые языки без «руками», 2) в CPO из коробки уже всё работает для моделирования лени (это строгость нужно специально ограничивать как подкатегорию).
Но терм, который не имеет нормальной формы, не задает никакого объекта. И сопоставлять, соответственно, нечему.
Такие термы это (\x. x x) (\x. x x), (Y I), bot(), f(false), f(bot()), Sched(...).run(...) и т.п. вещи которые должны редуцироваться (они не в нормальной форме) и которые могут делать это сколь угодно долго (не приходя в нормальную форму, то есть таковой просто нет, это называется «неразрешимый терм»), они существуют синтаксически, работают, полезны, в CPO для них есть морфизмы (читай самую первую часть у Плоткина), так как там есть морфизмы для всего что есть в языке и работает, иначе нафига вообще модель.
При чем тут код на си, если мы говорим о семантике? Мы же не для программ (термов) семантику пишем, а для объектов, которые задаются термами.
Я говорю как раз про обычную семантику программ (_всех_ определимых программ, тогда можно говорить о наличии модели и непротиворечивости какой-то теории языка), никаких промежуточных «объектов». У Плоткина это syntax, то есть множество типов/термов, и сразу semantic domains с denotations переводящими первое во второе.
В CPO тоже нельзя описать евент лупов и планировщиков, но тебя этот факт почему-то не смущает.
В CPO семантика для него не определена.
Можно и определена — все вычислимые функции и их композиции там представлены какими-то морфизмами, в том числе те f, bot, test, run и handlePossibleHalts.
Исходная версия quasimoto, :
Ну для теории множеств эти уравнения решаются в работах по теории множеств. То есть тебе нужны ссылки на теорию множеств таки?
В теории множеств они не решаются никак кроме D = 1 = {*}, что не годится как модель ULC. Ты говоришь, что они решаются нетривиально (и пригодно для модели) в какой-то Set_ — ссылки сюда.
Мы, видимо, про разные bot?
Я просто упрощаю задачу — пусть функция «без аргументов» будет функцией с одним аргументом типа unit, как в SML:
- ();
val it = () : unit
- fun bot() = bot() : bool;
val bot = fn : unit -> bool
- bot();
Interrupt
соответственно:
bool bot(const std::tuple<>&)
{
return bot({});
}
void test()
{
f(bot({}));
}
аналогично функции от многих аргументов суть функции из кортежей, многозначные — в кортежи. В итоге достаточно рассматривать только унарные функции. Как я понимаю, твоя модель такой bot это пустое множество как подмножество unit * bool.
А этой композиции не существует.
Ты уже «в домике» штоле? :) f(bot()), f(bot({})), Sched::handlePossibleHalts(Sched(...).run(...)) и т.п. есть в работающем и осмысленном коде — им нужна семантика, то есть правильная модель, то есть приписывание смысла таким композициям.
В математике все ф-и strict by design
В математике функция это частный случай отношения — тройка из домена, кодомена и графа (подмножества произведения домена на кодомен) с условиями единственности значения и тотальности по домену. Вопрос реализации такого соответствия тут вообще ортогонален (рекурсивные это функции, термы какого-то языка с какой-то стратегией вычисления, единожды полученные данные выписанные в таблицу — не важно).
если хочешь лени - добавляй руками через санки
Не хочу, 1) есть нормальные ленивые языки без «руками», 2) в CPO из коробки уже всё работает для моделирования лени (это строгость нужно специально ограничивать как подкатегорию).
Но терм, который не имеет нормальной формы, не задает никакого объекта. И сопоставлять, соответственно, нечему.
Такие термы это (\x. x x) (\x. x x), (Y I), bot(), Sched(...).run(...) и т.п. вещи которые должны редуцироваться (они _не_ в нормальной форме) и которые могут делать это сколь угодно долго (не приходя в нормальную форму, то есть таковой просто нет, это называется «неразрешимый терм»), они существуют синтаксически, работают, полезны, в CPO для них есть морфизмы (читай самую первую часть у Плоткина), так как там есть морфизмы для всего что есть в языке и работает, иначе нафига вообще модель.
При чем тут код на си, если мы говорим о семантике? Мы же не для программ (термов) семантику пишем, а для объектов, которые задаются термами.
Я говорю как раз про обычную семантику программ (_всех_ определимых программ, тогда можно говорить о наличии модели и непротиворечивости какой-то теории языка), никаких промежуточных «объектов». У Плоткина это syntax, то есть множество типов/термов, и сразу semantic domains с denotations переводящими первое во второе.
В CPO тоже нельзя описать евент лупов и планировщиков, но тебя этот факт почему-то не смущает.
В CPO семантика для него не определена.
Можно и определена — все вычислимые функции и их композиции там представлены какими-то морфизмами, в том числе те bot и test.