calendar@IBM.COM.UUCP (06/05/86)
IBM Almaden Research Center
650 Harry Road
San Jose, CA 95120-6099
RESEARCH CALENDAR
June 9 - 13, 1986
GOOD REWRITE STRATEGIES FOR FP
E. Wimmers, IBM Almaden Research Center
Computer Science Seminar Wednesday, June 11 2:30 P.M. Room: B2-307
In order to implement a language based on rewrite rules, it does not
suffice to know that there are enough rules in the language; we also
need to have a good strategy for determining the order in which to
apply them. But what is good? Corresponding to each notion of having
enough rules, there is a corresponding notion of a good rewrite
strategy. We examine and characterize these notions of goodness, and
give examples of a number of natural good strategies. Although we
have confined ourselves to FP here, we believe that our techniques
(some of which are nontrivial extensions of techniques first used in
the context of lambda-calculus) will apply well beyond the realm of FP
rewriting systems.
Host: J. Backus
...
ON THE PARALLEL COMPLEXITY OF UNIFICATION OF TERMS AND RELATED PROBLEMS
C. Dwork, IBM Almaden Research Center
Comp. Sci. Colloquium Thursday, June 12 3:00 P.M. Room: Rear Audit.
Unification of terms is a well known problem with applications to a
variety of symbolic computation problems. Two terms s and t,
involving function symbols and variables, are unifiable if there is a
substitution for the variables under which s and t become
syntactically identical. For example, f(x,x) and f(g(y),g(g(c))) are
unified by substituting g(c) for y and g(g(c)) for x. As parallel
architectures become technologically feasible, researchers in logic
programming have sought parallel unification algorithms running at
speeds subpolynomial in the length of the input. Unfortunately, the
existence of such an algorithm has been shown to be "popularly
unlikely," in that it would violate commonly held beliefs about the
structure of the class P of problems solvable in polynomial time. Two
special cases of unification are term matching and equivalence
testing, in which one or both of the terms contain no variables,
respectively. In contrast to the case for general unification, term
matching and testing for equivalence can both be solved
deterministically in time O((log n)**2) for inputs of size n, using
M(n**2) processors, where M(k) is the number of sequential operations
needed to multiply k-by-k matrices (roughly k**2.5). The processor
bound can be improved to M(k) if randomization is allowed. This is
joint work with Paris Kanellakis and Larry Stockmeyer.
Host: R. Strong
...