Отношение совместимости в исчислении Ламбека с операциями замещения

Два типа $A$ и $B$ некоторого исчисления называются совместимыми, если существует тип $C$, такой что секвенции $A \to C$ и $B \to C$ обе являются выводимыми. При этом свойства отношения совместимости тесно связаны с порождающей способностью грамматик, основанных на данном исчислении. В докладе рассматривается отношение совместимости для исчисления $\mathrm{HDL}$, представляющего собой несеквенциальный вариант исчисления Ламбека с операциями замещения. Будет доказано, что два типа данного исчисления совместимы тогда и только тогда, когда совпадают их интерпретации в свободной абелевой группе, порождённой примитивными типами.