هول (مساعد التدقيق)

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

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

تستخدم الأنظمة في عائلة HOL لغة ML أو اللغات اللاحقة لها. طُوّرت لغة ML في الأصل جنبًا إلى جنب مع LCF كلغة وصفية لأنظمة إثبات النظريات؛ في الواقع، يرمز الاسم إلى "اللغة الوصفية".

المنطق الأساسي

تستخدم أنظمة HOL متغيرات من منطق الرتبة العليا الكلاسيكي ، والذي يتميز بأسس بديهية بسيطة مع عدد قليل من البديهيات ودلالات مفهومة جيدًا. [ 1 ]

إن المنطق المستخدم في أدوات إثبات HOL يرتبط ارتباطًا وثيقًا بـ Isabelle/HOL، [ 2 ] وهو المنطق الأكثر استخدامًا في Isabelle .

تطبيقات HOL

لا يزال عدد من أنظمة HOL (التي تشترك في نفس المنطق بشكل أساسي) نشطًا وقيد الاستخدام:

  1. نظام HOL4 هو النظام الوحيد الذي يتم صيانته وتطويره حاليًا والمشتق من نظام HOL88، الذي كان تتويجًا لجهود تنفيذ نظام HOL الأصلي بقيادة مايك جوردون . تضمن نظام HOL88 تطبيقًا خاصًا به للغة ML ، والذي تم تنفيذه بدوره باستخدام لغة Common Lisp . تم تنفيذ جميع الأنظمة التي تلت HOL88 (HOL90 وhol98 وHOL4) باستخدام لغة Standard ML ؛ بينما يرتبط نظام hol98 بلغة Moscow ML ، يمكن بناء نظام HOL4 باستخدام لغة Moscow ML أو Poly/ML . تأتي جميع الأنظمة مزودة بمكتبات ضخمة من أكواد إثبات النظريات التي تُضيف أتمتة إضافية إلى الكود الأساسي البسيط. نظام HOL4 مرخص بموجب ترخيص BSD. [ 3 ]
  2. HOL Light — نسخة تجريبية "مبسطة" من HOL، تطورت لاحقًا لتصبح نسخة شائعة أخرى من HOL؛ ولا تزال أسسها المنطقية بسيطة بشكل غير عادي. HOL Light، التي طُبقت في الأصل بلغة Caml Light ، تستخدم الآن OCaml . HOL Light متاحة بموجب ترخيص BSD الجديد. [ 4 ]
  3. ProofPower هي مجموعة من ست أدوات مصممة لتوفير دعم خاص قائم على لغة HOL للعمل مع ترميز Z للمواصفات الرسمية. وكانت أداة PPDaz، التي تدعم مواصفات البرامج المكتوبة بمجموعة فرعية من لغة Ada والتحقق منها، تُقدم سابقًا بموجب ترخيص احتكاري فقط. أما الآن، فجميع الأدوات متاحة بموجب ترخيص GNU GPL الإصدار الثاني.
  4. HOL Zero — تطبيق بسيط يركز على الموثوقية. HOL Zero مرخص بموجب رخصة جنو العمومية العامة الإصدار 3+. [ 5 ]
  5. Candle — تطبيق HOL Light تم التحقق منه من البداية إلى النهاية على CakeML. [ 6 ]

تطورات البرهان الرسمي

قام مشروع CakeML بتطوير مُصرّف مُثبت رسميًا للغة ML. [ 7 ] سابقًا، تم استخدام HOL لتطوير تطبيق Lisp مُثبت رسميًا يعمل على معالجات ARM و x86 و PowerPC. [ 8 ]

استُخدمت لغة HOL أيضًا لإضفاء الطابع الرسمي على دلالات المعالجات المتعددة x86 [ 9 ] بالإضافة إلى رمز الآلة لبنى Power ISA و ARM . [ 10 ]

مراجع

  1. ↑ أندروز، بيتر ب. (2002). مقدمة في المنطق الرياضي ونظرية الأنواع: إلى الحقيقة من خلال البرهان . سلسلة المنطق التطبيقي. المجلد  27 (  الطبعة الثانية). دوردريخت: دار كلوير للنشر الأكاديمي. ISBN 978-1-4020-0763-7.
  2. ↑ توبياس نيبكو ؛ ماركوس وينزل؛ لورانس سي. بولسون (2002). إيزابيل/هول: مساعد إثبات لمنطق الرتبة العليا . برلين، هايدلبرغ: سبرينغر-فيرلاغ. ISBN 978-3-540-45949-1.
  3. ↑ "HOL Interactive Theorem Prover" .
  4. ↑ "ضوء هول" .
  5. ↑ انظر ملف الترخيص في ملف tarball المؤرشف بتاريخ 2012-03-03 في Wayback Machine .
  6. ↑ أبراهامسون، أوسكار؛ ميرين، ماغنوس أو.؛ ​​كومار، رامانا؛ سيويل، توماس (2022). أندرونيك، جون؛ دي مورا، ليوناردو (محررون). "Candle: تطبيق مُدقَّق لـ HOL Light" . المؤتمر الدولي الثالث عشر حول إثبات النظريات التفاعلي (ITP 2022) . وقائع لايبنيز الدولية في المعلوماتية (LIPIcs). 237. داغشتول، ألمانيا: قصر داغشتول - مركز لايبنيز للمعلوماتية: 3:1–3:17. doi : 10.4230/LIPIcs.ITP.2022.3 . ISBN 978-3-95977-252-5. S2CID 251323103 . 
  7. ↑ "CakeML" .
  8. ↑ ماغنوس أو. ميرين؛ مايكل جيه سي غوردون. تطبيقات LISP الموثقة على ARM و x86 و PowerPC (ملف PDF) . TPHOLs 2009. الصفحات 359-374 . 
  9. ↑ بيتر سيويل؛ سوسميت ساركار؛ سكوت أوينز؛ فرانشيسكو زابا نارديللي؛ ماغنوس أو. ميرين (2010). "x86-TSO: نموذج برمجة دقيق وقابل للاستخدام لمعالجات x86 المتعددة" (ملف PDF) . مجلة اتصالات ACM . 53 (7): 89-97 . doi : 10.1145/1785414.1785443 . S2CID 1999974 . 
  10. ↑ جايد ألغلاف ؛ أنتوني سي جيه فوكس؛ سامين اشتياق؛ ماغنوس أو. ميرين؛ سوسميت ساركار؛ بيتر سيويل؛ فرانشيسكو زابا نارديللي. دلالات الطاقة وشفرة آلة المعالجات المتعددة ARM (ملف PDF) . DAMP 2009. الصفحات 13-24 . 

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