بناء الجملة المجرد من الدرجة العليا

في علوم الحاسوب ، تعتبر الصيغة المجردة من الدرجة العليا (المختصرة HOAS ) تقنية لتمثيل أشجار الصيغة المجردة للغات ذات روابط المتغيرات .

يُعدّ بناء الجملة المجرد مجردًا لأنه يُمثَّل بكائنات رياضية ذات بنية محددة بطبيعتها. على سبيل المثال، في أشجار بناء الجملة المجرد من الدرجة الأولى ( FOAS )، الشائعة الاستخدام في المترجمات ، تُشير بنية الشجرة إلى علاقة التعبير الفرعي، مما يعني عدم الحاجة إلى أقواس لتوضيح البرامج (كما هو الحال في بناء الجملة الملموس ). يكشف بناء الجملة المجرد من الدرجة الأولى (HOAS) عن بنية إضافية: العلاقة بين المتغيرات ومواقع ربطها. في تمثيلات FOAS، يُمثَّل المتغير عادةً بمعرّف، وتُشار إلى العلاقة بين موقع الربط والاستخدام باستخدام المعرّف نفسه . أما في HOAS، فلا يوجد اسم للمتغير؛ فكل استخدام للمتغير يُشير مباشرةً إلى موقع الربط.

هناك عدة أسباب تجعل هذه التقنية مفيدة. أولًا، إنها توضح بنية الربط في البرنامج: فكما لا حاجة لشرح أسبقية المعاملات في تمثيل FOAS، لا حاجة لمعرفة قواعد الربط والنطاق لتفسير تمثيل HOAS. ثانيًا، البرامج المتكافئة ألفا (التي تختلف فقط في أسماء المتغيرات المرتبطة) لها تمثيلات متطابقة في HOAS، مما يجعل التحقق من التكافؤ أكثر كفاءة.

أحد الأشكال الرياضية التي يمكن استخدامها لتطبيق خوارزمية HOAS هو الرسم البياني الذي تُربط فيه المتغيرات بمواقع ارتباطها عبر الحواف . وهناك طريقة شائعة أخرى لتطبيق خوارزمية HOAS (في المترجمات، على سبيل المثال) وهي استخدام مؤشرات دي بروين .

كانت لغة البرمجة المنطقية عالية الرتبة λProlog أول لغة برمجة تدعم روابط λ في بناء الجملة بشكل مباشر . ^{[ 1 ]} استخدمت الورقة البحثية التي قدمت مصطلح HOAS ^{[ 2 ]} شيفرة λProlog لتوضيح ذلك. مع ذلك، عند نقل مصطلح HOAS من سياق البرمجة المنطقية إلى سياق البرمجة الوظيفية ، فإنه يشير ضمنيًا إلى تعريف الروابط في بناء الجملة بالدوال على التعبيرات. في هذا السياق الأخير، يكتسب مصطلح HOAS معنى مختلفًا وإشكاليًا. وقد تم تقديم مصطلح بناء جملة شجرة λ للإشارة تحديدًا إلى أسلوب التمثيل المتاح في سياق البرمجة المنطقية. ^{[ 3 ] [ 4 ]} على الرغم من اختلاف التفاصيل، فإن معالجة الروابط في λProlog مشابهة لمعالجتها في الأطر المنطقية، كما سيتم توضيحه في القسم التالي.

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

على سبيل المثال، يحتوي الإطار المنطقي LF على بنية λ، وهي من نوع السهم (→). لنفترض أننا نريد صياغة لغة بدائية للغاية ذات تعابير غير مُحددة النوع، ومجموعة مُدمجة من المتغيرات، وبنية let let <var> = <exp> in <exp'>التي تسمح بربط المتغيرات varبتعريفها expفي التعابير exp'. في صيغة Twelf ، يمكننا القيام بذلك على النحو التالي:

exp : type . var : type . v : var -> exp . let : var -> exp -> exp -> exp .

