النظام F

النظام F (ويُعرف أيضًا بحساب لامدا متعدد الأشكال أو حساب لامدا من الدرجة الثانية ) هو حساب لامدا مُنمّط يُضيف إلى حساب لامدا المُنمّط ببساطة آليةً للتكميم الشامل على الأنواع. يُضفي النظام F طابعًا رسميًا على تعدد الأشكال البارامتري في لغات البرمجة ، مُشكلاً بذلك أساسًا نظريًا للغات مثل هاسكل و ML . وقد اكتشفه بشكل مستقل كلٌ من عالم المنطق جان إيف جيرار (1972) وعالم الحاسوب جون سي. رينولدز .

بينما تحتوي حسابات لامدا المكتوبة ببساطة على متغيرات تتراوح بين الحدود، وروابط لها، فإن نظام F يحتوي أيضًا على متغيرات تتراوح بين الأنواع ، وروابط لها. على سبيل المثال، حقيقة أن دالة الهوية يمكن أن يكون لها أي نوع من الشكل A → A سيتم صياغتها رسميًا في نظام F على النحو التالي:

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }$

أين${\displaystyle \alpha }$هو متغير نوع . الحرف الكبير${\displaystyle \Lambda }$يُستخدم تقليديًا للدلالة على الدوال على مستوى النوع، على عكس الأحرف الصغيرة.${\displaystyle \lambda }$والتي تُستخدم لوظائف مستوى القيمة. (الرمز المرتفع)${\displaystyle \alpha }$هذا يعني أن المتغير المقيد x من النوع${\displaystyle \alpha }$; التعبير الذي يلي النقطتين هو نوع تعبير لامدا الذي يسبقه.)

باعتباره نظامًا لإعادة كتابة المصطلحات ، يتميز النظام F بتطبيع قوي . مع ذلك، فإن استنتاج النوع في النظام F (بدون تحديدات صريحة للنوع) غير قابل للتقرير . في ظل تماثل كاري-هوارد ، يتوافق النظام F مع منطق الحدس الافتراضي من الدرجة الثانية . يمكن اعتبار النظام F جزءًا من مكعب لامدا ، إلى جانب حسابات لامدا ذات أنواع أكثر تعبيرًا، بما في ذلك تلك التي تحتوي على أنواع تابعة .

بحسب جيرارد، تم اختيار حرف "F" في System F بالصدفة. ^{[ 1 ]}

قواعد كتابة نظام F هي قواعد حساب التفاضل والتكامل اللامدا المكتوب ببساطة مع إضافة ما يلي:

${\displaystyle {\frac {\Gamma \vdash M:\forall \alpha .\sigma }{\Gamma \vdash M\tau$ :\سيجما [\تاو /\alpha ]}}} (1)

${\displaystyle {\frac {\Gamma ,\alpha ~{\text{type}}\vdash M:\sigma }{\Gamma \vdash \Lambda \alpha .M:\forall \alpha .\sigma }}}$(2)

أين${\displaystyle \sigma ,\tau }$هي أنواع،${\displaystyle \alpha }$هو متغير نوع، و${\displaystyle \alpha ~{\text{type}}}$يشير السياق إلى أن${\displaystyle \alpha }$مُلزم. القاعدة الأولى هي قاعدة التطبيق، والثانية هي قاعدة التجريد. ^{[ 2 ] [ 3 ]}

ال${\displaystyle {\mathsf {Boolean}}}$يُعرَّف النوع على النحو التالي: ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$، أين${\displaystyle \alpha }$هو متغير نوعي . وهذا يعني:${\displaystyle {\mathsf {Boolean}}}$هو نوع جميع الدوال التي تأخذ كمدخلات نوعًا α وتعبيرين من النوع α ، وتنتج كمخرجات تعبيرًا من النوع α (لاحظ أننا نعتبر${\displaystyle \to }$أن يكون ارتباطيًا يمينيًا .)

التعريفان التاليان للقيم المنطقية${\displaystyle \mathbf {T} }$و${\displaystyle \mathbf {F} }$تُستخدم، مما يوسع تعريف العمليات المنطقية للكنيسة :

${\displaystyle \mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x}$

${\displaystyle \mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y}$

