Partial Orders and Lattices

By default, Fixen treats all sorts as discrete—two facts match only if their values are exactly equal. For some problems, this is sufficient. But for other problems like shortest paths or abstract interpretation, you need the solver to understand that some facts are “better” than others and can subsume weaker ones. This is where partial orders and lattices come in.

Lattice Declarations

A lattice declaration tells Fixen that a sort has a partial order, a join (least upper bound) operation and a meet (greatest lower bound) operation. Facts whose values are drawn from a lattice sort are automatically merged when they share the same key (the keys of a fact are its non-lattice arguments).

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

This declares Dist as a lattice based on Haskell’s Natural type. The leq field specifies the partial order: a >= b means that smaller distances are “greater” (better). The join field specifies how to merge two distances: min keeps the smaller distance.

When the solver derives DistTo "Paris" 5 and later DistTo "Paris" 3, it merges them using min 5 3 = 3, retaining only the better fact.

Lattice Fields

A lat declaration has four required fields:

Field	Syntax	Purpose	Example
type	Haskell Type	The underlying Haskell type	Natural
leq	Identifier	The partial order	(>=)
join	Identifier	The join operation (least upper bound)	min
meet	Identifier	The meet operation (greatest lower bound)	max

The fields of the lattice can refer to any type/term that is in scope of the generated Haskell module.

Given a lattice declaration whose underlying type is T:

• The leq function must have type T -> T -> Bool.
• The join and meet functions must have type T -> T -> T.

The meet field is used for variable unification: when two premises share a variable and both reference lattice-valued arguments, the solver computes their meet to find a common instantiation. See Variable Unification for details.

Partial Order Declarations

A partial order declaration is like a lattice, but without the join operation. Facts are still compared and subsumed, but they are never automatically merged.

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

The key difference from a lattice: when two facts share a key but have incomparable values, both are retained. This is essential for Pareto-optimal computations like multi-objective shortest paths, where a path that is shorter but slower should not be discarded in favor of a path that is faster but longer.

Partial Order Fields

A partial ord declaration has three required fields:

Field	Syntax	Purpose	Example
type	Haskell Type	The underlying Haskell type	Natural
leq	Identifier	The partial order	(>=)
mlbs	Identifier	Maximal lower bounds function	distMlbs

Given a partial-order declaration whose underlying type is T:

• The leq function must have type T -> T -> Bool.
• The mlbs function must have type T -> T -> [T].

The mlbs (maximal lower bounds) function computes the list of maximal elements that are lower bounds of two inputs. This is used for map-entry unification, analogous to meet in lattices. For discrete types, mlbs defaults to returning a singleton list for equal values and an empty list otherwise.

Relations and Lattices/Partial Orders

The right-hand side of relation declarations can make use of the declared lattice/partially ordered sorts. For instance, the relations for computing shortest paths can be as follows:

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

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

Note that the sort names do not appear in the generated Haskell module. Instead, their underlying types are used. When partial order or lattice operations are performed, Fixen directly uses the declared fields in the generated source code instead of declaring type classes and type-class instances for these sorts.

Subsumption

Partial orders and lattices define fact subsumption. Suppose facts f1 and f2 are instances of a relation R. Then, f1 subsumes f2 if f2 f1—that is, f1 is “greater than or equal to” f2 under the order on the relation on R.

Fact subsumption works at the level of tuples of arguments, i.e., relations are product partial orders of their argument sorts. For instance, given a relation R A B C, R a1 b1 c1 R a2 b2 c2 whenever all of the following hold:

• a1 a2 (based on the leq of A)
• b1 b2 (based on the leq of B) and
• c1 c2 (based on the leq of C).

Essentially, each sort contributes its own partial order to the product order. Sorts without an explicit ordering declaration (either partial ord or lat) are treated as discrete (equality only).

In the graph distance example, Dist is ordered by >= (smaller is better). Therefore, DistTo "Paris" 5 DistTo "Paris" 3 because 3 >= 5 is true under the declared order. The solver retains only DistTo "Paris" 3 and discards the subsumed fact.

Monotonicity of Rules

In Fixen, rules must be monotone, i.e., larger premises must derive larger conclusions. For example, the following rule is not monotone:

