| Project/Area Number |
11680338
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
MIDDELDORP Aart Institute of Information Sciences and Electronics Associate Professor, 電子・情報工学系, 助教授 (30251044)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
YAMADA Toshiyuki Institute of Information Sciences and Electronics Research Associate, 電子・情報工学系, 助手 (60312831)
IDA Tetsuo Institute of Information Sciences and Electronics Professor, 電子・情報工学系, 教授 (70100047)
|
|---|
| Project Period (FY) |
1999 – 2000
|
| Project Status |
Completed (Fiscal Year 2000)
|
| Budget Amount *help |
¥3,400,000 (Direct Cost: ¥3,400,000)
Fiscal Year 2000: ¥1,600,000 (Direct Cost: ¥1,600,000)
Fiscal Year 1999: ¥1,800,000 (Direct Cost: ¥1,800,000)
|
|---|
| Keywords | term rewriting / narrowing / symbolic computation / call-by-need strategies / modularity / termination / completeness / 文脈依存書き換え / 変換法 |
|---|
| Research Abstract |
Semantic labelling is a powerful tool for proving termination of term rewrite systems. The usefulness of the extension to equational term rewriting described in a paper of Zantema is however rather limited. In [1] we introduced a stronger version of equational semantical labelling, parameterized by three choices : (1) the order on the underlying algebra (partial order vs. quasi-order), (2) the relation between the algebra and the rewrite system (model vs. quasi-model), and (3) the labelling of the function symbols appearing in the equations (forbidden vs. allowed). We presented soundness and completeness results for the various instantiations, analyzed the relationships between them, and presented two applications of our equational semantic labelling technique.
We also continued our investigations into the completeness of lazy narrowing calculi. In an earlier paper we proved that the lazy conditional narrowing calculus LCNC is complete with respect to normalizable solutions for the clas
… More
s of confluent but not necessarily terminating conditional rewrite systems without so-called extra variables in the conditional parts of the rewrite rules. Unfortunately, the proof does not provide any useful complete selection function, hence in implementations we need to backtrack over the choice of equations in goals in order to guarantee that all solutions are enumerated. This is in contrast to the unconditional case where completeness with respect to the leftmost selection function is known. In [2] we closed the gap by proving the completeness of LCNC with respect to the leftmost selection strategy for the above-mentioned class of conditional rewrite systems.
In a joint paper with Irene Durand we introduced a powerful framework for the study of call by need computations. Using elementary tree automata techniques and ground tree transducers simple decidability proofs were obtained for a hierarchy of classes of rewrite systems that are much larger than earlier classes defined using the complicated sequentiality concept. In [3] we studied the modularity of membership in the new hierarchy. Surprisingly, it turned out that none of the classes in the hierarchy is preserved under signature extension. By imposing various conditions we recovered the preservation under signature extension. By imposing some more conditions we were able to strengthen the signature extension results to modularity for disjoint and constructor-sharing combinations. Less
|
