A lower bound for the intersection of regular forests

Regular Sigma X-forests continue to play an important role in programming languages, specifically in the design of type systems. They arise naturally as terms of constructor-based, recursive data types in logic and functional languages. Deciding whether the intersection of a sequence of regular Sigma X-forests is nonempty is an important problem in type inference. We show that this problem is PSPACE-hard and as a corollary that the problem of constructing a regular Sigma X-grammar representing their intersection is PSPACE-hard. Tree automata, Computational complexity.