(no subject)

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

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

Равенство действительно разрешимо, а вот стандартных 11 аксиом недостаточно. Все дело в том, что многочленов, имеющих натуральные значения на натуральных аргументах (integer-valued polynoms) больше, чем многочленов над натуральными числами, например n(n - 1)/2 натуральнозначен, не смотря на наличие в нем ненатуральных коэффициентов (1/2 дробное, а -1/2 ещё и отрицательное число, потому что всегда либо n, либо (n - 1) делится на два, а единственный случай, когда (n - 1) отрицательное не страшен, потому что тогда n = 0 и всё произведение зануляется. К счастью, Поля ещё в 1916 году доказал, что все натуральнозначные многочлены получаются из биномиальных коэффициентов, (n ! 2) = n(n - 1)/2, (n ! 3) = (n ! 2)*(n - 3)/3, ...

Так вот, чтобы можно было вывести все тождества про многочлены-с-возведением-в-степень, надо добавить к системе операции !m для каждого целого m больше нуля, и на каждую по аксиоме вида m * ( (n ! m) + (n ! (m - 1)) ) = (n ! (m - 1)), ну и (n ! 1) = n.

Если этого не сделать, часть верных тождеств нельзя будет вывести из-за невозможности вынести за скобки многочлены навроде n^2 - n + 1, как в знаменитом примере Wilkie, см. Википедию. А конечного набора аксиом, из которого можно было бы вывести все тождества для многочленов с возведением не бывает, так-то.

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

Ссылки:
http://en.wikipedia.org/wiki/Tarski%27s_high_school_algebra_problem
http://www.dicosmo.org/Papers/mscs-survey.pdf
http://www.cs.nott.ac.uk/~txa/talks/away13.pdf (Альтенкирх про типы)

(* На самом деле, он предлагал добавить не только возведение в степень, но ещё и тетрацию и все остальные стрелки Кнута.)

(no subject)

Мне очень давно было интересно понять, можно ли обобщить понятие алгебраической замкнутости с колец на полукольца. Если от колец потребовать, чтобы каждый многочлен ненулевой степени имел корень, они во-первых превращаются в поля (потому что многочлен ax - b должен иметь корень, и это как раз b/a со всеми потребными свойствами. Во-вторых, они обретают совершенно фундаментальное свойство, что у каждого эндоморфизма F^n есть собственный вектор, т.е. fixpoint.

На роль примера "алгебраически замкнутого полукольца", кажется, подходят полиномиальные функторы, для них определены ноль, единица, сумма и произведение с обычными законами полукольца, плюс каждая система уравнений
X1 = P1(X1,...,X_n)
X2 = ...
, где P полиномиальные выражения, существует решение.

В поле эта штука не превращается, зато превращается в замкнутое (в смысле наличия звёздочки Клини) полукольцо. И вот свойство, что у эндоморфизмов есть фикспоинт, кажется, тоже выходит. Это я посмотрел на отличную статью Brent Yorgey (из позапрошлого поста) про то, что для полиномиальных функторов определена операция ограничения регулярным выражением, обобщающая дифференцирование, диссекцию и конечные разности: http://dept.cs.williams.edu/%7Ebyorgey/pub/type-matrices.pdf

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