إعادة الصياغة

في الرياضيات واللغويات وعلوم الحاسوب والمنطق ، يشمل مصطلح إعادة الكتابة طيفًا واسعًا من أساليب استبدال الحدود الفرعية في الصيغة بحدود أخرى. ويمكن تحقيق هذه الأساليب من خلال أنظمة إعادة الكتابة (المعروفة أيضًا بأنظمة إعادة الكتابة ، أو محركات إعادة الكتابة ^،^أو أنظمة ^{الاختزال}⁾ . في أبسط صورها، تتكون هذه الأنظمة من مجموعة من العناصر، بالإضافة إلى ^علاقات تحدد كيفية تحويل هذه العناصر ^.

قد تكون عملية إعادة الكتابة غير حتمية . إذ يمكن تطبيق قاعدة واحدة لإعادة كتابة مصطلح ما بطرق مختلفة عليه، أو قد يكون أكثر من قاعدة قابلة للتطبيق. وبالتالي، لا توفر أنظمة إعادة الكتابة خوارزمية لتغيير مصطلح إلى آخر، بل مجموعة من التطبيقات الممكنة للقواعد. ومع ذلك، عند دمجها مع خوارزمية مناسبة، يمكن اعتبار أنظمة إعادة الكتابة برامج حاسوبية ، وقد استندت العديد من برامج إثبات النظريات ^{[ 3 ]} ولغات البرمجة التصريحية إلى إعادة كتابة المصطلحات. ^{[ 4 ]}^{[ 5 ]}

أمثلة توضيحية

منطق

في المنطق ، يمكن تطبيق إجراء الحصول على الصيغة الطبيعية الاقترانية (CNF) لصيغة ما كنظام إعادة كتابة. ^{[ 6 ]} على سبيل المثال، ستكون قواعد هذا النظام كما يلي:

\neg \neg A\to A

( حذف النفي المزدوج )

\neg (A\land B)\to \neg A\lor \neg B

( قوانين دي مورغان )

\neg (A\lor B)\to \neg A\land \neg B

(A\land B)\lor C\to (A\lor C)\land (B\lor C)

( خاصية التوزيع )

A\lor (B\land C)\to (A\lor B)\land (A\lor C),

^{[ ملاحظة 1 ]}

لكل قاعدة، يمثل كل متغير تعبيرًا فرعيًا، والرمز ( $\to$ يشير الرمز ) إلى إمكانية إعادة كتابة تعبير يطابق الجانب الأيسر منه ليصبح مطابقًا للجانب الأيمن. في هذا النظام، تمثل كل قاعدة تكافؤًا منطقيًا ، لذا فإن إعادة كتابة تعبير باستخدام هذه القواعد لا تُغير قيمته المنطقية. قد لا تحافظ أنظمة إعادة الكتابة المفيدة الأخرى في المنطق على القيم المنطقية، انظر على سبيل المثال: التكافؤ المُرضي .

الحساب

يمكن استخدام أنظمة إعادة كتابة الحدود لإجراء العمليات الحسابية على الأعداد الطبيعية . ولتحقيق ذلك، يجب ترميز كل عدد من هذه الأعداد كحد . أبسط ترميز هو المستخدم في بديهيات بيانو ، والذي يعتمد على الثابت 0 (صفر) ودالة التالي S. على سبيل المثال ، تُمثل الأعداد 0 و1 و2 و3 بالحدود 0 وS(0) وS(S(0)) وS(S(S(0))) على التوالي. يمكن بعد ذلك استخدام نظام إعادة كتابة الحدود التالي لحساب مجموع وحاصل ضرب الأعداد الطبيعية المعطاة. ^[⁷^]

{\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}}

على سبيل المثال، يمكن تكرار عملية حساب 2+2 للحصول على 4 عن طريق إعادة كتابة المصطلحات على النحو التالي:

S(S(0))+S(S(0))

\;\;{\stackrel {(2)}{\to }}\;\;

S(\;S(S(0))+S(0)\;)

\;\;{\stackrel {(2)}{\to }}\;\;

S(S(\;S(S(0))+0\;))

\;\;{\stackrel {(1)}{\to }}\;\;

S(S(S(S(0)))),

حيث تشير العلامة الموجودة أعلى كل سهم إلى القاعدة المستخدمة في كل عملية إعادة كتابة.

كمثال آخر، تبدو عملية حساب 2⋅2 كما يلي:

S(S(0))\cdot S(S(0))

\;\;{\stackrel {(4)}{\to }}\;\;

S(S(0))+S(S(0))\cdot S(0)

\;\;{\stackrel {(4)}{\to }}\;\;

S(S(0))+S(S(0))+S(S(0))\cdot 0

\;\;{\stackrel {(3)}{\to }}\;\;

S(S(0))+S(S(0))+0

\;\;{\stackrel {(1)}{\to }}\;\;

S(S(0))+S(S(0))

\;\;{\stackrel {\textrm {s.a.}}{\to }}\;\;

S(S(S(S(0)))),

حيث تتضمن الخطوة الأخيرة حساب المثال السابق.

اللغويات

في علم اللغة ، تُستخدم قواعد بنية العبارة ، والتي تُسمى أيضًا قواعد إعادة الصياغة ، في بعض أنظمة النحو التوليدي ، ^{[ 8 ]} كوسيلة لتوليد الجمل الصحيحة نحويًا في اللغة. وعادةً ما تأخذ هذه القاعدة الشكل التالي: ${\rm {A\rightarrow X}}$ حيث A هو تصنيف نحوي ، مثل عبارة اسمية أو جملة ، وX هو تسلسل من هذه التصنيفات أو المورفيمات ، مما يعبر عن حقيقة أنه يمكن استبدال A بـ X في تكوين البنية الأساسية للجملة. على سبيل المثال، القاعدة ${\rm {S\rightarrow NP\ VP}}$ يعني ذلك أن الجملة يمكن أن تتكون من عبارة اسمية (NP) متبوعة بعبارة فعلية (VP)؛ وستحدد القواعد الإضافية المكونات الفرعية التي يمكن أن تتكون منها العبارة الاسمية والعبارة الفعلية، وهكذا.

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

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

