ооп и функциональщина кратко, внятно.

В ULC у нас нет отдельного Bool, а именно что рефлексивный домен который естественным образом _уже_ устроен как CPO, а вычислимые функции _уже_ непрерывны.

Да ничего подобного. У нас сперва есть множество, на котором определены RE-функции, и потом уже оказывается, что мы можем построить топологию, относительно которой эти ф-и будут непрерывны.

Но суть в том, что мы можем и не строить. Потому что нинужно.

Так при чём тут перечислимые множества и какие уравнения ты собрался решать в какой-то «Set_»? Начни хотя бы с примера с Bool и f — что будет вместо ⊥, порядка и монотонности?

Ну например то же: D ≊ D × D ≊ [D ⇒ D], D ≠ 1, все вполне ок.

Всё ещё

Что все еще?

По ссылке нет никакого упоминания категории Set_

Ну конечно нет, потому что нинужно. Есть перечислимые множества (по ссылке они описаны) и кроме этого нам больше ничего не надо, все остальное - лишнее, оно ничего не дает. А раз это не надо - то никто это и не описывает. Зачем нам выделять какую-то специальную категорию для этих дел? Нафиг не надо. И без нее хорошо. Но если вдруг захочется - то можно и выделить, и получится Set_.

Речь-то шла чем считать типы — просто множествами значений?

Ну да. Именно так. Это естественная семантика, ни к каким противоречиям она не приводит, вся теория спокойно излагается, зачем тогда плоджить сущности, вводить топологии, непрерывности и прочее ненужное?

А я сказал, что в программировании с частичными функциями это множества со структурой, а сами вычислимые функции — определенные функции сохраняющие структуру.

Да нет, это не так. Это обычные множества и функции - это тоже обычные множества. И только потом выясняется, что мы при желании может задать какую-то структуру, которая будет вести себя так же, как эти обычные множества.

Что все еще?

«не говоришь где учебники про LC, его теории и модели которые бы не использовали теорию доменов».

А то с одной стороны есть куча информации, а с другой — твоё «нинужно».

Ну например то же: D ≊ D × D ≊ [D ⇒ D], D ≠ 1, все вполне ок.

Ну дык reference давай. Что значит D, _×_, _≊_, 1, [_⇒_]. Я дал штуки четыре.

Именно так.

То есть

f :: Bool -> Bool
f !x = if x then False else f x

t :: (Bool, Bool, Bool)
t = (f True, f False, let bot = bot in f bot)

Bool = {False, True} и f : Bool → Bool? А в f bot в f что из множества Bool передаётся? А f False что из множества Bool возвращает?

Ну дык reference давай. Что значит D, _×_, _≊_, 1, _≠_, [_⇒_].

Обычные теоретико-множественные обозначения, с поправкой на то, что множества - перечислимые

Bool = {False, True} и f : Bool → Bool?

Да.

А в f bot в f что из множества Bool передаётся?

какой bot? Никакого bot тут нету.

А f False что из множества Bool возвращает?

Ничего не возвращает. Это же частичная функция.

У нас обычные функции - это подмножества бинарного отношения, в которых для любого элемента домена есть пара, а в случае частичных ф-й это требование ослаблено, остается только требование единственности.

Хотя можно и его ослабить - тогда у нас в языке будут продолжения (и функции, возвращающие несколько значений).

Обычные теоретико-множественные обозначения

Это не reference.

какой bot?

Так, давай тогда на си:

#include <stdbool.h>

bool f(bool x)
{
    return x ? false : f(x);
}

bool bot()
{
    return bot();
}

void test()
{
    f(true);
    f(false);
    f(bot());
}

вот есть такая программа, нам нужно построить денотационную семантику для неё — модель для каждого типа и функции, пусть будет в виде множеств и функций, в виде каких?

Ничего не возвращает.

Денотационная семантика должна всякой нотации приписывать смысл (денотацию), «ничего не возвращает» это «мы ничего не знаем», а мы должны знать, например — f(true) возвращает false, f(false) возвращает ⊥, f(bot()) принимает и возвращает ⊥.

Это же частичная функция.

Ну то есть обычная функция D → D, где bool ⊂ D. Для нормальной пригодной семантики тебе нужно рассказать про D и про то как себя ведут функции на D.

И, кстати, частичная функция отменяет требование «для всех», но тогда f(bot()) вообще становится бессмысленным — bot() «ничего не возвращает», тогда f нечего принимать (для некоторых, но не для всех не даёт выбрать «ничего»), хотя смысл у конструкции должен быть — она существует.

Это не reference.

reference на что тебе нужен, я не понял? На теорию множеств?

вот есть такая программа, нам нужно построить денотационную семантику для неё — модель для каждого типа и функции, пусть будет в виде множеств и функций, в виде каких?

Множество {true, false} и функции в виде подмножеств {true, false}*{true, false}. bot() - пустое множество.

Денотационная семантика должна всякой нотации приписывать смысл (денотацию)

Она и описывает.

«ничего не возвращает» это «мы ничего не знаем»

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

А у CPO-семантики тут недостаток, да, приходится городить _|_-костыль, который наблюдаемому поведению противоречит. Но мы все вместе дружно притворяемся, что все в порядке.

Ну то есть обычная функция D → D, где bool ⊂ D.

