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