Approximate and Optimal Strategies for Non-Ambiguous and Left Linear Term Rewriting Systems (Classic Reprint)

Excerpt from Approximate and Optimal Strategies for Non-Ambiguous and Left Linear Term Rewriting Systems The termination and confluence properties of term rewriting systems (trs for short) have been studied thoroughly. To prove termination, many orderings, such as recursive path ordering, path orderings, etc., and polynomial interpretations can be For various applications of trs, any simple and effective proof method for termination may be invented. Confluence was studied in deep in [huet80] and the complete procedure to obtain a confluent system are introduced in So far, we are able to design terminating and confluent trsja term rewriting system that has both termination and confluence properties is called a canonical trs. In this report, we consider how to efficiently compute the normal form of a term for a canonical trs. In a canonical trs, any term has a unique normal form. This advantage of canonical trs is used to solve the word problem in equational logic and other problems in reduction systems. Computing normal forms of terms is a basic procedure in any application of trs. If we have some way to improve efficiency for normal form rewriting, efficiency for entire application will be improved. About the Publisher Forgotten Books publishes hundreds of thousands of rare and classic books. Find more at www.forgottenbooks.com This book is a reproduction of an important historical work. Forgotten Books uses state-of-the-art technology to digitally reconstruct the work, preserving the original format whilst repairing imperfections present in the aged copy. In rare cases, an imperfection in the original, such as a blemish or missing page, may be replicated in our edition. We do, however, repair the vast majority of imperfections successfully; any imperfections that remain are intentionally left to preserve the state of such historical works.