Ну да.

Для нормальной пригодной семантики тебе нужно рассказать про D и про то как себя ведут функции на D.

D - перечислимое множество, ведут себя так же, как обычные функции на перечислимых множествах.

В этом и суть - это для надстроек приходится рассказывать что такое D и как что себя ведет. А тут ничего рассказывать не надо - ведь это обычные множества и обычные функции.

хотя смысл у конструкции должен быть — она существует.

Нет, не существует. Какая у него нормальная форма, если оно существует?

reference на что тебе нужен, я не понял? На теорию множеств?

Если я пишу такие уравнения, то мне нужно давать ссылки не на Mac Lane с Awodey, то есть не на введения в ТК, а на литературу в которой такие уравнения мотивируются, формулируются, решаются и т.п. (ТК при этом часто уже предполагается известной), то есть на Barendregt, Scott, Plotkin, Abramsky & Jung, Lambek & Scott (другой) и т.п.

Множество {true, false} и функции в виде подмножеств {true, false}*{true, false}. bot() - пустое множество.

Ну ты пиши точнее. Функции частичны? То есть f(true) возвращает false, так что пара (true, false), f(false) это что и какая пара? Просто никакая? Что значит bot() пустое? Вообще-то bot : unit -> bool, то есть при передаче () типа unit оно возвращает что типа bool? Или ничего? Что это? Как тогда получается составить композицию f(bot())? Никакого «ничего» в домене f у тебя нет. Пусть ещё есть ленивая g : bool -> bool которая игнорирует аргумент и просто возвращает false, тогда есть g(bot()) — она ещё и определена на этом «ничего».

Какая у него нормальная форма, если оно существует?

Что-то ты путаешься в показаниях. Термы без нормальных форм уже не нужны? Сам же ратуешь за частичность. Event loops и планировщики писать, не? Ну и я же написал f(bot()); — валидный код на си, компилируется, работает, существует.

в С++ снимаются многие ограничения присущие С, например объявление переменных в любом месте

А в C нельзя было в заголовке for объявлять, скажем?

Event loops и планировщики писать

Для примера:

class Sched {

    ...

    enum class HaltState {
        to,
        se
    };

    // "bot"
    HaltState run(...) {
        while (true) {
            ...
            if (...) return HaltState::to;
            if (...) return HaltState::se;
        }
    }

    // "f"
    static void handlePossibleHalts(HaltState state) {
        ...
    }

};

    Sched::handlePossibleHalts(Sched(...).run(...));

Если я пишу такие уравнения, то мне нужно давать ссылки не на Mac Lane с Awodey, то есть не на введения в ТК, а на литературу в которой такие уравнения мотивируются, формулируются, решаются и т.п.

Ну для теории множеств эти уравнения решаются в работах по теории множеств. То есть тебе нужны ссылки на теорию множеств таки?

Ну ты пиши точнее. Функции частичны?

Конечно.

Просто никакая?

Просто никакая.

Что значит bot() пустое?

Значит пустое. Ты не знаешь, что такое пустое множество?

Вообще-то bot : unit -> bool

Мы, видимо, про разные bot?

Та bot(), про которую я говорил - это bot = bot. То есть ф-я, которая ничего не принимает и ничего не возвращает, пустое множество.

Как тогда получается составить композицию f(bot())?

А этой композиции не существует.

Пусть ещё есть ленивая

В математике все ф-и strict by design, если хочешь лени - добавляй руками через санки. То есть твоя g будет g: (unit -> bool) -> (unit -> bool) и не g(bot()), а g(_ -> bot())

Термы без нормальных форм уже не нужны?

Мы вроде о семантике говорили? То есть - термы задают некоторые объекты, и мы этим объектам сопоставляем некие другие объекты (морфизмы в CPO, частичные функции). Но терм, который не имеет нормальной формы, не задает никакого объекта. И сопоставлять, соответственно, нечему.

Ну и я же написал f(bot()); — валидный код на си, компилируется, работает, существует.

При чем тут код на си, если мы говорим о семантике? Мы же не для программ (термов) семантику пишем, а для объектов, которые задаются термами. Терм f(bot()); не задает никакого объекта.

Event loops и планировщики писать, не?

В CPO тоже нельзя описать евент лупов и планировщиков, но тебя этот факт почему-то не смущает.

И что должен продемонстрировать этот пример? В CPO семантика для него не определена.

Ну для теории множеств эти уравнения решаются в работах по теории множеств. То есть тебе нужны ссылки на теорию множеств таки?

В теории множеств они не решаются никак кроме 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.

В теории множеств они не решаются никак кроме D = 1 = {*}

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

Ты говоришь, что они решаются нетривиально (и пригодно для модели) в какой-то Set_ — ссылки сюда.

http://en.wikipedia.org/wiki/Recursively_enumerable_set

http://en.wikipedia.org/wiki/Computable_function

http://en.wikipedia.org/wiki/Set_theory

Вот ссылки, ничего кроме них для решения указанных уравнений не нужно.

Я просто упрощаю задачу — пусть функция «без аргументов» будет функцией с одним аргументом типа unit, как в SML:

Что-то у тебя вместе смешались кони, люди, ULC, SML, сишка какая-то откуда-то вылезла. Мы говорим о семантике для ULC - значит говорим о семантике ULC. Там любая функция принимает одн аргумент и им может быть что угодно, твоя bot будет: bot x = bot x. Это пустое множество. Пустое множество - функция, которая виснет на всех входах.

Как я понимаю, твоя модель такой bot это пустое множество как подмножество unit * bool.

Да. Только давай без юнитов и булей. У нас ULC. По-этому - пустое множество, как подмножество D*D, где D - множество перечислимых множеств.

ы уже «в домике» штоле? :) f(bot()), Sched::handlePossibleHalts(Sched(...).run(...)) и т.п. есть в работающем и осмысленном коде — им нужна семантика, то есть правильная модель, то есть приписывание смысла таким композициям.

Нужна, конечно, но в CPO у них семантики нет. А то, о чем я говорю, изоморфно CPO. Чего нету в CPO нет и тут. Чего нету тут - нету в CPO :)

В математике функция это частный случай отношения — тройка из домена, кодомена и графа (подмножества произведения домена на кодомен) с условиями единственности значения и тотальности по домену.

Я и говорю - strict by design.

Не хочу — 1) есть нормальные ленивые языки без «руками», 2) в CPO из коробки уже всё работает для моделирования лени (это строгость нужно специально ограничивать как подкатегорию).

Ну а тут наоборот - искаробки работает strict, а для лени надо насовать санок.

в CPO для них есть морфизмы (читай самую первую часть у Плоткина), так как там есть морфизмы для всего что есть в языке и работает, иначе нафига вообще модель.

В CPO для них есть один единственный морфизм - жопа. И сказать «этому у нас соответствует жопа» совершенно равносильно, что сказать «этому у нас ничего не соответствует», потому что жопа - это как раз специальный костыль для «ничего».

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

Я говорю как раз про обычную семантику программ (_всех_ определимых программ, тогда можно говорить о наличии модели и непротиворечивости какой-то теории языка), никаких промежуточных «объектов».

CPO не задает семантику программ, она задает семантику классов эквивалентности программ.

Можно и определена — все вычислимые функции и их композиции там представлены какими-то морфизмами, в том числе те f, bot, test, run и handlePossibleHalts.

Нет, не определена. Там стоит жопа. Повторяю, с формальной точки зрения нету совершенно никакой разницы обзовешь ты несуществующий объект жопой или скажешь, что его нет. Конструкции изоморфны. Из первой всегда можно сделать естественным образом вторую, а из второй - первую.

Перегрузка функций - удобная штуковина.

Такие термы это (\x. x x) (\x. x x), (Y I), bot(), f(false), f(bot()), Sched(...).run(...) и т.п. вещи которые должны редуцироваться (они не в нормальной форме) и которые могут делать это сколь угодно долго (не приходя в нормальную форму, то есть таковой просто нет, это называется «неразрешимый терм»), они существуют синтаксически, работают, полезны, в CPO для них есть морфизмы (читай самую первую часть у Плоткина), так как там есть морфизмы для всего что есть в языке и работает, иначе нафига вообще модель.

Перегрузка функций - удобная штуковина.

удобная? Ну для пары-тройки однотипных обработчиков разных данных - да. Для языка в целом мне кажется не очень

Хорошие нынче трёхзвёздочники пошли. Сезон, видимо.

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

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

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

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

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

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

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

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

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

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

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

Очевидно, что какое-то множество подходит

Я назвал вполне конкретное, которое подходит.

Хотя речь о том, что искомое решение не есть объект изучения теории множеств

С чего это вдруг? Как раз и есть.

Теория доменов изначально задумывалась для типизированного LC

Но мы говорим о нетипизированном. Не надо все мешать в одну кучу.

Расскажи лучше как делать эти частичные функции

Что значит «как делать»?

то есть как конкретно выглядит категория множеств (пусть любых) и частичных функций

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

я знаю только про эквивалентные Set* и Par (есть у Awodey), в которых как раз частичные функции моделируются как тотальные с добавлением ⊥ к множествам.

Тотальные ф-и из Set_ переходят в тотальные Set* (добавляем пару (_|_, _|_)), частичные из Set_ в тотальные из Set* (добавляем пары (a, _|_ для аргументов, на которых виснет)). Объекты у нас совпадают (и там и там - перечислимые множества, понятное дело). Так что Set_ естественным образом вкладывается в Set*, при этом она меньше, но в ней сохраняются все интересные нам конструкции.

Опять false. Это не морфизм

Морфизм в жопу, а не жопа, да.

это элемент домена

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

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

Ну так и в Set_ все также - мы прекрасно видим, как функция работает на своей области определения. А вне области определения - жопа. И больше мы сказать ничего не можем. Там где в CPO у нас стрелка в жопу, в Set_ просто стрелки нет (потому что и жопы нет). Но никакой информации, очевидно, не теряется, т.к. по Set_ можно восстановить СРО, она содержит всю ее структуру.

множество всех термов.

Нет, множество термов не подходит. Не путай термы и классы эквивалентности термов.

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

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

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

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

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_? Нет.

Как нет? СРО не можешь себе представить?

У доменов есть элементы

У доменов нет элементов. Не надо нести чушь.

Потому что в доменах есть ещё варианты ⊥ -> *

Нет, нету, у нас энергичная лямбда. Бывает только _|_ -> _|_