هنا، expيُمثل نوع جميع التعبيرات ونوع varجميع المتغيرات المُضمنة (التي قد تُنفذ كأعداد طبيعية ، وهو ما لم يُعرض). يعمل الثابت vكدالة تحويل، ويؤكد أن المتغيرات عبارة عن تعبيرات. أخيرًا، letيُمثل الثابت بنى let بالشكل التالي let <var> = <exp> in <exp>: يقبل متغيرًا، وتعبيرًا (يرتبط بالمتغير)، وتعبيرًا آخر (يرتبط المتغير ضمنه).

سيكون التمثيل المتعارف عليه للغة الكائنية نفسها في نظام HOAS كما يلي :

exp : type . let : exp -> ( exp -> exp ) -> exp .

في هذا التمثيل، لا تظهر متغيرات مستوى الكائن بشكل صريح. يأخذ الثابت letتعبيرًا (يتم ربطه) ودالة على مستوى أعلى exp→ exp (جسم let). هذه الدالة هي الجزء ذو الرتبة العليا : يُمثَّل التعبير الذي يحتوي على متغير حر كتعبير به ثغرات تُملأ بواسطة الدالة على مستوى أعلى عند تطبيقها. كمثال عملي، سنقوم بإنشاء تعبير مستوى الكائن

ليكن x = 1 + 2 في x + 3

(بافتراض وجود مُنشئات طبيعية للأعداد والجمع) باستخدام توقيع HOAS المذكور أعلاه كـ

دع ( زائد 1 2 ) ([ y ] زائد y 3 )

أين [y] eصيغة Twelf للدالة${\displaystyle \lambda ye}$.

يتميز هذا التمثيل المحدد بمزايا تتجاوز ما سبق ذكره: فمن خلال إعادة استخدام مفهوم الربط على المستوى الفوقي، يتمتع الترميز بخصائص مثل الاستبدال الحافظ للأنواع دون الحاجة إلى تعريفها أو إثباتها. وبهذه الطريقة، يمكن أن يقلل استخدام HOAS بشكل كبير من كمية التعليمات البرمجية النمطية المتعلقة بالربط في الترميز.

لا يُطبَّق بناء الجملة المجرد عالي المستوى عمومًا إلا عندما يُمكن فهم متغيرات لغة الكائن على أنها متغيرات بالمعنى الرياضي (أي كبدائل لعناصر عشوائية في مجال معين). وهذا هو الحال غالبًا، ولكن ليس دائمًا: على سبيل المثال، لا توجد أي مزايا تُجنى من ترميز HOAS للنطاق الديناميكي كما يظهر في بعض لهجات لغة Lisp، لأن المتغيرات ذات النطاق الديناميكي لا تتصرف كمتغيرات رياضية.

• نوع البيانات الجبرية المعممة
• بناء الجملة المجرد ذو الرتبة العليا البارامتري (PHOAS)

• ج. ديسبيرو؛ أ. فيلتي؛ أ. هيرشويتز (1995). "بنية الجملة المجردة من الرتبة العليا في Coq". حسابات لامدا المكتوبة وتطبيقاتها . سلسلة محاضرات في علوم الحاسوب. المجلد  902. الصفحات 124-138 . doi : 10.1007/BFb0014049 . ISBN  978-3-540-59048-4تمت أرشفة النسخة الأصلية بتاريخ 30-08-2006.
• مارتن هوفمان (1999). التحليل الدلالي للبنية المجردة من الرتبة العليا . المؤتمر السنوي الرابع عشر لمعهد مهندسي الكهرباء والإلكترونيات حول المنطق في علوم الحاسوب . ص  204. ISBN 0-7695-0158-3.
• إيلي بارزيلاي؛ ستيوارت ألين (2002). عكس بناء الجملة المجردة من الرتبة العليا في Nuprl (ملف PDF) . إثبات النظريات في منطق الرتبة العليا 2002. الصفحات 23-32 . ISBN  3-540-44039-9تمت أرشفة النسخة الأصلية (PDF) بتاريخ 11-10-2006.
• إيلي بارزيلاي (2006). مُقيِّم الاستضافة الذاتية باستخدام HOAS (ملف PDF) . ورشة عمل ICFP حول لغة Scheme والبرمجة الوظيفية 2006.