يمكن تعريف العديد من المفاهيم والرموز في الإطار العام لنظام ARS. ${\overset {*}{\rightarrow }}$ هو الإغلاق الانعكاسي المتعدي لـ $\rightarrow$ . $\leftrightarrow$ هو الإغلاق المتناظر لـ $\rightarrow$ . ${\overset {*}{\leftrightarrow }}$ هو الإغلاق الانعكاسي المتعدي المتناظر لـ $\rightarrow$ تتمثل المسألة اللفظية لنظام الاستجابة الآلية في تحديد ما إذا كان، بمعلومية x و y ، $x{\overset {*}{\leftrightarrow }}y$ يُطلق على الكائن x في المجموعة A اسم الكائن القابل للاختزال إذا وُجد كائن آخر y في المجموعة A بحيث $x\rightarrow y$ وإلا فإنه يُسمى غير قابل للاختزال أو شكلًا طبيعيًا . يُطلق على الكائن y اسم "شكل طبيعي لـ x " إذا $x{\stackrel {*}{\rightarrow }}y$ ويكون y غير قابل للاختزال. إذا كان الشكل الطبيعي لـ x فريدًا، فعادةً ما يُرمز إليه بـ $x{\downarrow }$ إذا كان لكل كائن شكل طبيعي واحد على الأقل، فإن نظام ARS يسمى بالتطبيع . $x\downarrow y$ أو يقال إن x و y قابلان للربط إذا وُجد عنصر z يتمتع بالخاصية التالية: $x{\overset {*}{\rightarrow }}z{\overset {*}{\leftarrow }}y$ يُقال إن شركة ARS تمتلك ملكية Church–Rosser إذا $x{\overset {*}{\leftrightarrow }}y$ يشير إلى $x\downarrow y$ تكون مجموعة ARS متقاربة إذا كان لكل w و x و y في A ، $x{\overset {*}{\leftarrow }}w{\overset {*}{\rightarrow }}y$ يشير إلى $x\downarrow y$ تكون مجموعة ARS متقاربة محليًا إذا وفقط إذا كان لكل w و x و y في A ، $x\leftarrow w\rightarrow y$ يشير إلى $x{\mathbin {\downarrow }}y$ يُقال إن نظام ARS منتهٍ أو نوثيري إذا لم تكن هناك سلسلة لانهائية $x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots$ . يُطلق على نظام ARS المتصل والمنتهي اسم النظام المتقارب أو النظام المتعارف عليه .

من أهم النظريات لأنظمة إعادة الكتابة المجردة أن نظام إعادة الكتابة المجردة يكون متقاربًا إذا وفقط إذا كان لديه خاصية Church-Rosser، ونظرية نيومان (نظام إعادة الكتابة المنتهي يكون متقاربًا إذا وفقط إذا كان متقاربًا محليًا)، وأن مشكلة الكلمات لنظام إعادة الكتابة المجردة غير قابلة للتقرير بشكل عام.

أنظمة إعادة كتابة السلاسل

يستغل نظام إعادة كتابة السلاسل ( SRS)، المعروف أيضًا باسم نظام شبه-ثو ، بنية المونويد الحرة للسلاسل (الكلمات) على الأبجدية لتوسيع علاقة إعادة الكتابة. $R$ ، إلى جميع السلاسل في الأبجدية التي تحتوي على الجانبين الأيسر والأيمن لبعض القواعد كسلاسل فرعية . رسميًا، نظام شبه ثيو هو مجموعة مرتبة $(\Sigma ,R)$ أين $\Sigma$ هي أبجدية (عادةً ما تكون محدودة)، و $R$ هي علاقة ثنائية بين بعض السلاسل (الثابتة) في الأبجدية، وتسمى مجموعة قواعد إعادة الكتابة . علاقة إعادة الكتابة بخطوة واحدة ${\underset {R}{\rightarrow }}$ ناتج عن $R$ على $\Sigma ^{*}$ يُعرَّف على النحو التالي: إذا $s,t\in \Sigma ^{*}$ أي سلاسل، إذن $s{\underset {R}{\rightarrow }}t$ إذا كان هناك $x,y,u,v\in \Sigma ^{*}$ بحيث $s=xuy$ ، $t=xvy$ ، و $uRv$ . منذ ${\underset {R}{\rightarrow }}$ هي علاقة على $\Sigma ^{*}$ الزوجان $(\Sigma ^{*},{\underset {R}{\rightarrow }})$ يتوافق مع تعريف نظام إعادة الكتابة المجرد. بما أن السلسلة الفارغة موجودة في $\Sigma ^{*}$ ، $R$ هي مجموعة فرعية من ${\underset {R}{\rightarrow }}$ إذا كانت العلاقة $R$ إذا كان النظام متناظرًا ، فإنه يُسمى نظام ثو .

في نظام SRS، علاقة التخفيض ${\overset {*}{\underset {R}{\rightarrow }}}$ متوافق مع عملية المونويد، مما يعني أن $x{\overset {*}{\underset {R}{\rightarrow }}}y$ يشير إلى $uxv{\overset {*}{\underset {R}{\rightarrow }}}uyv$ لجميع السلاسل $x,y,u,v\in \Sigma ^{*}$ وبالمثل، فإن الإغلاق الانعكاسي المتعدي المتناظر لـ ${\underset {R}{\rightarrow }}$ ، المشار إليه ${\overset {*}{\underset {R}{\leftrightarrow }}}$ ، هي علاقة تطابق ، أي أنها علاقة تكافؤ (بحكم التعريف)، وهي متوافقة أيضًا مع دمج السلاسل النصية. ${\overset {*}{\underset {R}{\leftrightarrow }}}$ يُطلق عليه اسم تطابق ثو الناتج عن $R$ في نظام الثلاثاء، أي إذا $R$ متناظرة، إعادة كتابة العلاقة ${\overset {*}{\underset {R}{\rightarrow }}}$ يتطابق مع تطابق ثو ${\overset {*}{\underset {R}{\leftrightarrow }}}$ .

