بازنویسی (ریاضی)

در ریاضیات، علوم کامپیوتر و منطق، بازنویسی طیف گسترده‌ای از روشهای (بالقوه غیر قطعی) را برای جایگزینی زیرشاخه‌های یک فرمول با عبارات دیگر در بر می‌گیرد. موضوعات مورد توجه این مقاله شامل سیستم‌های بازنویسی (موتورهای بازنویسی^[۱] یا سیستم‌های کاهش) هستند. در ابتدایی‌ترین شکل، آن‌ها از مجموعه ای از اشیا و روابطی در مورد نحوه تبدیل آن اشیا تشکیل شده‌اند.

بازنویسی می‌تواند غیر قطعی باشد. یک قانون برای بازنویسی یک اصطلاح، می‌تواند به روش‌های مختلفی برای آن اصطلاح اعمال شود، یا بیش از یک قانون قابل اجرا است. پس سیستم‌های بازنویسی الگوریتمی برای تغییر اصطلاح به اصطلاح دیگر ارائه نمی‌دهند، بلکه مجموعه ای از کاربردهای قانونی را ارائه می‌کنند که ممکن باشند. هرچند زمانی که سیستم‌های باز نویسی با یک الگوریتم مناسب ترکیب می‌شود، درواقع می‌توان آن‌ها را به عنوان برنامه‌های رایانه ای محسوب کرد. تعداد بسیاری از قضیه اثبات کننده^[۲]‌ها و زبان‌های برنامه‌نویسی اعلانی بر اساس بازنویسی اصطلاح هستند.^[۳][۴]

مثال‌ها

منطق

در منطق، فرایند به‌دست آوردن فرم نرمال پیوندی (CNF) یک فرمول می‌تواند به صورت یک سیستم بازنویسی پیاده‌سازی شود. قوانین نمونه ای از چنین سیستمی عبارتند از:

${\displaystyle \neg \neg A\to A}$ (نقیض مضاعف)

${\displaystyle \neg (A\land B)\to \neg A\lor \neg B}$ (قوانین دی مورگان)

${\displaystyle \neg (A\lor B)\to \neg A\land \neg B}$

${\displaystyle (A\land B)\lor C\to (A\lor C)\land (B\lor C)}$ (توزیع پذیری)

${\displaystyle A\lor (B\land C)\to (A\lor B)\land (A\lor C),}$

که در آن‌ها نماد (${\displaystyle \to }$) نشان می‌دهد که عبارتی که با سمت چپ قانون مطابقت دارد می‌تواند با عبارتی که در سمت راست تشکیل شده‌است بازنویسی شود و نمادها هر یک بیان فرعی(به انگلیسی: Subexpression) را نشان می‌دهند. در چنین سیستمی، هر قانون به گونه ای انتخاب می‌شود که سمت چپ معادل سمت راست باشد، و در نتیجه هنگامی که سمت چپ با یک بیان فرعی مطابقت دارد، انجام بازنویسی آن بیان از چپ به راست، قوام منطقی و مقدار کل عبارت را حفظ می‌کند.

محاسبات

برای محاسبه عملیات حساب روی اعداد طبیعی می‌توان از سیستم‌های بازنویسی استفاده کرد. برای این منظور، هر عددی باید به عنوان یک اصطلاح تعریف شود. ساده‌ترین رمزگذاری همان است که در بدیهیات Peano، بر اساس ثابت ۰ (صفر) و تابع جانشین S استفاده می‌شود.

به عنوان مثال:

${\displaystyle 0\to 0}$

${\displaystyle 1\to S(0)}$

${\displaystyle 2\to S(S(0))}$

${\displaystyle 3\to S(S(S(0)))}$

سپس برای محاسبه مجموع و حاصل از اعداد طبیعی داده شده می‌توان از سیستم بازنویسی اصطلاح زیر استفاده کرد.

${\displaystyle {\begin{aligned}A+0&\to A&{\textrm {(1)}},\\A+S(B)&\to S(A+B)&{\textrm {(2)}},\\A\cdot 0&\to 0&{\textrm {(3)}},\\A\cdot S(B)&\to A+(A\cdot B)&{\textrm {(4)}}.\end{aligned}}}$

