氏名: OULD SEYID AHMED (289834090)

論文題目: On Confluence of 3-CTRSs and Non-linear TRSs


論文概要

Term rewriting systems(TRSs) and conditional term rewriting systems (CTRSs) arise naturally in many computer sciences applications including algebraic computations, specifications of abstract data type and automated theorem proving. They have been also studied as a computational paradigm that combines logic programming and functional programing. Some of the most important properties of these systems rae: 1. Termination: no infinite derivation are possible. 2. determinism: each term has a normal form(UNF). 3. Confluence: reduction sequences always converge. The first property ensures the existence of a result for computation. The second implies the uniqueness of computational result, and the third saves time and memory needed for computational derivation, and guarantees the uniqueness of results. In 1996 Toyoma presented some conditions to ensure the confluence and determinism properties for non-left linear, non duplicating and right-linear TRSs. In 1995, Suzuki gave a sufficient condition to ensure the confluence of orthogonal 3-CTRSs. In 1996 Gramlich presented a condition to ensure the confluence and termination of CTRSs. This thesis is concerned with the properties mentioned above in both the conditional and unconditional case. For the conditional case, we present a sufficient condition for confluence of CTRSs in general, the sufficiency of this condition is proved by adopting a method that measures the reduction sequences with a multiset of labels ordered by the multiset extension. This condition is exploited to relax the syntactical conditions imposed by Suzuki in order to allow more shared variables between the right hand side of a condition and both of the left hand side of a rule and the left hand sides of other conditions. We also extend Suzuki's results to weakly CTRSs and overlay systems. We showed that Gramlich's result is not applicable to the the class of 3-CTRSs and give a condition to extend his results to this class. By using a conditional linearization, the results obtained for CTRSs are exploited to extend the results obtained by Toyoma for confluence of TRSs to non-right linear case, and to present conditions that ensure the UNF and termination of duplicating non-linear TRSs.


目次に戻る


提出時刻:2001/02/08 20:45:37