يتطابق مفهوم نظام شبه-ثو بشكل أساسي مع عرض أحادي . بما أن ${\overset {*}{\underset {R}{\leftrightarrow }}}$ إذا كانت تطابقًا، فيمكننا تعريف أحادي العامل ${\mathcal {M}}_{R}=\Sigma ^{*}/{\overset {*}{\underset {R}{\leftrightarrow }}}$ من المونويد الحر $\Sigma ^{*}$ بحسب تطابق ثو. إذا كان أحاديًا ${\mathcal {M}}$ متماثل مع ${\mathcal {M}}_{R}$ ثم نظام شبه ثو $(\Sigma ,R)$ يُطلق عليه اسم عرض أحادي لـ ${\mathcal {M}}$ .

نحصل فوراً على بعض الروابط المفيدة جداً مع مجالات أخرى في الجبر. على سبيل المثال، الأبجدية $\{a,b\}$ مع القواعد $\{ab\rightarrow \varepsilon ,ba\rightarrow \varepsilon \}$ ، أين $\varepsilon$ السلسلة الفارغة هي تمثيل للمجموعة الحرة على مولد واحد. أما إذا كانت القواعد هي فقط $\{ab\rightarrow \varepsilon \}$ ثم نحصل على تمثيل للمونويد ثنائي الدورة . وهكذا، تُشكل أنظمة شبه ثو إطارًا طبيعيًا لحل مسألة الكلمات للمونويدات والمجموعات. في الواقع، لكل مونويد تمثيل على الصورة التالية: $(\Sigma ,R)$ ، أي أنه يمكن دائمًا تقديمه بواسطة نظام شبه ثو، وربما على أبجدية لا نهائية.

إن مسألة الكلمات لنظام شبه ثو غير قابلة للتقرير بشكل عام؛ وتُعرف هذه النتيجة أحيانًا باسم نظرية ما بعد ماركوف . ^{[ 12 ]}

أنظمة إعادة كتابة المصطلحات

{\displaystyle l\longrightarrow r} — **الشكل 1:** رسم تخطيطي مثلثي لتطبيق قاعدة إعادة الكتابة $l\longrightarrow r$ في هذا المنصب $p$ في مصطلح، مع استبدال مطابق $\sigma$

{\displaystyle x*(y*z)} — **الصورة 2:** قاعدة الطرف الأيسر $x*(y*z)$ المطابقة في المصطلح ${\frac {a*((a+1)*(a+2))}{1*(2*3)}}$

نظام إعادة كتابة المصطلحات ( TRS ) هو نظام إعادة كتابة تكون عناصره مصطلحات ، وهي عبارة عن تعابير تتضمن تعابير فرعية متداخلة. على سبيل المثال، النظام الموضح في قسم المنطق أعلاه هو نظام إعادة كتابة مصطلحات. تتكون المصطلحات في هذا النظام من عوامل تشغيل ثنائية. $(\vee )$ و $(\wedge )$ والمُعامل الأحادي $(\neg )$ كما توجد في القواعد متغيرات، والتي تمثل أي مصطلح ممكن (على الرغم من أن المتغير الواحد يمثل دائمًا نفس المصطلح في جميع أنحاء القاعدة الواحدة).

على عكس أنظمة إعادة كتابة السلاسل النصية، التي تتكون عناصرها من تسلسلات من الرموز، فإن عناصر نظام إعادة كتابة المصطلحات تُشكل جبرًا للمصطلحات . يمكن تصور المصطلح كشجرة من الرموز، حيث تُحدد مجموعة الرموز المسموح بها بتوقيع مُعطى . من الناحية الشكلية، تتمتع أنظمة إعادة كتابة المصطلحات بكامل قدرات آلات تورينج ، أي أنه يمكن تعريف أي دالة قابلة للحساب بواسطة نظام إعادة كتابة المصطلحات. ^{[ 13 ]}

تعتمد بعض لغات البرمجة على إعادة كتابة المصطلحات. ومن الأمثلة على ذلك لغة Pure، وهي لغة برمجة وظيفية للتطبيقات الرياضية. ^{[ 14 ]}^{[ 15 ]}

التعريف الرسمي

قاعدة إعادة الكتابة هي زوج من المصطلحات ، تُكتب عادةً على النحو التالي: $l\rightarrow r$ للإشارة إلى إمكانية استبدال الطرف الأيسر $l$ بالطرف الأيمن $r$ . نظام إعادة كتابة المصطلحات هو مجموعة $R$ من هذه القواعد. قاعدة $l\rightarrow r$ يمكن تطبيق ذلك على الحد $s$ إذا كان الحد الأيسر $l$ يطابق حدًا فرعيًا من $s$ ، أي إذا كان هناك استبدال ما $\sigma$ بحيث يكون الحد الفرعي لـ $s$ إن الجذر عند موضع ما $p$ هو نتيجة تطبيق الاستبدال $\sigma$ إلى الحد $l$ . يُطلق على الحد الفرعي المطابق للجانب الأيسر من القاعدة اسم التعبير المختزل أو التعبير القابل للاختزال . ^{[ 16 ]} يكون الحد الناتج $t$ لتطبيق هذه القاعدة هو نتيجة استبدال الحد الفرعي في الموضع $p$ في $s$ بالحد $r$ مع الاستبدال $\sigma$ تم تطبيق ذلك، انظر الصورة رقم 1. في هذه الحالة، $s$ يقال إنه أعيد كتابته في خطوة واحدة ، أو أعيد كتابته مباشرة ، إلى $t$ بواسطة النظام $R$ ، ويشار إليه رسميًا باسم $s\rightarrow _{R}t$ ، $s{\underset {R}{\rightarrow }}t$ أو كما $s{\overset {R}{\rightarrow }}t$ من قبل بعض المؤلفين.

