الرسم البياني الإلكتروني

📅 آخر تحديث: ٣١ يوليو ٢٠٢٦
✍️ نُشر في: ٣١ يوليو ٢٠٢٦
📷 يحتوي على 48 صور
الموسوعة الحرة

في علوم الحاسوب ، الرسم البياني الإلكتروني هو بنية بيانات تخزن علاقة تكافؤ بين مصطلحات لغة معينة.

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

يتركΣ{\displaystyle \Sigma }لتكن مجموعة من الدوال غير المفسرة ، حيثΣن{\displaystyle \Sigma _{n}}هي مجموعة جزئية منΣ{\displaystyle \Sigma }تتكون من دوال ذات عدد معاملاتن{\displaystyle n}. يتركأناد{\displaystyle \mathbb {id} }يمكن أن تكون مجموعة قابلة للعد من المعرفات المبهمة التي يمكن مقارنتها للتأكد من تساويها، وتسمى معرفات الفئة الإلكترونية . تطبيقو∈Σن{\displaystyle f\in \Sigma _{n}}إلى معرفات الفصل الإلكترونيأنا1،أنا2،...،أنان∈أناد{\displaystyle i_{1},i_{2},\ldots ,i_{n}\in \mathbb {id} }يُشار إليه بـو(أنا1،أنا2،...،أنان){\displaystyle f(i_{1},i_{2},\ldots ,i_{n})}وتسمى العقدة الإلكترونية .

ثم يمثل الرسم البياني الإلكتروني فئات التكافؤ للعقد الإلكترونية، باستخدام هياكل البيانات التالية: [ 1 ]

  • بنية الاتحاد والبحثيو{\displaystyle U}تمثل فئات التكافؤ لمعرفات الفئة الإلكترونية، مع العمليات المعتادةوأناند{\displaystyle \mathrm {العثور} }،أدد{\displaystyle \mathrm {أضف} }ومهـرزهـ{\displaystyle \mathrm {دمج} }معرف الفصل الإلكترونيهـ{\displaystyle e}يُعتبر قانونيًا إذاوأناند(يو،هـ)=هـ{\displaystyle \mathrm {find} (U,e)=e}عقدة إلكترونيةو(أنا1،...،أنان){\displaystyle f(i_{1},\ldots ,i_{n})} يكون قانونيًا إذا كان كلأناج{\displaystyle i_{j}}هو قانوني (ج{\displaystyle j}في1،...،ن{\displaystyle 1,\ldots ,n}).
  • ربط معرّفات الفئات الإلكترونية بمجموعات من العقد الإلكترونية، تُسمى الفئات الإلكترونية . ويتكون هذا من
    • هاشكونز​ح{\displaystyle H}(أي ربط) من العقد الإلكترونية إلى معرفات الفئات الإلكترونية، و
    • خريطة الفصل الإلكترونيم{\displaystyle M}التي تربط معرّفات الفئات الإلكترونية بالفئات الإلكترونية، بحيثم{\displaystyle M}يربط المعرفات المتكافئة بنفس مجموعة العقد الإلكترونية:∀أنا،ج∈أناد،م[أنا]=م[ج]⇔وأناند(يو،أنا)=وأناند(يو،ج){\displaystyle \forall i,j\in \mathbb {id} ,M[i]=M[j]\Leftrightarrow \mathrm {find} (U,i)=\mathrm {find} (U,j)}

الثوابت

بالإضافة إلى البنية المذكورة أعلاه، يلتزم الرسم البياني الإلكتروني الصحيح بعدة ثوابت لبنية البيانات . [ 2 ] يكون عقدان إلكترونيان متكافئين إذا كانا ينتميان إلى نفس الفئة الإلكترونية. ينص ثابت التطابق على أن الرسم البياني الإلكتروني يجب أن يضمن أن التكافؤ مغلق تحت التطابق ، حيث يكون عقدان إلكترونيانو(أنا1،...،أنان)،و(ج1،...،جن){\displaystyle f(i_{1},\ldots ,i_{n}),f(j_{1},\ldots ,j_{n})}تكون متطابقة عندماوأناند(يو،أناك)=وأناند(يو،جك)،ك∈{1،...،ن}{\displaystyle \mathrm {find} (U,i_{k})=\mathrm {find} (U,j_{k}),k\in \{1,\ldots ,n\}}تنص خاصية hashcons الثابتة على أن hashcons تقوم بربط العقد الإلكترونية المتعارف عليها بمعرفات فئة e الخاصة بها.

