Abstract
Condmonal expressions of the form “if E=F then G else H,” where E,F,G,H may themselves be such expressions, have long been used to describe the semantics of assignments. We consider the problem of deciding if two nested condmonals of the above form compute the same values Three transformahons are used to solve the problem A dtstrtbutwe transformation converts any conditional to the sampler form if A =B then G else H, where A and B are variables rather than expressions. An trnphed test transformation finds all tests in subexpresslons whose outcome as Jmphed by prevtous tests. Finally, the useless test transformation is used to reduce expressions of the form if A= B then C else C to C When all tests are between variables and the expressions are represented by trees, then equivalence of expressions can be tested in polynomial time The remaining cases have been shown elsewhere to be NP-hard.
Original language | English (US) |
---|---|
Pages (from-to) | 667-674 |
Number of pages | 8 |
Journal | Journal of the ACM (JACM) |
Volume | 25 |
Issue number | 4 |
DOIs | |
State | Published - Oct 1 1978 |
Keywords
- conditional expressions
- emantics of assignment
- equality predicate
- expression simplification
- program verification
ASJC Scopus subject areas
- Software
- Control and Systems Engineering
- Information Systems
- Hardware and Architecture
- Artificial Intelligence