إذا كان المصطلح $t_{1}$ يمكن إعادة كتابتها في عدة خطوات إلى مصطلح $t_{n}$ أي إذا $t_{1}{\underset {R}{\rightarrow }}t_{2}{\underset {R}{\rightarrow }}\cdots {\underset {R}{\rightarrow }}t_{n}$ ، على المدى $t_{1}$ يقال إنه أعيدت كتابته إلى $t_{n}$ ، ويشار إليه رسميًا باسم $t_{1}{\overset {+}{\underset {R}{\rightarrow }}}t_{n}$ بمعنى آخر، العلاقة ${\overset {+}{\underset {R}{\rightarrow }}}$ هو الإغلاق المتعدي للعلاقة ${\underset {R}{\rightarrow }}$ ؛ وغالبًا ما يكون التدوين أيضًا ${\overset {*}{\underset {R}{\rightarrow }}}$ يُستخدم للدلالة على الإغلاق الانعكاسي المتعدي لـ ${\underset {R}{\rightarrow }}$ ، إنه، $s{\overset {*}{\underset {R}{\rightarrow }}}t$ لو $s=t$ أو $s{\overset {+}{\underset {R}{\rightarrow }}}t$ [ ¹⁷^{] إعادة}^كتابة المصطلح بواسطة مجموعة $R$ يمكن اعتبار مجموعة القواعد نظام إعادة كتابة مجرد كما هو موضح أعلاه ، مع اعتبار المصطلحات كائناتها و ${\underset {R}{\rightarrow }}$ كعلاقة إعادة كتابة لها.

على سبيل المثال، $x*(y*z)\rightarrow (x*y)*z$ هي قاعدة إعادة كتابة، تُستخدم عادةً لإنشاء شكل طبيعي فيما يتعلق بخاصية التجميع لـ $*$ يمكن تطبيق هذه القاعدة على البسط في الحد ${\frac {a*((a+1)*(a+2))}{1*(2*3)}}$ مع الاستبدال المطابق $\{x\mapsto a,\;y\mapsto a+1,\;z\mapsto a+2\}$ انظر الصورة 2. ^{[ ملاحظة 2 ]} بتطبيق هذا الاستبدال على الجانب الأيمن من القاعدة، نحصل على المصطلح $(a*(a+1))*(a+2)$ وباستبدال البسط بهذا الحد ينتج ${\frac {(a*(a+1))*(a+2)}{1*(2*3)}}$ وهو الحد الناتج عن تطبيق قاعدة إعادة الكتابة. وبشكل عام، فإن تطبيق قاعدة إعادة الكتابة قد حقق ما يسمى "تطبيق قانون التجميع لـ $*$ ل ${\frac {a*((a+1)*(a+2))}{1*(2*3)}}$ في الجبر الابتدائي. أو بدلاً من ذلك، كان من الممكن تطبيق القاعدة على مقام الحد الأصلي، مما ينتج عنه ${\frac {a*((a+1)*(a+2))}{(1*2)*3}}$ .

إنهاء الخدمة

تُعالج مشكلات إنهاء أنظمة إعادة الكتابة بشكل عام في قسم " نظام إعادة الكتابة المجرد#الإنهاء والتقارب" . أما بالنسبة لأنظمة إعادة كتابة المصطلحات على وجه الخصوص، فينبغي مراعاة التفاصيل الدقيقة الإضافية التالية.

يُعدّ إنهاء حتى نظام يتكون من قاعدة واحدة ذات جانب أيسر خطي مسألة غير قابلة للتقرير. ^{[ 18 ]}^{[ 19 ]} كما أن إنهاء الأنظمة التي تستخدم رموز الدوال الأحادية فقط غير قابل للتقرير؛ ومع ذلك، فهو قابل للتقرير بالنسبة للأنظمة ذات الأساس المحدود . ^{[ 20 ]}

نظام إعادة كتابة المصطلح التالي هو نظام تطبيع، ^{[ ملاحظة 3 ]} ولكنه ليس نظام إنهاء، ^{[ ملاحظة 4 ]} وليس نظامًا متقاربًا: ^{[ 21 ]} ${\begin{aligned}f(x,x)&\rightarrow g(x),\\f(x,g(x))&\rightarrow b,\\h(c,x)&\rightarrow f(h(x,c),h(x,x)).\\\end{aligned}}$

المثالان التاليان لأنظمة إعادة كتابة المصطلحات المنتهية يعودان إلى توياما: ^{[ 22 ]}

f(0,1,x)\rightarrow f(x,x,x)

و

g(x,y)\rightarrow x,

g(x,y)\rightarrow y.

اتحادهم نظام غير قابل للإنهاء، لأن

${\begin{aligned}&f(g(0,1),g(0,1),g(0,1))\\\rightarrow &f(0,g(0,1),g(0,1))\\\rightarrow &f(0,1,g(0,1))\\\rightarrow &f(g(0,1),g(0,1),g(0,1))\\\rightarrow &\cdots \end{aligned}}$ تُفنّد هذه النتيجة تخمين ديرشوفيتز [ ²³^{] الذي}^ادعى أن اتحاد نظامي إعادة كتابة المصطلحات المنتهية $R_{1}$ و $R_{2}$ سينتهي الأمر مرة أخرى إذا كانت جميع الجوانب اليسرى من $R_{1}$ والجانب الأيمن من $R_{2}$ هي خطية ، ولا توجد " تداخلات " بين الجوانب اليسرى من $R_{1}$ والجانب الأيمن من $R_{2}$ جميع هذه الخصائص تتحقق من خلال أمثلة توياما.

