This all sounds right. I will note that in practice in the Leuven compiler, rule priority is defined by the lexical ordering of rules. To implement Dijkstra’s algorithm I would have to introduce another constraint and probably two rules that establish reduction order dynamically.