التكرير (تقنية في البرمجة الوظيفية)

في نظرية المجموعات، يُستخدم الترميز ${\displaystyle Y^{X}}$ للدلالة على مجموعة الدوال من المجموعة ${\displaystyle X}$ إلى المجموعة ${\displaystyle Y}$. والتقييس هو تناظر تقابلي طبيعي بين المجموعة ${\displaystyle A^{B\times C}}$ للدوال من ${\displaystyle B\times C}$ إلى ${\displaystyle A}$، والمجموعة ${\displaystyle (A^{C})^{B}}$ للدوال من ${\displaystyle B}$ إلى مجموعة الدوال من ${\displaystyle C}$ إلى ${\displaystyle A}$. بالرموز:

${\displaystyle A^{B\times C}\cong (A^{C})^{B}}$

في الواقع، فإن هذا التناظر الطبيعي هو ما يُبرّر الترميز الرياضي لمجموعة الدوال. وكما هو الحال في جميع أمثلة التقييس، تصف الصيغة أعلاه زوجًا مقترنًا من الدوال المرافقة: لكل مجموعة ثابتة ${\displaystyle C}$، يكون التابع ${\displaystyle B\mapsto B\times C}$ هو المرافق الأيسر للتابع ${\displaystyle A\mapsto A^{C}}$.

في تصنيف المجموعات، يُطلق على كائن رياضي ${\displaystyle Y^{X}}$ اسم كائن أسي.

في نظرية فضاء دالي مثل تحليل دالي أو نظرية التجانس، غالبًا ما يهتم المرء بـدالة مستمرة بين فضاء طوبولوجي. يُكتب ${\displaystyle {\text{Hom}}(X,Y)}$ (أي دالة هوم) للدلالة على مجموعة "جميع" الدوال من ${\displaystyle X}$ إلى ${\displaystyle Y}$، ويُستخدم الترميز ${\displaystyle Y^{X}}$ للإشارة إلى الجزء الفرعي من الدوال المستمرة. هنا، تُعطى دالة ${\displaystyle {\text{curry}}}$ وفق تقابل (دالة):

${\displaystyle {\text{curry}}:{\text{Hom}}(X\times Y,Z)\to {\text{Hom}}(X,{\text{Hom}}(Y,Z)),}$

بينما تكون دالة uncurrying هي المعكوس لهذه الدالة. إذا أُعطيت المجموعة ${\displaystyle Y^{X}}$ من الدوال المستمرة من ${\displaystyle X}$ إلى ${\displaystyle Y}$ طوبولوجيا منفتحة مضغوطة، وكان الفضاء ${\displaystyle Y}$ هاوسدورف موضعيًا مضغوط، فإن:

${\displaystyle {\text{curry}}:Z^{X\times Y}\to (Z^{Y})^{X}}$

تكون تصاكل. ينطبق هذا أيضًا عندما تكون ${\displaystyle X}$ و${\displaystyle Y}$ و${\displaystyle Y^{X}}$ فضاءات مولدة بطريقة مضغوطة^{[17](chapter 5)[18]}، على الرغم من وجود حالات أكثر.^[19][20]

إحدى النتائج المفيدة هي أن الدالة تكون مستمرة إذا وفقط إذا كانت صورتها بطريقة curry مستمرة. نتيجة مهمة أخرى هي أن دالة "التطبيق"، والتي تُعرف عادةً باسم "التقييم" في هذا السياق، تكون مستمرة (لاحظ أن إيفال مفهوم مختلف تمامًا في علوم الحاسوب). أي أن:

${\displaystyle {\begin{aligned}&&{\text{eval}}:Y^{X}\times X\to Y\\&&(f,x)\mapsto f(x)\end{aligned}}}$

هي دالة مستمرة عندما يكون ${\displaystyle Y^{X}}$ بمنفتحة مضغوطة و${\displaystyle Y}$ هاوسدورف موضعيًا مضغوطًا.^[21] هاتان النتيجتان أساسيتان في إثبات استمرارية تحاول، أي عندما يكون ${\displaystyle X}$ هو الفترة الواحدة ${\displaystyle I}$، بحيث يمكن اعتبار ${\displaystyle Z^{I\times Y}\cong (Z^{Y})^{I}}$ إما تحاول بين دالتين من ${\displaystyle Y}$ إلى ${\displaystyle Z}$، أو مسارًا مستمرًا في ${\displaystyle Z^{Y}}$.

في طوبولوجيا جبرية، تُعد currying مثالًا على تطابق إيكمان–هيلتون، ولذلك تلعب دورًا مهمًا في سياقات متنوعة. على سبيل المثال، فضاء العقد هو المرافق لتعليق مختزل، ويُكتب عادة:

${\displaystyle [\Sigma X,Z]\approxeq [X,\Omega Z]}$

