DOCTORAL DISSERTATION DEFENSE

DEPARTMENT OF COMPUTER SCIENCE

Candidate: Ke Li

Advisor: Zvi Kedem

ON THE OPTIMIZATION OF TERM REWRITING

10:30 a.m., Wedensday, August 14, 1991

rm. 613, Warren Weaver Hall

DEPARTMENT OF COMPUTER SCIENCE

Candidate: Ke Li

Advisor: Zvi Kedem

ON THE OPTIMIZATION OF TERM REWRITING

10:30 a.m., Wedensday, August 14, 1991

rm. 613, Warren Weaver Hall

**Abstract**

*Term rewriting systems* (TRSs) are widely applied in
automated theorem proving, equational languages, logic programming,
specification of software and hardware, and other symbolic computations.
An important computation procedure in applications of TRSs is to reduce a
term to its normal form. The research of this thesis examines the
complexity of normal form computation and explores efficient rewriting
strategies for it.

A rewriting strategy is said *optimal* if for any term,
it always generates the shortest derivation when computing the term's normal
form. First, we prove that a universal optimal rewriting strategy
for any canonical TRS does not exist unless *NP*=*P*. We prove the same
result for AC TRS in which some functions are associative and commutative.

To find efficient rewriting strategies, we divide TRSs
into three categories: *variable-more*, *variable-equal*,
and *variable-fewer*, and propose optimal rewriting strategies for
the first two categories and approximate strategies for the last.

We have done experiments on RRL (Rewrite Rule Laboratory) -- an automated theorem prover with term rewriting as the basic inference rule. The experiment output confirm our theoretical results. Based on our theory and experiment results, we improve RRL by implementing new programs that automatically choose an efficient rewriting strategy for an given term rewriting system.