Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

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

В 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 (Альтенкирх про типы)

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

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 5 comments