Finite-state path expression (source code)

= Finite-state path expression
{title2=$R_{ij}^{(k)}$}

For numbered states of a <finite-state automaton>, $R_{ij}^{(k)}$ is a <regular expression> describing paths from $i$ to $j$ whose internal states have numbers at most $k$. Splitting a path at its visits to state $k$ gives $R_{ij}^{(k)}=R_{ij}^{(k-1)}+R_{ik}^{(k-1)}(R_{kk}^{(k-1)})^*R_{kj}^{(k-1)}$. At stage zero use individual edge labels and an empty-word option when the endpoints coincide. This proves the automaton-to-expression direction of <Kleene theorem>.