Solving Uninterpreted Equations with Context Free Expression Grammars,
Abstract
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 nlog(n) time plus the time required to do order nlog(n) comparisons between expressions where n is the size G.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1983
- Accession Number
- ADA133613
Entities
People
- David Allen Mcallester
Organizations
- Massachusetts Institute of Technology