Большинство алгебраических теорий, которые сегодня активно используются в computer science и формальной верификации, построены на

Большинство алгебраических теорий, которые сегодня активно используются в computer science и формальной верификации, построены на предположении об ассоциативности. Это касается теории идеалов, понятий регулярности, морфизмов, конгруэнций и многих других конструкций. Когда структура неассоциативная, почти вся эта классическая техника либо перестаёт работать, либо даёт сильно вырожденные результаты.

В то же время принято считать, что фундамент всей алгебры в конечном счёте опирается на теорию множеств. Однако и сама теория множеств, и построенная на ней алгебра в значительной степени используют ассоциативные структуры как базовый рабочий инструмент. Это создаёт определённую слепую зону: неассоциативные алгебры остаются заметно менее разработанными, особенно когда речь идёт о witness-ориентированных подходах и явной проверяемости вычислений.

В Singular STAR Algebras центральную роль играет элемент P0, который одновременно является левым нулём и правым идентификатором:

P0 * x = P0 x * P0 = x

Такое сочетание позволяет внутри строго конечной структуры моделировать поведение, которое в классических подходах обычно требует введения бесконечности или специальных предельных конструкций. P0 здесь работает как сингулярная точка и экстремум: он поглощает информацию слева и при этом сохраняет её справа. Благодаря этому предельные и граничные эффекты возникают без необходимости явно работать с бесконечными объектами.

Именно поэтому я и решил назвать это семейство алгебр STAR Algebras (SA). Название отражает наличие сингулярного элемента P0, который берёт на себя роли, обычно связанные с бесконечностью и предельными состояниями, оставаясь при этом внутри конечной алгебры.

Таким образом, хотя фундамент алгебры традиционно связывают с теорией множеств, можно посмотреть глубже. Значительная часть этого фундамента фактически покоится на структурах, где ассоциативность принимается как данность, а сингулярные и предельные явления либо выносятся за скобки, либо требуют дополнительных конструкций. STAR Algebras предлагают альтернативный взгляд, в котором неассоциативность и наличие такого сингулярного элемента становятся отправной точкой.

В этом случае witness перестаёт быть просто следствием классических доказательств и становится основным инструментом проверяемости, который извлекается напрямую из траектории вычисления. Такой подход пока развит слабо, и именно в этом направлении я продолжаю работу.

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