برمجة الدوال القابلة للحساب

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

في علوم الحاسوب ، تُعرف لغة برمجة الدوال القابلة للحساب ( PCF )، أو البرمجة باستخدام الدوال القابلة للحساب ، أو لغة البرمجة للدوال القابلة للحساب ، بأنها لغة برمجة مُصنفة ومبنية على البرمجة الوظيفية ، وقد قدمها جوردون بلوتكين عام 1977، [ 1 ] استنادًا إلى مواد سابقة غير منشورة لدانا سكوت . [ أ ] ويمكن اعتبارها نسخة موسعة من حساب لامدا المُصنف ، أو نسخة مُبسطة من لغات البرمجة الوظيفية الحديثة المُصنفة مثل ML أو Haskell .

قدّم روبن ميلنر أول نموذج تجريدي كامل لـ PCF . [ 2 ] ومع ذلك، ولأن نموذج ميلنر كان يعتمد أساسًا على بنية PCF، فقد اعتُبر غير مُرضٍ. [ 3 ] وُضِع أول نموذجين تجريديين كاملين لا يعتمدان على البنية خلال تسعينيات القرن الماضي. يعتمد هذان النموذجان على دلالات الألعاب [ 4 ] [ 5 ] وعلاقات كريپكي المنطقية. [ 6 ] لفترة من الزمن، ساد الاعتقاد بأن أيًا من هذين النموذجين غير مُرضٍ تمامًا، نظرًا لعدم إمكانية عرضهما بشكل فعّال. إلا أن رالف لودر أثبت أنه لا يمكن وجود نموذج تجريدي كامل قابل للعرض بشكل فعّال، لأن مسألة تكافؤ البرامج في الجزء النهائي من PCF غير قابلة للحسم. [ 7 ]

بناء الجملة

تُعرَّف أنواع بيانات PCF استقرائيًا على النحو التالي :

  • نات هو نوع
  • بالنسبة للنوعين σ و τ ، يوجد نوع دالة σ → τ

السياق عبارة عن قائمة من الأزواج x : σ ، حيث x اسم متغير و σ نوع، بحيث لا يتكرر أي اسم متغير. ثم تُحدد أحكام تحديد أنواع المصطلحات في السياق بالطريقة المعتادة للبنى النحوية التالية: 

  • المتغيرات (إذا كان x  : σ جزءًا من السياق Γ ، فإن Γ ⊢ x  : σ )
  • تطبيق (مصطلح من النوع σ → τ على مصطلح من النوع σ )
  • تجريد λ
  • مُركِّب النقطة الثابتة Y (يُنشئ حدودًا من النوع σ من حدود من النوع σ → σ )
  • العمليات اللاحقة ( succ ) والسابقة ( pred ) على العدد الطبيعي ( nat ) والثابت 0
  • الشرط if مع قاعدة الكتابة:
Γ⊢ت:نات،Γ⊢s0:σ،Γ⊢s1:σΓ⊢لو(ت،s0،s1):σ{\displaystyle {\frac {\Gamma \;\vdash \;t\;:{\textbf {nat}},\quad \quad \Gamma \;\vdash \;s_{0}\;:\sigma ,\quad \quad \Gamma \;\vdash \;s_{1}\;:\sigma }{\Gamma \;\vdash \;{\textbf {if}}(t,s_{0},s_{1})\;:\sigma }}}
( سيتم تفسير القيم الطبيعية هنا على أنها قيم منطقية، مع وجود اصطلاح مثل الصفر للدلالة على الصواب، وأي رقم آخر للدلالة على الخطأ)

علم الدلالة

الدلالات الدلالية

