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

منطق

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

${\displaystyle \mathrm{\neg }\mathrm{\neg }A\to A}$

(نقیض مضاعف)

${\displaystyle \mathrm{\neg }(A\wedge B)\to \mathrm{\neg }A\vee \mathrm{\neg }B}$

(قوانین دی مورگان)

${\displaystyle \mathrm{\neg }(A\vee B)\to \mathrm{\neg }A\wedge \mathrm{\neg }B}$

${\displaystyle (A\wedge B)\vee C\to (A\vee C)\wedge (B\vee C)}$

(توزیع پذیری)

${\displaystyle A\vee (B\wedge C)\to (A\vee B)\wedge (A\vee C),}$

که در آن‌ها نماد (${\displaystyle \to }$

محاسبات

برای محاسبه عملیات حساب روی اعداد طبیعی می‌توان از سیستم‌های بازنویسی استفاده کرد. برای این منظور، هر عددی باید به عنوان یک اصطلاح تعریف شود. ساده‌ترین رمزگذاری همان است که در بدیهیات 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 \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{\text{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

• 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
• محققان در مورد بازنویسی توسط آرت میدلدورپ، دانشگاه اینسبروک
• پورتال خاتمه