العمليات

تكشف الرسوم البيانية الإلكترونية عن أغلفة حولأدد{\displaystyle \mathrm {أضف} }،وأناند{\displaystyle \mathrm {العثور} }، ومهـرزهـ{\displaystyle \mathrm {دمج} }العمليات من عملية الاتحاد والبحث التي تحافظ على ثوابت الرسم البياني الإلكتروني. العملية الأخيرة، وهي المطابقة الإلكترونية، موصوفة أدناه.

الصيغ المتكافئة

يمكن أيضًا صياغة الرسم البياني الإلكتروني كرسم بياني ثنائي الأجزاءجي=(شمال⊎أناد،هـ){\displaystyle G=(N\uplus \mathrm {id} ,E)}أين

  • أناد{\displaystyle \mathrm {id} }هي مجموعة معرّفات الفئة الإلكترونية (كما هو مذكور أعلاه)،
  • شمال{\displaystyle N}هي مجموعة العقد الإلكترونية، و
  • هـ⊆(أناد×شمال)∪(شمال×أناد){\displaystyle E\subseteq (\mathrm {id} \times N)\cup (N\times \mathrm {id} )}هي مجموعة من الحواف الموجهة.

توجد حافة موجهة من كل فئة إلكترونية إلى كل عضو من أعضائها، ومن كل عقدة إلكترونية إلى كل من أبنائها. [ 3 ]

المطابقة الإلكترونية

يتركV{\displaystyle V}لتكن مجموعة من المتغيرات ولتكنتيهـرم(Σ،V){\displaystyle \mathrm {Term} (\Sigma ,V)}لتكن أصغر مجموعة تتضمن رموز الدوال ذات الرتبة الصفرية (وتسمى أيضًا الثوابت )، وتتضمن المتغيرات، وتكون مغلقة عند تطبيق رموز الدوال. بعبارة أخرى،تيهـرم(Σ،V){\displaystyle \mathrm {Term} (\Sigma ,V)}هي أصغر مجموعة بحيثV⊂تيهـرم(Σ،V){\displaystyle V\subset \mathrm {Term} (\Sigma ,V)}،Σ0⊂تيهـرم(Σ،V){\displaystyle \Sigma _{0}\subset \mathrm {Term} (\Sigma ,V)}ومتىx1،...،xن∈تيهـرم(Σ،V){\displaystyle x_{1},\ldots ,x_{n}\in \mathrm {Term} (\Sigma ,V)}وو∈Σن{\displaystyle f\in \Sigma _{n}}، ثمو(x1،...،xن)∈تيهـرم(Σ،V){\displaystyle f(x_{1},\ldots ,x_{n})\in \mathrm {Term} (\Sigma ,V)}يُطلق على المصطلح الذي يحتوي على متغيرات اسم النمط ، بينما يُطلق على المصطلح الذي لا يحتوي على متغيرات اسم الأساس .

