[proofplan] The word problem asks, given a grammar $G$ and a word $w$, whether $w \in \mathcal{L}(G)$. For a noncontracting grammar the Bounded Derivations theorem provides a computable bound $N$ on the length of a derivation witnessing membership: $w \in \mathcal{L}(G)$ if and only if a derivation of length at most $N$ exists. Since there are finitely many candidate derivations of length at most $N$ and each can be mechanically verified, an exhaustive search produces a decision procedure. The Inclusion of Grammar Classes result then extends this procedure to context-sensitive, context-free, and regular grammars, since every grammar in these three classes is in particular noncontracting. [/proofplan] [step:Fix the input and recall the derivation bound] The word problem for a given grammar class is the decision problem: > **Input.** A grammar $G = (\Sigma, V, P, S)$ in the class and a word $w \in \Sigma^\star$. > **Output.** "Yes" if $w \in \mathcal{L}(G)$, "No" otherwise. Assume $G$ is noncontracting. Let $\Omega := \Sigma \cup V$. By the [Bounded Derivations for Noncontracting Grammars](/theorems/1782) theorem, there exists $N \in \mathbb{N}$ depending only on $|w|$ and $|\Omega|$ such that \begin{align*} w \in \mathcal{L}(G) &\iff w \text{ has a $G$-derivation of length at most } N. \end{align*} Concretely, the theorem gives $N = \sum_{\ell = 1}^{|w|} |\Omega|^\ell$, which is a finite integer computable from the input. [/step] [step:Describe the finite search space of candidate derivations] A candidate $G$-derivation of length at most $N$ is a finite sequence $(\sigma_0, \sigma_1, \dots, \sigma_n)$ with $n \leq N$, where each $\sigma_i$ is a string over $\Omega$. By the length bound in the noncontracting theorem, we may restrict attention to candidate strings whose length does not exceed $|w|$: if any $|\sigma_i|$ exceeded $|w|$, the derivation could not terminate at $w$ because the lengths along a noncontracting derivation are nondecreasing. Hence \begin{align*} \sigma_i &\in \bigcup_{\ell = 0}^{|w|} \Omega^\ell, \qquad 0 \leq i \leq n. \end{align*} The set $\bigcup_{\ell = 0}^{|w|} \Omega^\ell$ is finite, with cardinality $\sum_{\ell = 0}^{|w|} |\Omega|^\ell$. Candidate derivations of length at most $N$ are therefore sequences of length at most $N+1$ over a finite set, forming a finite collection \begin{align*} \mathcal{C} &:= \bigcup_{n = 0}^{N} \left( \bigcup_{\ell = 0}^{|w|} \Omega^\ell \right)^{n+1}. \end{align*} The cardinality $|\mathcal{C}|$ is a computable function of $|w|$, $|\Omega|$, and $N$. [/step] [step:Describe the check that a candidate is a valid derivation ending at $w$] Given a candidate sequence $(\sigma_0, \sigma_1, \dots, \sigma_n) \in \mathcal{C}$, we verify mechanically whether it is a valid $G$-derivation of $w$ from $S$ by performing the following checks: (a) $\sigma_0 = S$. (b) $\sigma_n = w$. (c) For each $i \in \{0, 1, \dots, n-1\}$, the pair $(\sigma_i, \sigma_{i+1})$ witnesses a single-step $G$-reduction. Concretely, check whether there exist a rule $(\gamma \to \delta) \in P$ and strings $\alpha, \beta \in \Omega^\star$ such that \begin{align*} \sigma_i &= \alpha \gamma \beta, & \sigma_{i+1} &= \alpha \delta \beta. \end{align*} Check (a) is a string equality test. Check (b) is a string equality test. For check (c), $P$ is finite (by the grammar definition); for each of the finitely many rules $(\gamma \to \delta) \in P$, there are at most $|\sigma_i| + 1$ possible positions in $\sigma_i$ at which $\gamma$ could begin, and for each position we test whether $\sigma_i$ factors as $\alpha \gamma \beta$ with the chosen $\gamma$ at that position and whether substituting $\delta$ for $\gamma$ there produces $\sigma_{i+1}$. The number of positions $\times$ rules is finite, and each test is a string comparison. Hence check (c) terminates with a "yes" or "no" answer. Aggregating: a candidate $(\sigma_0, \dots, \sigma_n)$ is a valid $G$-derivation of $w$ from $S$ if and only if checks (a), (b), and (c) all return "yes", and this aggregate verification terminates. [/step] [step:Assemble the decision procedure for the noncontracting case] The decision procedure is: 1. On input $(G, w)$ with $G$ noncontracting, compute $N := \sum_{\ell = 1}^{|w|} |\Omega|^\ell$. 2. Enumerate the finite set $\mathcal{C}$ of candidate sequences from the second step. 3. For each candidate, apply the verification checks (a)–(c) from the third step. 4. If any candidate passes all three checks, output "Yes". Otherwise output "No". The procedure terminates because $\mathcal{C}$ is finite (step 2) and each candidate's verification terminates (step 3). **Correctness.** If the procedure outputs "Yes", it has exhibited a valid $G$-derivation of $w$ from $S$ (of length at most $N$), so $w \in \mathcal{L}(G)$. Conversely, if $w \in \mathcal{L}(G)$, the [Bounded Derivations](/theorems/1782) theorem asserts that there exists a $G$-derivation of $w$ from $S$ of length at most $N$. Such a derivation's intermediate strings all have length at most $|w|$ (by the nondecreasing-length argument of the cited theorem), so they lie in $\bigcup_{\ell = 0}^{|w|} \Omega^\ell$. Hence the derivation, viewed as a sequence, lies in $\mathcal{C}$, will be encountered in the enumeration, and will pass all three checks, producing output "Yes". Hence the word problem is solvable for noncontracting grammars. [guided] The strategy is: convert a search over an *a priori* infinite set (all finite derivations) into a search over a finite set, by using the length bound from the [Bounded Derivations](/theorems/1782) theorem. Without that bound, derivations could in principle be arbitrarily long, and exhaustive search would not terminate; the noncontracting hypothesis is what makes the space effectively finite. Two subtle points are worth highlighting. First, the verification of a single-step reduction in check (c) is itself a finite search: given $\sigma_i$ and $\sigma_{i+1}$, we must decide whether *some* rule applies *somewhere* in $\sigma_i$ to produce $\sigma_{i+1}$. There are $|P|$ rules and $O(|\sigma_i|)$ positions per rule, so the search is over at most $|P| \cdot (|\sigma_i| + 1)$ rule-position pairs, and each pair is checked by a constant number of string comparisons. This is where finiteness of $P$ (part of the definition of a grammar) is used. Second, it is important that we restricted candidates to strings of length at most $|w|$. If we had allowed arbitrary strings, $\mathcal{C}$ would be infinite and the enumeration would not terminate. The [Bounded Derivations](/theorems/1782) theorem guarantees that no valid derivation leaves this length regime, so restricting does not lose any witnesses. The decision procedure is not claimed to be efficient — indeed $|\mathcal{C}|$ grows exponentially in $|w|$ and $|\Omega|$. The theorem asserts only *decidability*, not polynomial-time computability. [/guided] [/step] [step:Extend the decision procedure to the other three classes] By the [Inclusion of Grammar Classes](/theorems/1780) theorem, every context-sensitive rule is noncontracting, every context-free rule is context-sensitive (hence noncontracting), and every regular rule is context-free (hence noncontracting). In each case, if every rule of $G$ has one of these stronger properties, then every rule of $G$ is noncontracting, so $G$ is a noncontracting grammar. Hence the decision procedure of the previous step, applied to such a $G$, correctly decides whether $w \in \mathcal{L}(G)$. This shows that the word problem is solvable for context-sensitive, context-free, and regular grammars, completing the proof. [/step]