Oℕ
взяли произведение в обратной категории - получили копроизведение в исходной
Size: a a a
2019 December 02
Oℕ
и т.п.
Oℕ
про физику ничего не знаю, но догадываюсь, что ток и время в обратном направлении - это скорее про dagger категории
V
С_op помимо функторов существует для того, чтобы не дублировать определения один в один друг на друга похожие, а просто добавлять co
Ещё есть примеры, где дульная категория сама по себе интересна. Например, фреймы/локали и коммутативные кольца/аффинные схемы.
ЕО
Проблема в том, что простое равенство, как последовательностей, не работает, нужно вводить классы эквивалентности (примерно с таким смыслом: эквивалентные процессы идут к одинаковому поведению). Эта эквивалентность кучерявая, и для неё сложно показывать единственность, как мне кажется.
Давайте к этому вернёмся. Вы хотите вычислениям приписать эквивалентности на уровне порядка изменения памяти, абстрагируясь от самого хода вычислений?
МБ
Давайте к этому вернёмся. Вы хотите вычислениям приписать эквивалентности на уровне порядка изменения памяти, абстрагируясь от самого хода вычислений?
Что означает "абстрагироваться от вычисления"? Код - это же часть процесса исполнения
ЕО
Ну зависит от модели вычисления, в общем случае нет. Просто мне непонятна (но интересна) задача :) В общем случае как-то кажется, что для вычислений лучше порядки подходят чем равенства
МБ
Ну зависит от модели вычисления, в общем случае нет. Просто мне непонятна (но интересна) задача :) В общем случае как-то кажется, что для вычислений лучше порядки подходят чем равенства
Задача примерно такая: есть VM. Она порождает трассы во время работы. Вопрос: будет ли у трасс структура ДЗК? Если будет, то машина "хорошая".
МБ
Ну зависит от модели вычисления, в общем случае нет. Просто мне непонятна (но интересна) задача :) В общем случае как-то кажется, что для вычислений лучше порядки подходят чем равенства
На порядках не очевидно мне, как получать эту самую ДЗК. Была идея рассматривать обогащения. Но в них же тоже требуются равенства морфизмов.
ЕО
А что семантически будет B^{A}?
МБ
А что семантически будет B^{A}?
Если программа заканчивается для некоторых значений (состояний памяти), то она вычисляет некую частичную функцию
ЕО
Ну тут какое-то несоответствие получается, либо смотреть на конечные значения, либо на поток вычисления. Если брать поток вычисления, то VM это, всё-таки, преобразование A -> Stream A
МБ
Ага. Но машины же так и работают. Надо познать машины!
Oℕ
Задача примерно такая: есть VM. Она порождает трассы во время работы. Вопрос: будет ли у трасс структура ДЗК? Если будет, то машина "хорошая".
Ну если декартово произведение, то например <pi1, pi2> = id
Поэтому сначала нужно придумать равенство между трассами соответствующее
Поэтому сначала нужно придумать равенство между трассами соответствующее
Oℕ
Т.е. это точно не может быть структурным равенством списков действий каких-то.
Как минимум должно быть равенство с точностью до каких-то преобразований или нормальной формы
Как минимум должно быть равенство с точностью до каких-то преобразований или нормальной формы
Oℕ
А нормальная форма и будет выглядеть зачастую просто как функция с какими-то эффектами/коэффектами
МБ
Т.е. это точно не может быть структурным равенством списков действий каких-то.
Как минимум должно быть равенство с точностью до каких-то преобразований или нормальной формы
Как минимум должно быть равенство с точностью до каких-то преобразований или нормальной формы
Ага. Поэтому всякие эквивалентности
ЕО
Ага. Но машины же так и работают. Надо познать машины!
Ну это достаточно хорошо познано как работают вычисления, по крайней мере если пространство вычислений эквивалентно пространству данных. А если нет — то претендовать на CCC бессмысленно :)
МБ
Ну это достаточно хорошо познано как работают вычисления, по крайней мере если пространство вычислений эквивалентно пространству данных. А если нет — то претендовать на CCC бессмысленно :)
Почему?