انظر ترتيب إعادة الكتابة وترتيب المسار (إعادة كتابة المصطلح) لعلاقات الترتيب المستخدمة في إثباتات الإنهاء لأنظمة إعادة كتابة المصطلح.

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

تُعدّ أنظمة إعادة الكتابة من الرتبة العليا تعميمًا لأنظمة إعادة كتابة الحدود من الرتبة الأولى لتشمل حدود لامدا ، مما يسمح باستخدام دوال ومتغيرات مقيدة من رتبة أعلى. ^{[ 24 ]} ويمكن إعادة صياغة العديد من النتائج المتعلقة بأنظمة إعادة كتابة الحدود من الرتبة الأولى لتشمل أنظمة إعادة الكتابة من الرتبة العليا أيضًا. ^{[ 25 ]}

أنظمة إعادة كتابة الرسوم البيانية

تُعد أنظمة إعادة كتابة الرسوم البيانية تعميمًا آخر لأنظمة إعادة كتابة المصطلحات، حيث تعمل على الرسوم البيانية بدلاً من المصطلحات ( الأساسية ) / تمثيلها الشجري المقابل .

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

توفر نظرية التتبع وسيلة لمناقشة المعالجة المتعددة بمصطلحات أكثر رسمية، مثل استخدام أحادي التتبع وأحادي التاريخ . ويمكن إجراء إعادة الكتابة في أنظمة التتبع أيضًا.

انظر أيضاً

الزوج الحرج (المنطقي)
المترجم
خوارزمية إكمال كنوت-بنديكس
تحدد أنظمة L عملية إعادة الكتابة التي تتم بالتوازي.
الشفافية المرجعية في علوم الحاسوب
إعادة الكتابة المنظمة
شبكات التفاعل

ملحوظات

↑ هذا الشكل من القاعدة السابقة ضروري لأن قانون التبديل A ∨ B = B ∨ A لا يمكن تحويله إلى قاعدة إعادة كتابة. قاعدة مثل A ∨ B → B ∨ A ستجعل نظام إعادة الكتابة غير منتهٍ.
↑ منذ تطبيق هذا الاستبدال على الجانب الأيسر من القاعدة $x*(y*z)$ ينتج عنه البسط $a*((a+1)*(a+2))$
↑ أي أنه لكل حد، يوجد شكل طبيعي ما، على سبيل المثال، h ( c , c ) له الشكلان الطبيعيان b و g ( b )، حيث أن h ( c , c ) → f ( h ( c , c ), h ( c , c )) → f ( h ( c , c ), f ( h ( c , c ), h ( c , c ))) → f ( h ( c , c ), g ( h ( c , c ))) → b ، و h ( c , c ) → f ( h ( c , c ), h ( c , c )) → g ( h ( c , c )) → ... → g ( b )؛ لا يمكن إعادة كتابة b ولا g ( b ) أكثر من ذلك، وبالتالي فإن النظام غير متقارب.
↑ أي أن هناك اشتقاقات لا نهائية، على سبيل المثال: h ( c , c ) → f ( h ( c , c ), h ( c , c )) → f ( f ( h ( c , c ), h ( c , c ))), h ( c , c )) → f ( f ( f ( h ( c , c ), h ( c , c ))), h ( c , c )), h ( c , c )) → ...

للمزيد من القراءة

بادر، فرانز ؛ نيبكو، توبياس (1999). إعادة صياغة المصطلحات وما إلى ذلك . مطبعة جامعة كامبريدج. ISBN 978-0-521-77920-3.316 صفحة.
مارك بيزيم ، جان ويليم كلوب ، رويل دي فريجر ("تيريز")، أنظمة إعادة كتابة المصطلح ("TeReSe")، مطبعة جامعة كامبريدج، 2003، ISBN 0-521-39115-6هذه أحدث دراسة شاملة في هذا المجال. ومع ذلك، فهي تستخدم قدراً لا بأس به من الرموز والتعريفات غير القياسية بعد. على سبيل المثال، تُعرَّف خاصية تشيرش-روسر بأنها مطابقة لخاصية الالتقاء.
ناحوم ديرشوفيتز وجان بيير جوانو، "أنظمة إعادة الكتابة" ، الفصل 6 في كتاب جان فان ليوين (محرر)، دليل علوم الحاسوب النظرية ، المجلد ب: النماذج الرسمية والدلالات ، دار النشر إلسيفير ومعهد ماساتشوستس للتكنولوجيا، 1990، رقم ISBN 0-444-88074-7، الصفحات 243 – 320. النسخة الأولية من هذا الفصل متاحة مجاناً من المؤلفين، ولكنها تفتقر إلى الأشكال.
ناحوم ديرشوفيتز وديفيد بلايستيد . "إعادة الكتابة" ، الفصل 9 في جون آلان روبنسون وأندريه فورونكوف (محرران)، دليل الاستدلال الآلي ، المجلد 1 .
جيرار هيوت وديريك أوبن، المعادلات وقواعد إعادة الكتابة، دراسة استقصائية (1980) مجموعة التحقق بجامعة ستانفورد، التقرير رقم 15 تقرير قسم علوم الكمبيوتر رقم STAN-CS-80-785
جان ويليم كلوب . "أنظمة إعادة كتابة المصطلحات"، الفصل 1 في سامسون أبرامسكي ، دوف إم. غاباي وتوم مايباوم (محررون)، دليل المنطق في علوم الحاسوب ، المجلد 2: الخلفية: الهياكل الحسابية .
ديفيد بلايستيد. "الاستدلال المعادلاتي وأنظمة إعادة كتابة المصطلحات" ، في دوف إم. غاباي ، سي جيه هوغر وجون آلان روبنسون (محررون)، دليل المنطق في الذكاء الاصطناعي وبرمجة المنطق ، المجلد 1 .
يورغن أفينهاوس وكلاوس مادلينر. "إعادة صياغة المصطلحات والاستدلال المعادلاتي". في رانان ب. بانيرجي (محرر)، التقنيات الرسمية في الذكاء الاصطناعي: كتاب مرجعي ، إلسيفير (1990).

