I learned from Herre & Schroeder-Heister's "Formal Languages and Systems" that

A formal system is based on a formal language $L$, endowing it with a consequence operation $C: 2^L\to 2^L$.

https://en.wikipedia.org/wiki/Rewriting says

In mathematics, computer science, and logic, rewriting covers a wide range of (potentially non-deterministic) methods of replacing subterms of a formula with other terms. The objects of focus for this article include rewriting systems (also known as rewrite systems, rewrite engines1 or reduction systems). In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.

It lists

(After reading them, I am not very sure of the differences between the three.)

What are the relations and differences between formal systems, rewriting systems (including the three listed), formal grammars and automata (considering their state transition functions)?

  • Is a rewriting system a formal system? Is a formal system a rewriting system? (Both seem yes to me, because the consequence operation and rewriting rules seem the same.)

  • Is a formal grammar a rewriting system? Is a formal grammar a formal system? (Both seem yes to me, because the grammar rules seem to be both consequence operation and rewriting rules.)

  • Is an automaton a rewriting system? Is an automaton a formal system? (Both seem yes to me, because the state transition functions seem to be both consequence operation and rewriting rules.)



1 Answer 1


None of the notions you list (formal system, abstract/string/term rewriting system, formal grammar, automaton) has a single, widely accepted formal definition. Automata in particular come in hundreds of different flavors. For each of my general definitions below you can find a book or article that uses the notion in a different way.

A formal system often consists of a language $L \subset \Sigma^*$ of valid formulas and a set of inference rules of the form $I \subset L^{n+1}$ that allow the deduction of a new formula from $n$ known formulas: $(v_1, \ldots, v_n, w) \in L$ intuitively means that the statement $w$ can be deduced/computed/produced from $v_1, \ldots, v_n$. Sometimes (some of) the $v_i$ are consumed in a deduction step and cannot be reused. Sometimes axioms from which the deductions start are part of the definition. We may then be interested in the language of those formulas that can be reached from the axioms by iterating the deduction relation, or maybe the dynamics of the relation itself. Herre and Schroeder-Heister have decided to use a more general abstract definition that nevertheless corresponds to an intuition of producing new formulas from existing ones in discrete steps.

A string rewriting system, in general, consists of a relation $R \subset (\Sigma^*)^2$, where $(v, w) \in R$ is understood as "$v$ can be transformed into $w$". It can be seen as a formal system with only one inference rule that has $n = 1$. We can split $R$ into more than one rule if we want to differentiate between them for some reason. Rewriting systems are used to model computation, especially if the rewriting relation is local in the sense that it only contains pairs of the form $(a v b, a w b)$ for $a, b \in \Sigma^*$ and $v, w \in F \subset \Sigma^*$, where $F$ is finite (or otherwise "small" or "simple"). There may be a special initial word from which the computation starts, and/or a sub-language where it halts. Abstract and term rewriting systems are similar, but instead of words, they use elements of some abstract set or labeled trees, respectively.

A formal grammar is usually a specific kind of rewriting system where the alphabet is divided into terminal and nonterminal symbols, and all inference rules are local and involve a nonterminal on the LHS. The computation starts from a specific initial nonterminal and halts when the word contains only terminals. The set of possible resulting words is the language defined by the grammar.

An automaton models a physical device that performs computation by processing a string given as input. It typically has a finite set $Q$ of internal states and a "head" that moves over the input and scans it one symbol at a time. It may be allowed to move freely on the input, or only in one direction. In addition, it may have counters, pebbles, stacks, read-write tapes or other types of memory that it can use. A typical automaton accepts an input word if it eventually reaches an accepting state (which are just some subset of $Q$). In this way it defines a language. Most automata can be simulated by rewriting systems, and in some books they are defined as specific kinds of rewriting systems. In addition to finite words, automata can be defined on infinite words, trees, graphs etc. and they can compute functions instead of deciding language membership.

  • $\begingroup$ Thanks. "Most automata can be simulated by rewriting systems, and in some books they are defined as specific kinds of rewriting systems." Could you be more specific? Are you talking about the similarity between the state transition function of an automaton to the inference rules of a formal system? What books on formal systems, rewriting systems, automata, and/or formal grammars would you recommend? $\endgroup$
    – Tim
    Aug 9, 2020 at 2:01
  • $\begingroup$ For example, consider an NFA with alphabet $\Sigma$, state set $Q$ and transition relation $\delta$. We can define a rewriting relation $R$ by $(q a w, q' w) \in R$ if $q' \in \delta(q, a)$, for all $w \in \Sigma^*$, $a \in \Sigma$ and $q, q' \in Q$. This way, if the rewriting is started from $q_0 w$ where $q_0$ is the initial state, it will "eat" $w$ one symbol at a time and eventually finish in a single state $q \in Q$. If that state is final, $w$ is accepted. Each rewriting step corresponds to a step of the transition relation, but is not exactly the same. $\endgroup$ Aug 9, 2020 at 7:09
  • $\begingroup$ Introduction to Automata Theory, Languages, and Computation by Hopcroft and Ullman is an easy-to-read classic. It spends a lot of time on basics and examples and doesn't go very deep, especially the second and third editions. Introduction to the Theory of Computation by Sipser is another classic that also covers more advanced topics. I don't remember offhand where I saw automata defined as rewriting systems. It was probably a more obscure book. $\endgroup$ Aug 9, 2020 at 7:15
  • $\begingroup$ Both books are freely available online as pdfs. $\endgroup$ Aug 9, 2020 at 10:38
  • $\begingroup$ Thanks. both books don't mention formal systems and rewriting systems, but only grammars and automata. I am interested when you remember where you saw automata defined as rewriting systems $\endgroup$
    – Tim
    Aug 9, 2020 at 14:19

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .