Теория конкатенации

Чтобы узнать о теории струн в физике, см. Теорию струн .

Теория конкатенации , также называемая теорией строк , теорией символьных строк или теоретическим синтаксисом , изучает строки символов в конечных алфавитах символов, знаков, символов или меток. Теория струн является основой формальной лингвистики , информатики, логики и метаматематики, особенно теории доказательств. Генеративную грамматику можно рассматривать как рекурсивное определение в теории струн.

Самая основная операция над строками — это конкатенация ; соедините две строки, чтобы сформировать более длинную строку, длина которой равна сумме длин этих двух строк. ABCDE — это объединение AB с CDE в символах ABCDE = AB ^ CDE. Строки и конкатенацию строк можно рассматривать как алгебраическую систему с некоторыми свойствами, напоминающими свойства сложения целых чисел; в современной математике эта система называется свободным моноидом .

В 1956 году Алонсо Чёрч писал: «Как и любая отрасль математики, теоретический синтаксис может и, в конечном итоге, должен изучаться аксиоматическим методом». Черч, очевидно, не знал, что теория струн уже имела две аксиоматизации 1930-х годов: одну Ганса Гермеса и одну Альфреда Тарского . По совпадению, первая английская презентация аксиоматических основ теории струн Тарского 1933 года появилась в 1956 году – в том же году, когда Чёрч призвал к такой аксиоматизации. Как отмечал сам Тарский, используя другую терминологию, серьезные трудности возникают, если строки интерпретировать как токены, а не типы в смысле различия типа и токена Пирса .