DSpace Repository

Solving Uninterpreted Equations with Context Free Expression Grammars

Show simple item record

dc.creator McAllester, David Allen
dc.date 2004-10-04T14:54:07Z
dc.date 2004-10-04T14:54:07Z
dc.date 1983-05-01
dc.date.accessioned 2013-10-09T02:45:02Z
dc.date.available 2013-10-09T02:45:02Z
dc.date.issued 2013-10-09
dc.identifier AIM-708
dc.identifier http://hdl.handle.net/1721.1/6380
dc.identifier.uri http://koha.mediu.edu.my:8181/xmlui/handle/1721
dc.description 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 symbols or an n-tuple of expressions; the difference between expressions and strings is that expressions have inherent phrase structure. The Downey, Sethi and Tarjan algorithm for computing congruence closures can be used to convert finite set of equations E to a context free expression grammar G such that for any expression u the equivalence class of u under E is precisely the language generated by an expression form I'(u) under grammar G. 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 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.
dc.format 5200160 bytes
dc.format 4073895 bytes
dc.format application/postscript
dc.format application/pdf
dc.language en_US
dc.relation AIM-708
dc.title Solving Uninterpreted Equations with Context Free Expression Grammars


Files in this item

Files Size Format View

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record

Search DSpace


Advanced Search

Browse

My Account