氏名: Ould Seyid Ahmed (289834090)

論文題目: Confluence of Weakly Orthogonal Conditional TRS with Extra Variables.


論文概要

Conditional term rewriting systems which are no more that a term rewriting systems with some conditions on the rules arise naturally in algebraic specifications of abstract data type. They also have been studied as a computational paradigm that combines logic and functional programming. One of the fundamental properties of these systems is confluence which plays a critical role in their completeness. This property also ensures the uniqueness of computational results, and saves time and memory needed to backtracking to consider other rewriting. In [2] Suzuki shows that the confluence property is satisfied by the class of orthogonal properly oriented right-stable CTRSs with extra variables that are not necessarily terminating under the restriction that the right-hand sides of the conditional part do not share variables neither with the left-hand side of the rule nor with other conditions. This thesis is concerned with the confluence property. First it gives a sufficient condition that guarantees the confluence in any conditional term rewriting system, and then uses this condition to simplify the proof method used by Suzuki, and to extend his results to weakly CTRSs in which the right-hand sides of the conditional part can share variables with other conditions and the left-hand side of the rule provided these variables do not appear in the right-hand side of the rule.


目次に戻る


asakura@nuie.nagoya-u.ac.jp