А ещё в более сложной ситуации разумно добавить в домен разные элементы как для non-termination, так и для разных исключений — опять будет различие видно в модели.

Снова ты в сторону ушел. Мы говорим о нетипизированной лямбде, у нас нету никаких исключений и прочей чуши. Исключения - это уже в реальном языке, в CS-теории нам исключения ни к чему (потому что моделировать реальные языки нам не нужно).

Множество всех синтаксических термов перечислимо (Godel numbering), нет?

Что значит синтаксических? Синтаксически корректных? Других и нету, это множество очевидно перечислимо, очевидно. И даже множество нормализуемых (то есть множество завершающихся программ) перечислимо.

А эквивалентность по какому признаку?

Ну как по какому? У нас лямбда-исчисление по определению - набор термов + эквивалентность (альфа/бета).

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

Ты, как обычно, забыл, о чем шел разговор. Ты сказал, что множество термов подходит в качестве модели - а оно не подходит. Потому что мы моделируем классы эквивалентности термов, а не термы. На термы нам плевать. Можно считать, что нету никаких термов, они вообще нужны только для удобства, с формальной же точки зрения они - лишняя сущность.

СРО не можешь себе представить?

Ты меня запутал.

https://en.wikipedia.org/wiki/Cartesian_closed_category

In order theory, complete partial orders (cpos) have a natural topology, the Scott topology, whose continuous maps do form a cartesian closed category (that is, the objects are the cpos, and the morphisms are the Scott continuous maps). Both currying and apply are continuous functions in the Scott topology, and currying, together with apply, provide the adjoint.

То теория доменов не нужна, как и топология Скотта, нужна некая Set_, то эта Set_ оказалась вдруг CPO (привет домены и топология Скотта).

У доменов нет элементов.

Забавно — у типов есть элементы, а у их моделей нет, ага. 1) http://homepages.inf.ed.ac.uk/gdp/publications/Domains_a4.ps — не искабельно, но ищи «element» и «value domain», я уже советовал почитать самую первую часть (и про домены, почему не множества, почему _|_, почему posets — частичный порядок и монотонность, про неподвижные точки и cpos — цепочки, топология и непрерывность), http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf — искабельно «element», 2) https://en.wikipedia.org/wiki/Complete_partial_order, https://en.wikipedia.org/wiki/Partially_ordered_set — домен это cpo (как вариант, см. Плоткина), cpo это poset, читай что такое элемент (множества) poset-а по второй ссылке.

у нас энергичная лямбда

Спасибо, не нужно, мне нужны модели для разных стратегий, в т.ч. ленивые лямбды. Между прочим, есть Чёрч-Россер, поэтому завязка на энергичность искусственна.

потому что моделировать реальные языки нам не нужно

Да ладно.

Других и нету, это множество очевидно перечислимо, очевидно.

Ну.

У нас лямбда-исчисление по определению - набор термов + эквивалентность (альфа/бета).

И /эта — я и говорю внешнее (extensional) равенство. В этом случае перечислить классы алгоритмически действительно не получится — сказать одинаково ли работают (или одинакова ли их нормальная форма, при наличии, если без эта) два терма по их виду это к проблеме останова, опять же. http://ncatlab.org/nlab/show/equality — без строгой нормализации (т.е. в случае ULC) computational будет undecidable.

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

Я привёл довод в пользу того что D = D * D = D -> D, поправка про эквивалентность это ок и она ничего не меняет — классов та же счётная бесконечность (то есть разбиение термов на классы явно не увеличивает (но и не уменьшает) мощность), а счётные бесконечности просто изоморфны.

То теория доменов не нужна, как и топология Скотта, нужна некая Set_, то эта Set_ оказалась вдруг CPO (привет домены и топология Скотта).

Set_ тривиальным образом вкладывается в СРО, при этом она содержит все интересное, что есть в СРО.

Забавно — у типов есть элементы, а у их моделей нет, ага.

Видать плохая модель.

Да ладно.

Ага.

И /эта

эта тут ничего не должна менять. ну да не суть.

В этом случае перечислить классы алгоритмически действительно не получится

Да их ни в каком случае перечислить не получится, потому что это неперечислимое множество. Просто по факту.

Я привёл довод в пользу того что D = D * D = D -> D

Ну выполняются эти равенства, и что? К чему ты их привел?

классов та же счётная бесконечность

Ну счетная и дальше что?

счётные бесконечности просто изоморфны.

Не в любой категории, очевидно. В том же CPO «счетные» домены совсем не обязательно должны быть изоморфными.

Set_ тривиальным образом вкладывается в СРО

Ацкий матан, я не поспеваю, сорри.

Видать плохая модель.

Нормальная, элементы-то у доменов есть :)

Ага.

http://www.softlab.ntua.gr/~nickie/Papers/papaspyrou-1998-fscpl.pdf, ACSL, JML, Coq?

Ну выполняются эти равенства, и что?

Ничего, это моё наивное наблюдение — посчитаем термы (их классы, да) как множество в обычной категории Set — будет у нас изоморфизм с N в ней, потом посчитаем лямбда-функции (значения) и кодирования кортежей — опять изоморфизм с N, изоморфизм транзитивен. А дальше можно брать определение модели из http://arxiv.org/pdf/0904.4756v1.pdf и строить подходящий объект в подходящей категории.

