نظام إعادة الكتابة المجردة

في المنطق الرياضي وعلوم الحاسوب النظرية ، يُعد نظام إعادة الكتابة المجرد (أو نظام الاختزال المجرد أو نظام إعادة الكتابة المجرد ؛ ويُختصر إلى ARS ) نموذجًا رسميًا يُجسد المفهوم والخصائص الأساسية لأنظمة إعادة الكتابة . في أبسط صوره، يتكون نظام إعادة الكتابة المجرد من مجموعة ( من "الكائنات") مع علاقة ثنائية ، ويُرمز لها تقليديًا بـ${\displaystyle \rightarrow }$يمكن تحسين هذا التعريف بشكل أكبر إذا قمنا بفهرسة (تسمية) مجموعات فرعية من العلاقة الثنائية. على الرغم من بساطته، فإن نظام إعادة الكتابة التلقائي (ARS) كافٍ لوصف خصائص مهمة لأنظمة إعادة الكتابة مثل الأشكال العادية ، والإنهاء ، ومفاهيم مختلفة للتقارب .

تاريخيًا، ظهرت عدة صياغات رسمية لإعادة الكتابة في سياق تجريدي، لكل منها خصائصها المميزة. ويعود ذلك جزئيًا إلى تكافؤ بعض المفاهيم، كما هو موضح أدناه في هذه المقالة. أما الصياغة الرسمية الأكثر شيوعًا في الدراسات والكتب الدراسية، والتي نتبعها هنا عمومًا، فهي من وضع جيرار هويه (1980). ^{[ 1 ]}

يُعدّ نظام الاختزال المجرد ( ARS ) المفهوم الأكثر عمومية (أحادي البُعد) لتحديد مجموعة من الكائنات والقواعد التي يُمكن تطبيقها لتحويلها. ومؤخرًا، يستخدم المؤلفون مصطلح نظام إعادة الكتابة المجردة أيضًا. ^{[ 2 ]} (يُمثل تفضيل كلمة "اختزال" هنا بدلًا من "إعادة كتابة" خروجًا عن الاستخدام الموحد لكلمة "إعادة كتابة" في أسماء الأنظمة التي تُعدّ تخصيصات لنظام الاختزال المجرد. ولأن كلمة "اختزال" لا تظهر في أسماء الأنظمة الأكثر تخصصًا، فإن نظام الاختزال في النصوص القديمة يُعتبر مرادفًا لنظام الاختزال المجرد.) ^{[ 3 ]}

مجموعة ARS هي مجموعة A ، تُسمى عناصرها عادةً بالكائنات، بالإضافة إلى علاقة ثنائية على A ، يُرمز لها تقليديًا بـ →، وتُسمى علاقة الاختزال ، أو علاقة إعادة الكتابة ^{[ 2 ]} ، أو ببساطة الاختزال . ^{[ 3 ]} هذا المصطلح (الراسخ) الذي يستخدم "الاختزال" مُضلل بعض الشيء، لأن العلاقة لا تُختزل بالضرورة مقياسًا ما للكائنات.

في بعض السياقات ، قد يكون من المفيد التمييز بين بعض المجموعات الفرعية من القواعد، أي بعض المجموعات الفرعية من علاقة الاختزال →، على سبيل المثال، قد تتكون علاقة الاختزال بأكملها من قواعد التجميع والتبديل . ونتيجة لذلك، يُعرّف بعض المؤلفين علاقة الاختزال → على أنها الاتحاد المفهرس لبعض العلاقات؛ على سبيل المثال إذا${\displaystyle {\rightarrow _{1}\cup \rightarrow _{2}}={\rightarrow }}$، والرمز المستخدم هو (A, → ₁ , → ₂ ).

ككائن رياضي ، يُعد نظام ARS مطابقًا تمامًا لنظام انتقال الحالة غير المُصنَّف ، وإذا اعتُبرت العلاقة اتحادًا مُفهرسًا، فإن نظام ARS يُصبح مطابقًا لنظام انتقال الحالة المُصنَّف حيث تُمثل الفهارس التصنيفات. مع ذلك، يختلف محور الدراسة والمصطلحات. ففي نظام انتقال الحالة ، يُهتم بتفسير التصنيفات على أنها أفعال، بينما في نظام ARS، ينصب التركيز على كيفية تحويل الكائنات (إعادة كتابتها) إلى كائنات أخرى. ^{[ 4 ]}

