Recipe: constructive "traces" for provenance tracking to explain/justify results to users

[arxanas]

You might want to know how a certain fact was derived:

• Example: Show a trace to the user to explain why something was returned.
• Example: Debugging purposes.
• Example: "Reflection", where you want to do logic based on "how" a fact was derived.
• Similarly: Soufflé has a provenance feature to determine the provenance of certain facts. (I found that it wasn't implemented for ADTs, though.)

The easiest way to implement this is to use a collection that implements Ord as a lattice.

• This is stricter than a lattice/partial ordering, but it means you can just add a derive for Ord on random stuff to quickly define a lattice.
  • (Well... I opened Feature request: expose ord_lattice_impl! macro #80 on that topic.)
• Since it's a total ordering, it also enforces monotonicity requirements and deterministic output.
  • Granted, the forced determinism may technically require the engine to do more work than e.g. Soufflé's choice-domain, but it wasn't a problem for me.

Here's an example of tracking the (shortest) dependency chain for some nodes via a Trace type:

lattice tdep(Node, Node, ascent::Dual<Trace>);
    tdep(x, y, ascent::Dual(trace)) <--
        dep(x, y),
        if x != y,
        let trace = Trace::new(x.clone()).push_front(y.clone());
    tdep(x, z, ascent::Dual(trace)) <--
        tdep(x, y, ?ascent::Dual(xy_trace)),
        dep(y, z),
        if x != z,
        let trace = xy_trace.clone().push_front(z.clone());

Instead of just nodes in a graph, you can imagine pushing elements of some type enum Reason to track which specific rules were executed, such as for a typechecker or interpreter.

For reference, here was my hand-written, persistent (concurrent) singly-linked list implementation of Trace.

Persistent singly-linked list implementation

This wraps elements of type Node (not shown) which is Ord.

macro_rules! ord_lattice_impl {
    ($t: ty) => {
        impl ::ascent::Lattice for $t {
            fn meet_mut(&mut self, other: Self) -> bool {
                #[allow(clippy::neg_cmp_op_on_partial_ord)]
                let changed = !(*self <= other);
                if changed {
                    *self = other;
                }
                changed
            }

            fn join_mut(&mut self, other: Self) -> bool {
                #[allow(clippy::neg_cmp_op_on_partial_ord)]
                let changed = !(*self >= other);
                if changed {
                    *self = other;
                }
                changed
            }
        }
    };
}

#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub(crate) struct TraceInner {
    length: usize,
    head: Node,
    tail: Option<Trace>,
}

#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub(crate) struct Trace(Arc<TraceInner>);

ord_lattice_impl!(Trace);

impl Serialize for Trace {
    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
    where
        S: serde::Serializer,
    {
        let nodes = self.iter().collect_vec();
        nodes.serialize(serializer)
    }
}

impl Trace {
    pub fn new(node: Node) -> Self {
        Self(Arc::new(TraceInner {
            length: Default::default(),
            head: node,
            tail: Default::default(),
        }))
    }

    pub fn push_front(self, rdep: Node) -> Self {
        let length = self.0.length + 1;
        Self(Arc::new(TraceInner {
            length,
            head: rdep,
            tail: Some(self),
        }))
    }

    pub fn iter(&self) -> impl Iterator<Item = &Node> {
        let Self(inner) = self;
        let TraceInner {
            length: _,
            head: node,
            tail: prev,
        } = inner.as_ref();
        let iter: Box<dyn Iterator<Item = &Node>> =
            Box::new(std::iter::once(node).chain(prev.iter().flat_map(|prev| prev.iter())));
        iter
    }
}

impl Debug for Trace {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        f.debug_list().entries(self.iter()).finish()
    }
}

You could also use Vec (if you're okay with copying the entire collection for each modification) or use a persistent container library, such as rpds::List.

---

Note that this is directly described in the Ascent paper, but it might not be obvious that "shortest path" can be used for constructive proofs generally:

5.2 Shortest Paths
We used the shortest paths program, introduced in 3.1 as a motivating example for lattices, to compare the performance of Ascent with Flix. We also wrote a version of the program that computes the actual shortest paths in addition to shortest path lengths. Modifying the shortest path lengths program to include the actual paths is straightforward in Ascent:

lattice shortest_path(i32, i32, (Dual<u32>, List<i32>));
shortest_path(x, z, (Dual(w + len), cons(x, p))) <--
edge(x, y, w),
shortest_path(y, z, ?(Dual(len), p));
// ...

Here, List<T>, used to store the paths between nodes, is a singly-linked list, and the type (Dual<u32>, List<i32>) is a total order with lexicographic ordering, making it a Lattice with the correct semantics for this problem.

(or you might not have read the paper)

[kmicinski]

One paper you should consider reading is this one: "Provenance Semirings." http://repository.upenn.edu/bitstreams/b598c0a7-0d24-4162-8279-5f51a17d29c2/download

It presents a method (using semirings) to keep algebraic provenance of facts as they flow through the fixed point. As you say, lattices can also track provenance as well--many semirings can be given lattice structure, etc. We have thought about implementing semirings on top of Ascent for a while--this is used pervasively in probabilistic Datalog implementations, and other systems that reason about provenance. The database research community has thought about this using semirings specifically and their algebraic properties for various reasons (e.g., they work nicely with diffing / semi-naive evaluation)