import Numeric.Natural

lat Nat where
  type = Natural
  leq = (<=)
  join = max
  meet = min

rel A: Nat

rule notMonotone: A x, if x == 0 |- A (x + 2)

It is not monotone because A 1 invalidates the condition x == 0 and thus does not cause the rule to fire. However, A 0, which is subsumed by A 1, validates the condition x == 0. Thus, actually, given fact A 1, the rule should fire and conclude A 2. Fixen does not know this as it keeps track of only the largest facts in the database, so this Fixen program will wrongly not conclude A 2.

Variable Unification

When two premises in a rule share a variable and both reference lattice-valued (or partially ordered) arguments, the solver must find a common instantiation. This is called variable unification.

For lattice sorts, this corresponds to the meet (greatest lower bound) operation. For general partial orders, the solver uses the mlbs function to compute a list of maximal lower bounds, non-deterministically instantiating the shared variable with each candidate.

Consider this Fixen program fragment:

lat Nat where
  type = Natural
  leq = (<=)
  join = max
  meet = min

rel R: Nat, Nat

rule transitive: R x y, R y z |- R x z

If the database contains R 5 2 and R 4 7, a naive solver would fail to fire this rule because 2 4. But under the lattice order <=, the fact R 4 7 subsumes R 2 7 (since 2 <= 4). The solver computes meet 2 4 = min 2 4 = 2, instantiating the shared variable y as 2, and derives R 5 7.

Well-Sortedness

Variables in rules must have a single sort, not just a single type. For instance, the following rule is well-typed, but not well-sorted:

import Numeric.Natural

lat Nat where
  type = Natural
  leq = (<=)
  join = max
  meet = min

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

rel A: Nat
rel B: Nat'
rel C

rule illSorted: A x, B x |- C

The illSorted rule instantiates the variable x with Haskell’s Naturals. However, it belongs to sort Nat (based on A) and Nat' (based on B). Fixen does not know how to unify variables in this scenario.

Complete Example: Shortest Paths

The following is a complete, self-contained program implementing a shortest-path algorithm. It demonstrates how relations, rules, and a lattice declaration work together.

Download: shortest-paths.tar.gz

SHA-256: ac2123a26811084aa58cc8c3995236b8c893c4c826c674fcd13a227ba9f558bc

1. First, set up a cabal project with the following structure:

   • Directoryshortest-paths

     • shortest-paths.cabal
     • Directoryapp

       • Main.hs
     • Directoryfix

       • ShortestPath.fix

2. Populate the files with the following:

   Fixen Program

   fix/ShortestPath.fix

   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')
   
   query distances: DistTo - -

   The lat Dist declaration is what makes this program terminate on cyclic graphs. Without it, the addDist rule would keep deriving longer and longer paths around cycles. With the lattice, DistTo "A" 13 is subsumed by DistTo "A" 0 (since 13 >= 0 is true), and the solver retains only the shorter distance. Note that the program will still work if we replaced lat with partial ord

   Driver Code

   app/Main.hs

   module Main where
   
   import ShortestPath
   
   main :: IO ()
   main = do
     let facts = [ DistTo "A" 0 -- our starting vertex
                 , Edge "A" "B" 1
                 , Edge "B" "C" 2
                 , Edge "C" "A" 10
                 , Edge "C" "D" 1
                 ]
         db = solve facts
     -- db now contains the shortest distances from "A" to all reachable vertices
     print (distances db)

   Cabal File

   shortest-paths.cabal

   cabal-version:      3.0
   name:               shortest-paths
   version:            0.1.0.0
   build-type:         Simple
   common warnings
       ghc-options: -Wall
   executable shortest-paths
       import:           warnings
       main-is:          Main.hs
       other-modules:    ShortestPath
       build-depends:    base
                       , pqueue
                       , unordered-containers
       hs-source-dirs:   app
       default-language: GHC2021

3. Build and run the project!

   Terminal

   ~/shortest-paths $ fixen --output app/ShortestPath.hs fix/ShortestPath.fix
   ~/shortest-paths $ cabal run
   [DistTo "A" 0,DistTo "D" 4,DistTo "C" 3,DistTo "B" 1]