لنفترض أن مجموعة العناصر هي T = { a , b , c } وأن العلاقة الثنائية مُعطاة بالقواعد a → b ، b → a ، a → c ، و b → c . لاحظ أنه يمكن تطبيق هذه القواعد على كل من a و b للحصول على c . علاوة على ذلك، لا يمكن تطبيق أي شيء على c لتحويله أكثر من ذلك. من الواضح أن هذه الخاصية مهمة.

أولاً، حدد بعض المفاهيم والرموز الأساسية. ^{[ 5 ]}

• ${\displaystyle {\stackrel {+}{\rightarrow }}}$هو الإغلاق المتعدي لـ${\displaystyle \rightarrow }$.
• ${\displaystyle {\stackrel {*}{\rightarrow }}}$هو الإغلاق الانعكاسي المتعدي لـ${\displaystyle \rightarrow }$أي الإغلاق المتعدي لـ${\displaystyle (\rightarrow )\cup (=)}$حيث يمثل الرمز = علاقة التطابق . وبصورة مكافئة،${\displaystyle {\stackrel {*}{\rightarrow }}}$هو أصغر طلب مسبق يحتوي على${\displaystyle \rightarrow }$.
• بصورة مماثلة،${\displaystyle {\stackrel {+}{\leftarrow }}}$، و${\displaystyle {\stackrel {*}{\leftarrow }}}$إغلاق${\displaystyle {\leftarrow }}$، العلاقة العكسية لـ${\displaystyle {\rightarrow }}$.
• ${\displaystyle \leftrightarrow }$هو الإغلاق المتناظر لـ${\displaystyle \rightarrow }$أي اتحاد${\displaystyle \rightarrow }$مع${\displaystyle {\leftarrow }}$.
• ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$هو الإغلاق الانعكاسي المتعدي المتناظر لـ${\displaystyle \rightarrow }$أي الإغلاق المتعدي لـ${\displaystyle (\leftrightarrow )\cup (=)}$أو بعبارة أخرى،${\displaystyle {\stackrel {*}{\leftrightarrow }}}$هي أصغر علاقة تكافؤ تحتوي على${\displaystyle \rightarrow }$.

يُطلق على الكائن x في المجموعة A اسم الكائن القابل للاختزال إذا وُجد كائن آخر y في المجموعة A و${\displaystyle x\rightarrow y}$وإلا فإنه يُسمى غير قابل للاختزال أو شكلًا طبيعيًا . يُسمى الكائن y شكلًا طبيعيًا لـ x إذا${\displaystyle x{\stackrel {*}{\rightarrow }}y}$ويكون y غير قابل للاختزال. إذا كان لـ x شكل طبيعي وحيد ، فعادةً ما يُرمز إليه بـ${\displaystyle x\downarrow }$في المثال 1 أعلاه، c هي صيغة طبيعية، و${\displaystyle c=a\downarrow =b\downarrow }$إذا كان لكل كائن شكل طبيعي واحد على الأقل، فإن نظام ARS يسمى بالتطبيع .

ثمة مفهوم ذو صلة، ولكنه أضعف من مفهوم وجود الأشكال الطبيعية، وهو مفهوم قابلية دمج كائنين : يُقال إن x و y قابلان للدمج إذا وُجد كائن z يتمتع بالخاصية التالية:${\displaystyle x{\stackrel {*}{\rightarrow }}z{\stackrel {*}{\leftarrow }}y}$من هذا التعريف، يتضح أنه يمكن تعريف علاقة الربط على النحو التالي:${\displaystyle {\stackrel {*}{\rightarrow }}\circ {\stackrel {*}{\leftarrow }}}$، أين${\displaystyle \circ }$هي تركيب العلاقات . وعادةً ما يُشار إلى قابلية الربط، بشكلٍ مُربكٍ إلى حدٍ ما، أيضًا بـ${\displaystyle \downarrow }$لكن في هذه الصيغة، يمثل السهم المتجه للأسفل علاقة ثنائية، أي نكتب${\displaystyle x\mathrel {\downarrow } y}$إذا كان x و y قابلين للربط.