إعادة كتابة السلاسل

رونالد ف. بوك وفريدريش أوتو، أنظمة إعادة كتابة السلاسل ، سبرينغر (1993).
بنيامين بنينغهوفن، سوزان كيمريش ومايكل إم ريختر ، أنظمة التخفيضات . LNCS 277 ، سبرينغر-فيرلاغ (1987).

آخر

مارتن ديفيس ، رون سيغال ، إيلين ج. ويوكر ، (1994) الحوسبة، والتعقيد، واللغات: أساسيات علوم الحاسوب النظرية - الطبعة الثانية ، دار النشر الأكاديمية، رقم ISBN 0-12-206382-1.

روابط خارجية

الصفحة الرئيسية لإعادة الكتابة
مجموعة العمل 1.6 التابعة للاتحاد الدولي لمعالجة المعلومات
باحثون في مجال إعادة الصياغة بقلم آرت ميدلدورب ، جامعة إنسبروك
بوابة الإنهاء
نظام مود - تطبيق برمجي لنظام إعادة كتابة المصطلحات العامة. ^{[ 5 ]}

مراجع

↑ جوزيف جوجين "الإثبات وإعادة الكتابة" المؤتمر الدولي للبرمجة الجبرية والمنطقية، 1990 نانسي، فرنسا، الصفحات 1-24
↑ سكولثورب، نيل؛ فريسبي، نيكولاس؛ جيل، آندي (2014). "محرك إعادة كتابة جامعة كانساس" (ملف PDF) . مجلة البرمجة الوظيفية . 24 (4): 434-473 . doi : 10.1017/S0956796814000185 . ISSN 0956-7968 . S2CID 16807490. مؤرشف (ملف PDF) من الأصل بتاريخ 22-09-2017 . تم الاطلاع عليه بتاريخ 12-02-2019 .
↑ هسيانغ، جيه؛ كيرشنر، هيلين؛ ليسكان، بيير؛ روسينوفيتش، مايكل (1992). "نهج إعادة كتابة المصطلحات لإثبات النظريات آليًا" . مجلة البرمجة المنطقية . 14 ( 1-2 ): 71-99 . doi : 10.1016/0743-1066(92)90047-7 .
↑ فروويرث، ثوم (1998). "نظرية وممارسة قواعد معالجة القيود" . مجلة البرمجة المنطقية . 37 ( 1-3 ): 95-138 . doi : 10.1016/S0743-1066(98)10005-5 .
1 2 كلافيل، م.؛ دوران، ف.؛ إيكر، س.؛ لينكولن، ب.؛ مارتي-أوليت، ن.؛ ميسيغوير، ج.؛ كيسادا، ج.ف. (2002). "مود: المواصفات والبرمجة في منطق إعادة الكتابة" . علوم الحاسوب النظرية . 285 (2): 187-243 . doi : 10.1016/S0304-3975(01)00359-0 .
↑ كيم ماريوت؛ بيتر ج. ستوكي (1998). البرمجة مع القيود: مقدمة . مطبعة معهد ماساتشوستس للتكنولوجيا. ص 436 وما بعدها. ISBN 978-0-262-13341-8.
↑ يورغن أفينهاوس؛ كلاوس مادلينر (1990). "إعادة صياغة المصطلحات والاستدلال المعادلاتي". في آر بي بانيرجي (محرر). التقنيات الرسمية في الذكاء الاصطناعي . كتاب مرجعي. إلسيفير. ص 1-43 . هنا: مثال في القسم 4.1، صفحة 24.
^ روبرت فريدين (1992). أسس بناء الجملة التوليدي . مطبعة معهد ماساتشوستس للتكنولوجيا. رقم ISBN 978-0-262-06144-5.
1 2 بوك وأوتو، ص 10
↑ بيزيم وآخرون، ص 7،
↑ بيزيم وآخرون، ص 7
^ مارتن ديفيس وآخرون. 1994، ص. 178
^ ديرشوفيتز ، جوانود (1990)، القسم 1، ص 245
↑ ألبرت، غراف (2009). "معالجة الإشارات في لغة البرمجة البحتة" . مؤتمر لينكس الصوتي .
^ ريبي ، فون مايكل (18 نوفمبر 2009). "Pure – eine einfache funktionale Sprache" . مؤرشفة من الأصلي في 19 آذار (مارس) 2011.
↑ كلوب، ج. و. "أنظمة إعادة كتابة المصطلحات" (ملف PDF) . أوراق بحثية لناحوم ديرشوفيتز وطلابه . جامعة تل أبيب. ص 12. مؤرشف (ملف PDF) من الأصل بتاريخ 15 أغسطس 2021. تم الاطلاع عليه بتاريخ 14 أغسطس 2021 .
↑ ن. ديرشوفيتز، ج.-ب. جوانو (1990). جان فان ليوين (محرر). أنظمة إعادة الكتابة . دليل علوم الحاسوب النظرية. المجلد ب. إلسيفير. الصفحات 243-320 . هنا: القسم 2.3
↑ ماكس دوشيه (1989). "محاكاة آلات تورينج باستخدام قاعدة إعادة كتابة خطية يسارية". وقائع المؤتمر الدولي الثالث حول تقنيات إعادة الكتابة وتطبيقاتها . سلسلة محاضرات في علوم الحاسوب. المجلد 355. سبرينغر. الصفحات 109-120 .
↑ ماكس دوشيه (سبتمبر 1992). "محاكاة آلات تورينج بواسطة قاعدة إعادة كتابة منتظمة" . علوم الحاسوب النظرية . 103 (2): 409-420 . doi : 10.1016/0304-3975(92)90022-8 .
↑ جيرارد هويه، دي إس لانكفورد (مارس 1978). حول مشكلة التوقف الموحد لأنظمة إعادة كتابة المصطلحات (ملف PDF) (تقرير فني). IRIA. ص 8. 283. تاريخ الاطلاع: 16 يونيو 2013 .
↑ برنارد غرامليش (يونيو 1993). "ربط الإنهاء الداخلي والضعيف والموحد والنمطي لأنظمة إعادة كتابة المصطلحات" . في: فورونكوف، أندريه (محرر). وقائع المؤتمر الدولي حول البرمجة المنطقية والاستدلال الآلي (LPAR) . سلسلة محاضرات في الذكاء الاصطناعي. المجلد 624. سبرينغر. الصفحات 285-296 . مؤرشف من الأصل في 4 مارس 2016. تم الاطلاع عليه في 19 يونيو 2014 . هنا: المثال 3.3
↑ يوشيهيتو توياما (1987). "أمثلة مضادة لإنهاء المجموع المباشر لأنظمة إعادة كتابة المصطلحات" (ملف PDF) . رسائل معالجة المعلومات 25 ( 3): 141-143 . doi : 10.1016/0020-0190(87)90122-0 . hdl : 2433/99946 . مؤرشف (PDF) من الأصل بتاريخ 13 نوفمبر 2019. تم الاطلاع عليه بتاريخ 13 نوفمبر 2019 .
↑ ن. ديرشوفيتز (1985). "الإنهاء" (ملف PDF) . في جان بيير جوانو (محرر). وقائع RTA . سلسلة محاضرات علوم الحاسوب. المجلد 220. سبرينغر. الصفحات 180-224 . مؤرشف (ملف PDF) من الأصل بتاريخ 12 نوفمبر 2013. تم الاطلاع عليه بتاريخ 16 يونيو 2013 . هنا: ص 210
↑ وولفرام، د. أ. (1993). نظرية الجمل في الأنماط . مطبعة جامعة كامبريدج. ص 47-50 . doi : 10.1017/CBO9780511569906 . ISBN 9780521395380. S2CID 42331173 .
↑ نيبكو، توبياس؛ بريهوفر، كريستيان (1998). "إعادة الصياغة من الرتبة العليا والاستدلال المعادلاتي" . في: بيبل، دبليو؛ شميت، بي (محرران). الاستدلال الآلي - أساس للتطبيقات. المجلد الأول: الأسس . كلوير. الصفحات 399-430 . مؤرشف من الأصل بتاريخ 16 أغسطس 2021. تم الاطلاع عليه بتاريخ 16 أغسطس 2021 .

