𝔽₁

[akuklev]

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

И поэтому сегодня я хотел поговорить о матрицах - прямоугольных табличках чисел, и эти таблички можно перемножать, если число столбцов в первой равно числу строчек во второй, и это умножение ассоциативно. И есть нейтральные элементы у этого умножения - квадратные матрицы n × n с единицами на главной диагонали и нулями за её пределами. Это по-математически называется “матрицы образуют категорию”.

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

Однако числа, как известно, бывают разные. Можно говорить о матрицах вещественных чисел или матрицах рациональных чисел, например. А имеет ли смысл говорить о матрицах, скажем, натуральных чисел?

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

Чтобы можно было определить умножение и сложение матриц, и все законы этих действий выполнялись (по-математически, “матрицы всё ещё образовывали дистрибутивную симметричную моноидальную категорию”), достаточно чтобы числа в них образовывали унитальное полукольцо. Такую структуру альтернативно называют https://ncatlab.org/nlab/show/rig. Натуральные числа его образуют.

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

Так вот, это наводит на мысль ввести понятие “частичных унитальных полуколец” (partial rig) и матриц над ними.

Например мы можем взять комплексные числа по модулю не больше единицы, и, соответственно, все суммы выходящие по модулю за 1 запрещаются - это про амплитуды в квантовой механике. Или вещественные числа в интервале [0, 1] - это про вероятности. Или натуральные числа, в которых запретили все числа больше 1, - это получается partial rig (обозначим его через 𝔽₁) из двух элементов {0, 1}, а матрицы над ним - матрицы из нулей и единиц, где в каждом столбце разрешается не более одной единицы.

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

Если partial rig обладает тем свойством, что всякая несигнулярная квадратная матрица над ним обратима, мы будем называть его partial field. Вот это вот вышеупомянутое 𝔽₁ оказывается partial field. И я много лет именно так думаю о так называемом “поле с одним элементом” (https://en.wikipedia.org/wiki/Field_with_one_element).

Категория матриц над ним (её ещё можно назвать “категория векторных пространств над полем с одним элементов”) - это в точности категория множеств с частичными отображениями между ними. Ну или, если угодно, эквивалентно категория пространств с выделенной точкой и сохраняющих точку отображений между ними.

Ещё, кстати, можно ввести гипотетическое определения partial ACF (алгебраически замкнутого частичного поля) - это такое частичное поле, что у всякой квадратной матрицы над ним существует собственный вектор.

* * *

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

Теории типов и исчисления построений, оперирующие только платоническими математическими объектами сравнительно хорошо поняты, и ключевую роль там играют индуктивные типы (вообще говоря, фактор-индуктивные типы) - инициальные модели алгебраических теорий (https://en.wikipedia.org/wiki/Algebraic_theory), а произвольная модель алгебраической теории с носителем T это то же самое, что мотив элиминации из соответствующего индуктивного типа. То есть мы там имеем для каждой алгебраической теории F полиморфный тип F-алгебр Alg_F[T : *].

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

Статья которую я читал ночью - Functorial Semantics for Partial Theories (https://arxiv.org/abs/2011.06644), что выглядит для меня как корректно нащупанный подход к определению алгебраических теорий над частичным полем с одним элементом 𝔽₁.

Следующий шаг - понять как это должно работать для произвольного частичного поля, и как на самом деле правильно определять частичное поле. Вот уже семь лет как мне кажется, что правильный путь описан в статье Алена Конна и Катерины Консани https://arxiv.org/abs/1502.05585. Я убеждён, что в терминах таких теорий мы сможем элегантно описывать eventual consistency в распределённом программировани и квантовую спутанность в физике.

Upd: Пока я писал этот пост, я нашёл их новую статью про это https://arxiv.org/pdf/2307.06748.pdf, которую ещё не читал.