Browse Prior Art Database

Algorithm for Canonicalization of Data Type Representations

IP.com Disclosure Number: IPCOM000081194D
Original Publication Date: 1974-Apr-01
Included in the Prior Art Database: 2005-Feb-27
Document File: 4 page(s) / 46K

Publishing Venue

IBM

Related People

Auslander, MA: AUTHOR [+6]

Abstract

Many programming languages allow the definition of a data type to make use of itself. Such data types can be viewed as the solutions to a series of equations with the type generators as operators. The diagrams for such data types are not trees, but are cyclic graphs. For example the type whose graph is shown in Fig. 1 may be defined as: t1=tuple(int,ref(t2)) t2=union(real,ref(t1)) or even as: t1-tuple(int,ref(union(real,ref(t1)))).

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 39% of the total text.

Page 1 of 4

Algorithm for Canonicalization of Data Type Representations

Many programming languages allow the definition of a data type to make use of itself. Such data types can be viewed as the solutions to a series of equations with the type generators as operators. The diagrams for such data types are not trees, but are cyclic graphs. For example the type whose graph is shown in Fig. 1 may be defined as: t1=tuple(int,ref(t2))

t2=union(real,ref(t1)) or even as:

t1-tuple(int,ref(union(real,ref(t1)))).

The essence of the canonicalization algorithm is the successive refinement of a partitioning of the nodes in the graph, each such refinement making use of the preceding partition to compute the next. The blocks of the partition contain those nodes of the graph which have not been demonstrated to be different by the preceding refinements. In addition to describing a partition, the blocks are ordered in a fashion such that further partitioning never alters the relative order of two nodes in different blocks of the partition.

Each refinement has two stages. In the first stage, those nodes which are not tagged as "union" are processed. Each block of the previous partition is refined by placing into separate blocks those nodes which have different tags, or which have corresponding elements in different blocks of the previous partition. In the ordering of the blocks, these new blocks all take the place of the block from which they were derived. Among themselves, they are ordered first by a fixed ordering on the tags, and second by the order in the preceding partition of the blocks of the first different corresponding successor. In the second stage, each node tagged "union" is first reduced as described below, and is then classified in the same manner as the nodes processed in the first stage.

In order to reduce a node tagged "union", the previous partition is assumed to define equivalence between nodes. The inclusion axioms are used to compute the subset relations between the nodes. This relation is then used to "cast out" any redundant successors in the union. If the result is a union of one successor, the reduction is that successor. Otherwise the successors in the union sorted by the block number in the partition generated by the first stage in which the successor node resides, and the resulting union node is the reduction.

After the new partition is produced, it is compared with the preceding partition. If they are different, further refinements are performed. If they are the same, then those nodes in the same block of the partition are equivalent.

At this point in the algorithm, it may be the case that some blocks of the partition do not correspond to nodes in the canonical graph. The only nodes which must be in the canonical graph are those corresponding to the blocks of the partition reachable from the block containing the starting node. Therefore, beginning with the nodes in the block containing the starting node, and proceeding to successor...