رسم بياني إلكترونيهـ{\displaystyle E}يمثل مصطلحًا أساسيًات∈تيهـرم(Σ،∅){\displaystyle t\in \mathrm {Term} (\Sigma ,\emptyset )}إذا كان أحد فصولها الإلكترونية يمثلت{\displaystyle t}فصل إلكترونيج{\displaystyle C}يمثلت{\displaystyle t}إذا كان هناك عقدة إلكترونيةو(أنا1،...،أنان)∈ج{\displaystyle f(i_{1},\ldots ,i_{n})\in C}يفعل. عقدة إلكترونيةو(أنا1،...،أنان)∈ج{\displaystyle f(i_{1},\ldots ,i_{n})\in C}يمثل مصطلحًاز(ج1،...،جن){\displaystyle g(j_{1},\ldots ,j_{n})}لوو=ز{\displaystyle f=g}وكل فصل دراسي إلكترونيم[أناك]{\displaystyle M[i_{k}]}يمثل المصطلحجك{\displaystyle j_{k}}(ك{\displaystyle k}في1،...،ن{\displaystyle 1,\ldots ,n}).

المطابقة الإلكترونية هي عملية تأخذ نمطًاص∈تيهـرم(Σ،V){\displaystyle p\in \mathrm {Term} (\Sigma ,V)}ورسم بياني إلكترونيهـ{\displaystyle E}، وينتج جميع الأزواج(σ،ج){\displaystyle (\sigma ,C)}أينσ⊂V×أناد{\displaystyle \sigma \subset V\times \mathbb {id} }هي عملية استبدال تربط المتغيرات فيص{\displaystyle p}إلى معرفات الفصل الإلكتروني وج∈أناد{\displaystyle C\in \mathbb {id} }هو معرف فئة إلكترونية بحيث يكون المصطلحσ(ص){\displaystyle \sigma (p)}يمثلهاج{\displaystyle C}توجد عدة خوارزميات معروفة للمطابقة الإلكترونية، [ 4 ] [ 5 ] وتعتمد خوارزمية المطابقة الإلكترونية العلائقية على عمليات الربط المثلى في أسوأ الحالات ، وهي خوارزمية مثلى في أسوأ الحالات. [ 6 ]

اِستِخلاص

بافتراض وجود فئة إلكترونية ودالة تكلفة تربط كل رمز دالة فيΣ{\displaystyle \Sigma }عند تحويل عدد طبيعي إلى عدد حقيقي، تتمثل مشكلة الاستخراج في إيجاد حد أساسي بأقل تكلفة إجمالية يُمثله الصنف الإلكتروني المُعطى. هذه المشكلة من فئة NP-hard . [ 7 ] كما لا توجد خوارزمية تقريبية ذات عامل ثابت لهذه المشكلة، وهو ما يمكن إثباته بالاختزال من مشكلة تغطية المجموعة . مع ذلك، بالنسبة للرسوم البيانية ذات عرض الشجرة المحدود ، توجد خوارزمية خطية الزمن ذات معلمات ثابتة قابلة للحل . [ 8 ]

تعقيد

  • يمكن إنشاء رسم بياني إلكتروني يحتوي على n من المتساويات في زمن قدره O( n log n ). [ 9 ]

تشبع المساواة

تشبع المساواة هو أسلوب لبناء مُجمِّعات مُحسِّنة باستخدام الرسوم البيانية الإلكترونية. [ 10 ] يعمل هذا الأسلوب من خلال تطبيق مجموعة من عمليات إعادة الكتابة باستخدام المطابقة الإلكترونية حتى يتم تشبع الرسم البياني الإلكتروني، أو الوصول إلى مهلة زمنية، أو الوصول إلى حد أقصى لحجم الرسم البياني الإلكتروني، أو تجاوز عدد مُحدد من التكرارات، أو الوصول إلى شرط توقف آخر. بعد إعادة الكتابة، يتم استخراج مصطلح أمثل من الرسم البياني الإلكتروني وفقًا لدالة تكلفة معينة، ترتبط عادةً بحجم شجرة بناء الجملة المجردة أو اعتبارات الأداء.

التطبيقات

