التقاء (إعادة كتابة مجردة)

في علوم الحاسوب والرياضيات، يُعدّ التقارب خاصيةً لأنظمة إعادة الكتابة ، إذ يصف المصطلحات التي يمكن إعادة كتابتها بأكثر من طريقة للحصول على النتيجة نفسها. تتناول هذه المقالة خصائص نظام إعادة الكتابة المجرد في أكثر حالاته تجريدًا .

تُشكّل القواعد المعتادة للحساب الابتدائي نظام إعادة كتابة مجرد. على سبيل المثال، يمكن حساب قيمة التعبير (11 + 9) × (2 + 4) بدءًا من القوس الأيسر أو الأيمن؛ ومع ذلك، في كلتا الحالتين نحصل على النتيجة نفسها في النهاية. إذا كانت كل عبارة حسابية تُعطي النتيجة نفسها بغض النظر عن استراتيجية الاختزال، يُقال إن نظام إعادة الكتابة الحسابي متقارب من الأساس. قد تكون أنظمة إعادة الكتابة الحسابية متقاربة أو متقاربة من الأساس فقط، وذلك اعتمادًا على تفاصيل نظام إعادة الكتابة. ^{[ 1 ]}

ويمكن الحصول على مثال ثانٍ أكثر تجريدًا من البرهان التالي على أن كل عنصر من عناصر المجموعة يساوي معكوس معكوسه: ^{[ 2 ]}

This proof starts from the given group axioms A1–A3, and establishes five propositions R4, R6, R10, R11, and R12, each of them using some earlier ones, and R12 being the main theorem. Some of the proofs require non-obvious, or even creative, steps, like applying axiom A2 in reverse, thereby rewriting "1" to "a⁻¹ ⋅ a" in the first step of R6's proof. One of the historical motivations to develop the theory of term rewriting was to avoid the need for such steps, which are difficult to find by an inexperienced human, let alone by a computer program .

If a term rewriting system is confluent and terminating, a straightforward method exists to prove equality between two expressions (also known as terms) s and t: Starting with s, apply equalities^{[note 1]} from left to right as long as possible, eventually obtaining a term s′. Obtain from t a term t′ in a similar way. If both terms s′ and t′ literally agree, then s and t are proven equal. More importantly, if they disagree, then s and t cannot be equal. That is, any two terms s and t that can be proven equal at all can be done so by that method.

The success of that method does not depend on a certain sophisticated order in which to apply rewrite rules, as confluence ensures that any sequence of rule applications will eventually lead to the same result (while the termination property ensures that any sequence will eventually reach an end at all). Therefore, if a confluent and terminating term rewriting system can be provided for some equational theory,^{[note 2]} not a tinge of creativity is required to perform proofs of term equality; that task hence becomes amenable to computer programs. Modern approaches handle more general abstract rewriting systems rather than term rewriting systems; the latter are a special case of the former.

يمكن التعبير عن نظام إعادة الكتابة كرسم بياني موجه ، حيث تمثل العقد التعبيرات وتمثل الحواف عمليات إعادة الكتابة. على سبيل المثال، إذا أمكن إعادة كتابة التعبير a إلى b ، فإننا نقول إن b هو اختزال لـ a (أو أن a يختزل إلى b ، أو أن a هو توسيع لـ b ). يُعبَّر عن ذلك باستخدام رمز السهم؛ يشير a → b إلى أن a يختزل إلى b . وبشكل بديهي، هذا يعني أن الرسم البياني المقابل يحتوي على حافة موجهة من a إلى b .

إذا وُجد مسار بين عقدتين في الرسم البياني c و d ، فإنه يُشكّل متتالية اختزال . على سبيل المثال، إذا كان c → c′ → c′′ → ... → d′ → d ، فيمكننا كتابة c ∗ → d ، مما يدل على وجود متتالية اختزال من c إلى d . رسميًا، ∗ → هو الإغلاق الانعكاسي المتعدي لـ →. باستخدام المثال من الفقرة السابقة، لدينا (11+9)×(2+4) → 20×(2+4) و 20×(2+4) → 20×6، لذا (11+9)×(2+4) ∗ → 20×6.

