Об одном классе неравенств для ортонормированных систем // Матем. заметки. <...> Поступила в редакцию 01.03.2010 УДК 510.649 О ДЛИНЕ СОВМЕЩАЮЩЕГО ТИПА В ИСЧИСЛЕНИИ ЛАМБЕКА А.А. <...> Сорокин1 В 1992 г. М.Р. Пентусом был установлен критерий существования такого типа C,что для данных типов A и B секвенции A→C и B →C являются выводимыми в исчислении Ламбека. <...> В настоящей статье предлагается алгоритм построения типа C (в случае, если он существует) и доказывается квадратичная верхняя оценка его длины. <...> Ключевые слова: исчисление Ламбека, интерпретация в свободной группе, совместимость, совмещающий тип. <...> Pentus established a criterion for the existence of a type C such that for given types A and B the sequents A → C and B → C are derivable in the Lambek calculus. <...> Исчисление Ламбека было введено в статье [1] для моделирования синтаксической структуры предложения. <...> Назовем примитивными типами элементы множества Pr = {p1,p2,.} <...> . Тогда множество Tp типов исчисления Ламбека есть наименьшее 1Сорокин Алексей Андреевич — студ. каф. математической логики и теории алгоритмов мех.-мат. ф-та МГУ; e-mail: alexey.sorokin@list.ru. <...> №3 11 по включению множество, удовлетворяющее следующим условиям: Pr ⊂ Tp и для всех типов A и B из Tp элементы (A · B), (B\A) и (A/B) также принадлежат Tp. <...> Внешние скобки в записи типа мы будем опускать. <...> Определим длину типа l(A) как число вхождений примитивных типов. <...> Элементы Tp будем обозначать большими латинскими буквами A,B,C,., а последовательности типов — большими греческими буквами Π,Γ,∆,. <...> Выражения вида Γ→A, где последовательность Γ непуста, называются секвенциями исчисления Ламбека. <...> Исчисление Ламбека имеет единственную аксиому A → A. <...> Это позволит нам опускать скобки в выражениях вида A · B · C и C\A/B. <...> В приложениях часто возникает вопрос построения такого типа C, что в исчислении Ламбека вывоdual(B)\Pdual(A), dual(B\A) = dual(A)/dual(B), dual <...>