User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Journal Article

Modular Proofs for Completeness of hierarchical term rewriting systems


Krishna Rao,  M. R. K.
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Krishna Rao, M. R. K. (1995). Modular Proofs for Completeness of hierarchical term rewriting systems. Theoretical Computer Science, 151(2), 487-512.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-AD0E-0
In this paper, we study modular aspects of hierarchical combinations of term rewriting systems. System $\R_0 \cup \R_1$ is a hierarchical combination if the defined symbols of two subsystems, $\R_0$ and $\R_1$ are disjoint, some of the defined symbols of $\R_0$ are constructors in $\R_1$ and the defined symbols of $\R_1$ do not occur in $\R_0$. It is shown that in hierarchical combinations, a reduction can increase the rank of a term. Therefore, techniques employed in proving modularity results for direct sums and constructor sharing systems are not applicable for hierarchical combinations. We propose a set of sufficient conditions for modularity of completeness of hierarchical combinations. The sufficient conditions are syntactic ones (about recursion) based on constructor discipline. We prove our result by showing that hierarchical combination $\R_0 \cup \R_1$ satisfying our sufficient conditions is innermost normalizing and locally confluent, if $\R_0$ and $\R_1$ are complete constructor systems. The result generalizes Middeldorp and Toyama's result on modularity of completeness for shared constructor systems.