Теория последовательностей

Теория последовательностей или теория строк, называемая также чистым синтаксисом — изучает символьные строки, над конечными алфавитами, в виде символов, знаков, обозначений или меток. Теория строк является основой формальной лингвистики^[англ.], информатики, логики и метаматематики, особенно теории доказательств^[1]. Порождающая грамматика, может рассматриваться, как рекурсивное определение, в теории строк.

Наиболее простой операцией над строками является конкатенация:

Соединение двух строк, для получения более длинной строки, информация о которой складывается из суммы значений этих строк.

ABCDE — конкатенация AB и CDE, в символах ABCDE = AB ^ CDE.

Строки и конкатенация строк могут рассматриваться как алгебраическая система со свойствами, напоминающими свойства сложения целых чисел. В современной математике такая система называется свободным моноидом^[англ.].

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