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 0. 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 runs. Each run con- sists of one or more node definitions, followed by a `#' character, followed by two node numbers, which 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 0: the first line of a run has node number 0, the second node number 1, etc. The is a letter. There can be 0 to 10 ren, each of which is a node number that is a non-negative integer. The input can contain whitespace, SPACEs, TABs, or LINE FEEDs, before or after any node number, node label, or punctuation mark (`:', `;', or `#'). Or such whitespace may be omitted, except between consecutive node numbers. Input ends with an end of file. Output ------ For each run in which the unification is NOT successful, the output consists of the two lines: (1) A blank line. (2) A line containing `NOT UNIFIED'. For each run in which the unification IS successful, the output consists of the lines: (1) A blank line. (2) A line containing `UNIFIES'. (3) For each node in order of node number, a line 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. The output must be PRECISELY as described. Example Input ------- ----- 0: c 1 0; 1: i; 2: c 3 2; 3: X; # 0 2 0: c 1 0; 1: i; 2: c 3 2; 3: j; # 0 2 0: a 1; 1: b 2 0; 2: X; 3: a 4; 4: b 5 7; 5: f 6; 6: Y; 7: a 8; 8: b 9 3; 9: f 10; 10: g; # 0 3 Example Output ------- ------ UNIFIES 0==0 1==1 2==0 3==1 NOT UNIFIED UNIFIES 0==0 1==1 2==2 3==0 4==1 5==2 6==6 7==0 8==1 9==2 10==6 File: unify.txt Author: Bob Walton Date: Fri Apr 28 10:31:39 EDT 2006 The authors have placed this file in the public domain; they make no warranty and accept no liability for this file. RCS Info (may not be true date or author): $Author: hc3 $ $Date: 2006/04/28 14:32:15 $ $RCSfile: unify.txt,v $ $Revision: 1.4 $