حيث ${\displaystyle [A,B]}$ هي مجموعة تحاول بين الدوال ${\displaystyle A\rightarrow B}$، و${\displaystyle \Sigma A}$ هو تعليق لـ"A"، و${\displaystyle \Omega A}$ هو فضاء العقد لـ"A". من حيث الجوهر، يمكن اعتبار التعليق ${\displaystyle \Sigma X}$ كحاصل الضرب الكارتيزي لـ${\displaystyle X}$ مع الفترة الواحدة، مع معاملته بعلاقة تكافؤ لتحويل الفترة إلى حلقة. الصورة بواسطة curry تربط الفضاء ${\displaystyle X}$ إلى فضاء الدوال من الحلقات إلى ${\displaystyle Z}$، أي من ${\displaystyle X}$ إلى ${\displaystyle \Omega Z}$.^[21] وبالتالي، فإن ${\displaystyle {\text{curry}}}$ هو دالة مرافق تربط التعليقات بفضاءات العقد، وuncurrying هو النظير لها.^[21]

يمكن فهم الازدواجية بين مخروط التضمين وألياف التضمين (أي إدراج وإسقاط)^{[17](chapters 6,7)} كشكل من أشكال curry، مما يؤدي بدوره إلى الازدواجية بين متتالية منضبطة ومتتاليات بوبي العكسية.

في الجبر التماثلي، تُعرف العلاقة بين curry وuncurry باسم مرافقة الجداء التنسوري والدالة هوم، حيث تظهر ظاهرة مثيرة للاهتمام: قد لا تُرفع دالة هوم ودالة جداء موتر إلى متتالية منضبطة؛ ما يؤدي إلى تعريف دالة إكست ودالة تور.

في نظرية الترتيب، أي نظرية شبكة لمجموعة مرتبة جزئيًا، تكون ${\displaystyle {\text{curry}}}$ دالة مستمرة عندما تُزود الشبكة بطوبولوجيا سكوت.^[22] لقد دُرست الدوال المستمرة وفق سكوت في البداية كجزء من محاولة لإيجاد دلالات لـتكامل لامدا (نظرًا لعدم كفاية نظرية المجموعات العادية لذلك). بشكل أعم، تُدرس هذه الدوال في نظرية المجالات، التي تشمل دراسة الدلالات التصويرية لخوارزميات الحاسوب. لاحظ أن طوبولوجيا سكوت تختلف كثيرًا عن العديد من الطوبولوجيات الشائعة في فئة الفضاءات الطوبولوجية؛ فهي عادةً ما تكون أدق، وليست فضاء رصين.

في علم الحاسوب النظري، يوفر الكرّيان وسيلة لدراسة الدوال متعددة الوسائط ضمن نماذج نظرية بسيطة جدًا، مثل حساب لامبدا، حيث تأخذ الدوال وسيطًا واحدًا فقط. لنفترض وجود دالة ${\displaystyle f(x,y)}$ تأخذ وسيطين وتملك النوع ${\displaystyle (X\times Y)\to Z}$، مما يعني أن x يجب أن يكون من النوع ${\displaystyle X}$، وy من النوع ${\displaystyle Y}$، بينما تُرجع الدالة نفسها قيمة من النوع ${\displaystyle Z}$. الشكل المُكرّى للدالة f يُعرّف على النحو التالي:

${\displaystyle {\text{curry}}(f)=\lambda x.(\lambda y.(f(x,y)))}$

حيث ${\displaystyle \lambda }$ هو معامل التجريد في حساب لامبدا. وبما أن الكرّيان يأخذ كمدخل دوال من النوع ${\displaystyle (X\times Y)\to Z}$، فإن نوع الكرّيان ذاته يُستنتج كالتالي:

${\displaystyle {\text{curry}}:((X\times Y)\to Z)\to (X\to (Y\to Z))}$

عادةً ما يُعتبر معامل ${\displaystyle \to }$ تجميعيًا إلى اليمين، لذلك يُكتب النوع ${\displaystyle X\to (Y\to Z)}$ غالبًا بصيغة مختصرة ${\displaystyle X\to Y\to Z}$. وبالمقابل، فإن تطبيق الدالة يُعتبر تجميعيًا إلى اليسار، لذا فإن التعبير ${\displaystyle f(x,y)}$ يعادل:

${\displaystyle (({\text{curry}}(f)\;x)\;y)={\text{curry}}(f)\;x\;y}$.

أي أن الأقواس ليست ضرورية لتوضيح ترتيب التطبيق.

يمكن استخدام الدوال المُكرّاة في أي لغة برمجة تدعم الإغلاق. ومع ذلك، غالبًا ما تُفضّل الدوال غير المُكرّاة لأسباب تتعلق بالكفاءة، إذ يمكن تجنب تكلفة التطبيق الجزئي وإنشاء الإغلاقات في معظم استدعاءات الدوال.