يُعد نموذج سكوت نموذجًا دلاليًا بسيطًا نسبيًا للغة . في هذا النموذج،

  • يتم تفسير الأنواع على أنها مجالات معينة .
    • [[نات]]:=شمال⊥{\displaystyle [\![{\textbf {nat}}]\!]:=\mathbb {N} _{\bot }}(الأعداد الطبيعية مع عنصر سفلي ملحق بها، مع الترتيب المسطح)
    • [[σ→τ]]{\displaystyle [\![\sigma \to \tau \,]\!]}يُفسَّر على أنه مجال الدوال المتصلة سكوت من[[σ]]{\displaystyle [\![\sigma ]\!]\,}ل[[τ]]{\displaystyle [\![\tau ]\!]\,}، مع الترتيب النقطي.
  • سياقx1:σ1،...،xن:σن{\displaystyle x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}}يُفسر على أنه المنتج[[σ1]]×...×[[σن]]{\displaystyle [\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]}
  • المصطلحات في سياقهاΓ⊢x:σ{\displaystyle \Gamma \;\vdash \;x\;:\;\sigma }تُفسَّر على أنها دوال متصلة[[Γ]]→[[σ]]{\displaystyle [\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]}
    • تُفسَّر المصطلحات المتغيرة على أنها إسقاطات
    • يتم تفسير تجريد وتطبيق لامدا من خلال استخدام البنية المغلقة الديكارتية لفئة المجالات والدوال المتصلة
    • يتم تفسير Y عن طريق أخذ أصغر نقطة ثابتة للوسيط

هذا النموذج ليس مجرداً تماماً بالنسبة للغة PCF؛ ولكنه مجرد تماماً بالنسبة للغة التي تم الحصول عليها بإضافة عامل " أو" متوازٍ إلى PCF. [ 4 ] : ​​293

ملحوظات

  1. ↑ "PCF هي لغة برمجة للوظائف القابلة للحساب، تعتمد على LCF، منطق سكوت للوظائف القابلة للحساب." [ 1 ] تم استخدام برمجة الوظائف القابلة للحساب بواسطة ( ميتشل 1996 ).

مراجع

  1. 1 2 بلوتكين، جوردون د. (ديسمبر 1977). "LCF باعتبارها لغة برمجة" (ملف PDF) . علوم الحاسوب النظرية . 5 (3): 223-255 . doi : 10.1016/0304-3975(77)90044-5 .
  2. ↑ ميلنر، روبن (فبراير 1977). "نماذج مجردة تمامًا لحسابات لامدا المكتوبة" (ملف PDF) . علوم الحاسوب النظرية . 4 (1): 1-22 . doi : 10.1016/0304-3975(77)90053-6 . hdl : 20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1 .
  3. ↑ أونغ، سي.-إتش إل (1995). "التوافق بين الدلالات التشغيلية والدلالات التفسيرية: مشكلة التجريد الكامل لـ PCF" . في: أبرامسكي، إس.؛ غاباي، دي.؛ مايباو، تي إس إي (محررون). دليل المنطق في علوم الحاسوب . مطبعة جامعة أكسفورد. ص 269-356 . مؤرشف من الأصل في 7 يناير 2006. تم الاطلاع عليه في 19 يناير 2006 . 
  4. 1 2 هايلاند، جيه إم إي؛ أونغ، سي إتش إل (15 ديسمبر 2000). "حول التجريد الكامل لـ PCF" . المعلومات والحوسبة . 163 (2): 285-408 . doi : 10.1006/inco.2000.2917 .
  5. ↑ أبرامسكي، س.؛ جاغاديسان، ر.؛ مالاكاريا، ب. (15 ديسمبر 2000). "التجريد الكامل لـ PCF" . المعلومات والحوسبة . 163 (2): 409-470 . doi : 10.1006/inco.2000.2930 .
  6. ↑ أوهيرن، بي دبليو؛ ريكي، جي جي (1995). "علاقات كريپكي المنطقية وPCF" . المعلومات والحوسبة . 120 (1): 107-116 . doi : 10.1006/inco.1995.1103 .
  7. ↑ لودر، ر. (2001). "لا يمكن تحديد PCF المحدود" . علوم الحاسوب النظرية . 266 ( 1-2 ): 341-364 . doi : 10.1016/S0304-3975(00)00194-8 .