[7] هذا الشكل من القاعدة السابقة ضروري لأن قانون التبديل A ∨ B = B ∨ A لا يمكن تحويله إلى قاعدة إعادة كتابة. قاعدة مثل A ∨ B → B ∨ A ستجعل نظام إعادة الكتابة غير منتهٍ.

[19] منذ تطبيق هذا الاستبدال على الجانب الأيسر من القاعدة $x*(y*z)$ ينتج عنه البسط $a*((a+1)*(a+2))$

[23] أي أنه لكل حد، يوجد شكل طبيعي ما، على سبيل المثال، h ( c , c ) له الشكلان الطبيعيان b و g ( b )، حيث أن h ( c , c ) → f ( h ( c , c ), h ( c , c )) → f ( h ( c , c ), f ( h ( c , c ), h ( c , c ))) → f ( h ( c , c ), g ( h ( c , c ))) → b ، و h ( c , c ) → f ( h ( c , c ), h ( c , c )) → g ( h ( c , c )) → ... → g ( b )؛ لا يمكن إعادة كتابة b ولا g ( b ) أكثر من ذلك، وبالتالي فإن النظام غير متقارب.

[24] أي أن هناك اشتقاقات لا نهائية، على سبيل المثال: h ( c , c ) → f ( h ( c , c ), h ( c , c )) → f ( f ( h ( c , c ), h ( c , c ))), h ( c , c )) → f ( f ( f ( h ( c , c ), h ( c , c ))), h ( c , c )), h ( c , c )) → ...

[1] جوزيف جوجين "الإثبات وإعادة الكتابة" المؤتمر الدولي للبرمجة الجبرية والمنطقية، 1990 نانسي، فرنسا، الصفحات 1-24

[SculthorpeFrisby2014-2] سكولثورب، نيل؛ فريسبي، نيكولاس؛ جيل، آندي (2014). "محرك إعادة كتابة جامعة كانساس" (ملف PDF) . مجلة البرمجة الوظيفية . 24 (4): 434-473 . doi : 10.1017/S0956796814000185 . ISSN 0956-7968 . S2CID 16807490. مؤرشف (ملف PDF) من الأصل بتاريخ 22-09-2017 . تم الاطلاع عليه بتاريخ 12-02-2019 .

[3] هسيانغ، جيه؛ كيرشنر، هيلين؛ ليسكان، بيير؛ روسينوفيتش، مايكل (1992). "نهج إعادة كتابة المصطلحات لإثبات النظريات آليًا" . مجلة البرمجة المنطقية . 14 ( 1-2 ): 71-99 . doi : 10.1016/0743-1066(92)90047-7 .

[4] فروويرث، ثوم (1998). "نظرية وممارسة قواعد معالجة القيود" . مجلة البرمجة المنطقية . 37 ( 1-3 ): 95-138 . doi : 10.1016/S0743-1066(98)10005-5 .

[Clavel.Duran.Eker.2002-5] 1 2 كلافيل، م.؛ دوران، ف.؛ إيكر، س.؛ لينكولن، ب.؛ مارتي-أوليت، ن.؛ ميسيغوير، ج.؛ كيسادا، ج.ف. (2002). "مود: المواصفات والبرمجة في منطق إعادة الكتابة" . علوم الحاسوب النظرية . 285 (2): 187-243 . doi : 10.1016/S0304-3975(01)00359-0 .

