Lattices of polynomials under substitution (Q2366141)

Given two polynomial symbols \(p\) and \(q\), write \(q\geq p\) if \(p\) can be obtained from \(q\) by uniform substitution of polynomial symbols for the variables which occur in \(q\): for example, \(xy+xz\geq xx+x(xx)\) by the substitution \(\{x/y,xx/z\}\). If we identify polynomial symbols which can be obtained from one another by a renaming of variables then \(\geq\) is a partial ordering of the polynomial symbols of a fixed type, and, given \(p\), the polynomial symbols \(q\) such that \(q\geq p\) form a lattice \(L(p)\) (Theorem 1); this result is an easy corollary of the unification theorem from the theory of resolution-based theorem proving. In case \(p\) is linear in the sense that no variable or nullary operational symbol occurs more than once in \(p\), we determine the structure of \(L(p)\) (Theorem 2 is a somewhat more general result), and deduce that \(L(p)\) is distributive; examples show that if \(p\) is not linear then \(L(p)\) map or may not be distributive or modular. We also show that the linear polynomials built up from variables and a single \(n\)-ary operational symbol (i.e. the \(n\)- ary bracketings of finite sequences of distinct symbols) form a distributive lattice \(C_ n\) (Theorem 3); the notation is suggested by the fact that the number of elements of \(C_ 2\) at depth \(k\) is the \(k\)- th Catalan number.