http://www.softlab.ntua.gr/~nickie/Papers/papaspyrou-1998-fscpl.pdf, ACSL, JML, Coq?

И?

А дальше можно брать определение модели из http://arxiv.org/pdf/0904.4756v1.pdf и строить подходящий объект в подходящей категории.

Например в Set_.

И?

Не реальные языки моделируются?

Реальные. Но нужным оно от этого не становится же.

То есть теории приложения не нужны? Зачем нужна денотационная семантика ЯП, если для реальных ЯП её не делать?

То есть теории приложения не нужны?

Нужны. Но их нет.

Зачем нужна денотационная семантика ЯП, если для реальных ЯП её не делать?

За тем, чтобы исследовать свойства языков в общем. А моделирование конкретного ЯП ничего не дает, т.к. отсутствует матаппарат для анализа модели. То есть в этом смысле модель языка ничего не привносит к описанию самого языка - это то же самое описание, но просто сделанное другими словами. Лишняя сущность.

Но их нет.

ACSL, JML, Coq

То есть CompCert, Frama-C, Why2/3 (Krakatoa/Jessie), F*. Но если это никуда не годится, то ок — будем подождать.

отсутствует матаппарат для анализа модели

Ну строится та или иная _формальная_ модель (даже если это тупо синтаксическое дерево и типы) и проводится какой-то model checking.

http://www.cis.upenn.edu/~bcpierce/sf/index.html, http://adam.chlipala.net/cpdt/, http://pauillac.inria.fr/~xleroy/courses/VTSA-2013/ (Relation with denotational semantics тут — http://gallium.inria.fr/~xleroy/publi/coindsem-journal.pdf), http://pauillac.inria.fr/~xleroy/courses/Eugene-2012/.

ACSL, JML, Coq

Ээээ... а при чем тут приложения? Это не приложения.

Ну строится та или иная _формальная_ модель

Ну модель-то мы строим, но ничего делать с ней не умеем на данный момент. То есть как например если бы у нас были уравнения Максвелла, но мы бы не умели решать диффуры - в этом случае наличие уравнений ничем не лучше просто словесного их описания.

На практике же мы умеем диффуры анализировать - как качественно, так и количественно (решая), то есть получать результаты, которые бы мы без диффуров не получили (или получили какими-то жутко более затратными методами). А вот в случае с моделями языков беда. Модель языков не добавляет ничего к стандарту этого языка.

То есть формализация вообще нужна зачем? Чтобы можно было применять к этой формализации стандартные методы анализа. А в данном случае никаких методов анализа не существует, потому и формализация ничем не лучше обычного словесного описания (а обычно даже хуже, так как очень неудобна).

Это не приложения

http://krakatoa.lri.fr/, http://www.lri.fr/~marche/moy09phd.pdf, http://en.wikipedia.org/wiki/Abstract_interpretation, http://profs.sci.univr.it/~giaco/paperi/incubo.ps.gz.

Как это нет?

Ну модель-то мы строим, но ничего делать с ней не умеем на данный момент.

Вот я не пойму чего ты не умеешь с ней делать.

http://www.cis.upenn.edu/~bcpierce/sf/StlcProp.html, http://adam.chlipala.net/cpdt/html/StackMachine.html, http://pauillac.inria.fr/~xleroy/courses/VTSA-2013/Sem.html.

Progress, preservation, substitution, context invariance, type uniqueness, normalization для самого языка и soundness, completeness, correctness для преобразований, например, считается за что-то?

Скажи что конкретно ты бы хотел видеть, то есть какие результаты нужны.

Как это нет?

Ну так нет.

Вот я не пойму чего ты не умеешь с ней делать.

проводить анализ, определять свойства. А вообще говоря неясно о чем речь - на данный момент-то не то что методов анализа, но и формализации не существует.

Progress, preservation, substitution, context invariance, type uniqueness, normalization для самого языка и soundness, completeness, correctness для преобразований, например, считается за что-то?

Конечно же нет.

Скажи что конкретно ты бы хотел видеть, то есть какие результаты нужны.

Ну все просто, на примере тех же уравнений Максвелла. Есть четкое и корректное описание уравнений на естественной языке, без формул. И в принципе этого вполне достаточно, чтобы электростанции работали, лампочки горели, электроплита грела и т.д., но нам же хочется большего? По-этому мы переводим уравнения на язык диффур и применяем матаппарат дифференциального исчисления. И, например, узнаем, что электро-магнитные процессы лоренц-инвариантны - факт, который из словесного описания вывести весьма малореально (вобщем-то вывод инвариантности из диффуров - это уже и не чистое дифф. исчисление, а группы Ли во все поля).

Значит как оно в приложении к CS? Берется _уже существующий_ язык, ну который дан, который успешен, который популярен. Ну, не знаю, пусть будет джава как конкретный пример. Мы вполне можем писать на джаве и иметь профит - но вот нам мало, по-этому мы берем какой-то формализм и описываем на нем джаву, весь ее стандарт, со всеми гофовскими паттернами и прочей хренью (но такого формализма нет, беда), причем полностью описываем, безо всяких там «подмножеств», понятное дело. Потом смотрим, и внезапно оказывается, что язык удовлетворяет какому-то свойству Х, которого мы не ожидали! И, оказывается, на нем можно делать какое-то Y, которое мы, читая стандарт языка, и не думали, что можно! Вот это и называется практическим результатом.

