Solving Uninterpreted Equations with Context Free Expression Grammars
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...
| Main Author: | |
|---|---|
| Language: | en_US |
| Published: |
2004
|
| Online Access: | http://hdl.handle.net/1721.1/6380 |
| _version_ | 1811073721584058368 |
|---|---|
| author | McAllester, David Allen |
| author_facet | McAllester, David Allen |
| author_sort | McAllester, David Allen |
| collection | MIT |
| 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. |
| first_indexed | 2024-09-23T09:37:33Z |
| id | mit-1721.1/6380 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T09:37:33Z |
| publishDate | 2004 |
| record_format | dspace |
| spelling | mit-1721.1/63802019-04-11T01:11:30Z Solving Uninterpreted Equations with Context Free Expression Grammars McAllester, David Allen 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. 2004-10-04T14:54:07Z 2004-10-04T14:54:07Z 1983-05-01 AIM-708 http://hdl.handle.net/1721.1/6380 en_US AIM-708 5200160 bytes 4073895 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | McAllester, David Allen Solving Uninterpreted Equations with Context Free Expression Grammars |
| title | Solving Uninterpreted Equations with Context Free Expression Grammars |
| title_full | Solving Uninterpreted Equations with Context Free Expression Grammars |
| title_fullStr | Solving Uninterpreted Equations with Context Free Expression Grammars |
| title_full_unstemmed | Solving Uninterpreted Equations with Context Free Expression Grammars |
| title_short | Solving Uninterpreted Equations with Context Free Expression Grammars |
| title_sort | solving uninterpreted equations with context free expression grammars |
| url | http://hdl.handle.net/1721.1/6380 |
| work_keys_str_mv | AT mcallesterdavidallen solvinguninterpretedequationswithcontextfreeexpressiongrammars |