Solving Uninterpreted Equations with Context Free Expression Grammars,
MASSACHUSETTS INST OF TECH CAMBRIDGE ARTIFICIAL INTELLIGENCE LAB
Pagination or Media Count:
It is shown here that the equivalence class of an expression under the congruence closure of any finite set of equations between ground terms is a context free expression language. An expression is either a symbol or an n-tuple of expressions the difference between expressions and strings is that expressions have inherent phrase structure. The fact that context free expression languages are closed under intersection is used to derive an algorithm for computing a grammar for the equivalence class of a given expression under any finite disjunction of finite sets of equations between ground expressions. This algorithm can also be used to derive a grammar representing the equivalence class of conditional expressions of the form if P then u else v. The description of an equivalence class by a context free expression grammar can also be used to simplify expressions under well behaved simplicity orders. Specifically if G is a context free expression grammar which generates an equivalence class of expressions then for any well behaved simplicity order there is a subset G of the productions of G such that the expressions generated by G are exactly those expressions of the equivalence class which are simplicity bounds and whose subterms are also simplicity bounds. Furthermore G can be computed from G in order nlogn time plus the time required to do order nlogn comparisons between expressions where n is the size G.