Advanced Topics in Term Rewriting

تکنیک‌های بازنویسی اصطلاحات در زمینه‌های مختلف علوم کامپیوتر قابل استفاده هستند: در مهندسی نرم‌افزار (مانند انواع داده‌های انتزاعی مشخص شده معادل)، در زبان‌های برنامه‌نویسی (مانند برنامه‌نویسی تابعی-منطقی)، در جبر کامپیوتری (مانند محاسبات نمادین، مبانی گرابنر)، در راستی‌آزمایی برنامه (مثلاً اثبات خودکار خاتمه برنامه‌ها)، در اثبات قضیه خودکار (مانند یکسان سازی معادله)، و در جبر (مثلاً جبر بولی، نظریه گروه). به عبارت دیگر، بازنویسی اصطلاح در علوم کامپیوتر عملی، علوم کامپیوتر نظری و ریاضیات کاربرد دارد. به طور کلی، تکنیک‌های بازنویسی اصطلاح را می‌توان با موفقیت در حوزه‌هایی به کار برد که نیازمند روش‌های کارآمد برای استدلال با معادلات هستند. یکی از مشکلات عمده ای که در تئوری بازنویسی اصطلاحات با آن مواجه می شود، مشخص کردن کلاس هایی از سیستم های بازنویسی است که دارای خاصیت مطلوبی مانند تلاقی یا خاتمه هستند. اگر یک سیستم بازنویسی اصطلاح به هم پیوسته باشد، آنگاه شکل عادی یک اصطلاح معین منحصر به فرد است. یک سیستم بازنویسی پایان‌دهنده اجازه محاسبات بی‌نهایت را نمی‌دهد، یعنی هر محاسباتی که از یک عبارت شروع می‌شود باید به شکل عادی ختم شود. بنابراین، در سیستمی که هم پایانی و هم متلاشی است، هر محاسباتی بدون توجه به ترتیبی که قوانین بازنویسی در آن اعمال می‌شوند، به نتیجه‌ای منحصربفرد منجر می‌شود. این کتاب مطالعه جامعی از ختم و تلاقی و همچنین ویژگی‌های مرتبط ارائه می‌کند.

Term rewriting techniques are applicable in various fields of computer sci­ ence: in software engineering (e.g., equationally specified abstract data types), in programming languages (e.g., functional-logic programming), in computer algebra (e.g., symbolic computations, Grabner bases), in pro­ gram verification (e.g., automatically proving termination of programs), in automated theorem proving (e.g., equational unification), and in algebra (e.g., Boolean algebra, group theory). In other words, term rewriting has applications in practical computer science, theoretical computer science, and mathematics. Roughly speaking, term rewriting techniques can suc­ cessfully be applied in areas that demand efficient methods for reasoning with equations. One of the major problems one encounters in the theory of term rewriting is the characterization of classes of rewrite systems that have a desirable property like confluence or termination. If a term rewriting system is conflu­ ent, then the normal form of a given term is unique. A terminating rewrite system does not permit infinite computations, that is, every computation starting from a term must end in a normal form. Therefore, in a system that is both terminating and confluent every computation leads to a result that is unique, regardless of the order in which the rewrite rules are applied. This book provides a comprehensive study of termination and confluence as well as related properties.