Modular Proofs for Completeness of Hierarchical Term Rewriting Systems

Krishna Rao, M. R. K.

doi:10.1016/0304-3975(95)00075-8

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

タグ情報を表示リリース履歴を表示詳細要約

公開

学術論文

Modular Proofs for Completeness of Hierarchical Term Rewriting Systems

MPS-Authors

/persons/resource/persons44846

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

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

1-s2.0-0304397595000758-main.pdf
(出版社版), 2MB

付随資料 (公開)

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

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