Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Modular Proofs for Completeness of Hierarchical Term Rewriting Systems

MPG-Autoren
/persons/resource/persons44846

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

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)

1-s2.0-0304397595000758-main.pdf
(Verlagsversion), 2MB

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. doi:10.1016/0304-3975(95)00075-8.


Zitierlink: https://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.