33.1. Introduction🔗

A canonical labelling algorithm takes a finite graph and renames its vertices in a standard way, so that two graphs receive the same result exactly when they are isomorphic. The most widely used program for this task is Brendan McKay's nauty. This chapter is a complete written specification of the exact function computed by one pinned version of that program: dense nauty 2.9.3, run with the fixed options listed at the end of part one. HexGraphIso reimplements this algorithm in Lean, with identical behaviour.

No published document specifies this function. Three descriptions come closest:

• Brendan D. McKay's Practical graph isomorphism (1981) gives pseudocode detailed enough to reimplement the algorithm as it stood in 1981. Later releases of nauty changed details that affect the output.

• Stephen G. Hartke and A. J. Radcliffe's McKay's canonical graph labeling algorithm (2009) explains the main ideas and why the algorithm is correct. It deliberately omits the implementation choices that decide which result is returned.

• Brendan D. McKay and Adolfo Piperno's Practical graph isomorphism, II (2014) and the nauty and Traces User's Guide, version 2.9.3 describe a family of algorithms with several interchangeable components. Every member of the family computes some canonical form. These documents do not say which member the program densenauty is.

For the exact output, the C source code has previously been the only specification. The source interleaves two kinds of code: choices that determine the answer, and shortcuts that only make the program faster. This chapter separates them. Part one describes a complete search that examines every candidate ordering the program could ever consider, and the rule that selects one of them. Part two presents the Lean implementation of that description. The shortcuts in the real program skip most of the search, and the Lean development proves that skipping never changes the selected answer, so the shortcuts need no place in the specification.

One distinction runs through the whole chapter. The statement "the Lean implementation computes the maximum described in part one" is a theorem, proved in Lean. The statement "the Lean implementation agrees with the C program" is not a theorem about anything; it is an empirical claim, supported by conformance tests that compare the two programs on large families of inputs. The HexGraphIso library never treats the C program as a formal object.