Если же берется какой-то готовый язык типа агды там, петуха или идриса, который изначально заточен под определенную формализацию - то тут никакого профита не будет, понятное дело, все, где написано про зависимые типы и всякие агды - это не наука, это бестолковая херня. Ну просто господа, которые занимаются CS, не могут осилить настоящие задачи, а потому переливают из пустое в порожнее - я их в этом понимаю, конечно. Статьи, диссеры, гранты - все это нахаляву, безо всякого труда, сложность работ на уровне средней школы. Кто не соблазнится? Но вот тех людей, которые это читают, нахваливают и просят еще - я понять не могу.

Собсно ситуация просто смешна - вот представь себе, есть инженер, ему сказали - спроектируй мост вот от сих до сих, требования к конструкции такие-то, материалы такие-то, работай. На это инженер отвечает, что требования писали идиоты, материалы их - говно, т.к. мосты надо делать из абсолютно твердых материалов, да и вообще, правильный мост - он в вакууме и желательно сферический. А если кто-то по такому мосту ездить не хочет и предпочитает бетонный по соседству - то они просто неосиляторы, которые не в силах понять гениальной концепции сферического абсолютно твердого моста.

Вот последний абзац - это совершенно точная зарисовка нынешней ситуации в CS.

Так собственно о «моделях для реальных языков», я немного уточню, а то я немного некорреткно высказался. Модели дляр реальных языков, конечно, нужны, но, во-первых для нормальных языков, а не академических игрушек вроде петухов с хаскелями, а во-вторых - нормальные модели, которые дают профит (неожиданные свойства). Формализма, дающего профит, для каких-либо языков (в том числе для петухов) на данный момент нет. Для нормальных языков формализма нет вообще.

Есть какие-то общие подходы, которые дают какой-то локальный профит. Ну, например, тот факт, что подтипирование легко сделать неразрешим для тайпчека для меня был достаточно неожиданнен, когда я его впервые увидел. Уверен, для кого-то есть еще факты такого рода. Так что _в общем_ какой-то профит есть. Хоть и капля.

Так вот, эти ваши классы даже в учебнике называют почти структурами, а мизерное отличие сомнительного профита легко можно решить и в анси си(далее - ансися) при ближайшем обновлении.

facepalm. ты ничего не понял в классах и пытаешься строить из себя умного. Исчезни из development пока не осилишь талмуд Страуструпа и Exceptional C++ Саттера.

Ну так нет.

проводить анализ, определять свойства.

Эм, http://toccata.lri.fr/gallery/index.en.html, http://hisseo.saclay.inria.fr/gallery.html, http://www.lri.fr/~sboldo/research.html. Проводи анализ, определяй свойства, почему нет-то?

Конечно же нет.

Ок, тогда CompCert (верифицируемый на тему как раз корректности компилятор (подмножества) си -_-) не считаем.

не академических игрушек вроде петухов с хаскелями

Вот я специально про них не говорю.

Для нормальных языков формализма нет вообще.

Ещё раз — JML для Java, ACSL — для ANSI/ISO C. Первый используется в Krakatoa (это я совсем не смотрел, если что), второй — Frama-C. Coq и прочие интерактивные и автоматические чекеры используются уже как бакенды для проведения (автоматических или ручных) доказательств заявленных свойств программ, эти свойства описывают некий _модельный_ язык соответствующий реальному, понятное дело.

Основания для моделей это, в том числе, abstract interpretation (http://www.lri.fr/~marche/moy09phd.pdf — integer analysis, memory/pointer analysis), которая используется также в статическом анализе (C/C++ обычно, см. википедию на тему abstract interpretation) и компиляторах (polyhedral models, например — http://en.wikipedia.org/wiki/Frameworks_supporting_the_polyhedral_model).

Про отсутствие формализма для того же си — 4.2, я уже приводил ссылку http://www.softlab.ntua.gr/~nickie/Papers/papaspyrou-1998-fscpl.pdf, вот обзор того же человека — http://www.softlab.ntua.gr/~nickie/Papers/papaspyrou-2001-dsac.pdf.

Есть, сэр

На это инженер отвечает

Дык не отвечает же. Потыкает модельку в агде и идёт писать на C++ :)

все, где написано про зависимые типы и всякие агды - это не наука, это бестолковая херня.

Зависимые типы это математические вещи которые просто существуют, ну типа как октонионы, например.

Есть, товарищ лейтенант

Так правильно

так точно, сэр товарищ лейтенант! А по факту, как вижу - так и говорю, ООП и плюсы в частности вызывают негатив

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

Проводи анализ, определяй свойства, почему нет-то?

Какие, как? Можно пример, как кто-то нашел какие-то неожиданные свойства существующего языка, которые без формализации были неочевидны?

Ок, тогда CompCert (верифицируемый на тему как раз корректности компилятор (подмножества) си -_-) не считаем.

Конечно, не считаем, даже если бы был полный. Корректность программы/преобразования/чего-либо - самое неинтересное свойство. Ну мы ж когда программу пишем, то мы специально пишем ее так, чтобы она была корректна. И если мы доказали корректность - это нам ничего не дает, это то же самое, что заявить, что 2*2=4. Все и так это знают. Это ожидаемо. Любой ожидаемый результат бесполезен.

