\begin{definition}[Definition:Length of String]
The '''length''' of a finite string in a formal language is the number of symbols it contains.
The '''length''' of a string $S$ can be denoted $\map \len S$ or $\size S$.
\end{definition}