next up previous contents
Next: An example Up: Naming the Nodes Previous: Naming the Nodes

Introduction

In a recursive datatype, we can name each node by the path that was traversed from the root node in order to create it. The name produced will be far from unique if the some of the directions are commutative. Ideally, we want to be able to convert arbitrary paths into a normalised version, this way we can name each node uniquely. We show firstly that such a unique node name exists, and secondly, exhibit an algorithm for determining it and prove its correctness.



Timothy Lewis
11/12/1997