Ещё раз — JML для Java

JML это не формализм для джава, во-первых. Во-вторых - это бесполезная на практике игрушка. Ты его видел вообще? Де-факто, JML - это такой язык, причем сам чуть ли не сложнее джавы, то есть вероятность посадить ошибку в JML выше чем в джава-коде, который ты этим JML аннотируешь. То есть можно для любого языка X взять семантически близкий, но синтаксически далекий (чтобы нельзя было копипастить) язык и заставить программиста любой код писать сразу на обоих ЯП, а потом компилятор будет сравнивать две программы на равенство и кричать «аларм, аларм», если равенство у него вывести не выходит. Вот это и делает JVM.

доказательств заявленных свойств программ

Да не надо доказывать свойства программ. Это неинтересно, это ничего не дает. Я вообще не про это. Я про свойства языков. Про формализм для описания и анализа _языков_, а не программ.

Про отсутствие формализма для того же си

Ну я уточнил на счет формализма. Смысл формализма в том, что мы можем на его основании получить неожиданный/невозможный в случае отсутствия формализма результат. Иначе это не формализм, а протсо переливание из пустого в порожнее. Какие результаты анализа языка «си» получены в результате использования указанного формализма?

На си идет писать водитель, который полюбовался на сферически вакуумный идеально твердый мост, и поехал через реку по нормальному. Инженеры в данном случае - люди, занимающиеся CS, а не программированием (то есть обслуживающие программистов).

В математике вообще бесконечно много чего существует, при этом большая часть - херня. Скорее всего, даже почти все (в мат. смысле) - херня.

Ну то есть вообще говоря ничего плохого в этом нет - кто-то пишет стихи, кто-то рисует картины, кто-то записывает рэпчик с корешами, а кто-то - надрачивает на зависимые типы с октанионами. Это вещи одного порядка, и они не являются плохими сами по себе - главное, чтобы продукт в результате качественный получался.

Можно пример, как кто-то нашел какие-то неожиданные свойства существующего языка, которые без формализации были неочевидны?

Там про свойства конкретных программ, то есть то что нужно на практике.

Свойства целого языка это другое. Если это то о чём ты хочешь говорить — ты уже сказал про подтипирование и неразрешимость. Зависимые типы — неразрешимость вывода типов. Выяснение правильности для отношения типизации. Ещё выяснение нормализации может быть интересно. Выяснение корректности трансляции source в target. Поиск моделей, то есть непротиворечивость, в случае ULC, например, целая решётка теорий от наименьшей противоречивой до наибольшей непротиворечивой. Curry-Howard-Lambek-Seely-.... Дуальности. Монады в «системах частичности» (partiality monad), системах эффектов и семантике/интерпретации лично мне показались интересными. Полиномиальные типы-функторы и «производные» от них. Коиндукция, корекурсия. Ну и так далее, «для кого-то есть еще факты такого рода».

Тем не менее, с чего вообще формализация обязана выявлять какие-то «новые свойства» жабы или ещё чего-то? Все свойства уже экспериментально известны. Зато она может помогать в статическом анализе (хотел «анализ» же :)) и оптимизациях.

Ты его видел вообще?

Нет, я сказал что не смотрел Krakatoa вообще, так как Java не использую. Я Jessie тыкал палочкой — внешний язык в комментариях для описания свойств, да, сложный (выразительный то есть), да (и поэтому я не представляю как можно «засадить ошибку» в propositions), но он опирается на модельную формализацию си (иначе что он тогда вообще описывает?) о которой можно почитать в публикациях про Jessie (одна ссылка уже была выше).

Это неинтересно, это ничего не дает. Я вообще не про это. Я про свойства языков.

Ок.

Какие результаты анализа языка «си» получены в результате использования указанного формализма?

Я выше тоже уточнил — какие вообще результаты тут могут быть? Си же не идиоты создавали, да и до си были языки (и до первых ЭВМ) — всё основное известно, поэтому модели таких объезженных языков полезны для анализа свойств конкретных программ (семантика) и их трансляций (оптимизации).

В разработке _новых_ языков такие формализации могут быть полезны. На самом деле http://en.wikipedia.org/wiki/Turing_Award — списочек имён. Ещё интересно взять этот списочек (и вообще раннее CS) и посмотреть (http://www.youtube.com/watch?v=kO-8RteMwfw) кто был в advisors. Ещё — посмотреть статьи Stepanov, SPJ, Odersky, сколько угодно продолжать, и какие формализации они вовлекают.

На си идет писать водитель, который полюбовался на сферически вакуумный идеально твердый мост, и поехал через реку по нормальному. Инженеры в данном случае - люди, занимающиеся CS, а не программированием (то есть обслуживающие программистов).

Программист <: Инженер, ящитаю. Ну и человек на видео утверждает, что не полюбовался, а написал модель, поизучал её и сделал ручной extraction в C++ (не си). Дизайнеры STL, MPL (boost), Fusion (boost) тоже не один C++ изучали, очевидно (суммы и произведения типов? BiCCC? — не проблема :)).

В математике вообще бесконечно много чего существует, при этом большая часть - херня. Скорее всего, даже почти все (в мат. смысле) - херня.