به عنوان مثال، محاسبه ۲ + ۲ در نتیجه ۴ می‌تواند با بازنویسی اصطلاح به شرح زیر کپی شود:

${\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))}$

${\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}$ ${\displaystyle S(\;S(S(0))+S(0)\;)}$

${\displaystyle S(S(S(S(0)))),}$${\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}$${\displaystyle S(S(\;S(S(0))+0\;))}$

که در آن اعداد قانون در بالای پیکان بازنویسی آورده شده‌است.

به عنوان مثال دیگر، محاسبه ۲⋅۲ به شکل زیر است:

${\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}$ ${\displaystyle S(S(0))\cdot S(S(0))}$

${\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}$${\displaystyle S(S(0))+S(S(0))\cdot S(0)}$

${\displaystyle \;\;{\stackrel {(3)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))+S(S(0)\cdot 0)}$

${\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}$${\displaystyle S(S(0))+S(S(0))+0)}$

${\displaystyle S(S(S(S(0)))),}$ ${\displaystyle \;\;{\stackrel {\textrm {s.a.}}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))}$

به طوری که آخرین مرحله شامل محاسبه مثال قبلی است.

زبانشناسی

در زبانشناسی، قوانین بازنویسی، که به آنها قوانین ساختار عبارات نیز گفته می‌شود، در بعضی از سیستم‌های دستور زبان مولد، به عنوان ابزاری برای تولید جملات صحیح دستوری یک زبان استفاده می‌شود. چنین قانونی معمولاً به شکل A → X، که در آن A برچسب دسته نحوی است، مانند عبارت اسمی یا جمله، و X دنباله ای از برچسب یا تکواژ هاییست به طوری که A را می‌توان با X در تولید جایگزین ساختار سازنده یک جمله جایگزین کرد. به عنوان مثال، قانون S → NP VP به این معنی است که یک جمله(به انگلیسی: Sentence) می‌تواند از یک عبارت اسمی(به انگلیسی: noun phrase) و به دنبال آن یک عبارت فعلی (به انگلیسی: verb phrase) تشکیل شود. قوانین بعدی مشخص خواهد کرد که یک عبارت اسمی و یک عبارت فعلی می‌تواند از چه زیر ترکیبات تشکیل شده باشد و به همین شکل تا آخر.

ردیابی سیستم‌های بازنویسی

نظریه ردیابی ابزاری را برای بحث در مورد پردازش چندگانه (به انگلیسی: Multiprocessing) به صورت رسمی‌تر ارائه می‌کند. ابزارهایی همچون مونوئید ردیابی و مونوئید تاریخ. بازنویسی را می‌توان در سیستم‌های ردیابی نیز انجام داد.

فلسفه

سیستم‌های بازنویسی را می‌توان به عنوان برنامه‌هایی تلقی کرد که از لیستی از روابط علت و معلولی، نتایج نهایی را استنباط می‌کنند. به این ترتیب می‌توان سیستم‌های بازنویسی را به عنوان اثبات کننده‌های خودکار علیت در نظر گرفت.^{[نیازمند منبع]}

جستارهای وابسته

• جفت انتقادی (منطق)
• الگوریتم تکمیل Knuth – Bendix
• سیستم‌های L بازنویسی را مشخص می‌کنند که به‌طور موازی انجام می‌شود.
• شفافیت مرجع در علوم کامپیوتر
• بازنویسی تنظیم شده
• حساب Rho

منابع

1. Sculthorpe, Neil; Frisby, Nicolas; Gill, Andy (2014). "The Kansas University rewrite engine" (PDF). Journal of Functional Programming. 24 (4): 434–473. doi:10.1017/S0956796814000185. ISSN 0956-7968.
2. Hsiang, Jieh; Kirchner, Hélène; Lescanne, Pierre; Rusinowitch, Michaël (1992). "The term rewriting approach to automated theorem proving". The Journal of Logic Programming. 14 (1–2): 71–99. doi:10.1016/0743-1066(92)90047-7.
3. Frühwirth, Thom (1998). "Theory and practice of constraint handling rules". The Journal of Logic Programming. 37 (1–3): 95–138. doi:10.1016/S0743-1066(98)10005-5.
4. Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J.F. (2002). "Maude: Specification and programming in rewriting logic". Theoretical Computer Science. 285 (2): 187–243. doi:10.1016/S0304-3975(01)00359-0.

