Implementation techniques for rewriting and narrowing
Josephson, Norman Alan
This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.
Permalink
https://hdl.handle.net/2142/21931
Description
Title
Implementation techniques for rewriting and narrowing
Author(s)
Josephson, Norman Alan
Issue Date
1989
Doctoral Committee Chair(s)
Dershowitz, Nachum
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Computer Science
Language
eng
Abstract
Rewrite systems are directed equations that can be used to compute by repeatedly rewriting an initial term until a final form is obtained. Such systems provide a nondeterministic programming language having convenient mathematical properties. Programs are easy to understand, as they have very simple syntax and semantics, based on equalities, with no explicit control. By allowing variables within the initial term, the term may be thought of as a logical query. It is possible to solve queries by narrowing, i.e. using the left-hand sides of rules to identify subterms with instances to which rules apply, and repeating the process until instantiations of the variables are constructed that can be shown by rewriting to satisfy the query.
In this dissertation, we explore a class of optimizations relating to the repeated rewriting or normalization of a term. By maintaining more and more detailed information about the rewriting process, successive refinements of a basic normalization algorithm are possible which accelerate the discovery of a simplest form at the expense of the space required to store the information about the computation. In addition, we describe implementation techniques for enforcing an eager rewriting/lazy narrowing approach within the context of these optimizations. Rather than backtracking over narrowing steps to capture all solutions to a query, we demonstrate structure sharing techniques that allow us to make use of shared computation paths during the enumeration of solutions. We investigate extensions to the methods that allow us to handle conditional rules. An implementation, R scITE, is described and its performance on several examples is demonstrated.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
