Теория конкатенации , также называемая теорией струн , теорией символьных строк или теоретическим синтаксисом , изучает строки символов над конечными алфавитами символов, знаков, символов или отметок. Теория струн является основополагающей для формальной лингвистики , компьютерной науки, логики и метаматематики, особенно теории доказательств. [1] Генеративную грамматику можно рассматривать как рекурсивное определение в теории струн.
Самая простая операция над строками — конкатенация ; соединение двух строк для формирования более длинной строки, длина которой равна сумме длин этих двух строк. ABCDE — это конкатенация AB с CDE, в обозначениях ABCDE = AB ^ CDE. Строки и конкатенацию строк можно рассматривать как алгебраическую систему с некоторыми свойствами, напоминающими свойства сложения целых чисел; в современной математике эта система называется свободным моноидом .
В 1956 году Алонзо Чёрч писал: «Как и любая ветвь математики, теоретический синтаксис может и в конечном итоге должен изучаться аксиоматическим методом». [2] Чёрч, очевидно, не знал, что у теории струн уже было две аксиоматизации 1930-х годов: одна Ганса Гермеса и одна Альфреда Тарского . [3] По совпадению, первое английское представление аксиоматических основ теории струн Тарского 1933 года появилось в 1956 году — в том же году, когда Чёрч призвал к таким аксиоматизациям. [4] Как заметил сам Тарский, используя другую терминологию, возникают серьёзные трудности, если строки интерпретируются как токены, а не типы в смысле различия типа и токена Пирса .