استراتيجية التخفيض
في إعادة الصياغة ، تُعرَّف استراتيجية الاختزال أو استراتيجية إعادة الصياغة بأنها علاقة تحدد إعادة صياغة لكل عنصر أو مصطلح، بما يتوافق مع علاقة اختزال معينة. [ 1 ] يستخدم بعض المؤلفين هذا المصطلح للإشارة إلى استراتيجية التقييم . [ 2 ] [ 3 ]
التعريفات
بشكل رسمي، بالنسبة لنظام إعادة الكتابة المجرداستراتيجية التخفيضهي علاقة ثنائية علىمع، أينهو الإغلاق المتعدي لـ(ولكن ليس الإغلاق الانعكاسي). [ 1 ] بالإضافة إلى ذلك، يجب أن تكون الأشكال الطبيعية للاستراتيجية هي نفسها الأشكال الطبيعية لنظام إعادة الكتابة الأصلي، أي لجميعيوجدمعإذا[ 4 ]
استراتيجية التخفيض بخطوة واحدة هي استراتيجية حيثوإلا فإنها ستكون استراتيجية متعددة الخطوات . [ 5 ]
الاستراتيجية الحتمية هي التيهي دالة جزئية ، أي لكليوجد واحد على الأكثربحيثوإلا فإنها استراتيجية غير حتمية . [ 5 ]
إعادة صياغة المصطلحات
في نظام إعادة كتابة المصطلحات، تحدد استراتيجية إعادة الكتابة، من بين جميع المصطلحات الفرعية القابلة للاختزال ( redex )، أي منها يجب اختزاله ( تقليصه ) داخل المصطلح.
تتضمن استراتيجيات إعادة صياغة المصطلحات بخطوة واحدة ما يلي: [ 5 ]
- leftmost-innermost: في كل خطوة، يتم تقليص أقصى اليسار من الريدكسات الداخلية، حيث أن الريدكس الداخلي هو ريدكس لا يحتوي على أي ريدكسات [ 6 ]
- أقصى اليسار - أقصى الخارج: في كل خطوة يتم تقليص أقصى اليسار من الريدكسات الخارجية، حيث أن الريدكس الخارجي هو ريدكس غير موجود في أي ريدكسات [ 6 ]
- أقصى اليمين من الداخل، أقصى اليمين من الخارج: بالمثل
تتضمن الاستراتيجيات متعددة الخطوات ما يلي: [ 5 ]
- يُختزل المتوازي الداخلي جميع الاختزالات الداخلية في آنٍ واحد. وهذا مُحدد جيدًا لأن الاختزالات منفصلة تمامًا.
- متوازي-خارجي: بالمثل
- اختزال غروس-كنوث، [ 7 ] ويُسمى أيضًا بالاستبدال الكامل أو اختزال كلين: [ 5 ] يتم اختزال جميع الاختزالات في المصطلح في آن واحد
يُعدّ كلٌّ من الاختزال الخارجي المتوازي واختزال غروس-كنوث من الاختزالات فائقة التطبيع لجميع أنظمة إعادة كتابة المصطلحات شبه المتعامدة، مما يعني أن هذه الاستراتيجيات ستصل في النهاية إلى شكل طبيعي إن وُجد، حتى عند إجراء عدد محدود من عمليات الاختزال العشوائية بين التطبيقات المتتالية للاستراتيجية. [ 8 ]
ستراتيجو هي لغة برمجة خاصة بمجال معين، مصممة خصيصًا لبرمجة استراتيجيات إعادة كتابة المصطلحات. [ 9 ]
حساب التفاضل والتكامل لامدا
في سياق حساب لامدا ، يشير الاختزال ذو الرتبة الطبيعية إلى الاختزال من أقصى اليسار إلى أقصى الخارج بالمعنى المذكور أعلاه . [ 10 ] يُعدّ الاختزال ذو الرتبة الطبيعية اختزالًا معياريًا، بمعنى أنه إذا كان للمصطلح شكل معياري، فإن الاختزال ذو الرتبة الطبيعية سيصل إليه في النهاية، ومن هنا جاءت تسميته بالمعياري. يُعرف هذا بنظرية التوحيد القياسي. [ 11 ] [ 12 ]
يُستخدم مصطلح "الاختزال الأيسر" أحيانًا للإشارة إلى "الاختزال الترتيبي العادي"، حيث تتطابق المفاهيم مع مفهوم "الترتيب المسبق" . وبالمثل، فإن "الاختزال الأيسر الخارجي" هو الاختزال الذي يبدأ بأول حرف على اليسار عندما يُنظر إلى مصطلح لامدا كسلسلة من الأحرف. [ 13 ] [ 14 ] أما عند تعريف "الأيسر" باستخدام " الترتيب الداخلي " ، فإن المفاهيم تكون مختلفة. على سبيل المثال، في المصطلحمعوفقًا للتعريف الوارد هنا ، فإن أقصى نقطة إعادة فهرسة يسارية في عملية اجتياز الترتيب الداخلي هيبينما يمثل التعبير الكامل التعبير الموجود في أقصى اليسار. [ 15 ]
يشير اختزال الترتيب التطبيقي إلى الاختزال من أقصى اليسار إلى أقصى الداخل. [ 10 ] على عكس الترتيب العادي، قد لا ينتهي اختزال الترتيب التطبيقي، حتى عندما يكون للمصطلح شكل عادي. [ 10 ] على سبيل المثال، باستخدام اختزال الترتيب التطبيقي، يكون تسلسل الاختزالات التالي ممكنًا:
لكن باستخدام اختزال الترتيب الطبيعي، فإن نقطة البداية نفسها تختزل بسرعة إلى الشكل الطبيعي:
يشير مصطلح "الاختزال الكامل بيتا" إلى استراتيجية غير حتمية أحادية الخطوة تسمح باختزال أي مُختزل في كل خطوة. [ 3 ] أما "الاختزال المتوازي بيتا" لتاكاهاشي فهو الاستراتيجية التي تختزل جميع المُختزلات في المصطلح في آن واحد. [ 16 ]
انخفاض ضعيف
يتميز اختزال الترتيب العادي والتطبيقي بقوتهما في السماح بالاختزال ضمن تجريدات لامدا. في المقابل، لا يسمح الاختزال الضعيف بالاختزال ضمن تجريدات لامدا. [ 17 ] يُعد اختزال الاستدعاء بالاسم استراتيجية اختزال ضعيفة تُختزل فيها الدالة الخارجية اليسرى غير الموجودة ضمن تجريد لامدا، بينما يُعد اختزال الاستدعاء بالقيمة استراتيجية اختزال ضعيفة تُختزل فيها الدالة الداخلية اليسرى غير الموجودة ضمن تجريد لامدا. صُممت هاتان الاستراتيجيتان لتعكسا استراتيجيتي تقييم الاستدعاء بالاسم والاستدعاء بالقيمة . [ 18 ] في الواقع، طُور اختزال الترتيب التطبيقي في الأصل لنمذجة تقنية تمرير المعاملات بالاستدعاء بالقيمة الموجودة في لغة Algol 60 ولغات البرمجة الحديثة. عند دمجه مع فكرة الاختزال الضعيف، يُصبح اختزال الاستدعاء بالقيمة الناتج تقريبًا دقيقًا. [ 19 ]
لسوء الحظ، لا يُعدّ الاختزال الضعيف متقاربًا ، [ 17 ] ومعادلات الاختزال التقليدية لحساب لامدا غير مجدية، لأنها تُشير إلى علاقات تُخالف نظام التقييم الضعيف. [ 19 ] مع ذلك، من الممكن توسيع النظام ليصبح متقاربًا بالسماح بصيغة مُقيّدة من الاختزال ضمن تجريد، لا سيما عندما لا يتضمن المُختزل المتغير المُقيّد بالتجريد. [ 17 ] على سبيل المثال، يكون التعبير λx .( λy.x ) z في الصيغة الطبيعية لاستراتيجية الاختزال الضعيف لأن المُختزل ( λy.x ) z مُضمن في تجريد لامدا. لكن لا يزال من الممكن اختزال الحد λx . ( λy.y ) z في ظل استراتيجية الاختزال الضعيف المُوسّعة ، لأن المُختزل ( λy.y ) z لا يُشير إلى x . [ 20 ]
التخفيض الأمثل
يستند الاختزال الأمثل إلى وجود حدود لامدا حيث لا توجد سلسلة من عمليات الاختزال التي تختزلها دون تكرار العمل. على سبيل المثال، ضع في اعتبارك
((λg.(g(g(λx.x)))) (λh.((λf.(f(f(λz.z)))) (λw.(h(w(λy.y))))))))
يتكون هذا التعبير من ثلاثة حدود متداخلة: a=((λg. ... ) (λh.b)) و b=((λf. ...) c) و c=(λw. ...) . يوجد هنا نوعان فقط من عمليات اختزال بيتا، أحدهما على a والآخر على b. يؤدي اختزال الحد الخارجي a أولًا إلى تكرار الحد الداخلي b، وسيتعين اختزال كل نسخة منه. أما اختزال الحد الداخلي b أولًا فيؤدي إلى تكرار وسيطه c، مما يتسبب في تكرار العمل عند معرفة قيمتي h و w. [ a ]
لا يُعدّ الاختزال الأمثل استراتيجية اختزال لحساب لامدا بالمعنى الضيق، لأنّ إجراء اختزال بيتا يُفقد المعلومات المتعلقة بالاختزالات المُستبدلة المُشتركة. بل يُعرَّف لحساب لامدا المُصنَّف ، وهو حساب لامدا مُعلَّق يُجسِّد مفهومًا دقيقًا للعمل الذي ينبغي مُشاركته. [ 21 ] : 113-114
تتكون التصنيفات من مجموعة لا نهائية قابلة للعد من التصنيفات الذرية، والتسلسلات.، التبطيناتوالتسطيرمن التسميات. الحد المُسمى هو حد في حساب التفاضل والتكامل لامدا حيث يكون لكل حد فرعي تسمية. تُعطي التسمية الأولية القياسية لحد لامدا كل حد فرعي تسمية ذرية فريدة. [ 21 ] : 132 يُعطى اختزال بيتا المُسمى بواسطة: [ 22 ]
أينيقوم بدمج التصنيفات،، والاستبداليتم تعريفها على النحو التالي (باستخدام اتفاقية باريندريخت ): [ 22 ] يمكن إثبات أن النظام متقارب. يُعرَّف الاختزال الأمثل بأنه الاختزال بالترتيب الطبيعي أو الاختزال من اليسار إلى الخارج باستخدام الاختزال حسب العائلات، أي الاختزال المتوازي لجميع الاختزالات التي تحمل نفس تسمية جزء الوظيفة. [ 23 ] تُعد هذه الاستراتيجية مثالية لأنها تُنفذ العدد الأمثل (الأدنى) من خطوات اختزال العائلات. [ 24 ]
وُصفت خوارزمية عملية للاختزال الأمثل لأول مرة عام 1989، [ 25 ] أي بعد أكثر من عقد من تعريف الاختزال الأمثل لأول مرة عام 1974. [ 26 ] تُعد آلة بولونيا المثلى ذات الرتبة العليا (BOHM) نموذجًا أوليًا لتطبيق امتداد هذه التقنية ليشمل شبكات التفاعل . [ 21 ] : 362 [ 27 ] أما لامداسكوب فهو تطبيق أحدث للاختزال الأمثل، ويستخدم أيضًا شبكات التفاعل. [ 28 ] [ ب ]
تقليل المكالمات حسب الحاجة
يمكن تعريف الاختزال بالاستدعاء عند الحاجة بشكل مشابه للاختزال الأمثل، باعتباره اختزالًا ضعيفًا من اليسار إلى الخارج باستخدام اختزال متوازٍ لمصطلحات الاختزال التي تحمل نفس التسمية، وذلك لحساب لامدا مُصنَّف بشكل مختلف قليلًا. [ 17 ] يُغيّر تعريف بديل قاعدة بيتا إلى عملية تجد الحساب "المطلوب" التالي، وتُقيّمه، ثم تستبدل النتيجة في جميع المواقع. يتطلب هذا توسيع قاعدة بيتا للسماح باختزال المصطلحات غير المتجاورة نحويًا. [ 29 ] كما هو الحال مع الاستدعاء بالاسم والاستدعاء بالقيمة، صُمِّم الاختزال بالاستدعاء عند الحاجة لمحاكاة سلوك استراتيجية التقييم المعروفة باسم "الاستدعاء عند الحاجة" أو التقييم الكسول .
انظر أيضاً
ملحوظات
- ↑ بالمناسبة، يختزل المصطلح أعلاه إلى دالة التطابق (λy.y) ، ويتم إنشاؤه عن طريق إنشاء أغلفة تجعل دالة التطابق متاحة للروابط g=λh... ، f=λw... ، h=λx.x (في البداية)، و w=λz.z (في البداية)، وكلها يتم تطبيقها على المصطلح الداخلي λy.y.
- ↑ يمكن الاطلاع على ملخص للأبحاث الحديثة حول الاختزال الأمثل في المقالة القصيرة حول الاختزال الفعال لمصطلحات لامدا .
مراجع
- 1 2 كيرشنر، هيلين (26 أغسطس 2015). "استراتيجيات إعادة الكتابة وبرامج إعادة الكتابة الاستراتيجية" . في مارتي-أوليت، نارسيسو؛ أولفيتسكي، بيتر تشابا؛ تالكوت، كارولين (محررون). المنطق، وإعادة الكتابة، والتزامن: مقالات مهداة إلى خوسيه ميسيغوير بمناسبة عيد ميلاده الخامس والستين . سبرينغر. ISBN 978-3-319-23165-5تم الاطلاع عليه بتاريخ 14 أغسطس 2021 .
- ↑ سيلينجر، بيتر؛ فاليرون، بينوا (2009). "حساب لامدا الكمي" (ملف PDF) . التقنيات الدلالية في الحوسبة الكمية : 23. doi : 10.1017/CBO9781139193313.005 . ISBN 9780521513746تم الاطلاع عليه بتاريخ 21 أغسطس 2021 .
- 1 2 بيرس، بنجامين سي. (2002). الأنواع ولغات البرمجة . مطبعة معهد ماساتشوستس للتكنولوجيا . ص 56. ISBN 0-262-16209-1.
- ^ كلوب ، جان ويليم. فان أوستروم، فنسنت؛ فان رامسدونك، فيمكي (2007). “استراتيجيات التخفيض والتقلبية” (PDF) . إعادة الكتابة والحساب والإثبات . ملاحظات محاضرة في علوم الكمبيوتر. المجلد. 4600. ص 89 – 112. CiteSeerX 10.1.1.104.9139 . دوى : 10.1007/978-3-540-73147-4_5 . رقم ISBN 978-3-540-73146-7.
- 1 2 3 4 5 كلوب، جيه دبليو. "أنظمة إعادة كتابة المصطلحات" (ملف PDF) . أوراق بحثية لناحوم ديرشوفيتز وطلابه . جامعة تل أبيب. ص 77. تاريخ الاطلاع: 14 أغسطس 2021 .
- 1 2 هورويتز، سوزان ب. "حساب لامدا" . ملاحظات CS704 . جامعة ويسكونسن ماديسون . تم الاسترجاع في 19 أغسطس 2021 .
- ^ باريندريجت، إتش بي؛ إيكلين، إم سي جي دي؛ جلاورت، جي آر دبليو؛ كينواي، جي آر؛ بلازميجر، إم جي . النوم، السيد (1987). إعادة كتابة الرسم البياني المدى . البنى الموازية واللغات في أوروبا. المجلد. 259. ص 141 – 158. دوى : 10.1007 / 3-540-17945-3_8 . اتش دي ال : 2066/17285 .
- ↑ أنتوي، سيرجيو؛ ميدلدورب، آرت (سبتمبر 1996). "استراتيجية الاختزال التسلسلي" (ملف PDF) . علوم الحاسوب النظرية . 165 (1): 75-95 . doi : 10.1016/0304-3975(96)00041-2 . تاريخ الاسترجاع: 8 سبتمبر 2021 .
- ↑ كيبرتز، ريتشارد ب. (نوفمبر 2001). "منطق لإعادة كتابة الاستراتيجيات" . ملاحظات إلكترونية في علوم الحاسوب النظرية . 58 (2): 138-154 . doi : 10.1016/S1571-0661(04)00283-X .
- 1 2 3 مازولا، جويرينو؛ ميلمايستر، جيرار؛ فايسمان، جودي (21 أكتوبر 2004). الرياضيات الشاملة لعلماء الحاسوب 2. سبرينغر ساينس آند بيزنس ميديا. ص 323. ISBN 978-3-540-20861-7.
- ↑ كاري، هاسكل ب .؛ فيس، روبرت (1958). المنطق التوافقي . المجلد الأول. أمستردام: نورث هولاند. الصفحات 139-142 . ISBN 0-7204-2208-6.
{{cite book}}عدم توافق رقم ISBN / التاريخ ( مساعدة ) - ↑ كاشيما، ريو. "برهان نظرية التقييس في حساب لامدا" (ملف PDF) . معهد طوكيو للتكنولوجيا . تاريخ الاسترجاع: 19 أغسطس 2021 .
- ^ فيال ، بيير (7 ديسمبر 2017). عوامل الكتابة غير العاجزة، خارج حساب التفاضل والتكامل (PDF) (دكتوراه). مدينة السوربون باريس. ص. 62.
- ↑ بارتين، ويليام د. (ديسمبر 1989). اختزال الرسوم البيانية بدون مؤشرات (ملف PDF) (أطروحة دكتوراه). جامعة نورث كارولينا في تشابل هيل . تم الاطلاع عليه بتاريخ 10 يناير 2022 .
- ↑ فان أوستروم، فينسنت؛ توياما، يوشيهيتو (2016). التطبيع عن طريق التدرج العشوائي (ملف PDF) . المؤتمر الدولي الأول حول الهياكل الرسمية للحوسبة والاستنتاج. ص 32:3. doi : 10.4230/LIPIcs.FSCD.2016.32 .
- ↑ تاكاهاشي، م. (أبريل 1995). "الاختزالات المتوازية في حساب لامدا" . المعلومات والحوسبة . 118 (1): 120-127 . doi : 10.1006/inco.1995.1057 .
- 1 2 3 4 بلانك، توماش؛ ليفي، جان جاك؛ مارانجيه، لوك (2005). "المشاركة في حساب لامدا الضعيف". العمليات والمصطلحات والدورات: خطوات على طريق اللانهاية: مقالات مهداة إلى يان ويليم كلوب بمناسبة عيد ميلاده الستين . سبرينغر. ص 70-87 . CiteSeerX 10.1.1.129.147 . doi : 10.1007/11601548_7 . ISBN 978-3-540-32425-6.
- ↑ سيستوفت، بيتر (2002). "إثبات اختزال حساب لامدا" (ملف PDF) . في: موجنسن، ت؛ شميدت، د؛ سودبورو، آي إتش (محررون). جوهر الحوسبة: التعقيد، التحليل، التحويل. مقالات مهداة إلى نيل د. جونز . سلسلة محاضرات في علوم الحاسوب. المجلد 2566. سبرينغر-فيرلاغ. الصفحات 420-435 . ISBN 3-540-00326-6.
- 1 2 فيليسين، ماتياس (2009). هندسة الدلالات باستخدام PLT Redex . كامبريدج، ماساتشوستس: مطبعة معهد ماساتشوستس للتكنولوجيا. ص 42. ISBN 978-0262062756.
- ↑ سيستيني، فيليبو (2019). التطبيع بالتقييم لاختزال لامدا الضعيف المكتوب (ملف PDF) . المؤتمر الدولي الرابع والعشرون حول أنواع البراهين والبرامج (TYPES 2018). doi : 10.4230/LIPIcs.TYPES.2018.6 .
- 1 2 3 أسبرتي، أندريا؛ غيريني، ستيفانو (1998). التنفيذ الأمثل للغات البرمجة الوظيفية . كامبريدج، المملكة المتحدة: مطبعة جامعة كامبريدج. ISBN 0521621127.
- 1 2 فرنانديز، ماريبيل؛ سيافاكاس، نيكولاوس (30 مارس 2010). "حسابات لامدا المُعَلَّمة مع النسخ والمسح الصريحين". وقائع إلكترونية في علوم الحاسوب النظرية . 22 : 49-64 . arXiv : 1003.5515v1 . doi : 10.4204/EPTCS.22.5 . S2CID 15500633 .
- ↑ ليفي، جان جاك (9-11 نوفمبر 1987). المشاركة في تقييم تعابير لامدا (ملف PDF) . الندوة الفرنسية اليابانية الثانية حول برمجة حواسيب الجيل القادم. كان، فرنسا. ص 187. ISBN 0444705260.
- ↑ تيريز (2003). أنظمة إعادة كتابة المصطلحات . كامبريدج، المملكة المتحدة: مطبعة جامعة كامبريدج. ص 518. ISBN 978-0-521-39115-3.
- ↑ لامبينغ، جون (1990). خوارزمية للاختزال الأمثل لحساب التفاضل والتكامل اللامدا (ملف PDF) . الندوة السابعة عشرة لجمعية ACM SIGPLAN-SIGACT حول مبادئ لغات البرمجة - POPL '90. الصفحات 16-30 . doi : 10.1145/96709.96711 .
- ^ ليفي، جان جاك (يونيو 1974). Réductions Sures dans le lambda-calcul (PDF) (دكتوراه) (باللغة الفرنسية). جامعة باريس السابعة. ص 81 – 109. OCLC 476040273 . تم الاسترجاع في 17 أغسطس 2021 .
- ↑ أسبرتي، أندريا. "آلة بولونيا المثلى من الرتبة العليا، الإصدار 1.1" . جيت هاب .
- ^ فان أوستروم، فنسنت. فان دي لويج، كيس جان؛ زويتسرلود، مارين (2004). (Lambdascope): تطبيق أمثل آخر لحساب التفاضل والتكامل لامدا (PDF) . ورشة عمل حول الجبر والمنطق على أنظمة البرمجة (ALPS). مؤرشف من الأصل (PDF) بتاريخ 2017-07-06 . تم الاسترجاع 2021-08-18 .
- ↑ تشانغ، ستيفن؛ فيليسين، ماتياس (2012). "حساب لامدا عند الحاجة، مُعاد النظر فيه" (ملف PDF) . لغات البرمجة والأنظمة . سلسلة محاضرات في علوم الحاسوب. المجلد 7211. الصفحات 128-147 . doi : 10.1007/978-3-642-28869-2_7 . ISBN 978-3-642-28868-5. S2CID 6350826 .
روابط خارجية
- أنظمة إعادة الكتابة
- حساب التفاضل والتكامل لامدا
