Permutability of inferences and categorical equivalence of derivations in IMLL

Основным результатом статьи является доказательсво теоремы, что отношение эквивалентности на выводах интуиционистской мультипликативной линейной логики, порожденное перестановками правил в стиле Клини, совпадает с отношением эквивалентности, порожденным структурой свободной симметрической моноидальной замкнутой категории на том же исчислении. Как известно, в категорной структуре формулы играют роль объектов, связкам соответствуют функторы, а морфизмами являются классы эквивалентности выводов секвенций вида А -> В. Интерес к этому исчислению объясняется, с одной стороны, богатством категорных моделей (от модулей над коммутативными кольцами с 1 до множеств с отмеченной точкой и частичных порядков), а с другой - его нетривиальностью с точки зрения теории доказательств. Основной результат статьи позволит улучшить сложностные характеристики существующих разрешающих алоритмов для категорией эквивалентности. Ряд лемм сформулирован для более сильных отношений эквивалентности, соотвествующих несвободным категорным моделям, что позволяет применить методы теории доказательств для их изучения, в том числе, в задаче проверки коммутативности диаграмм в категориях, преставляющих интерес с точки зрения алгоритмов, используеых в системах символьных вычислений.