An Exercise in Graph Theory

Abstract

We define a function that finds a path between two given nodes of a given directed graph, if such a path exists. We prove the function terminates and we prove that it is correct. Aside from illustrating one way to formalize directed graphs in ACL2, this chapter illustrates the importance of the user’s decomposition of a problem into mathematically tractable parts and the importance of defining new concepts to formalize those parts. Our proof involves such auxiliary notions as that of a simple (loop-free) path, the process for obtaining a simple path from an arbitrary path, and an algorithm for collecting all simple paths. The algorithm we analyze is a naive one that executes in time exponential in the number of edges. This chapter requires no specialized knowledge of graph theory; indeed, the main thrusts of the chapter have nothing to do with graph theory. They are: to develop your formalization skills and to refine your expectations of what a formalization will involve. Appropriate expectations of a project are often the key to success.