A branch of automata theory which attempts to formulate the grammar of a language in mathematical terms; it has been applied to automatic language translation and to the construction of higher-level programming languages and systems such as the propositional calculus, nerve networks, sequential machines, and programming schemes.