Документ взят из кэша поисковой машины. Адрес оригинального документа : http://www.mccme.ru/lifr/clkr2012/abssorokin.pdf Дата изменения: Wed May 23 17:44:42 2012 Дата индексирования: Tue Oct 2 13:01:52 2012 Кодировка: Windows-1251 Поисковые слова: http astrokuban.info astrokuban

Длина совмещающего типа в исчислении Ламбека
А. А. Сорокин

Тип в

C

называется совмещающим типом для типов

A

и

B

в секвенциаль-

ном исчислении

L,

если секвенции

AC

и

BC A, B

являются выводимыми соответствующего типа

L.

В случае исчисления Ламбека и мультипликативной линейной логики

критерий существования для данных типов

C

был доказан M. Р. Пентусом в 1993 г. В настоящем докладе приводятся

верхние оценки на минимальную длину совмещаюшего типа (в случае его существования) для обоих исчислений, а также нижняя оценка на его длину в случае мультипликативной линейной логики (следовательно, эта оценка справедлива и для исчисления Ламбека). Как верхняя, так и нижняя оценка являются квадратичными.

1