[MarriottStuckey1998-6] كيم ماريوت؛ بيتر ج. ستوكي (1998). البرمجة مع القيود: مقدمة . مطبعة معهد ماساتشوستس للتكنولوجيا. ص 436 وما بعدها. ISBN 978-0-262-13341-8.

[8] يورغن أفينهاوس؛ كلاوس مادلينر (1990). "إعادة صياغة المصطلحات والاستدلال المعادلاتي". في آر بي بانيرجي (محرر). التقنيات الرسمية في الذكاء الاصطناعي . كتاب مرجعي. إلسيفير. ص 1-43 . هنا: مثال في القسم 4.1، صفحة 24.

[Freidin1992-9] روبرت فريدين (1992). أسس بناء الجملة التوليدي . مطبعة معهد ماساتشوستس للتكنولوجيا. رقم ISBN 978-0-262-06144-5.

[Book_and_Otto,_p._10-10] 1 2 بوك وأوتو، ص 10

[11] بيزيم وآخرون، ص 7،

[12] بيزيم وآخرون، ص 7

[13] مارتن ديفيس وآخرون. 1994، ص. 178

[14] ديرشوفيتز ، جوانود (1990)، القسم 1، ص 245

[15] ألبرت، غراف (2009). "معالجة الإشارات في لغة البرمجة البحتة" . مؤتمر لينكس الصوتي .

[16] ريبي ، فون مايكل (18 نوفمبر 2009). "Pure – eine einfache funktionale Sprache" . مؤرشفة من الأصلي في 19 آذار (مارس) 2011.

[Klop-17] كلوب، ج. و. "أنظمة إعادة كتابة المصطلحات" (ملف PDF) . أوراق بحثية لناحوم ديرشوفيتز وطلابه . جامعة تل أبيب. ص 12. مؤرشف (ملف PDF) من الأصل بتاريخ 15 أغسطس 2021. تم الاطلاع عليه بتاريخ 14 أغسطس 2021 .

[18] ن. ديرشوفيتز، ج.-ب. جوانو (1990). جان فان ليوين (محرر). أنظمة إعادة الكتابة . دليل علوم الحاسوب النظرية. المجلد ب. إلسيفير. الصفحات 243-320 . هنا: القسم 2.3

[20] ماكس دوشيه (1989). "محاكاة آلات تورينج باستخدام قاعدة إعادة كتابة خطية يسارية". وقائع المؤتمر الدولي الثالث حول تقنيات إعادة الكتابة وتطبيقاتها . سلسلة محاضرات في علوم الحاسوب. المجلد 355. سبرينغر. الصفحات 109-120 .

[21] ماكس دوشيه (سبتمبر 1992). "محاكاة آلات تورينج بواسطة قاعدة إعادة كتابة منتظمة" . علوم الحاسوب النظرية . 103 (2): 409-420 . doi : 10.1016/0304-3975(92)90022-8 .

[22] جيرارد هويه، دي إس لانكفورد (مارس 1978). حول مشكلة التوقف الموحد لأنظمة إعادة كتابة المصطلحات (ملف PDF) (تقرير فني). IRIA. ص 8. 283. تاريخ الاطلاع: 16 يونيو 2013 .

[25] برنارد غرامليش (يونيو 1993). "ربط الإنهاء الداخلي والضعيف والموحد والنمطي لأنظمة إعادة كتابة المصطلحات" . في: فورونكوف، أندريه (محرر). وقائع المؤتمر الدولي حول البرمجة المنطقية والاستدلال الآلي (LPAR) . سلسلة محاضرات في الذكاء الاصطناعي. المجلد 624. سبرينغر. الصفحات 285-296 . مؤرشف من الأصل في 4 مارس 2016. تم الاطلاع عليه في 19 يونيو 2014 . هنا: المثال 3.3

[26] يوشيهيتو توياما (1987). "أمثلة مضادة لإنهاء المجموع المباشر لأنظمة إعادة كتابة المصطلحات" (ملف PDF) . رسائل معالجة المعلومات 25 ( 3): 141-143 . doi : 10.1016/0020-0190(87)90122-0 . hdl : 2433/99946 . مؤرشف (PDF) من الأصل بتاريخ 13 نوفمبر 2019. تم الاطلاع عليه بتاريخ 13 نوفمبر 2019 .

[27] ن. ديرشوفيتز (1985). "الإنهاء" (ملف PDF) . في جان بيير جوانو (محرر). وقائع RTA . سلسلة محاضرات علوم الحاسوب. المجلد 220. سبرينغر. الصفحات 180-224 . مؤرشف (ملف PDF) من الأصل بتاريخ 12 نوفمبر 2013. تم الاطلاع عليه بتاريخ 16 يونيو 2013 . هنا: ص 210

[Wolfram-28] وولفرام، د. أ. (1993). نظرية الجمل في الأنماط . مطبعة جامعة كامبريدج. ص 47-50 . doi : 10.1017/CBO9780511569906 . ISBN 9780521395380. S2CID 42331173 .

[29] نيبكو، توبياس؛ بريهوفر، كريستيان (1998). "إعادة الصياغة من الرتبة العليا والاستدلال المعادلاتي" . في: بيبل، دبليو؛ شميت، بي (محرران). الاستدلال الآلي - أساس للتطبيقات. المجلد الأول: الأسس . كلوير. الصفحات 399-430 . مؤرشف من الأصل بتاريخ 16 أغسطس 2021. تم الاطلاع عليه بتاريخ 16 أغسطس 2021 .

،

الاختزال

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ ملاحظة 1 ]

[

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[ 13 ]

[ 14 ]

[ 15 ]

[ 16 ]

17

[ ملاحظة 2 ]

[ 18 ]

[ 19 ]

[ 20 ]

[ ملاحظة 3 ]

[ ملاحظة 4 ]

[ 21 ]

[ 22 ]

23

[ 24 ]

[ 25 ]

اللغة	العربية (RTL)
روابط موسوعية	30 رابطاً
المصدر الأصلي	ويكيبيديا ↗