Lagmental Vicfred

Full Digit DP Tracks Position, Tightness, and Automaton State by Vicfred

tags: mathematics, dynamic programming, semirings, state spaces

Counting constrained integers up to N requires a prefix position, a tight flag, and the property state. I want the notation, the mechanism, and the failure mode visible at the same time.

Objects and notation

A full dynamic-programming state \(dp[i][s]\) states exactly which prefix \(i\) and mathematical state \(s\) have been processed. The recurrence is a theorem about transitions between these states.

$$ dp[i][t][s]=\#\{\text{length-}i\text{ prefixes with tight flag }t\text{ and state }s\} $$

There are two layers here: the object \(\mathsf D\) and the law \(\mathsf C\). Writing them separately makes the direction of \(\Longrightarrow\) visible and keeps an accidental converse from slipping in.

$$ dp[i+1][t'][\delta(s,d)]\mathrel{+}=dp[i][t][s] $$

Push the symbols

Here is a concrete symbolic test. Reading it from left to right reveals which transformation is reversible and which is only an implication.

$$ \begin{aligned}0\le d&\le\begin{cases}N_i,&t=1,\\9,&t=0,\end{cases}\\t'&=t\wedge(d=N_i).\end{aligned} $$

Structural reading

The invariant statement is the one that does not depend on a convenient choice of coordinates, representatives, basis, or enumeration.

$$ \begin{aligned} \mathsf{D}\;&:\quad dp[i][t][s]=\#\{\text{length-}i\text{ prefixes with tight flag }t\text{ and state }s\},\\[5pt] \mathsf{C}\;&:\quad dp[i+1][t'][\delta(s,d)]\mathrel{+}=dp[i][t][s]. \end{aligned} $$

A hypothesis worth keeping

State compression is an implementation change, not the definition. Loop order is safe only after the uncompressed dependency graph is understood.

$$ \boxed{\begin{gathered} \text{compact conclusion}\\[-2pt] dp[i+1][t'][\delta(s,d)]\mathrel{+}=dp[i][t][s] \end{gathered}} $$

The important habit is to remember what was fixed before the calculation began and what was proved only afterward. The final display preserves that order.

This article was posted on Sat 07 August 2021. Facts and circumstances may have changed since publication.
Please contact me before jumping to conclusions if something seems wrong or unclear.