#матлог #учёба #спецсеминар

Семинар "Вычислимость и неклассические логики" работает по пятницам с 16.45 в аудитории 425.

14 ноября 2025 г.

Г. Г. Черевиченко
"Номинальная унификация" (продолжение доклада от 31 октября)
Унификация в простейшем случае — это решение уравнений в свободных алгебраических системах. Например, рассмотрим алфавит из двух символов a,b и уравнение aX=Yb, где X и Y обозначают слова в этом алфавите (которые надо найти). Слова с операцией приписывания образуют свободную полугруппу. Решение выглядит так: берём произвольное слово Z и полагаем X=Zb, Y=aZ, тогда aX=aZb=Yb. Мы как бы подобрали слово (aZb), подходящее под оба шаблона aX и Yb, от этого слово "унификация". В более хитрых случаях слова (например, формулы логики первого порядка или лямбда-термы) могут содержать связывающие операции (кванторы, лямбды) и рассматривать их надо с точностью до переименования связанных переменных. Проблема унификации в этом случае имеет неожиданное красивое решение.

➰ ВК