تُستخدم الرسوم البيانية الإلكترونية في إثبات النظريات الآلي . وهي جزء أساسي من حلول SMT الحديثة مثل Z3 [ 11 ] و CVC4 ، حيث تُستخدم لتحديد النظرية الفارغة عن طريق حساب إغلاق التطابق لمجموعة من المتساويات، ويُستخدم التطابق الإلكتروني لإنشاء المُكمِّمات. [ 12 ] في الحلول القائمة على DPLL(T) والتي تستخدم تعلم البنود المُوجَّه بالتعارض (المعروف أيضًا باسم التراجع غير الزمني)، يتم توسيع الرسوم البيانية الإلكترونية لإنتاج شهادات الإثبات. [ 13 ] كما تُستخدم الرسوم البيانية الإلكترونية في مُثبت نظرية التبسيط في ESC/Java . [ 14 ]

يُستخدم تشبع المساواة في مُجمِّعات التحسين المتخصصة ، [ 15 ] على سبيل المثال في التعلّم العميق [ 16 ] ، والجبر الخطي [ 17 ] ، والتحويل التلقائي إلى متجهات لمعالجات الإشارات الرقمية [ 18 ] . كما استُخدم تشبع المساواة أيضًا للتحقق من صحة الترجمة المُطبَّقة على سلسلة أدوات LLVM . [ 19 ]

تم تطبيق الرسوم البيانية الإلكترونية على العديد من المشكلات في تحليل البرامج ، بما في ذلك اختبار البرمجيات العشوائي [ 20 ] ، والتفسير المجرد [ 21 ] ، وتعلم المكتبات [ 22 ] .

