Индексированное исчисление Ламбека с передвижением

Исчисление Ламбека обычно интерпретируют как логику строк и конкатенации строк; именно в таком качестве оно используется в лингвистических приложениях. Однако давно замечено, что с точки зрения лингвистических приложений такой простой структуры обычно оказывается недостаточно, и требуется рассматривать более сложные объекты и операции.
Мы определяем специфическую алгебру термов, которые обозначают упорядоченные последовательности строк и могут комбинироваться между собой более сложными способами, чем простая конкатенация. Далее мы вводим систему типов для таких термов. Эта система представляет собой неассоциативное, но частично коммутативное расширение исчисления Ламбека, которое нам кажется с одной стороны достаточно простым и интересным, а с другой стороны достаточно выразительным.