Я про «существует» и при этом «связно со всем остальным» и «универсально», отсюда — скорее всего, оно фундаментально. То есть понятно, что можно в математике найти что-то существующее и не особо нужное — просто составить какое-нибудь доказуемое, но сложное утверждение, например — существует, но зачем?

а кто-то - надрачивает на зависимые типы с октанионами

Октонионы они как комплексные числа (и кватернионы). Про применения в квантовой физике всех трёх можешь погуглить.

Ну а зависимые типы это суть квантификации («для всех» и «существует»), под- функциональные пространства с декартовыми произведениями или нетривиальные расслоения (сечения и втягивания). Для примера — Nat -> Nat и Nat * Nat — обычные функциональное пространство и произведение, P(n : Nat). Vec T n и S(n : Nat). is-odd n — эти самые, или как с лентой Мёбиуса — обычным произведением будет цилиндр. Вообще, если есть топос (или LCCC) — есть зависимые типы (во внутренней системе типов топоса). Причём зависимые суммы и произведения и дуальны и универсальные конструкции в таких категориях.

А в программирование их нужно тащить потому что нельзя не тащить (если мы тащим статическую типизацию, потом параметризм, потом индексацию, то в определённый момент без зависимых типов становится хреново — до этого уже докатились C++, Scala и Haskell, ну и в системах лямбда куба вершина это единственная система где можно иметь Term = Type, это же насильно заставляет вводить в язык систему частичности и эффектов — номер два «хорошо», можно нахваливать не только отделение эффектов и чистого кода, но и отделение тотального и частичного).

Там про свойства конкретных программ

Свойства конкретных программ нам на практике не нужны.

Тем не менее, с чего вообще формализация обязана выявлять какие-то «новые свойства» жабы или ещё чего-то?

Не обязана. Но если она этого не делает - то она не нужна.

Все свойства уже экспериментально известны.

Дык неожиданные свойства на то и неожиданные, что до их открытия все думали, что они известны :) Почитай первую часть гидродинамики Биркгофа :)

да, сложный (выразительный то есть), да (и поэтому я не представляю как можно «засадить ошибку» в propositions

Ты сам себе противоречишь. Вероятность возникновения ошибки прямо пропорциональна (количество кода)*(сложность кода) По-этому когда язык описания сложнее языка, который мы описываем, а по вербозности от него не сильно далек - то выходит, что насадить там ошибок гораздо проще. И по факту, как я выше сказал, это описание ничем не отличается от обычного с проверкой компилятором того факта, что оба дубля делают одно и то же.дублирования.

В разработке _новых_ языков такие формализации могут быть полезны.

В разработке новых через формализацию они как раз бесполезны, т.к. тогда точно никаких новых свойств не будет. А значит формализация снова не нужна.

Программист <: Инженер, ящитаю.

в моей аналогии программист - водитель грузовика, который едет по мосту. Инженер - ну тот же SPJ :)

Я про «существует» и при этом «связно со всем остальным» и «универсально», отсюда — скорее всего, оно фундаментально.

Оно вся связано и фундаментально. И при этом - херня.

То есть понятно, что можно в математике найти что-то существующее и не особо нужное — просто составить какое-нибудь доказуемое, но сложное утверждение, например — существует, но зачем?

Да не надо ничего сложного там составлять. 99.999% всей математики на данный момент - это оно и есть, существует, но зачем?

Так получается просто потому, что почти вся математика относится как раз к классу «существует но зачем».

Октонионы они как комплексные числа (и кватернионы). Про применения в квантовой физике всех трёх можешь погуглить.

Да ну ради бога, пусть они где-то локально очень редко применяются 3.5 анонимусами, при этом с нулевым практическим результатом (даже в плане удобства языка). А какие-то пацаны, как я уже сказал, рэпчик сочиняют. Ничего плохого.

Ну а зависимые типы это суть квантификации

Зависимые типы - это просто ненужное усложнение концепций, которым уже 50 лет.

То есть если говорить о корректности программ - ее доказывать может любой школьник, безо всяких зависимых типов и прочего говна. 50 лет назад так и доказывали. И с тех пор ничего не изменилось качественно - используют те же принципы, только за счет общего развития компьютерной техники некоторые вещи автоматизированы. А зависимые типы-- опять же, еще одна попытка ненужного размножения сущностей, люди пытаются назвать те же понятия другими словами, не получают отсюда никакого профита, но довольны - диссеры-то идут!

А в программирование их нужно тащить потому что нельзя не тащить

В программирование их тащить нельзя, потому что не нужно.

Смотри, есть очень узкий класс программ, которым действительно нужна доказанная корректность. Это единицы программ, на них приходятся миллионы, в которых корректность не нужна. Соответственон, зависимые типы там сразу тоже становятся совершенно ненужны. Это бесспорный факт, и из него следует другой бесспорный факт - практическая применимость зависимых типов так и останется в рамках единичных программ.

Если же нам нужна корректность - то зависимые типы снова не нужны, т.к., как я выше сказал, ее может любой сообразительный ученик средней школы доказывать не хуже любителя агды, с тем же успехом, при этом без теорката, лямбда-куба и прочей ненужной фигни. Просто потому что любитель агд с теоркатами делает ровно то же самое, что и тот школьник, только называет другими словами.