Complete Example: Bi-objective Shortest Paths

Now consider a variant where each edge has both a distance and a cost. We want to find all Pareto-optimal (distance, cost) pairs for each vertex—paths that are not dominated by any other path on both metrics.

Download: bosp.tar.gz

SHA-256: 3a2ea1e5175c3309895d937dd2d5a7d12930002a6da94df9cbd288d9117846ab

1. First, set up a cabal project with the following structure:

   • Directorybosp

     • bosp.cabal
     • Directoryapp

       • Main.hs
     • Directoryfix

       • BOSP.fix

2. Populate the files with the following:

   Fixen Program

   fix/BOSP.fix

   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')
   
   query distances: DistTo - - -

   The key difference from the previous shortest-path algorithm is the use of partial ord instead of lat. When the solver derives DistTo "C" 3 10 and later DistTo "C" 10 3, these are incomparable under the partial order (neither 3 >= 10 && 10 >= 3 nor 10 >= 3 && 3 >= 10 holds). A lattice would merge them via min, producing DistTo "C" 3 3—a spurious path that doesn’t exist in the graph. The partial order preserves both facts, maintaining the true Pareto frontier.

   Driver Code

   app/Main.hs

   module Main where
   
   import BOSP
   
   main :: IO ()
   main = do
     let facts = [ DistTo "A" 0 0 -- our starting vertex
                 , Edge "A" "B" 5 1
                 , Edge "A" "B" 1 5
                 , Edge "B" "C" 3 1
                 , Edge "C" "D" 1 3
                 ]
         db = solve facts
     -- db now contains the shortest distances from "A" to all reachable vertices
     print (distances db)

   Cabal File

   bosp.cabal

   cabal-version:      3.0
   name:               bosp
   version:            0.1.0.0
   build-type:         Simple
   common warnings
       ghc-options: -Wall
   executable bosp
       import:           warnings
       main-is:          Main.hs
       other-modules:    BOSP
       build-depends:    base
                       , pqueue
                       , unordered-containers
       hs-source-dirs:   app
       default-language: GHC2021

3. Build and run the project!

   Terminal

   ~/bosp $ fixen --output app/BOSP.hs fix/BOSP.fix
   ~/bosp $ cabal run
   [ DistTo "A" 0 0, DistTo "D" 9 5, DistTo "D" 5 9
   , DistTo "C" 4 6, DistTo "C" 8 2, DistTo "B" 1 5
   , DistTo "B" 5 1 ]

Choosing Between Lattices and Partial Orders

The choice between lat and partial ord determines how the solver handles incomparable facts:

• Lattices — every pair of values has a join. When two facts share a key with different lattice values, they are automatically merged via the join operation(s). This is appropriate when you want a single representative value per key (e.g., shortest distances, interval bounds).

• Partial orders — not every pair is comparable, and there is no automatic merge. This is appropriate when you need to preserve the full set of non-dominated values (e.g., Pareto frontiers in multi-objective optimization).

Tip

Relations in Fixen can have arbitrarily many discrete, partially ordered and lattice sorts. For instance, you are free to define a relation with all three:

partial ord B where
  ...
lat C where
  ...

rel R: A, B, B, C, C

The arguments of sort A and B are the keys of R, while the arguments of sort C are the values of R. Two facts of R are merged as long as their keys match (or they each subsume other facts that have matching keys, obtained via mlbs), and their values are merged via the lattice join specified by the declaration of C.

As a rule of thumb:

• Use lat when you want subsumption and for relation arguments to be the result of an aggregation (using join).
• Use partial ord when you just need subsumption and need to track multiple incomparable facts.

Summary

• Lattices (lat) define a partial order with a join operation. Facts sharing a key are automatically merged via join.
• Partial orders (partial ord) define a partial order without automatic merging. Incomparable facts are retained.
• Subsumption is defined by the product of partial orders over relation arguments.
• Variable unification uses meet (lattices) or mlbs (partial orders) to match variables across premises.
• Choose lat for subsumption and aggregation; choose partial ord for just subsumption and the maintenance of Pareto frontiers.