مراجع

  1. ↑ ( ويلسي وآخرون 2021 )
  2. ↑ ( ويلسي وآخرون 2021 )
  3. ↑ ( جوهارشادي، لام وبارو 2024 )
  4. ^ ( دي مورا وبيورنر 2007 )
  5. ↑ موسكال، ميخال؛ لوبوزانسكي، ياكوب؛ كينيري، جوزيف ر. (2008-05-06). "المطابقة الإلكترونية للمتعة والربح" . الملاحظات الإلكترونية في علوم الحاسوب النظرية . وقائع ورشة العمل الدولية الخامسة حول قابلية الإرضاء وفقًا للنظريات (SMT 2007). 198 (2): 19-35 . doi : 10.1016/j.entcs.2008.04.078 . ISSN 1571-0661 . 
  6. ↑ تشانغ، ييهونغ؛ وانغ، ييسو ريمي؛ ويلسي، ماكس؛ تاتلوك، زاكاري (12 يناير 2022). "المطابقة الإلكترونية العلائقية" . وقائع مؤتمر ACM للغات البرمجة . 6 (POPL): 35:1–35:22. arXiv : 2108.02290 . doi : 10.1145/3498696 . S2CID 236924583 . 
  7. ↑ ستيب، مايكل بنجامين (2011). تشبع المساواة: التحديات الهندسية والتطبيقات (أطروحة دكتوراه). الولايات المتحدة الأمريكية: جامعة كاليفورنيا في سان دييغو. ISBN 978-1-267-03827-2.
  8. ↑ ( جوهارشادي، لام وبارو 2024 )
  9. ↑ ( فلات وآخرون 2022 ، ص 2) 
  10. ↑ ( تيت وآخرون، 2009 )
  11. ↑ دي مورا، ليوناردو؛ بيورنر، نيكولاي (2008). "Z3: حلّ فعال لـ SMT". في راماكريشنان، سي آر؛ ريهوف، جاكوب (محرران). أدوات وخوارزميات لبناء وتحليل الأنظمة . سلسلة محاضرات في علوم الحاسوب. المجلد 4963. برلين، هايدلبرغ: سبرينغر. الصفحات 337-340 . doi : 10.1007/978-3-540-78800-3_24 . ISBN   978-3-540-78800-3.
  12. ↑ رومر، فيليب (2012). "المطابقة الإلكترونية مع المتغيرات الحرة". في: بيورنر، نيكولاي؛ فورونكوف، أندريه (محرران). المنطق للبرمجة والذكاء الاصطناعي والاستدلال. وقائع المؤتمر الدولي الثامن عشر، LPAR-18، ميريدا، فنزويلا، 11-15 مارس 2012. سلسلة محاضرات في علوم الحاسوب. المجلد 7180. برلين، هايدلبرغ: سبرينغر. الصفحات 359-374 . doi : 10.1007/978-3-642-28717-6_28 . ISBN   978-3-642-28717-6.
  13. ↑ ( فلات وآخرون 2022 ، ص 2) 
  14. ↑ ديتليفز، ديفيد؛ نيلسون، جريج؛ ساكس، جيمس ب. (مايو 2005). "Simplify: أداة إثبات نظريات للتحقق من البرامج". مجلة ACM . 52 (3): 365-473 . doi : 10.1145/1066100.1066102 . ISSN 0004-5411 . S2CID 9613854 .  
  15. ↑ جوشي، راجيف؛ نيلسون، جريج؛ راندال، كيث (17 مايو 2002). "دينالي: مُحسِّن فائق موجه نحو الهدف". إشعارات ACM SIGPLAN . 37 (5): 304-314 . doi : 10.1145/543552.512566 . ISSN 0362-1340 . 
  16. ^ يانغ ، يتشن. فوثيليمثا، فيتشايا مانجبو؛ وانغ، يسو ريمي؛ ويلسي، ماكس. روي، سوديب؛ بينار ، جاك (2021-03-17). “تشبع المساواة للتحسين الفائق للرسم البياني للتنسور”. أرخايف : 2101.01332 [ cs.AI ].
  17. ↑ وانغ، ييسو ريمي؛ هاتشيسون، شانا؛ ليانغ، جوناثان؛ هاو، بيل؛ سوتشيو، دان (22-12-2020). "SPORES: تحسين مجموع الضرب عبر تشبع المساواة العلائقية للجبر الخطي واسع النطاق". arXiv : 2002.07951 [ cs.DB ].
  18. ↑ توماس، صموئيل؛ بورنهولت، جيمس (2026-06-01). "التوليد التلقائي لمترجمات المتجهات لمعالجات الإشارات الرقمية القابلة للتخصيص" . اتصالات ACM . 69 (6): 97-105 . doi : 10.1145/3802600 . ISSN 0001-0782 . 
  19. ↑ ستيب، مايكل؛ تيت، روس؛ ليرنر، سورين (2011). "مدقق ترجمة قائم على المساواة لـ LLVM". في: جوبالاكريشنان، غانيش؛ قدير، شاز (محرران). التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 6806. برلين، هايدلبرغ: سبرينغر. الصفحات 737-742 . doi : 10.1007/978-3-642-22110-1_59 . ISBN   978-3-642-22110-1.
  20. ↑ "Wasm-mutate: Fuzzing WebAssembly Compilers with E-Graphs (EGRAPHS 2022) - PLDI 2022" . pldi22.sigplan.org . تاريخ الاسترجاع: 3 فبراير 2023 .
  21. ↑ كوارد، صموئيل؛ قسطنطينيدس، جورج أ.؛ درين، ثيو (2022-03-17). "التفسير المجرد على الرسوم البيانية الإلكترونية". arXiv : 2203.09191 [ cs.LO ].كوارد، صموئيل؛ قسطنطينيدس، جورج أ.؛ درين، ثيو (30-05-2022). "دمج الرسوم البيانية الإلكترونية مع التفسير المجرد". arXiv : 2205.14989 [ cs.DS ].
  22. ↑ كاو، ديفيد؛ كونكل، روز؛ ناندي، تشاندراكانا؛ ويلسي، ماكس؛ تاتلوك، زاكاري؛ بوليكاربوفا، ناديا (9 يناير 2023). "ثرثرة: تعلم تجريدات أفضل باستخدام الرسوم البيانية الإلكترونية ومضادة التوحيد". وقائع مؤتمر ACM حول لغات البرمجة . 7 (POPL): 396-424 . arXiv : 2212.04596 . doi : 10.1145/3571207 . ISSN 2475-1421 . S2CID 254536022 .