اثنا عشر

الموسوعة الحرة

Twelf هو تطبيق للإطار المنطقي LF الذي طوره فرانك بفينينغ وكارستن شورمان في جامعة كارنيجي ميلون . [ 1 ] ويستخدم في البرمجة المنطقية وفي صياغة نظرية لغات البرمجة .

مقدمة

في أبسط صورها، برنامج Twelf (يُسمى "توقيعًا") عبارة عن مجموعة من تعريفات عائلات الأنواع (العلاقات) والثوابت التي تنتمي إلى تلك العائلات. على سبيل المثال، فيما يلي التعريف القياسي للأعداد الطبيعية، حيث zيرمز إلى الصفر، و sإلى عامل التتابع.

nat : type .z : nat . s : nat -> nat .

هذا natنوع، و zو sمصطلحات ثابتة. وباعتباره نظامًا يعتمد على الأنواع ، يمكن فهرسة الأنواع بواسطة المصطلحات، مما يسمح بتعريف عائلات أنواع أكثر تعقيدًا. إليك تعريف الجمع:

بالإضافة إلى : nat -> nat -> nat -> اكتب .plus_zero : { M: nat } plus M z M .plus_succ : { M: nat } { N: nat } { P: nat } plus M ( s N ) ( s P ) <- plus M N P .

تُقرأ عائلة الأنواع plusكعلاقة بين ثلاثة أعداد طبيعية M، Nو ، و P، بحيث يكون M + N = P. ثم نُعطي الثوابت التي تُعرّف العلاقة: plus_zeroيُشير الثابت إلى أن M + 0 = M. ويمكن قراءة المُكمِّم {M:nat}على أنه "لكل Mمن النوع nat".

يُحدد الثابت plus_succالحالة التي يكون فيها الوسيط الثاني هو العدد التالي لعدد آخر N(انظر مطابقة الأنماط ). والنتيجة هي العدد التالي لـ P، حيث Pيُمثل مجموع Mو . يتم Nهذا الاستدعاء التكراريplus M N P عبر الهدف الفرعي ، الذي تم تقديمه باستخدام <-. يمكن فهم السهم عمليًا على أنه في لغة برولوج :-، أو كاستلال منطقي ("إذا كان M + N = P، فإن M + (s N) = (s P)")، أو بشكل أدق وفقًا لنظرية الأنواع، كنوع الثابت plus_succ("عند إعطاء حد من النوع plus M N P، يتم إرجاع حد من النوع plus M (s N) (s P)").

تتميز Twelf بإعادة بناء النوع وتدعم المعلمات الضمنية، لذلك عمليًا، لا يحتاج المرء عادةً إلى كتابة {M:nat}(إلخ) أعلاه بشكل صريح.

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

الاستخدامات

البرمجة المنطقية

يمكن تنفيذ توقيعات Twelf عبر إجراء بحث. جوهرها أكثر تعقيدًا من Prolog ، نظرًا لكونها لغة من الرتبة العليا وذات أنواع تابعة، لكنها تقتصر على المعاملات البحتة: لا يوجد فيها قطع أو معاملات غير منطقية أخرى (مثل تلك المستخدمة في عمليات الإدخال /الإخراج ) كما هو شائع في تطبيقات Prolog، مما قد يجعلها أقل ملاءمة لتطبيقات البرمجة المنطقية العملية. يمكن الاستفادة من بعض قواعد القطع في Prolog من خلال تعريف انتماء معاملات معينة إلى عائلات أنواع حتمية، مما يجنب إعادة الحساب. كذلك، وكما هو الحال في λProlog ، تعمم Twelf عبارات Horn إلى صيغ Harrop الوراثية ، مما يسمح بمفاهيم تشغيلية منطقية راسخة لتوليد أسماء جديدة وتوسيع نطاق قاعدة بيانات العبارات.

إضفاء الطابع الرسمي على الرياضيات

يُستخدم نظام Twelf اليوم بشكل أساسي لصياغة الرياضيات، وخاصةً نظرية ما وراء لغات البرمجة . ولذلك، فهو يرتبط ارتباطًا وثيقًا بنظامي Rocq و Isabelle / HOL / HOL Light . مع ذلك، وعلى عكس تلك الأنظمة، تُطوَّر براهين Twelf عادةً يدويًا. على الرغم من ذلك، بالنسبة لمجالات المسائل التي يتفوق فيها، غالبًا ما تكون براهين Twelf أقصر وأسهل في التطوير من تلك الموجودة في الأنظمة الآلية ذات الأغراض العامة.

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

استُخدمت لغة Twelf لصياغة العديد من المنطق ولغات البرمجة المختلفة (تُرفق أمثلة مع التوزيعة). ومن بين المشاريع الأكبر حجماً: برهان أمان لغة Standard ML ، [ 2 ] ونظام لغة تجميع أساسي مُنمّط من جامعة كارنيجي ميلون، [ 3 ] ونظام أساسي لإثبات الشفرة من جامعة برينستون.

تطبيق

برنامج Twelf مكتوب بلغة Standard ML، وتتوفر ملفات تنفيذية لأنظمة Linux وWindows. اعتبارًا من عام 2006وهي قيد التطوير النشط، ومعظمها في جامعة كارنيجي ميلون.

انظر أيضاً

مراجع

  1. ↑ بفينينغ، فرانك؛ كارستن شورمان (يوليو 1999). وصف النظام: Twelf - إطار عمل منطقي شامل للأنظمة الاستنتاجية (ملف PDF) . وقائع المؤتمر الدولي السادس عشر حول الاستدلال الآلي (CADE-16) . تاريخ الاسترجاع: 8 مايو 2019 .
  2. ↑ لي، دانيال؛ كارل كراري؛ روبرت هاربر (يناير 2007). نحو نظرية ميتافيزيقية آلية للغة ML القياسية (ملف PDF) . وقائع ندوة 2007 حول مبادئ لغات البرمجة . نيس ، فرنسا . تاريخ الاسترجاع: 8 فبراير 2007 .
  3. ↑ كراري، كارل (2003). نحو لغة تجميع أساسية مكتوبة (ملف PDF) . وقائع ندوة 2003 حول مبادئ لغات البرمجة . تم الاطلاع عليه بتاريخ 8 فبراير 2007 .