Free lattice algorithms
In the late 1930s Philip Whitman gave an algorithm for deciding for lattice terms \(v\) and \(u\) if \(v\leq u\) in the free lattice on the variables in \(v\) and \(u\). He also showed that each element of the free lattice has a shortest term representing it and gave an algorithm for finding this term. Using Ralph McKenzie's work, J. B. Nation and the author have developed efficient algorithms for deciding if a lattice term v has a lower cover and for finding them if it does. This paper studies the efficiency of all these algorithms. It is shown that although it is often quite fast, the straightforward implementation of Whitman's algorithm for testing \(v\leq u\) is exponential in time in the worst case. A modification of Whitman's algorithm is given which is polynomial and has constant minimum time. The algorithms of Freese and Nation are also shown to be polynomial.
scientific article; zbMATH DE number 4019124
scientific article