Data.Comp.Dag

This module implements a representation of directed acyclic graphs (DAGs) as compact representations of trees (or Terms).

Documentation

data Dag f

The type of directed acyclic graphs (DAGs). Dags are used as a compact representation of Terms.

Instances

(ShowF f, Functor f) => Show (Dag f)

termTree :: Functor f => Term f -> Dag f

Turn a term into a graph without sharing.

reifyDag :: Traversable f => Term f -> IO (Dag f)

This function takes a term, and returns a Dag with the implicit sharing of the input data structure made explicit. If the sharing structure of the term is cyclic an exception of type CyclicException is thrown.

unravel :: forall f. Functor f => Dag f -> Term f

This function unravels a given graph to the term it represents.

bisim :: forall f. (EqF f, Functor f, Foldable f) => Dag f -> Dag f -> Bool

Checks whether two dags are bisimilar. In particular, we have the following equality

bisim g1 g2 = (unravel g1 == unravel g2)

That is, two dags are bisimilar iff they have the same unravelling.

iso :: (Traversable f, Foldable f, EqF f) => Dag f -> Dag f -> Bool

Checks whether the two given DAGs are isomorphic.

strongIso :: (Functor f, Foldable f, EqF f) => Dag f -> Dag f -> Bool

Checks whether the two given DAGs are strongly isomorphic, i.e. their internal representation is the same modulo renaming of nodes.