Tree Automata can be used to model sets of values of a Herbrand Universe, for example, to model possible values in a functional program.

Systems of subtype constraints over set expressions have decidable satisfiability, but this is EXPTIME complete, and NEXPTIME complete when projections are allowed in expressions. See here and here.

I'm wondering, has the set constraints problem over equality constraints, instead of subset constraints, been studied? Clearly it's not a harder problem than with subsets, but is it easier? Are there simpler solutions than tree Automata for solving such systems?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.