Priorities

By default, Fixen applies rules in an unspecified order until a fixed point is reached. For many problems, this is fine — the final set of derived facts is the same regardless of order. But for some algorithms, the order in which rules fire directly impacts performance. Processing facts in the wrong order can cause redundant derivations, turning an efficient algorithm into a much slower one.

Rule-instance priorities give you control over evaluation order, enabling algorithm-level optimizations without changing the rules themselves.

Priority Declarations

Priorities are declared with the priority keyword:

priority: (d1 + d1') > (d2 + d2')
          |- addDist { d = d1, d' = d1' } < addDist { d = d2, d' = d2' }

This declares that addDist rule instances with shorter total distances have higher priority (are processed first). The > on the left of |- is a condition that must hold for the priority to apply. The < on the right specifies that the left instance has lower priority than the right instance.

How Priorities Work

During execution, the Fixen solver replaces the standard work-list with a priority queue of rule instances. A rule instance is a rule whose variables have been fully instantiated with ground terms. The solver continuously dequeues the highest-priority rule instance, evaluates its conclusion, and inserts it into the fact database. If the conclusion is a newly discovered fact, the solver derives all subsequent rule instances that can be instantiated from it, schedules them into the priority queue, and repeats.

The custom priorities you declare are used by the priority queue to determine which rule instance to process next. This maps directly to scheduling optimizations: for example, Dijkstra’s algorithm achieves its optimal complexity by greedily processing vertices closest to the source, and this is expressed by prioritizing addDist instances with shorter distances.

Priority Syntax

A priority declaration has the form:

priority: condition |- instance1 < instance2

The condition (left of |-) is a Haskell expression of type Bool that must hold for the priority to apply. If omitted (i.e., the condition is empty), the priority always applies.
The instances (right of |-) are rule instantiations of the form ruleName { var = value, ... }. The < symbol indicates that the left instance has strictly lower priority than the right instance.

Multiple priority declarations are allowed, and priorities can compare instances of any two rules. The solver combines all priority declarations to form a strict weak order over rule instances.

Example: Dijkstra’s Algorithm

Download: shortest-paths.tar.gz

SHA-256: a2fa0ddfd33123299d4ea6341d8a8b034886be150fdb880fd0bb01f99236ff98

Without priorities, a naive FPOP graph-distance algorithm repeatedly revisits vertices with suboptimal path lengths, degrading to Bellman-Ford performance. With priorities, we get Dijkstra’s optimal behavior:

module ShortestPath where

import Numeric.Natural

```hs
type Vertex = String
```

lat Dist where
  type = Natural
  leq = (>=)
  join = min
  meet = max

rel Edge: Vertex, Vertex, Dist
rel DistTo: Vertex, Dist

rule addDist: DistTo a d, Edge a b d' |- DistTo b (d + d')

priority: (d1 + d1') > (d2 + d2')
          |- addDist { d = d1, d' = d1' } < addDist { d = d2, d' = d2' }

query distances: DistTo - -

The priority ensures that addDist instances producing shorter distances are processed first, mirroring Dijkstra’s greedy vertex selection.

Example: Bi-objective Shortest Paths

Download: bosp.tar.gz

SHA-256: abf1d2cf8e180c12d69bd0ccaa7188ec3703968ec941b8d5a21caeeb53fa20bf

For bi-objective shortest paths (distance and cost), priorities can impose a lexicographical order:

module BOSP where

import Numeric.Natural

```hs
type Vertex = String
distMlbs :: Natural -> Natural -> [Natural]
distMlbs x y = if x <= y then [y] else [x]
```

partial ord Dist where
  type = Natural
  leq = (>=)
  mlbs = distMlbs

-- Now our relations have two `Dist` components
rel Edge: Vertex, Vertex, Dist, Dist
rel DistTo: Vertex, Dist, Dist

rule addDist: DistTo a w1 w2, Edge a b w1' w2'
              |- DistTo b (w1 + w1') (w2 + w2')

priority: ((w11 + w11') > (w21 + w21')) ||
            (((w11 + w11') == (w21 + w21')) && ((w12 + w12') > (w22 + w22')))
          |- addDist { w1 = w11, w1' = w11', w2 = w12, w2' = w12' }
             < addDist { w1 = w21, w1' = w21', w2 = w22, w2' = w22' }

query distances: DistTo - - -

This prioritizes instances with smaller total distance, breaking ties by preferring smaller total cost.

Comparing Arbitrary Instances

Priorities are not limited to comparing instances of the same rule, nor are you limited to one priority declaration for each program. You can compare instances of different rules:

priority: True |- rule1 { } < rule2 { }

This unconditionally gives instances of rule2 higher priority than instances of rule1, regardless of the instantiated values. Such cross-rule priorities can be used to stratify rule execution.

Performance Implications

Choosing the right priorities is crucial for performance. In our examples above, rule-instance priorities significantly improves the performance of our algorithms. However, writing the wrong priorities can make algorithms slower, as the solver may process facts in an order that generates more redundant work.

Priorities require domain-specific knowledge of the algorithm. They are an optimization lever, not a correctness mechanism. The final set of derived facts is the same regardless of priority ordering (provided the rules are monotone).

Summary

Priorities control the order in which rule instances are processed.
They are declared with priority: followed by a condition and an ordering between rule instances.
The solver uses a priority queue of rule instances, dequeuing the highest-priority instance at each step.
Correct priorities enable algorithm-level optimizations (e.g., Dijkstra’s greedy selection).
Priorities affect performance, not correctness—the final result is the same regardless of ordering.
Multiple priorities can compare instances of the same or different rules.