محبوبترین نویسندگان :
نویسندگان مقالات پربازدید :
مجله استدلال خودکار 2013
جزئیات رویداد
همایش ، رویداد ، ژورنال
اینستاگرام تی پی بین

  • non-linear rewrite closure and weak normalization

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 712
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     a rewrite closure is an extension of a term rewrite system with new rules, usually deduced by transitivity. rewrite closures have the nice property that all rewrite derivations can be transformed into derivations of a simple form. this property has been useful for proving decidability results in term rewriting. unfortunately, when the term rewrite system is not linear, the construction of a rewrite closure is quite challenging. in this paper, we construct a rewrite closure for term rewrite systems that satisfy two properties: the right-hand side term in each rewrite rule contains no repeated variable (right-linear) and contains no variable occurring at depth greater than one (right-shallow). the left-hand side term is unrestricted, and in particular, it may be non-linear. as a consequence of the rewrite closure construction, we are able to prove decidability of the weak normalization problem for right-linear right-shallow term rewrite systems. proving this result also requires tree automata theory. we use the fact that right-shallow right-linear term rewrite systems are regularity preserving. moreover, their set of normal forms can be represented with a tree automaton with disequality constraints, and emptiness of this kind of automata, as well as its generalization to reduction automata, is decidable. a preliminary version of this work was presented at lics 2009 (creus 2009).

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم
مقالات جدیدترین رویدادها
مقالات جدیدترین ژورنال ها