In theoretical computer science, Dickson's lemma (or one of its equivalent forms) is frequently used to show that various problems involving the behavior of structured transition systems are decidable. One example is the coverability problem for vector addition systems: given an alphabet of vectors $\{ v_1, \ldots , v_k \}\subset \mathbb{Z}^n$ and starting/target vectors $v_0, u\in \mathbb{Z}_{\ge 0}^n$, we're looking for a sequence $v_{i_1},\ldots , v_{i_k}$ such that $v_0 + v_1 + \ldots + v_{i_j}\ge 0$ for all $j$ and $v_0 + v_1 + \ldots + v_{i_k}\ge u$---or a certificate that no such sequence exists. Rackoff proved that, if such a sequence exists, we may take $k$ to be doubly exponential in $n.$ [1] The proof technique can be understood in terms of ascending chains of monomial ideals---in another language, these are *descending* chains of *order ideals*. [2]

The complexity of this and related problems are connected to the following effective variant of Hilbert's basis theorem: how long can a strictly ascending chain of ideals $$I_1\subsetneq I_2 \subsetneq \cdots \subsetneq I_l$$  in $k[x_1,\ldots , x_n]$ be? To make some sense of the question we should control the degrees of the generators of each $I_i$---assume we have some explicit function $f: \mathbb{N} \to \mathbb{N}$ such that each $I_i$ is generated in degree $f(i).$ For each fixed $n,$ if the function $f$ is primitive recursive, then there exists a bound (depending primitive-recursively on $f$) on the length of such a chain. [3] However, the dependence of this bound on $n,$ even when $f(i)$ grows linearly in $i,$ is generally not primitive recursive! [4] This is somewhat remarkable, given that we "expect" doubly-exponential bounds for similar-looking questions.

This problem was also studied in the context of polynomial dynamical systems. [5] In the case of interest to the authors, they are able to determine better bounds (doubly exponential) by exploiting the fact that the dimensions of successive colon ideals $\dim (I_k:I_{k+1})$ are non-increasing. 

Some personal context is that these problems came up in my master's research---part of which was incorporated into the paper [6].

[1] Rackoff, Charles. "The covering and boundedness problems for vector addition systems." Theoretical Computer Science 6.2 (1978): 223-231.

[2] Lazić, Ranko, and Sylvain Schmitz. "The ideal view on Rackoff’s coverability technique." International Workshop on Reachability Problems. Springer, Cham, 2015.

[3] Seidenberg, A. "On the length of a Hilbert ascending chain." Proceedings of the American Mathematical Society 29.3 (1971): 443-450.

[4] Socias, Guillermo Moreno. "Length of polynomial ascending chains and primitive recursiveness." Mathematica Scandinavica (1992): 181-205.

[5] Novikov, Dmitri, and Sergei Yakovenko. "Trajectories of polynomial vector fields and ascending chains of polynomial ideals." Annales de l'institut Fourier. Vol. 49. No. 2. 1999.

[6] Benedikt, Michael, et al. "Polynomial automata: Zeroness and applications." Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE Press, 2017.