Оценки на длину совмещающего типа в исчислении Ламбека

Тип $C$ называется совмещающим типом для типов $A$ и $B$ в секвенциальном исчислении $L$, если секвенции $A \rightarrow C$ и $B \rightarrow C$ являются выводимыми в $L$. В случае исчисления Ламбека и мультипликативной линейной логики критерий существования для данных типов $A$, $B$ соответствующего типа $C$ был доказан M. Р. Пентусом в 1993г. В настоящем докладе приводятся верхние оценки на минимальную длину совмещающего типа (в случае его существования) для обоих исчислений, а также нижняя оценка на его длину в случае мультипликативной линейной логики (следовательно, эта оценка справедлива и для исчисления Ламбека). Как верхняя, так и нижняя оценка являются квадратичными.