%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "verma95.ltx",
%%%     date      = "20 September 1995",
%%%     time      = "13:15:08 EDT",
%%%     author    = "David M. Jones",
%%%     email     = "jacm@theory.lcs.mit.edu",
%%%     url       = "http://theory.lcs.mit.edu/~jacm/",
%%%     address   = "Journal of the ACM
%%%                  MIT Laboratory for Computer Science
%%%                  Room NE43-316
%%%                  545 Technology Square
%%%                  Cambridge, MA 02139
%%%                  USA",
%%%     telephone = "(617) 253-5936",
%%%     FAX       = "(617) 253-3480",
%%%     checksum  = "54287 123 625 4957",
%%%     codetable = "ISO/ASCII",
%%%     supported = "yes",
%%%     docstring = "Copyright (c) 1995 by ACM, Inc.
%%%                  Permission to make digital or hard copies of part
%%%                  or all of this work for personal or classroom use
%%%                  is granted without fee provided that copies are
%%%                  not made or distributed for profit or direct
%%%                  commercial advantage and that copies bear this
%%%                  notice and the full citation on the first page.
%%%                  Copyrights for components of this work owned by
%%%                  others than ACM must be honored. Abstracting with
%%%                  credit is permitted. To copy otherwise, to
%%%                  republish, to post on servers, or to redistribute
%%%                  to lists, requires prior specific permission
%%%                  and/or a fee. Request permissions from
%%%                  Publications Dept, ACM Inc., fax +1 (212)
%%%                  869-0481, or permissions@acm.org.
%%%
%%%                  This is a LaTeX2e file.  To process it, you will
%%%                  need a copy of the acmabs document class, which is
%%%                  available via the following URL:
%%%
%%%                  http://theory.lcs.mit.edu/~jacm/acmart/acmabs.cls
%%%                  ",
%%%  }
%%% ====================================================================

\documentclass{acmabs}

\begin{document}

\Journal{Journal of the ACM}

\refkey{Verma95}

\title{A Theory of Using History for Equational Systems with Applications}

\author{Rakesh~M. Verma}

\Month{September}

\Year{1995}

\Volume{42}

\Number{5}

\note{To appear}

\maketitle

\begin{abstract}

Implementation of programming language interpreters, proving theorems of the
  form $A = B$, implementation of abstract data types, and program optimization
  are all problems that can be reduced to the problem of finding a normal form
  for an expression with respect to a finite set of equations. In 1980, Chew
  proposed an elegant congruence closure based simplifier (CCNS) for computing
  with regular systems, which stores the history of its computations in a
  compact data structure. In 1990, Verma and Ramakrishnan showed that it can
  also be used for noetherian systems with no overlaps. \par In this paper we
  develop a general theory of using CCNS for computing normal forms and present
  several applications. Our results are more powerful and widely applicable
  than earlier work. We present an independent set of postulates and prove that
  CCNS can be used for any system that satisfies them. (This proof is based on
  the notion of \emph{strong closure}.) We then show that CCNS can be used for
  consistent convergent systems and for various kinds of priority rewrite
  systems. This is the first time that the applicability of CCNS has been shown
  for priority systems. Finally, we present a new and simpler translation
  scheme for converting convergent systems into effectively nonoverlapping
  convergent priority systems. Such a translation scheme had been proposed
  earlier, but we show that it is incorrect. \par Because CCNS requires some
  strong properties of the given system, our demonstration of its wide
  applicability is both difficult and surprising. The tension between demands
  imposed by CCNS and our efforts to satisfy them gives our work much general
  significance. Our results are partly achieved through the idea of effectively
  simulating ``bad'' systems by almost-equivalent ``good'' ones, partly through
  our theory that substantially weakens the demands, and partly through the
  design of a powerful and unifying reduction proof method.

\end{abstract}

\begin{categories}

F.4.1 [\textbf{Mathematical Logic and Formal Languages}]: Mathematical
Logic---\emph{computational logic\textup; mechanical theorem proving
\textup; proof theory};
I.2.3 [\textbf{Artificial Intelligence}]: Deduction and Theorem
Proving---\emph{deduction}

\end{categories}

\begin{terms}

Algorithms, Theory

\end{terms}

\begin{keywords}

Equational logic, proof theory, term rewriting, rewrite systems,
  congruence-closure algorithm, rewrite system transformation

\end{keywords}

\end{document}
