Skip to content

Example 4. DataGraphs

Jump to bottom
Daniel Balasubramanian edited this page Oct 17, 2022 · 1 revision

This last example gives a more complex transform module. Before getting into that, we have to specify a few domains and introduce a little bit about domain composition using the extends keyword:

domain Digraphs
{
   V ::= fun (lbl: Integer -> dat: Integer).
   E ::= new (src: V, dst: V).
}

domain DAGs extends Digraphs
{
   path ::= (V, V).
   path(u, w) :- E(u, w); E(u, v), path(v, w).  
   conforms no path(u, u).
}

domain Trees extends DAGs
{
   conforms no { w | E(u, w), E(v, w), u != v }.
}

 domain AlgTrees
{
   Node ::= new (dat: Integer, left: any Node + { NIL }, right: any Node + { NIL }).
   Tree ::= new (any Node).
   conforms count({ t | t is Tree}) <= 1.
}

The first domain Digraphs are directed graphs which can be represented by the vertices V and the directed edges E. The set of all DAGs (directed acyclic graphs) is a subset of the set of all directed graphs, and the set of trees is a subset of the set of DAGs. This chain of restrictions can be specified using extends as in the example code. The keyword extends is used to merge domain declarations and automatically inherits conformance constraints.

The AlgTrees domain shows an algebraic representation of trees. Algebra is a powerful tool for studying the structure of a tree. The transformation from algebra trees to regular trees is very important with respect to using this tool. Here we have this transform AlgToRelTree which takes algebra trees as input and returns the corresponding regular trees:

  transform AlgToRelTree (tree:: AlgTrees) returns (graph:: Trees)
  {
    Path     ::= ({ LEFT, RIGHT }, Path + { NIL }).
    PathData ::= (path: Path + { NIL }, node: Node, id: Integer).
    IdMax    ::= (path: Path + { NIL }, id: Integer).

    PathData(NIL, n, 0) :- Tree(n).   
    PathData(Path(LEFT, p),  n, i')  :- PathData(p, Node(_, n, _), i), i' = i + 1, n : Node.
    PathData(Path(RIGHT, p), n, i')  :- PathData(p, Node(_, NIL, n), i), i' = i + 1, n : Node;
                                   PathData(p, Node(_, m, n), _), IdMax(Path(LEFT, p), i), i' = i + 1, n : Node.
                                     
    IdMax(pd.path, pd.id) :- pd is PathData, pd.node = Node(_, NIL, NIL).  
    IdMax(pd.path, i)     :- pd is PathData, pd.node = Node(_, n, NIL), IdMax(Path(LEFT, pd.path), i);
                        pd is PathData, pd.node = Node(_, _, n), IdMax(Path(RIGHT, pd.path), i).       
                          
    V(id, n.dat) :- PathData(_, n, id).

    E(V(pid, prnt.dat), V(cid, chld.dat)) :- PathData(p, chld,  cid), PathData(p', prnt, pid), p = Path(_, p').
 }

This transformation uses the equivalence relation expressed in the image below. Each node in the algebra tree corresponds to a vertex in the graph, which a function mapping its PathData id to its node dat. Meanwhile, the parent-child relations in the algebra tree give the directions of the edges.

The first step of the transformation is to develop intermediate tools we will be using to recover the directed graph. And this is where Path, PathData and IdMax come in. Path is defined recursively and the direction is always from root to end. It is constructed by extending a Path(including empty path, i.e. NIL) to the left child or right child of its end node. The PathData records not only the Path itself, but also its end node and an integer id that indicates the length of the path in some sense. We will discuss the definition of IdMax a while later. Here is an image illustrating the three rules and showing how we construct PathData:

The first rule is for the root node. Since it has no preceding path, the `PathData` records `NIL` and therefore the id is 0. The second rule deals with the case where we reach for the left child n to the path and adding 1 to the path id. The third rule for the right child is a bit more complicated than the others, for it has two bodies and also involves the `IdMax`.

So now the transform has come down to how we define a path's max id, i.e. IdMax:

IdMax of a path should be the id of its fully extended path, as shown in Case 1. In Case 2, we have demonstrated the way for extending a path: if it has a right child, then go for it; if not, then go for the left child. By doing this we can track the path all the way down to its end and define the max id for it.

Clone this wiki locally