Inference of a measure for a decreasing chain

Question

Set $I_n = \{0,\ldots,n-1\}$.

Given integers $v_0,\dots,v_{n-1} \in \mathbb{N}$, find an integer $t>0$, a map $f:\mathbb{N} \times I_n \to \mathbb{N}^t$, and a well-founded order $>_t$ on $\mathbb{N}^t$ such that: $$\forall i \in I_n, m \in \mathbb{N}. f(m,i) >_t f(m+v_i,i+_n 1)$$

where $+_n$ is addition in $\mathbb{Z}_n$ and $v_0+\dots+v_{n-1}<0$. Is there an efficient algorithm to do that?

Explanation and motivation

The directed weighted graph $0 \stackrel{v_0}\to 1 \stackrel{v_2}\to \ldots \stackrel{v_{n-2}}\to n-1 \stackrel{v_{n-1}}\to 0$ describes how a magnitude $m \in \mathbb{N}$ varies. For transition $i \stackrel{v}{\to} j$, $m$ gets updated with $m+v$. It must hold that $\sum_{i = 1}^n v_i < 0$. Consider the following problem:

Give an assignment of values in $\mathbb{N}^t$ to nodes and an order that decreases at each transition. That is, if $\text{nodes} = \{0,\ldots,n-1\}$, I want to build a map $f:\mathbb{N} \times \text{nodes} \to \mathbb{N}^t$ with $t > 0$ satisfying: $\forall i \in \text{nodes}. f(m,i) >_t f(m+v_i, i +_n 1)$ where $>_t$ is a well-founded order on $\mathbb{N}^t$.

Is there an algorithm that can built such an $f$ and $<_t$?

Example (my try):

Assume you have the following chain is given:

$1 \stackrel{+3}{\to} 2 \stackrel{-2}{\to} 3 \stackrel{-2}{\to} 1$

In this case, $+3-2-2 = -1 < 0$.

Let's start at 1.

Since $m$ increases, I will annotate measure $(2,m)$ in $1$ and measure $(1,m)$ in $2$ so that lexicographic order decreases.

At $2$, measure $m$ decreases so I can leave annotation $(1,m)$ as it was.

At $3$, measure $m$ decreases so I can copy annotation $(1,m)$ from $2$.

Coming back to $1$, I have a problem, since I had annotated $(2,m)$ before, but now I have annotated $(1,m)$ and these are clearly different measures.

Can you help me out of this problem?

Note on the meaning of the specification

Just to make sure the specification matches my needs, the problem tries to model how some quatity $m$ varies in a loop of successive function applications. The functions form a loop that ends at $0$. It is guaranteed that when traversing the whole loop, quantity $m$ decreases (according to the variations $v_i$). In each function one have to check that in the next call certain measure $f$ (depending on the parameter $m$) decreases.

Answer 1

Yes. This is possible. $t=1$ suffices. Take

$$\begin{align*} f(m,n-1) &= Cm + D\\ f(m,n-2) &= f(m+v_{n-2},n-1) + 1 = Cm + C v_{n-2} + D + 1\\ f(m,n-3) &= f(m+v_{n-3},n-2) + 1 = Cm + C v_{n-3} + C v_{n-2} + D + 2\\ &\ldots\\ f(m,i) &= Cm + C v_{i} + \dots + C v_{n-2} + D + n-1-i \end{align*}$$

where we take the constant $C>0$ to be at least $n$; we choose a constant $D>0$ that's large enough that the output of $f$ is always positive; we take $t=1$; and we use the standard order on $\mathbb{N}$. Then you can verify that this satisfies all the conditions.

How do you find this? As always, start with small cases. Start with $n=2$ and see what has to hold of $f$, and try to construct a $f$ that meets the conditions. (One way to ensure that $x>_t y$ is to set $x=y+1$; in the construction above, I used that to construct $f$ that satisfies the condition by definition.) Then try $n=3$. Then generalize. The above definition follows as a straightforward consequence of your requirements; if you choose elements of $f$ in the right order, it becomes routine to fill out the truth table of $f$ so all the requirements are met.

Answer 2

I have to post this answer since it is probably what I will implement in practice because it is more extendable to other settings and it can be well encoded in my system by logical formulas. However, I will still refer to D.W.'s approach since is mathematically more appealing and for me as a mathematician opens a lot of questions.

Here is the approach:

One begins with a measure $(m,0)$ at node $0$. And in subsequent nodes, makes reference to the decreased measure $m'$ which is obtained encoding the semantic meaning of transversing the loop one time ($m'$ is an expression, not an explicit number). More precisely, $m'$ will be different at each node: node $0$ takes into account all the loop, node $1$ takes into account the loop from $1$, and so on.

I was probably confused by the fact that my system failed with some of these instances. The problem is that measures need to be positive and again as in the case of D.W. we have to introduce a linear shift that gets all inferred measures to be positive.