# Inferring ranking functions in a general code graph with partial information

Let me define the notion of call graph:

A program consists on a set of functions $f,g,h,\ldots$ where each function $n$ is as a mapping $n: D^l \to D^m$. Here $D$ is the datatype representing program values (it could be potentially different for each component). Whenever a function $f$ calls a function $g$ we can represent this by their composition or alternatively by the graph $f \to g$. In this way the code graph can be seen as a graph where each arrow can be think as labelled with the condition that leads to the call.

In such directed graph we can give the notion of path as usual as the sequence of functions calls of the form $f \to g \to h \to \ldots \to s$. We can in fact associate a relation to this path:

Indeed, starting from its input parameter $p$, $f$ will modify $p$ and call $g$ with another parameter that we can denote $c_f(p)$. Similarly, $g$ will modify $c_f(p)$ and call $g$ with some parameter $c_g(c_f(p))$. Finally, $s$ will get called finish its execution (with a call to another function or not) with some parameter $c(p) = c_s(\ldots c_g(c_f(p)) \ldots)$. We will call $c$ the relation associated to the path.

of course for each path, its relation can be easily computed and we can take it as a known data of our problem.

Now I define the notion of measure for a node in the graph:

A node $n$ can be given a measure, which is a function $m: D^l \to \mathbb{N}^t$ (where $l$ is the arity for the domain of $n$), that verifies the following property:

Whenever there is a path between two nodes $n_1,n_2$ in the graph given by a relation $c$, it must hold that: $$\forall p \in D^{arity(n_1)}.m_2(c(p)) < m_1(p)$$ where $<$ is a suitable fixed well-founded order in $\mathbb{N}^t$.

The problem

Given a graph $G = (V,\overrightarrow{E})$ and a set of measures for a subset of nodes $M \subseteq V$ (which cannot be changed), I'm asking how to construct measures for the nodes in $V \setminus M$.

For a preliminary example I suggest to tackle the ones induced in these figures (but this is not the full answer I'm looking for):

Notes

The order $<$ is fixed meaning that the property has to hold with the same order for each instance. But it can be chosen, meaning that the goal is to find such an order and measures such that the property holds.

References

• What does it mean for there to be a "path given by a relation $c$"? I don't see that defined anywhere. I don't know what "the index for the domain in the node function". What are we given? Are we given the measures for all nodes in $M$? Are we given the order $<$? Are we given the relations $c$? Please proof-read your question from the perspective of a reader who doesn't know what you are asking and lacks context, to make sure you introduce and define all relevant context, terms, and notation. – D.W. Sep 17 '18 at 20:41
• @D.W. just to make it clear the measure for $M$, relations $c$ are given. $<$ can be chosen but needs to be fixed so that you use the very same order in all the instances of $p$ in the formula above – Rodrigo Sep 18 '18 at 8:55