بناءً على ذلك، يمكن تعريف الالتقاء على النحو التالي: يُعتبر a ∈ S متقاربًا إذا كان لكل زوج b ، c ∈ S بحيث يكون a ∗ → b و a ∗ → c ، يوجد a d ∈ S بحيث يكون b ∗ → d و c ∗ → d (يُشار إليه بـ${\displaystyle b\mathbin {\downarrow } c}$إذا كان كل عنصر a ∈ S متقاربًا، نقول إن → متقارب. تُسمى هذه الخاصية أحيانًا خاصية المعين ، نسبةً إلى شكل الرسم البياني الموضح على اليمين. يخصص بعض المؤلفين مصطلح خاصية المعين لنوع من الرسم البياني ذي اختزالات أحادية في كل مكان؛ أي، كلما كان a → b و a → c ، فلا بد من وجود a d بحيث يكون b → d و c → d . يُعد نوع الاختزال الأحادي أقوى من نوع الاختزال المتعدد.

ملتقى محلي

يُقال عن العنصر a ∈ S أنه متقارب محليًا (أو متقارب ضعيفًا ^{[ 5 ]} ) إذا كان لكل b و c ∈ S حيث a → b و a → c يوجد d ∈ S حيث b ∗ → d و c ∗ → d . إذا كان كل a ∈ S متقاربًا محليًا، فإن → يُسمى متقاربًا محليًا، أو يتمتع بخاصية تشيرش-روسر الضعيفة . يختلف هذا عن التقارب في أن b و c يجب اختزالهما من a في خطوة واحدة. قياسًا على ذلك، يُشار إلى التقارب أحيانًا بالتقارب الشامل .

يمكن اعتبار العلاقة ∗ → ، المُقدَّمة كرمز لمتتاليات الاختزال، نظام إعادة كتابة بحد ذاته، حيث تمثل علاقتها الإغلاق الانعكاسي-المتعدي لـ → . وبما أن متتالية متتاليات الاختزال هي متتالية اختزال أخرى (أو بصورة مكافئة، لأن تكوين الإغلاق الانعكاسي-المتعدي هو عملية متطابقة )، فإن ∗ ∗ → = ∗ → . ويترتب على ذلك أن → تكون متصلة إذا وفقط إذا كانت ∗ → متصلة محليًا.

قد يكون نظام إعادة الكتابة متقاربًا محليًا دون أن يكون متقاربًا عالميًا. تظهر أمثلة على ذلك في الشكلين 1 و2. ومع ذلك، تنص مبرهنة نيومان على أنه إذا لم يكن لنظام إعادة الكتابة المتقارب محليًا أي متواليات اختزال لانهائية (وفي هذه الحالة يُقال إنه نظام منتهٍ أو نظام تطبيع قوي )، فإنه يكون متقاربًا عالميًا.

• إن اختزال كثيرات الحدود modulo an ideal هو نظام إعادة كتابة متقارب بشرط أن يعمل المرء مع أساس Gröbner .
• تستنتج نظرية ماتسوموتو من التقاء علاقات الجدائل.
• إن اختزال بيتا للمصطلحات λ يتحد بواسطة نظرية تشيرش-روسر .

• التقارب (المنطقي)
• الزوج الحرج (المنطقي)
• الشكل الطبيعي (إعادة الكتابة المجردة)

• "تيريز" ؛ بيزم، مارك. كلوب, جان ويليم ; رويل دي فريجر (2003). أنظمة إعادة كتابة المصطلح . مسالك كامبريدج في علوم الكمبيوتر النظرية. مطبعة جامعة كامبريدج. رقم ISBN 0-521-39115-6.
• بادر، فرانز ؛ نيبكو، توبياس (1998). إعادة صياغة المصطلحات وما إلى ذلك . مطبعة جامعة كامبريدج. ISBN 978-0-521-77920-3.
• بلاسيوس، خ. بوركيرت، H.-J.، محرران. (1992). نظام الخصومات . أولدنبورغ. ص.  291.

• فايستين، اريك دبليو. “متموجة” . عالم الرياضيات .