في نظرية النمط، يتم تنظيم الفكرة العامة لنظام الأنواع في علم الحاسوب ضمن جبر محدد للأنواع. فعلى سبيل المثال، عند كتابة ${\displaystyle f\colon X\to Y}$، فإن المقصود أن ${\displaystyle X}$ و${\displaystyle Y}$ هما أنواع، بينما السهم ${\displaystyle \to }$ هو منشئ نوع، وبشكل خاص، يمثل نوع الدالة أو نوع السهم. وبالمثل، فإن حاصل الضرب الديكارتي ${\displaystyle X\times Y}$ للأنواع يُنشأ بواسطة منشئ نوع الضرب ${\displaystyle \times }$.

يُعبَّر عن هذا النهج النمطي في لغات برمجة مثل إم إل واللغات المتفرعة منها أو المتأثرة بها مثل كامل وهاسكل، وإف.

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

بموجب تطابق كاري-هوارد، فإن وجود الكرّيان واللاكرّيان يعادل النظريّة المنطقية ${\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}$ (والمعروفة أيضًا باسم التصدير)، إذ إن النوع الضربي (بالإنجليزية: product type) يُقابل اقترانًا منطقيًا، ونوع الدالة يُقابل الاقتضاء.

في فئة جبر هايتنغ، يُكتب الكائن الأسي ${\displaystyle Q^{P}}$ عادةً على شكل اقتضاء منطقي ${\displaystyle P\to Q}$. وتُعد الجبرات التوزيعية من نوع هايتنغ جبور بولية، ويأخذ الكائن الأسي فيها الشكل الصريح ${\displaystyle \neg P\lor Q}$، مما يُبرز أن الكائن الأسي يُمثّل في الحقيقة الاقتضاء المادي. ^[23]

تجد مفاهيم الكرّيان واللاكرّيان أوضح تعبيراتها العامة والمجردة في نظرية الفئات. يُعدّ الكرّيان خاصية شاملة للكائن الأسي (كائن أسي)، وينتج عنه اقتران في الفئات المغلقة الديكارتية. أي أن هناك تماكل طبيعي (تحويل طبيعي) بين التشاكلات من الجداء الثنائي ${\displaystyle f\colon (X\times Y)\to Z}$ والتشاكلات إلى كائن أسي ${\displaystyle g\colon X\to Z^{Y}}$.

ويُعمّم هذا على نتيجة أوسع في فئة مغلقة أحادية: يُمثّل الكرّيان القول إن الجداء التوتري (جداء الفئة الأحادية) والهوم الداخلي هما دوال مراعية مقترنة؛ أي أن لكل كائن ${\displaystyle B}$ يوجد تماثل طبيعي على النحو الآتي:

${\displaystyle \mathrm {Hom} (A\otimes B,C)\cong \mathrm {Hom} (A,B\Rightarrow C).}$

حيث يُشير "هوم" إلى الدالة المراعية (الخارجية) التي تجمع جميع التشاكلات في الفئة، في حين يُمثل ${\displaystyle B\Rightarrow C}$ الهوم الداخلي في الفئة المغلقة الأحادية. في فئة المجموعات، يتطابق الاثنان. وعندما يكون الجداء هو الجداء الديكارتي، يصبح الهوم الداخلي ${\displaystyle B\Rightarrow C}$ هو الكائن الأسي ${\displaystyle C^{B}}$.

قد يفشل الكرّيان في حالتين. الأولى، إذا لم تكن الفئة مغلقة، وبالتالي تفتقر إلى دالة هوم داخلية (ربما لوجود أكثر من خيار ممكن لهذه الدالة). والثانية، إذا لم تكن أحادية، أي أنها تفتقر إلى جداء (أي لا يوجد بها طريقة لتكوين أزواج من الكائنات). الفئات التي تمتلك كلاً من الجداءات والهومات الداخلية هي بالضبط الفئات المغلقة الأحادية.

يُعد إطار الفئات المغلقة الديكارتية كافيًا لمناقشة المنطق الكلاسيكي؛ أما الإطار العام للفئات المغلقة الأحادية فهو مناسب لـ الحوسبة الكمومية.^[24]

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

وعلى النقيض، فإن الجداء في الفئات الأحادية (مثل فضاء هيلبرت أو الفضاءات المتجهية في التحليل الدالي) هو جداء موتر. وتُعد المنطق الخطي هو اللغة الداخلية لهذه الفئات، وهي أحد أشكال المنطق الكمومي؛ ويُقابلها نظام الأنواع الخطي. تُستخدم هذه الفئات في توصيف التشابك الكمومي، كما تسمح — على نحو أوسع — بتعميم واسع لـ تطابق كاري-هوارد إلى ميكانيكا الكم، والمتعددات الحدية في الطوبولوجيا الجبرية، ونظرية الأوتار.^[3]