Problem #59
Originator: M. Kurihara, M. Krishna Rao
Date: June 1993
Summary:
What are sufficient condition for the modularity of confluence?
One of the earliest results established on modularity of combinations of
term-rewriting systems is the confluence of the union of two confluent systems
which share no symbols [Toy87]; if symbols are shared modularity is
not preserved by union [KO92]. Some sufficient conditions for
modularity of confluence of constructor-sharing systems that are terminating
have been found [KO92][MT91]. Are there interesting
sufficient conditions that are independent of termination?
Remark
Left-linearity is a sufficient condition, as shown long ago in
[RV80]. In [Ohl94], it is established that
confluence is modular in the presence of the weak normalization property.
(This result has been extended in [Rao95, Rao98] for hierarchical
combinations.) In [Der97], some results are given when only one of the
systems is terminating.
There are other sufficient conditions for modularity of confluence that do not
require termination of the combined system even when function symbols are
shared. One set of conditions, viz., “persistence”, “relative
termination”, and lr-disjointness, is given in [Ver95, Ver96]. An
abstract confluence theorem without termination is given in [Ges90].
References
-
[Der97]
-
Nachum Dershowitz.
Innocuous constructor-sharing combinations.
In Hubert Comon, editor, 8th
International Conference on Rewriting Techniques and Applications, volume
1232 of Lecture
Notes in Computer Science, pages 202–216, Barcelona, Spain, June 1997.
Springer-Verlag.
- [Ges90]
-
Alfons Geser.
Relative Termination.
PhD thesis, qUniversität Passau, Passau, Germany, 1990.
- [KO92]
-
M. Kurihara and A. Ohuchi.
Modularity of simple termination of term rewriting systems with
shared constructors.
Theoretical Computer
Science, 103:273–282, 1992.
- [MT91]
-
Aart Middeldorp and Yoshihito Toyama.
Completeness of combinations of constructor systems.
In Ronald. V. Book, editor, 4th International Conference on
Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer
Science, pages 174–187, Como, Italy, April 1991.
Springer-Verlag.
- [Ohl94]
-
Enno Ohlebusch.
On the modularity of confluence of constructor-sharing term rewriting
systems.
In 19th Colloquium on Trees in Algebra and Programming, volume
787 of LNCS, pages 261–275. Springer-Verlag, 1994.
- [Rao95]
-
M.R.K. Krishna Rao.
Semi-completeness of hierarchical and super-hierarchical combinations
of term rewriting systems.
In Theory and practice of Software Development, TAPSOFT’95,
volume 915 of Lecture Notes in Computer Science, pages 379–393.
Springer-Verlag, 1995.
- [Rao98]
-
M.R.K. Krishna Rao.
Modular aspects of term graph rewriting.
Theoretical Computer
Science, 208(1–2):59–86, 1998.
Special issue on Rewriting Techniques and Applications conference
RTA’96.
- [RV80]
-
Jean-Claude Raoult and Jean Vuillemin.
Operational and semantic equivalence between recursive programs.
J. of the Association for
Computing Machinery, 27(4):772–796, October 1980.
- [Toy87]
-
Yoshihito Toyama.
On the Church-Rosser property for the direct sum of term rewriting
systems.
J. of the Association for
Computing Machinery, 34(1):128–143, January 1987.
- [Ver95]
-
Rakesh M. Verma.
Unique normal forms and confluence for rewrite systems.
In Int’l Joint Conf. on Artificial Intelligence, pages
362–368, 1995.
- [Ver96]
-
Rakesh M. Verma.
Unicity and modularity of confluence for term rewriting systems.
Technical report, University of Houston, 1996.