Concatenation theory, also called string theory, character-string theory, or theoretical syntax , studies character strings over finite alphabets of characters, signs, symbols, or marks. String theory is foundational for formal linguistics, computer science, logic, and metamathematics especially proof theory. [1] A generative grammar can be seen as a recursive definition in string theory.
The most basic operation on strings is concatenation; connect two strings to form a longer string whose length is the sum of the lengths of those two strings. ABCDE is the concatenation of AB with CDE, in symbols ABCDE = AB ^ CDE. Strings, and concatenation of strings can be treated as an algebraic system with some properties resembling those of the addition of integers; in modern mathematics, this system is called a free monoid.
In 1956 Alonzo Church wrote: "Like any branch of mathematics, theoretical syntax may, and ultimately must, be studied by the axiomatic method". [2] Church was evidently unaware that string theory already had two axiomatizations from the 1930s: one by Hans Hermes and one by Alfred Tarski. [3] Coincidentally, the first English presentation of Tarski's 1933 axiomatic foundations of string theory appeared in 1956 – the same year that Church called for such axiomatizations. [4] As Tarski himself noted using other terminology, serious difficulties arise if strings are construed as tokens rather than types in the sense of Peirce's type-token distinction.