برای مطالعه بیشتر

• Baader, Franz؛ نیپکو، توبیاس (۱۹۹۹). بازنویسی مدت و همه اینها . انتشارات دانشگاه کمبریج. شابک Baader, Franz Baader, Franz 316 صفحه. یک کتاب درسی مناسب برای دانشجویان دوره کارشناسی.
• مارک بزم، یان ویلم کلوپ، رول دو وریجر ("ترزی")، سیستم‌های بازنویسی ترم ("TeReSe") ، انتشارات دانشگاه کمبریج، ۲۰۰۳ ،شابک ‎۰-۵۲۱-۳۹۱۱۵-۶. این جدیدترین تک نگاری جامع است. با این وجود از معاملات و تعاریف غیراستاندارد استاندارد استفاده می‌کند. به عنوان مثال، ویژگی Church-Rosser یکسان با محل تلاقی تعریف شده‌است.
• Nachum Dershowitz و Jean-Pierre Jouannaud "بازنویسی سیستمها"، فصل ۶ در Jan van Leeuwen (ویراستار)، کتابچه راهنمای علوم رایانه نظری، جلد B: مدلهای رسمی و معناشناسی، الزویر و مطبوعات MIT، ۱۹۹۰ ،شابک ‎۰-۴۴۴-۸۸۰۷۴-۷، صص. 243 – ۳۲۰. قبل از مطبوعات و این فصل به صورت رایگان از نویسندگان دسترس است، اما آن را از دست رفته‌است آمار و ارقام.
• ناخوم درساوویتس و دیوید پلاستید . "بازنویسی"، فصل ۹ در جان آلن رابینسون و آندره وورونکوف (ادس)، کتاب راهنمای استدلال خودکار، جلد ۱.
• جرارد هویت و درک اوپن ، معادلات و قوانین بازنویسی ، یک نظر سنجی (۱۹۸۰) گروه تأیید استنفورد، گزارش شماره ۱۵ گزارش گروه علوم کامپیوتر شماره STAN-CS-80-785
• جان ویلم کلوپ. "سیستمهای بازنویسی مدت"، فصل ۱ در سامسون آبرامسکی، داو م گبای و تام مایباوم (ادس)، کتاب راهنمای منطق در علوم کامپیوتر، دوره ۲: زمینه: ساختارهای محاسباتی.
• دیوید پلاست "استدلال معادلات و سیستمهای بازنویسی اصطلاح"، در Dov M. Gabbay , CJ Hogger و John Alan Robinson (Eds.)، کتاب راهنمای منطق در هوش مصنوعی و برنامه‌نویسی منطق، جلد ۱.
• یورگن آونهاوس و کلاوس مادلنر. "بازنویسی اصطلاح و استدلال معادله ای". در Ranan B. Banerji (ویراستار)، تکنیک‌های رسمی در هوش مصنوعی: کتاب منبع، الزویر (۱۹۹۰).

بازنویسی رشته

• رونالد وی بوک و فردریش اتو، سیستم‌های بازنویسی رشته، اسپرینگر (۱۹۹۳).
• بنجامین بنینگ هوفن، سوزان کمریچ و مایکل ام. ریشتر، سیستمهای کاهش. LNCS 277، Springer-Verlag (1987).

دیگر

• مارتین دیویس، رون سیگال، الین جی ویوکر، (۱۹۹۴) محاسبه پذیری، پیچیدگی و زبان‌ها: مبانی علوم نظری رایانه - چاپ دوم، مطبوعات علمی ،شابک ‎۰-۱۲-۲۰۶۳۸۲-۱.

پیوند به بیرون

• بازنویسی صفحه اصلی
• گروه کاری IFIP 1.6
• محققان در مورد بازنویسی توسط آرت میدلدورپ، دانشگاه اینسبروک
• پورتال خاتمه