(لاحظ أن الدالتين المذكورتين أعلاه تتطلبان ثلاثة وسائط - وليس اثنين . يجب أن يكون الوسيطان الأخيران تعبيرات لامدا، بينما يجب أن يكون الوسيط الأول نوعًا. وينعكس هذا في كون نوع هذه التعبيرات هو${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$؛ يُقابل المُكمِّم العام الذي يربط α المُكمِّم Λ الذي يربط α في تعبير لامدا نفسه. لاحظ أيضًا أن${\displaystyle {\mathsf {Boolean}}}$هو اختصار مناسب لـ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$لكنها ليست رمزًا للنظام F نفسه، بل هي بالأحرى "رمز فوقي". وبالمثل،${\displaystyle \mathbf {T} }$و${\displaystyle \mathbf {F} }$وهي أيضًا "رموز فوقية"، اختصارات ملائمة، لـ "تجميعات" النظام F (بمعنى بورباكي )؛ وإلا، إذا كان من الممكن تسمية هذه الوظائف (داخل النظام F)، فلن تكون هناك حاجة إلى جهاز التعبير عن لامدا القادر على تعريف الوظائف بشكل مجهول، ولا إلى مُركِّب النقطة الثابتة ، الذي يتجاوز هذا القيد.

ثم، مع هذين الاثنين${\displaystyle \lambda }$- من حيث، يمكننا تعريف بعض عوامل التشغيل المنطقية (التي هي من النوع${\displaystyle {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}}$):

${\displaystyle {\begin{align}\mathrm {AND} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,y\,\mathbf {F} \\\mathrm {OR} &=\lambda x^{\mathsf {منطقية}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {T} \,y\\\mathrm {NOT} &=\lambda x^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {F} \,\mathbf {T} \end{محاذاة}}}$

لاحظ أنه في التعريفات أعلاه،${\displaystyle {\mathsf {Boolean}}}$هو وسيط نوع لـ${\displaystyle x}$، مع تحديد أن المعلمتين الأخريين اللتين يتم إعطاؤهما لـ${\displaystyle x}$هي من النوع${\displaystyle {\mathsf {Boolean}}}$كما هو الحال في ترميزات الكنيسة، لا حاجة لدالة IFTHENELSE حيث يمكن استخدام البيانات الخام مباشرةً.${\displaystyle {\mathsf {Boolean}}}$المصطلحات المصنفة كدوال قرار. ومع ذلك، إذا طُلب أحدها:

${\displaystyle \mathrm {IFTHENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Boolean}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz}$

حسنًا. الدالة الشرطية هي دالة تُرجع${\displaystyle {\mathsf {Boolean}}}$القيمة المحددة النوع. أهم دالة أساسية هي ISZERO التي تُرجع${\displaystyle \mathbf {T} }$إذا وفقط إذا كانت وسيطتها هي الرقم الكنسي 0 :

${\displaystyle \mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\,(\lambda x^{\mathsf {Boolean}}{.}\mathbf {F} )\,\mathbf {T} }$

علاوة على ذلك، يمكن تنفيذ المُكمِّم الوجودي (وبالتالي الأنواع الوجودية) في النظام F على النحو التالي: ^{[ 4 ] [ 5 ]}

${\displaystyle \exists X.A=\forall Y.(\forall X.A\rightarrow Y)\rightarrow Y}$

يُتيح النظام F تضمين البنى التكرارية بطريقة طبيعية، على غرار نظرية مارتن-لوف للأنواع . تُنشأ البنى المجردة ( S ) باستخدام الدوال البانية . وهي دوال مُصنفة على النحو التالي:

${\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}$.

تتجلى الخاصية التكرارية عندما يظهر S نفسه ضمن أحد الأنواع${\displaystyle K_{i}}$إذا كان لديك m من هذه المُنشئات، فيمكنك تعريف نوع S على النحو التالي:

${\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha }$

على سبيل المثال، يمكن تعريف الأعداد الطبيعية كنوع بيانات استقرائي N مع مُنشئات

${\displaystyle {\begin{aligned}{\mathit {zero}}&:\mathrm {N} \\{\mathit {succ}}&:\mathrm {N} \rightarrow \mathrm {N} \end{aligned}}}$

نوع النظام F المقابل لهذا الهيكل هو ${\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$تتضمن المصطلحات من هذا النوع نسخة مطبوعة من أرقام الكنيسة ، وأولى هذه المصطلحات هي:

${\displaystyle {\begin{aligned}0&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x\\1&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx\\2&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)\\3&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))\end{aligned}}}$

إذا عكسنا ترتيب الحجج المُدمجة ( أي،${\displaystyle \forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }$إذا كان لدينا عددان من نوع Church، فإن العدد n هو دالة تأخذ دالة f كمعامل وتعيد القوة النونية لـ f ^. أي أن العدد Church هو دالة من الرتبة العليا - فهو يأخذ دالة ذات معامل واحد f ، ويعيد دالة أخرى ذات معامل واحد.

يُستخدم في هذه المقالة نظام F بصيغة حسابية صريحة النوع، أو ما يُعرف بحساب تشيرش. وتُسهّل معلومات النوع المُضمنة في حدود λ عملية التحقق من النوع . وقد حسم جو ويلز (1994) "مشكلة مفتوحة مُحرجة" بإثبات أن التحقق من النوع غير قابل للتقرير بالنسبة لمتغير من نظام F بنمط كاري، أي المتغير الذي يفتقر إلى تعليقات النوع الصريحة. ^{[ 6 ] [ 7 ]}

تشير نتيجة ويلز إلى استحالة استنتاج النوع في النظام F. يوجد قيد على النظام F يُعرف باسم " هيندلي-ميلنر " أو اختصارًا "HM"، ويحتوي على خوارزمية سهلة لاستنتاج النوع، ويُستخدم في العديد من لغات البرمجة الوظيفية ذات الأنواع الثابتة ، مثل هاسكل 98 وعائلة لغات ML . مع مرور الوقت، ومع اتضاح قيود أنظمة الأنواع من نمط HM، اتجهت اللغات تدريجيًا نحو منطق أكثر تعبيرًا لأنظمة أنواعها. يتجاوز مُصرّف GHC ، وهو مُصرّف للغة هاسكل، نمط HM (حتى عام 2008) ويستخدم النظام F المُوسّع بمساواة الأنواع غير النحوية؛ ^{[ 8 ]} وتشمل ميزات نظام أنواع OCaml غير HM، GADT . ^{[ 9 ] [ 10 ]}

في منطق الحدس من الرتبة الثانية ، اكتشف جيرارد (1972) حساب لامدا متعدد الأشكال من الرتبة الثانية (F2)، ثم اكتشفه رينولدز (1974) بشكل مستقل. ^{[ 11 ]} أثبت جيرارد نظرية التمثيل : أنه في منطق المسندات الحدسي من الرتبة الثانية (P2)، تشكل الدوال من الأعداد الطبيعية إلى الأعداد الطبيعية التي يمكن إثبات كليتها، إسقاطًا من P2 إلى F2. ^{[ 11 ]} أثبت رينولدز نظرية التجريد : أن كل حد في F2 يحقق علاقة منطقية، يمكن تضمينها في العلاقات المنطقية P2. ^{[ 11 ]} أثبت رينولدز أن إسقاط جيرارد متبوعًا بتضمين رينولدز يشكلان التطابق، أي تماثل جيرارد-رينولدز . ^{[ 11 ]}

بينما يتوافق النظام F مع المحور الأول لمكعب لامدا لباريندريخت ، فإن النظام F _ω أو حساب لامدا متعدد الأشكال من الدرجة الأعلى يجمع بين المحور الأول (تعدد الأشكال) مع المحور الثاني ( عوامل النوع )؛ إنه نظام مختلف وأكثر تعقيدًا.

يمكن تعريف النظام F _ω استقرائياً على مجموعة من الأنظمة، حيث يعتمد الاستقراء على الأنواع المسموح بها في كل نظام:

• ${\displaystyle F_{n}}$أنواع التصاريح:
  • ${\displaystyle \star }$(أنواع الأنواع) و
  • ${\displaystyle J\Rightarrow K}$أين${\displaystyle J\in F_{n-1}}$و${\displaystyle K\in F_{n}}$(نوع الدوال من أنواع إلى أنواع، حيث يكون نوع الوسيط من رتبة أدنى)

في النهاية، يمكننا تعريف النظام${\displaystyle F_{\omega }}$يكون

• ${\displaystyle F_{\omega }={\underset {1\leq i}{\bigcup }}F_{i}}$

أي أن F _ω هو النظام الذي يسمح للدوال من أنواع إلى أنواع حيث يمكن أن يكون الوسيط (والنتيجة) من أي رتبة.

لاحظ أنه على الرغم من أن F _ω لا يفرض أي قيود على ترتيب الوسائط في هذه التعيينات، إلا أنه يقيد نطاق الوسائط لهذه التعيينات: يجب أن تكون أنواعًا وليست قيمًا. لا يسمح النظام F _{ω بالتعيينات من القيم إلى الأنواع (} الأنواع التابعة )، على الرغم من أنه يسمح بالتعيينات من القيم إلى القيم (${\displaystyle \lambda }$التجريد)، والتحويلات من الأنواع إلى القيم (${\displaystyle \Lambda }$التجريد)، والتحويلات من أنواع إلى أنواع (${\displaystyle \lambda }$التجريد على مستوى الأنواع).

نظام F _{< :} ، الذي يُنطق "إف-ساب"، هو امتداد لنظام F مع خاصية التنميط الفرعي . وقد حظي نظام F _{< : بأهمية مركزية في} نظرية لغات البرمجة منذ ثمانينيات القرن الماضي، لأن جوهر لغات البرمجة الوظيفية ، مثل تلك الموجودة في عائلة ML ، يدعم كلاً من تعدد الأشكال البارامتري والتنميط الفرعي للسجلات ، والذي يمكن التعبير عنه في نظام F _{< :} . ^{[ 12 ] [ 13 ]}

• الأنواع الوجودية - النظائر الكمية الوجودية للأنواع العالمية
• نظام يو
• مكعب لامدا

• بيرس، بنيامين (2002). "تعدد الأشكال V، الفصل 23: الأنواع العامة، الفصل 25: تطبيق ML لنظام F" . الأنواع ولغات البرمجة . مطبعة معهد ماساتشوستس للتكنولوجيا. الصفحات 339-362 ، 381-388 . ISBN  0-262-16209-1.

• ملخص كتاب "النظام F" لفرانك بينارد.
• نظام F _ω : العمود الفقري للمترجمات الحديثة بقلم جريج موريسيت