ну вот утверждается, что в Set декартово произведение является произведением, а значит термин "произведение" взяли не с потолка.

поэтому и "масло масляное"

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

В коке\идрисе для доказательств подобных тоже вводят ФЭ как аксиому

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

Проблема в том, что простое равенство, как последовательностей, не работает, нужно вводить классы эквивалентности (примерно с таким смыслом: эквивалентные процессы идут к одинаковому поведению). Эта эквивалентность кучерявая, и для неё сложно показывать единственность, как мне кажется.

push; cur(q); swap; cur(p); go; swap; go; cons; pop - такой кусок кода, и поди докажи, что другого быть не может.

Так тоже можно. В теории типов это называется эта-эквивалентностью, и она в точности соответствует уникальности.

Вы пытаетесь ввести равенства на тьюринг-полных вычислениях? А что будете делать если код зациклился?

Собственно. Это и есть основной мой интерес в этой работе. Нашёл два варианта.

1. Можно рассмотреть ленивые вычисления. Тогда всё ok (для процессов исполнения, которые бесконечные) и довольно просто.

2. Можно ввести в модель прерывания: сидит оператор, и иногда тыкает кнопку skip. Эквивалентность с точностью до skip-ов определить получилось. Но вот с произведением засада. Равенства для проекций выполняются. А с единственностью не понятно.

Равенства выполняются на классах skip-эквивалентных процессов. Даже если они зацикливаются.

А вы про теорию доменов Скотта читали? Кажется, что вы пытаетесь изобрести велосипед
P.S. И переход к ленивым вычислениям не спасает, потому что не у всех термов есть даже слабая нормальная форма

На русском, правда, про неё только у Барендрегта есть

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

У Скотта этот момент плохо прописан. У него декартово произведение определено с учётом существования элементов (\bottom, b) и (a, \bottom). В таком случае всё хорошо. Но в реальности мы не можем построить такие вычислительные процессы. Поэтому он сам говорит: в реальности у нас не произведение, а smashed-произведение: если завис один компонент вычисления, то зависло всё. Но такое проиведение не будет декартовым.

Ну. Или нужно отказываться от тьюринг-полноты. А не хочется.

У вас процесс, который одно значение возвращает?

Или многоэлементный стрим?

Стрим

В общем случае на стримах с эффектами\асинхронных\конкурентных\распределённых вроде и не получается нормального декартова произведения.
Там обычно строится моноидальная категория с несколькими произведениями

И чем их больше, тем лучше!
(почти даже и не шутка)