Cyclic Graph Unification
  
Preface

Labeled trees are commonly used to represent data
types. Cyclic labeled graphs can also be so used,
as in:
____
 
v 
L == cons 
/ \__
1 2
v
integer
which represents an infinite list of integers. Here
`cons' denotes the type of a data structure with two
components: the first component is the first item on the
list, and the second component is the rest of the list.
L is a variable whose value is the `cons' node; L can
be used to denote the data type represented by this
node.
In such a graph, the nodes have labels that are
identifiers, and the arrows originating at a node have
labels 1, 2, 3, ... that are consecutive integers
beginning with 1. The targets of these labels are
called the `children' of the node, even though this is
a graph and not a tree, and there can be cycles (so
there is no good notion of descendant or ancestor).
Each node represents a data type. We will use variables
whose values are nodes of such a graph. We will used
the convention that the labels of nodes will begin with
a lower case letter, and the names of variables will
begin with an upper case letter.
A data type can also have unknown parts that are
denoted by variables which represent graph nodes. For
example, the graph:
____
 
v 
LX == cons 
/ \__
1 2

v
X
can represent a type in which X is some yet unknown
graph node. Here X has been used as the label of a
graph node that has NO children: we call this a
`variable node'. So a graph with variable nodes
represents a data type with unknown pieces.
Compilers need to determine when two types are the
same. We do this with the help of a `graph
equivalence relation'.
An equivalence relation on graph nodes is a set of
subsets of the nodes such that each node belongs to
exactly one subset. The subsets are called `equivalence
classes'. Two nodes are said to be `equivalent' if and
only if they belong to the same equivalence class.
A graph equivalence relation is an equivalence
relation on graph nodes such that whenever two nodes
are equivalent then:
Either
(1) One of the nodes is a variable node
(i.e. has a label beginning with
a capital letter.)
or
(2) Both the following are true:
(2a) Both nodes have the same label and
number of children.
(2b) Corresponding children of the nodes
are equivalent.
Given two nodes, computing the smallest graph
equivalence relation that makes the two nodes
equivalent is called `unifying' the nodes. Two nodes
representing types are said to represent the same type
if and only if the nodes can be unified.
Most pairs of graph nodes, of course, CANNOT be unified.
That is, the attempt to compute the smallest graph
equivalence relation making them equivalent will fail.
Problem

You are given a graph and are asked to compute the
smallest graph equivalence relation that unifies two
nodes in the graph, or to indicate that there is no
such relation.
The nodes of the graph are numbered with consecutive
integers beginning with 1. The label of each node
is a single letter. A node is a variable node
if and only if its label is a capital letter.
An arrow from a node to one of its children is
represented by the node number of the child.
Variable nodes have no children.
There can be at most 100 nodes and each node can have
at most 10 children.
You are to read in a graph and a pair of node numbers,
and try to unify the given pair of nodes. The output
of a successful unification is an equivalence relation,
and for each node you are asked to print the the name
of the equivalence class to which the node belongs.
Here the name of the equivalence class, which is a
subset of nodes, is defined to be the smallest node
number of any node in the equivalence class.
We suggest the following algorithm. Start with a set
of equivalence classes each containing a single node.
You will discover when two such classes need to be
merged. First the classes containing the two nodes
to be unified will need to be merged.
When you discover that two classes need to be merged,
check (2a), and if it is violated, fail. Otherwise
merge the classes, and then use (2b) to find more
classes that need to be merged. If there are no more,
you are done.
Input

The input consists of one or more test cases. Each case
begins with a test case name line. This is followed by
a line containing
n x y
where n is the number of nodes and x and y are the
numbers of the two nodes that are to be unified.
A node definition is a line in the format:
: *
The s are consecutively increasing integers
beginning with 1: the first line of a test case has node
number 1, the second node number 2, and the last node
number n.
The is a letter.
There can be 0 to 10 ren, each of which is
a node number in the range 1 .. n.
Spaces indicated above are any sequence of single space
and tab characters. No input line is longer than 80
characters.
Input ends with an end of file.
Output

For each test case, output begins with an exact copy of
the input test case name line.
Then for each run in which the unification is NOT
successful, the second line is just:
NOT UNIFIED
But if unification IS successful, the second line is
just:
UNIFIES
followed by one line for each node in order of node
number of the format:
==
where the class name is the smallest node
number of any node in the equivalence class
of the node whose number is on the left of
the `==.'
No output line is to have SPACE or TAB characters
except for the single space in `NOT UNIFIED'.
Sample Input
 
 SAMPLE 1 
4 1 3
1: c 2 1
2: i
3: c 4 3
4: X
 SAMPLE 2 
4 1 3
1: c 2 1
2: i
3: c 4 3
4: j
 SAMPLE 3 
11 1 4
1: a 2
2: b 3 1
3: X
4: a 5
5: b 6 8
6: f 7
7: Y
8: a 9
9: b 10 4
10: f 11
11: g
Sample Output
 
 SAMPLE 1 
UNIFIES
1==1
2==2
3==1
4==2
 SAMPLE 2 
NOT UNIFIED
 SAMPLE 3 
UNIFIES
1==1
2==2
3==3
4==1
5==2
6==3
7==7
8==1
9==2
10==3
11==7
File: unify.txt
Author: Bob Walton
Date: Tue Feb 24 15:16:13 EST 2015
The authors have placed this file in the public domain;
they make no warranty and accept no liability for this
file.