يُقال إن شركة ARS تمتلك خاصية Church–Rosser إذا وفقط إذا${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$يشير إلى${\displaystyle x\mathrel {\downarrow } y}$لكل كائنين x و y . وبصورة مكافئة، تعني خاصية تشرش-روسر أن الإغلاق الانعكاسي المتعدي المتناظر مُضمن في علاقة الربط. أثبت ألونسو تشرش وج . باركلي روسر في عام 1936 أن حساب لامدا يتمتع بهذه الخاصية؛ ^{[ 6 ]} ومن هنا جاء اسم الخاصية. ^{[ 7 ]} في نظام ARS مع خاصية تشرش-روسر، يمكن اختزال المسألة اللفظية إلى البحث عن خليفة مشترك. في نظام تشرش-روسر، يمتلك الكائن شكلًا طبيعيًا واحدًا على الأكثر ؛ أي أن الشكل الطبيعي للكائن فريد إن وُجد، ولكنه قد لا يكون موجودًا.

تكافئ خصائصٌ عديدة، أبسط من خصائص تشرش-روسر، خصائصَ تشرش-روسر. ويُتيح وجود هذه الخصائص المكافئة إثباتَ أن النظام يتبع تشرش-روسر بجهدٍ أقل. علاوةً على ذلك، يُمكن تعريف مفاهيم الالتقاء كخصائص لكائنٍ مُحدد، وهو أمرٌ غير ممكن في تشرش-روسر.${\displaystyle (A,\rightarrow )}$يقال إنه،

• تكون متقاربة إذا وفقط إذا كان لكل w و x و y في A ، ${\displaystyle x{\stackrel {*}{\leftarrow }}w{\stackrel {*}{\rightarrow }}y}$يشير إلى${\displaystyle x\mathrel {\downarrow } y}$باختصار، يُشير مفهوم الالتقاء إلى أنه بغض النظر عن مدى تباعد مسارين من أصل مشترك ( w )، فإنهما يلتقيان عند نقطة مشتركة لاحقة. ويمكن توضيح هذا المفهوم كخاصية لكائن معين (w) ، ويُطلق على النظام اسم "الالتقاء" إذا كانت جميع عناصره متقاربة.
• تكون شبه متصلة إذا وفقط إذا كان لكل w و x و y في A ، ${\displaystyle x\leftarrow w{\stackrel {*}{\rightarrow }}y}$يشير إلى${\displaystyle x\mathrel {\downarrow } y}$يختلف هذا عن التقارب من خلال الاختزال بخطوة واحدة من w إلى x .
• تكون متقاربة محليًا إذا وفقط إذا كان لكل w و x و y في A ، ${\displaystyle x\leftarrow w\rightarrow y}$يشير إلى${\displaystyle x\mathrel {\downarrow } y}$تُسمى هذه الخاصية أحيانًا بالتقارب الضعيف .

نظرية. بالنسبة لـ ARS، فإن الشروط الثلاثة التالية متكافئة: (1) أن يكون له خاصية Church–Rosser، (2) أن يكون متصلاً، (3) أن يكون شبه متصل. ^{[ 8 ]}

نتيجة . ^{[ 9 ]} في نظام ARS متصل إذا${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$ثم

• إذا كان كل من x و y شكلين طبيعيين، فإن x = y .
• إذا كانت y صيغة طبيعية، فإن${\displaystyle x{\stackrel {*}{\rightarrow }}y}$.

بسبب هذه المكافئات، نجد تباينًا ملحوظًا في التعريفات في المراجع. على سبيل المثال، في كتاب تيريز، تُعرَّف خاصية تشيرش-روسر والتقارب على أنهما مترادفان ومتطابقان مع تعريف التقارب المُقدَّم هنا؛ وتبقى خاصية تشيرش-روسر، كما عُرِّفت هنا، غير مُسمَّاة، ولكنها تُقدَّم كخاصية مُكافئة؛ وهذا الاختلاف عن النصوص الأخرى مقصود. ^{[ 10 ]} وبسبب النتيجة المذكورة أعلاه، يُمكن تعريف الشكل الطبيعي y لـ x على أنه شكل غير قابل للاختزال y يتمتع بالخاصية التالية:${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$هذا التعريف، الموجود في كتاب وأوتو، يعادل التعريف الشائع الوارد هنا في نظام متقارب، ولكنه أكثر شمولاً في نظام ARS غير المتقارب.

من ناحية أخرى، لا يُعدّ الالتقاء المحلي مكافئًا لمفاهيم الالتقاء الأخرى الواردة في هذا القسم، ولكنه أضعف منه بكثير. والمثال المضاد النموذجي هو${\displaystyle \{b\rightarrow c,c\rightarrow b,b\rightarrow a,c\rightarrow d\}}$، وهو متصل محليًا ولكنه غير متصل (انظر الصورة).

يُقال عن نظام إعادة الكتابة المجرد أنه نظام نهائي أو نوثيري إذا لم تكن هناك سلسلة لانهائية${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }$(هذا يعني ببساطة أن علاقة إعادة الكتابة هي علاقة نوثرية ). في علاقة إعادة كتابة منتهية، يمتلك كل كائن شكلًا طبيعيًا واحدًا على الأقل، وبالتالي فهي علاقة تطبيع. والعكس غير صحيح. في المثال 1 على سبيل المثال، توجد سلسلة إعادة كتابة لا نهائية، وهي:${\displaystyle a\rightarrow b\rightarrow a\rightarrow b\rightarrow \cdots }$على الرغم من أن النظام في حالة تطبيع، يُطلق على نظام ARS المتقارب والمتصل اسم النظام المعياري [ ^{11 ]} أو النظام المتقارب . في نظام ARS المتقارب، يمتلك كل عنصر شكلًا طبيعيًا ^فريدًا . ولكن يكفي أن يكون النظام متصلًا ومُطَبِّعًا حتى يوجد شكل طبيعي فريد لكل عنصر، كما هو موضح في المثال 1.

نظرية ( مبدأ نيومان ): يكون ARS المنتهي متقاربًا إذا وفقط إذا كان متقاربًا محليًا.

كان برهان نيومان الأصلي لهذه النتيجة عام 1942 معقدًا نوعًا ما. ولم ينشر هويه برهانًا أبسط بكثير إلا في عام 1980، مستغلًا حقيقة أنه عندما${\displaystyle \rightarrow }$عندما تنتهي العملية، يمكننا تطبيق الاستقراء المبني على أسس متينة . ^{[ 12 ]}

• المسائل اللفظية (الرياضيات) - وخاصة القسم المتعلق بأنظمة إعادة الصياغة المجردة

• بادر، فرانز ؛ نيبكو، توبياس (1998). إعادة صياغة المصطلحات وما إلى ذلك . مطبعة جامعة كامبريدج. ISBN 9780521779203.كتاب دراسي مناسب لطلاب المرحلة الجامعية الأولى.
• ناحوم ديرشوفيتز وجان بيير جوانو ، أنظمة إعادة الكتابة ، الفصل 6 في كتاب جان فان ليوين (محرر)، دليل علوم الحاسوب النظرية، المجلد ب: النماذج الرسمية والدلالات ، دار النشر إلسيفير ومعهد ماساتشوستس للتكنولوجيا، 1990، رقم ISBN 0-444-88074-7، الصفحات  243 – 320. النسخة الأولية من هذا الفصل متاحة مجاناً من المؤلفين، لكنها تفتقر إلى الأشكال.
• بوك، رونالد ف .؛ أوتو، فريدريش (1993). "1، "أنظمة الاختزال المجرد"أنظمة إعادة كتابة السلاسل النصية . سبرينغر. رقم ISBN 0-387-97965-4.
• مارك بيزيم ; جان ويليم كلوب ؛ رويل دي فريجر ; تيريز (2003). "1". أنظمة إعادة كتابة المصطلح . مطبعة جامعة كامبريدج. رقم ISBN 0-521-39115-6.هذه دراسة شاملة. إلا أنها تستخدم قدراً كبيراً من الرموز والتعريفات غير الشائعة في مصادر أخرى. فعلى سبيل المثال، تُعرَّف خاصية تشيرش - روسر بأنها مطابقة لخاصية الالتقاء.
• هاريسون، جون (2009). "4 "المساواة"" دليل المنطق العملي والاستدلال الآلي"، مطبعة جامعة كامبريدج . رقم ISBN 978-0-521-89957-4.إعادة صياغة المجرد من منظور عملي لحل المشكلات في المنطق المعادلاتي .
• جيرار هويه ، الاختزالات المتقاربة: الخصائص المجردة والتطبيقات على أنظمة إعادة كتابة المصطلحات ، مجلة ACM ( JACM )، أكتوبر 1980، المجلد 27، العدد 4، الصفحات 797-821.  أرست ورقة هويه العديد من المفاهيم والنتائج والرموز الحديثة.
• Sinyor, J.; "The 3x+1 Problem as a String Rewriting System" , International Journal of Mathematics and Mathematical Sciences , Volume 2010 (2010), Article ID 458563, 6 pages.
• دافي، ديفيد أ. (1991). مبادئ إثبات النظريات الآلي . وايلي.
• تشرش، ألونسو؛ روسر، جيه بي (1936). "بعض خصائص التحويل" . معاملات الجمعية الرياضية الأمريكية . 39 (3): 472-482 . doi : 10.2307/1989762 . ISSN 0002-9947 . JSTOR 1989762 .