Generally speaking,confluence property is not preserved when Term Rewriting Systems(TRSs) are combined,even if they are canonical.In this paper we give some sufficient conditions for ensuring the confluence property o...Generally speaking,confluence property is not preserved when Term Rewriting Systems(TRSs) are combined,even if they are canonical.In this paper we give some sufficient conditions for ensuring the confluence property of combined left-linear,overlapping TRSs.展开更多
We define here the concept of head boundedness,head normal form and head confluence of term rewriting systems that allow infinite derivations.Head confluence is weaker than confluence,but suffi- cient to guarantee the...We define here the concept of head boundedness,head normal form and head confluence of term rewriting systems that allow infinite derivations.Head confluence is weaker than confluence,but suffi- cient to guarantee the correctness of lazy implementations of equational logic programming languages. Then we prove several results.First,if a left-linear system is locally confluent and head-bounded,then it is head-confluent.Second,head-confluent and head-bounded systems have the head Church-Rosser proper- ty.Last,if an orthogonal system is head-terminating,then it is bead-bounded.These results can be ap- plied to generalize equational logic programming languages.展开更多
Further research about nonterminating rewritings is introduced. First, the previousdefinition of head boundedness is modified to exclude nonfair reduction sequences.A sufficient condition is then given to determine he...Further research about nonterminating rewritings is introduced. First, the previousdefinition of head boundedness is modified to exclude nonfair reduction sequences.A sufficient condition is then given to determine head boundedness of term rewritingsystems. The condition is then developed to a method to determine head boundednessof constructor systems.展开更多
This paper investigates the semantics of conditional term rewriting systemswith negation (denoted by EI-CTRS), called constructor-based EI-model se-mantics. The introduction of '≠' in EI-CTRS make EI-CTRS mor...This paper investigates the semantics of conditional term rewriting systemswith negation (denoted by EI-CTRS), called constructor-based EI-model se-mantics. The introduction of '≠' in EI-CTRS make EI-CTRS more difficult tostudy. This is in part because of a failure of EI-CTRS to guarantee that thereexist least Herbrand models in classical logical point of views. The key idea ofEI-model is to explain that 't ≠ s' means that the two concepts representedby t and s respectively actually belong to distinguished basic concepts repre-sented by two constructor-ground terms. We define the concept of EI-model,and show that there exist least Herbrand ELmodels for EI-satisfiable EI-CTRS.From algebraic and logic point of view, we show that there are very strong rea-sons for regarding the least Herbrand EI-models as the intended semantics ofEI-CTRS. According to fixpoint theory, we develop a method to construct leastHerbrand EI-models in a bottom-up manner. Moreover, we discuss soundnessand completeness of EI-rewrite for EI-model semantics.展开更多
In this paper, the notion of partial completion of equational theories is proposed, which is a procedure to construct a confluent term rewriting system from an equational theory without requirement of termination cond...In this paper, the notion of partial completion of equational theories is proposed, which is a procedure to construct a confluent term rewriting system from an equational theory without requirement of termination condition. A partial completion algorithm is presented with a brief description of its application in a program development system.展开更多
基金This work was supported partly by The National Science FoundationThe Ministry of Electronic Industries and High Technology Program under The National Commission of Science & Technology.
文摘Generally speaking,confluence property is not preserved when Term Rewriting Systems(TRSs) are combined,even if they are canonical.In this paper we give some sufficient conditions for ensuring the confluence property of combined left-linear,overlapping TRSs.
基金The project is supported by the National Natural Science Foundation of China.
文摘We define here the concept of head boundedness,head normal form and head confluence of term rewriting systems that allow infinite derivations.Head confluence is weaker than confluence,but suffi- cient to guarantee the correctness of lazy implementations of equational logic programming languages. Then we prove several results.First,if a left-linear system is locally confluent and head-bounded,then it is head-confluent.Second,head-confluent and head-bounded systems have the head Church-Rosser proper- ty.Last,if an orthogonal system is head-terminating,then it is bead-bounded.These results can be ap- plied to generalize equational logic programming languages.
文摘Further research about nonterminating rewritings is introduced. First, the previousdefinition of head boundedness is modified to exclude nonfair reduction sequences.A sufficient condition is then given to determine head boundedness of term rewritingsystems. The condition is then developed to a method to determine head boundednessof constructor systems.
文摘This paper investigates the semantics of conditional term rewriting systemswith negation (denoted by EI-CTRS), called constructor-based EI-model se-mantics. The introduction of '≠' in EI-CTRS make EI-CTRS more difficult tostudy. This is in part because of a failure of EI-CTRS to guarantee that thereexist least Herbrand models in classical logical point of views. The key idea ofEI-model is to explain that 't ≠ s' means that the two concepts representedby t and s respectively actually belong to distinguished basic concepts repre-sented by two constructor-ground terms. We define the concept of EI-model,and show that there exist least Herbrand ELmodels for EI-satisfiable EI-CTRS.From algebraic and logic point of view, we show that there are very strong rea-sons for regarding the least Herbrand EI-models as the intended semantics ofEI-CTRS. According to fixpoint theory, we develop a method to construct leastHerbrand EI-models in a bottom-up manner. Moreover, we discuss soundnessand completeness of EI-rewrite for EI-model semantics.
文摘In this paper, the notion of partial completion of equational theories is proposed, which is a procedure to construct a confluent term rewriting system from an equational theory without requirement of termination condition. A partial completion algorithm is presented with a brief description of its application in a program development system.
