de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Modular Proofs for Completeness of hierarchical term rewriting systems

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44846

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-AD0E-0
Zusammenfassung
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.