الكاري

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

في الرياضيات وعلوم الحاسوب ، يعتبر التكييف الجزئي أسلوبًا لترجمة دالة تأخذ وسائط متعددة إلى سلسلة من عائلات الدوال، كل منها يأخذ وسيطًا واحدًا.

في المثال النموذجي، يبدأ المرء بدالةو:(X×Y)→Z{\displaystyle f:(X\times Y)\to Z}يتطلب ذلك وسيطين، أحدهما منX{\displaystyle X}وواحد منY،{\displaystyle Y,}وينتج أشياء فيZ.{\displaystyle Z.}تتعامل الصيغة المعدلة لهذه الدالة مع الوسيط الأول كمعامل، وذلك لإنشاء مجموعة من الدوالوx:Y→Z.{\displaystyle f_{x}:Y\to Z.}تم ترتيب العائلة بحيث يكون لكل عنصرx{\displaystyle x}فيX،{\displaystyle X,}هناك وظيفة واحدة فقطوx{\displaystyle f_{x}}بحيث يكون لأيy{\displaystyle y}فيY{\displaystyle Y}،وx(y)=و(x،y){\displaystyle f_{x}(y)=f(x,y)}.

في هذا المثال،كاري{\displaystyle {\mbox{curry}}}تصبح هي نفسها دالة تأخذو{\displaystyle f}كوسيط، ويعيد دالة تقوم بتعيين كلx{\displaystyle x}لوx.{\displaystyle f_{x}.}إنّ الصيغة الصحيحة للتعبير عن هذا هي صيغة مطوّلة. الدالةو{\displaystyle f}ينتمي إلى مجموعة الدوال(X×Y)→Z.{\displaystyle (X\times Y)\to Z.} في أثناء،وx{\displaystyle f_{x}}ينتمي إلى مجموعة الدوالY→Z.{\displaystyle Y\to Z.}وبالتالي، شيء يرسم الخرائطx{\displaystyle x}لوx{\displaystyle f_{x}}سيكون من النوعX→[Y→Z].{\displaystyle X\to [Y\to Z].}باستخدام هذه الصيغة،كاري{\displaystyle {\mbox{curry}}}هي دالة تأخذ عناصر من المجموعة الأولى، وتعيد عناصر من المجموعة الثانية، وهكذا يكتب المرءكاري:[(X×Y)→Z]→(X→[Y→Z]).{\displaystyle {\mbox{curry}}:[(X\times Y)\to Z]\to (X\to [Y\to Z]).}هذا مثال غير رسمي إلى حد ما؛ ترد أدناه تعريفات أكثر دقة لما يُقصد بـ "الشيء" و"الوظيفة". وتختلف هذه التعريفات باختلاف السياق، وتتخذ أشكالاً مختلفة تبعاً للنظرية المتبعة.

تُعدّ عملية التخصيص الجزئي (Currying) مرتبطةً بالتطبيق الجزئي (Partical Application) ، ولكنها ليست مرادفةً له . [ 1 ] [ 2 ] يمكن استخدام المثال أعلاه لتوضيح التطبيق الجزئي؛ فهو مشابهٌ له إلى حدٍ كبير. التطبيق الجزئي هو الدالةيتقدم{\displaystyle {\mbox{apply}}}هذا يأخذ الزوجينو{\displaystyle f}وx{\displaystyle x}معًا كحجج، والعائداتوx.{\displaystyle f_{x}.}باستخدام نفس الترميز المذكور أعلاه، فإن التطبيق الجزئي له التوقيع التالييتقدم:([(X×Y)→Z]×X)→[Y→Z].{\displaystyle {\mbox{apply}}:([(X\times Y)\to Z]\times X)\to [Y\to Z].}بهذه الطريقة، يمكن اعتبار التطبيق مكملاً لعملية الكاري.

يمكن تعريف عملية تطبيق دالة ذات أكثر من وسيطين باستخدام الاستقراء.

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

طُرح مفهوم الكاري من قِبل غوتلوب فريجه ، [ 4 ] [ 5 ] وطوّره موسى شونفينكل ، [ 6 ] [ 5 ] [ 7 ] [ 8 ] [ 9 ] [ 10 ] [ 11 ] ثمّ طوّره هاسكل كاري . [ 8 ] [ 10 ] [ 12 ] [ 13 ]

يُعدّ إلغاء التقسيم الوظيفي (Uncurrying) التحويل المزدوج للتقسيم الوظيفي، ويمكن اعتباره شكلاً من أشكال إلغاء الوظيفة . فهو يأخذ وظيفةو{\displaystyle f}والتي تكون قيمتها المُعادة دالة أخرىز{\displaystyle g}، وينتج عنه دالة جديدةو′{\displaystyle f'}يأخذ ذلك كمعاملات وسيطات كليهماو{\displaystyle f}وز{\displaystyle g}، ويعيد، نتيجة لذلك، تطبيقو{\displaystyle f}وبعد ذلك،ز{\displaystyle g}بالنسبة لتلك الحجج. يمكن تكرار العملية.

تحفيز

يُتيح تطبيق تقنية "التقسيم الجزئي" (Currying) التعامل مع الدوال التي تأخذ وسائط متعددة، واستخدامها في أطر عمل قد لا تأخذ فيها الدوال سوى وسيط واحد. على سبيل المثال، لا يمكن تطبيق بعض التقنيات التحليلية إلا على الدوال ذات الوسيط الواحد. بينما غالبًا ما تأخذ الدوال العملية وسائط أكثر من ذلك. وقد بيّن فريجه أنه يكفي تقديم حلول لحالة الوسيط الواحد، إذ يُمكن تحويل الدالة ذات الوسائط المتعددة إلى سلسلة من الدوال ذات الوسيط الواحد. هذا التحويل هو العملية المعروفة الآن باسم "التقسيم الجزئي". [ 14 ] يُمكن تطبيق تقنية التقسيم الجزئي على جميع الدوال "العادية" التي قد تُصادف عادةً في التحليل الرياضي أو في برمجة الحاسوب . مع ذلك، توجد فئات لا يُمكن فيها تطبيق هذه التقنية؛ وأكثر الفئات عمومية التي تسمح بها هي الفئات الأحادية المغلقة .

تستخدم بعض لغات البرمجة الدوال المُجزأة بشكل شبه دائم لتحقيق وسائط متعددة؛ ومن الأمثلة البارزة على ذلك لغتا ML و Haskell ، حيث تحتوي جميع الدوال في كلتا اللغتين على وسيط واحد فقط. هذه الخاصية موروثة من حساب التفاضل والتكامل اللامدا ، حيث تُمثَّل الدوال متعددة الوسائط عادةً بصيغة مُجزأة.

يرتبط تطبيق الدوال الجزئية (currying) بتطبيق الدوال الجزئية (partial application) ، ولكنه ليس نفسه . [ 1 ] [ 2 ] عمليًا، يمكن استخدام تقنية البرمجة الخاصة بالإغلاقات (closures) لتنفيذ تطبيق جزئي ونوع من تطبيق الدوال الجزئية، وذلك عن طريق إخفاء الوسائط في بيئة تنتقل مع الدالة المُطبقة.

تاريخ

يشير مصطلح "كاري" في "كاريينغ" إلى عالم المنطق هاسكل كاري ، الذي استخدم المفهوم على نطاق واسع، لكن موسى شونفينكل كان صاحب الفكرة قبل كاري بست سنوات. [ 10 ] وقد اقتُرح اسم بديل هو "شونفينكليزيشن". [ 15 ] أما في السياق الرياضي، فيمكن تتبع هذا المبدأ إلى عمل قام به فريجه عام 1893. [ 4 ] [ 5 ]

لا يُعرف أصل مصطلح "التطبيق الجزئي" (currying). يقول ديفيد تيرنر إن كريستوفر ستراشي هو من صاغ المصطلح في محاضراته عام 1967 بعنوان " المفاهيم الأساسية في لغات البرمجة " [ 16 ] ، لكن هذا المصدر يُعرّف المفهوم بأنه "أداة ابتكرها شونفينكل"، ولا يُستخدم مصطلح "التطبيق الجزئي" (currying)، بينما يُذكر مصطلح "كاري" (Curry) لاحقًا في سياق الدوال ذات الرتبة العليا. [ 7 ] عرّف جون سي. رينولدز "التطبيق الجزئي" (currying) في ورقة بحثية عام 1972، لكنه لم يدّعِ أنه هو من صاغ المصطلح. [ 8 ]

تعريف

يُمكن فهم مفهوم "التقسيم الجزئي" (Currying) بسهولة أكبر من خلال البدء بتعريف غير رسمي، والذي يُمكن تعديله لاحقًا ليناسب العديد من المجالات المختلفة. أولًا، يجب تحديد بعض الرموز.X→Y{\displaystyle X\to Y}يشير إلى جميع الدوال منX{\displaystyle X}لY{\displaystyle Y}. لوو{\displaystyle f}إذا كانت هذه دالة، فإننا نكتبو:X→Y{\displaystyle f\colon X\to Y}. يتركX×Y{\displaystyle X\times Y}تشير إلى الأزواج المرتبة لعناصرX{\displaystyle X}وY{\displaystyle Y}على التوالي، أي حاصل الضرب الديكارتي لـX{\displaystyle X}وY{\displaystyle Y}. هنا،X{\displaystyle X}وY{\displaystyle Y}قد تكون مجموعات، أو قد تكون أنواعًا، أو قد تكون أنواعًا أخرى من الكائنات، كما هو موضح أدناه.

بالنظر إلى دالة

و:(X×Y)→Z{\displaystyle f\colon (X\times Y)\to Z}،

يؤدي تطبيق تقنية "currying" إلى إنشاء دالة جديدة

ز:X→(Y→Z){\displaystyle g\colon X\to (Y\to Z)}.

إنه،ز{\displaystyle g}يأخذ وسيطًا من نوعX{\displaystyle X}وتعيد دالة من النوعY→Z{\displaystyle Y\to Z}يتم تعريفها بواسطة

ز(x)(y)=و(x،y){\displaystyle g(x)(y)=f(x,y)}

لx{\displaystyle x}من النوعX{\displaystyle X}وy{\displaystyle y}من النوعY{\displaystyle Y}ثم نكتب أيضًا

كاري(و)=ز.{\displaystyle {\text{curry}}(f)=g.}

عملية فك الانحناء هي التحويل العكسي، ويمكن فهمها بسهولة أكبر من خلال الدالة المرافقة اليمنى لها.يتقدم.{\displaystyle \operatorname {apply} .}

نظرية المجموعات

في نظرية المجموعات ، يُستخدم الرمزYX{\displaystyle Y^{X}}يُستخدم للدلالة على مجموعة الدوال من المجموعةX{\displaystyle X}إلى المجموعةY{\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}}.

في فئة المجموعات ، الكائنYX{\displaystyle Y^{X}}يُطلق عليه اسم الكائن الأسي .

مساحات الوظائف

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

كاري:هوم(X×Y،Z)→هوم(X،هوم(Y،Z))،{\displaystyle {\text{curry}}:{\text{Hom}}(X\times Y,Z)\to {\text{Hom}}(X,{\text{Hom}}(Y,Z)),}

بينما عملية فك التقسيم هي عملية عكسية. إذا كانت المجموعةYX{\displaystyle Y^{X}}من الدوال المتصلة منX{\displaystyle X}لY{\displaystyle Y}إذا كانت لدينا طوبولوجيا مفتوحة مضغوطة ، وإذا كان الفضاءY{\displaystyle Y}إذا كانت هاوسدورف متراصة محليًا ، فإن

كاري:ZX×Y→(ZY)X{\displaystyle {\text{curry}}:Z^{X\times Y}\to (Z^{Y})^{X}}

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

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

تقييم:YX×X→Y(و،x)↦و(x){\displaystyle {\begin{aligned}&&{\text{eval}}:Y^{X}\times X\to Y\\&&(f,x)\mapsto f(x)\end{aligned}}}

تكون متصلة عندماYX{\displaystyle Y^{X}}هو مضغوط-مفتوح وY{\displaystyle Y}هاوسدورف المدمجة محليًا. [ 21 ] هاتان النتيجتان أساسيتان لإثبات استمرارية التماثل ، أي عندماX{\displaystyle X}هي فترة الوحدةأنا{\displaystyle I}، لهذا السببZأنا×Y≅(ZY)أنا{\displaystyle Z^{I\times Y}\cong (Z^{Y})^{I}}يمكن اعتبارها إما تماثلًا لدالتين منY{\displaystyle Y}لZ{\displaystyle Z}أو، بشكل مكافئ، مسار واحد (متصل) فيZY{\displaystyle Z^{Y}}.

الطوبولوجيا الجبرية

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

[ΣX،Z]≊[X،ΩZ]{\displaystyle [\Sigma X,Z]\approxeq [X,\Omega Z]}

أين[أ،ب]{\displaystyle [A,B]}هي مجموعة فئات التماثل للتطبيقاتأ→ب{\displaystyle A\rightarrow B}، وΣأ{\displaystyle \Sigma A}هو تعليق A ، وΩأ{\displaystyle \Omega A}هي مساحة الحلقة لـ A. في جوهرها، التعليقΣX{\displaystyle \Sigma X}يمكن اعتبارها بمثابة حاصل الضرب الديكارتي لـX{\displaystyle X}باستخدام الفترة الوحدوية، يتم تطبيق علاقة تكافؤ لتحويل الفترة إلى حلقة. ثم يقوم الشكل المُجزأ برسم خريطة للفضاء.X{\displaystyle X}إلى فضاء الدوال من الحلقات إلىZ{\displaystyle Z}أي منX{\displaystyle X}داخلΩZ{\displaystyle \Omega Z}[ 21 ] ثم​كاري{\displaystyle {\text{curry}}}[ 21 ] هو المؤثر المرافق الذي يحول عمليات التعليق إلى فضاءات الحلقات، وفك التداخل هو المؤثر المزدوج.

يمكن فهم الازدواجية بين مخروط التخطيط وألياف التخطيط ( التليف المشترك والتليف ) [ 17 ] : الفصول 6 و7 على أنها شكل من أشكال التظليل، مما يؤدي بدوره إلى ازدواجية متواليات Puppe الطويلة الدقيقة والمتزامنة .

في الجبر التماثلي ، تُعرف العلاقة بين تطبيق التظليل الجزئي وإلغاء تطبيقه باسم اقتران التماثل الموتري . وهنا، يبرز جانب مثير للاهتمام: قد لا يرتفع كل من دالة التماثل ودالة جداء الموترات إلى متتالية تامة ؛ وهذا ما يؤدي إلى تعريف دالة الامتداد ودالة الانعكاس .

نظرية المجال

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

يظهر مفهوم الاستمرارية في نظرية نوع التماثل ، حيث يمكن اعتبار برنامجين حاسوبيين متماثلين، أي يحسبان نفس النتائج، إذا كان من الممكن إعادة هيكلتهما "بشكل مستمر" من أحدهما إلى الآخر.

حسابات لامدا

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

كاري(و)=λx.(λy.(و(x،y))){\displaystyle {\text{curry}}(f)=\lambda x.(\lambda y.(f(x,y)))}

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

كاري:((X×Y)→Z)→(X→(Y→Z)){\displaystyle {\text{curry}}:((X\times Y)\to Z)\to (X\to (Y\to Z))}

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

((كاري(و)x)y)=كاري(و)xy{\displaystyle (({\text{curry}}(f)\;x)\;y)={\text{curry}}(f)\;x\;y}.

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

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

نظرية الأنواع

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

يتم التعبير عن النهج القائم على نظرية الأنواع في لغات البرمجة مثل ML واللغات المشتقة منها والمستوحاة منها: Caml و Haskell و F# .

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

منطق

بموجب تطابق كاري-هوارد ، فإن وجود كل من تطبيق تقنية كاري على الطبقات وإلغاء تطبيقها يكافئ النظرية المنطقية.((أ∧ب)→ج)⇔(أ→(ب→ج)){\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}(المعروف أيضًا باسم التصدير )، حيث أن المجموعات ( نوع المنتج ) تتوافق مع الاقتران في المنطق، ونوع الدالة يتوافق مع الاستلزام.

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

نظرية الفئات

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

يُعمم هذا إلى نتيجة أوسع في الفئات المونيدية المغلقة : التَجْبِيد هو القول بأن حاصل الضرب الموتري و Hom الداخلي هما دالتان مترافقتان ؛ أي، لكل كائنب{\displaystyle B}يوجد تماثل طبيعي :

حoم(أ⊗ب،ج)≅حoم(أ،ب⇒ج).{\displaystyle \mathrm {Hom} (A\otimes B,C)\cong \mathrm {Hom} (A,B\Rightarrow C).}

هنا، يرمز Hom إلى دالة Hom الخارجية لجميع التشكلات في الفئة، بينماب⇒ج{\displaystyle B\Rightarrow C}يرمز إلى دالة التماثل الداخلي في الفئة المونيدية المغلقة. بالنسبة لفئة المجموعات ، يكون الاثنان متطابقين. عندما يكون حاصل الضرب هو حاصل الضرب الديكارتي، فإن دالة التماثل الداخليب⇒ج{\displaystyle B\Rightarrow C}يصبح كائنًا أسيًاجب{\displaystyle C^{B}}.

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

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

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

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

قارن بتطبيق الدالة الجزئية

غالبًا ما يُخلط بين تطبيق الدوال الجزئي وتطبيق الدوال الجزئي. [ 1 ] [ 2 ] أحد الفروق الجوهرية بينهما هو أن استدعاء دالة مُطبقة جزئيًا يُعيد النتيجة فورًا، وليس نتيجة دالة أخرى في سلسلة تطبيق الدوال الجزئي؛ ويمكن توضيح هذا الفرق بوضوح للدوال التي يزيد عدد معاملاتها عن اثنين. [ 25 ]

بالنظر إلى دالة من النوعو:(X×Y×Z)→شمال{\displaystyle f\colon (X\times Y\times Z)\to N}إنتاج الكاريكاري(و):X→(Y→(Z→شمال)){\displaystyle {\text{curry}}(f)\colon X\to (Y\to (Z\to N))}أي أنه بينما يمكن تمثيل تقييم الدالة الأولى على النحو التاليو(1،2،3){\displaystyle f(1,2,3)}، ويمكن تمثيل تقييم الدالة المعدلة على النحو التالي:والكاري(1)(2)(3){\displaystyle f_{\text{curried}}(1)(2)(3)}بتطبيق كل وسيط بدوره على دالة ذات وسيط واحد تم إرجاعها من الاستدعاء السابق. لاحظ أنه بعد استدعاءوالكاري(1){\displaystyle f_{\text{curried}}(1)}، يتبقى لدينا دالة تأخذ وسيطًا واحدًا وتعيد دالة أخرى، وليس دالة تأخذ وسيطين.

في المقابل، يشير تطبيق الدالة الجزئي إلى عملية تحديد عدد من الوسائط لدالة ما، مما ينتج عنه دالة أخرى ذات عدد وسائط أقل. وبالنظر إلى تعريفو{\displaystyle f}أعلاه، قد نثبت (أو "نربط") الوسيط الأول، مما ينتج عنه دالة من النوعجزئي(و):(Y×Z)→شمال{\displaystyle {\text{partial}}(f)\colon (Y\times Z)\to N}يمكن تمثيل تقييم هذه الدالة على النحو التالي:وجزئي(2،3){\displaystyle f_{\text{partial}}(2,3)}لاحظ أن نتيجة تطبيق الدالة الجزئية في هذه الحالة هي دالة تأخذ وسيطين.

بشكل بديهي، يُشير تطبيق الدالة الجزئية إلى أنه "إذا ثبّتّ الوسيط الأول للدالة، فستحصل على دالة للوسائط المتبقية". على سبيل المثال، إذا كانت الدالة div تُمثل عملية القسمة x / y ، فإن div مع تثبيت قيمة الوسيط x عند 1 (أي div 1) تُمثل دالة أخرى: وهي نفسها الدالة inv التي تُعيد المعكوس الضربي لوسيطها، والمُعرّفة بالعلاقة inv ( y ) =  1/ y .

يكمن الدافع العملي للتطبيق الجزئي في أن الدوال التي يتم الحصول عليها بتمرير بعض الوسائط وليس كلها إلى دالة ما تكون مفيدة في كثير من الأحيان؛ على سبيل المثال، تحتوي العديد من لغات البرمجة على دالة أو عامل مشابه لـ plus_one. يُسهّل التطبيق الجزئي تعريف هذه الدوال، على سبيل المثال عن طريق إنشاء دالة تمثل عامل الجمع مع تحديد 1 كوسيطها الأول.

يمكن اعتبار التطبيق الجزئي بمثابة تقييم دالة مُقَيَّمة عند نقطة ثابتة، على سبيل المثال، بالنظر إلىو:(X×Y×Z)→شمال{\displaystyle f\colon (X\times Y\times Z)\to N}وأ∈X{\displaystyle a\in X}ثمكاري(جزئي(و)أ)(y)(z)=كاري(و)(أ)(y)(z){\displaystyle {\text{curry}}({\text{partial}}(f)_{a})(y)(z)={\text{curry}}(f)(a)(y)(z)}أو ببساطةجزئي(و)أ=كاري1(و)(أ){\displaystyle {\text{partial}}(f)_{a}={\text{curry}}_{1}(f)(a)}أينكاري1{\displaystyle {\text{curry}}_{1}}يُجري عملية التناسب على المعامل الأول للدالة f.

وبالتالي، يُختزل التطبيق الجزئي إلى دالة مُعدّلة عند نقطة ثابتة. علاوة على ذلك، فإن الدالة المُعدّلة عند نقطة ثابتة هي (بشكل بديهي) تطبيق جزئي. وللمزيد من الأدلة، لاحظ أنه، بالنظر إلى أي دالةو(x،y){\displaystyle f(x,y)}، دالةز(y،x){\displaystyle g(y,x)}يمكن تعريفها بحيثز(y،x)=و(x،y){\displaystyle g(y,x)=f(x,y)}وبالتالي، يمكن اختزال أي تطبيق جزئي إلى عملية كاري واحدة. وعليه، يُعرَّف الكاري بشكل أدق بأنه عملية تُطبَّق، في كثير من الحالات النظرية، بشكل متكرر، ولكنها نظريًا لا يمكن تمييزها (عند اعتبارها عملية) عن التطبيق الجزئي.

لذا، يمكن تعريف التطبيق الجزئي بأنه النتيجة الموضوعية لتطبيق واحد لعامل الكاري على ترتيب معين لمدخلات دالة ما.

انظر أيضاً

مراجع

  1. 1 2 3 cdiggins (24 مايو 2007). "التقسيم الجزئي  للدالة لا يساوي التطبيق الجزئي المعمم؟!" . لامدا: المدونة الإلكترونية للغات البرمجة .
  2. 1 2 3 "تطبيق الدالة الجزئية ليس تطبيقًا جزئيًا" . The Uncarved Block . 7 أغسطس 2020. مؤرشف من الأصل في 23 أكتوبر 2016.
  3. 1 2 بايز، جون سي؛ ستاي، مايك (6 يونيو 2009). "الفيزياء، والطوبولوجيا، والمنطق، والحوسبة: حجر رشيد". في كوك، بوب (محرر). هياكل جديدة للفيزياء (PDF) . سلسلة محاضرات في الفيزياء. المجلد 813: هياكل جديدة للفيزياء. برلين، هايدلبرغ: سبرينغر (نُشر في 5 يوليو 2010). الصفحات 95-172 . arXiv : 0903.0340 . doi : 10.1007/978-3-642-12821-9_2 . ISBN   978-3-642-12821-9. S2CID 115169297 . مؤرشف من الأصل (PDF) في 5 ديسمبر 2022. 
  4. 1 2 فريج ، جوتلوب (1893). "§ 36" . Grundgesetze der arithmetik (باللغة الألمانية). كتاب من مجموعات جامعة ويسكونسن - ماديسون، رقمنته جوجل في 26 أغسطس 2008. جينا: هيرمان بوهلي. ص 54 – 55. 
  5. 1 2 3 كوين، دبليو في (1967). "مقدمة لكتاب موسى شونفينكل لعام 1924 بعنوان "حول اللبنات الأساسية للمنطق الرياضي"في: فان هيجينورت، جان (محرر). من فريجه إلى غودل: كتاب مرجعي في المنطق الرياضي، 1879-1931 . مطبعة جامعة هارفارد. الصفحات 355-357 . ISBN  9780674324497.
  6. ^ شونفينكل، موسى (سبتمبر 1924) [تم تقديمه في Mathematischen Gesellschaft (جمعية الرياضيات) في غوتنغن في 7 ديسمبر 1920. استلمته Mathematische Annalen في 15 مارس 1924.]. "Über die Bausteine ​​der mathematischen Logik" [ حول اللبنات الأساسية للمنطق الرياضي ] (PDF) . الرياضيات أنالن . 92 ( 3-4 ). برلين: سبرينغر: 305-316 . دوى : 10.1007 / BF01448013 . S2CID 118507515 . 
  7. 1 2 ستراشي، كريستوفر (أبريل 2000) [تشكل هذه الورقة جوهر سلسلة محاضرات أُلقيت في المدرسة الصيفية الدولية لبرمجة الحاسوب في كوبنهاغن في أغسطس 1967]. " المفاهيم الأساسية في لغات البرمجة" . الحوسبة الرمزية والحسابات من الرتبة العليا . 13 : 11-49 . CiteSeerX 10.1.1.332.3161 . doi : 10.1023/A:1010000313106 . ISSN 1573-0557 . S2CID 14124601. يوجد جهاز ابتكره شونفينكل، لاختزال المعاملات ذات المعاملات المتعددة إلى تطبيق متتابع لمعاملات ذات معامل واحد.   
  8. ١ ٢ ٣ نُشرت في الأصل بعنوان: رينولدز، جون سي. (١ أغسطس ١٩٧٢). "مفسرات تعريفية للغات البرمجة عالية المستوى" . في: شيلدز، روزماري (محررة). وقائع المؤتمر السنوي لجمعية آلات الحوسبة - ACM '72 . المجلد ٢. مطبعة جمعية آلات الحوسبة. الصفحات ٧١٧-٧٤٠ . doi : 10.1145/800194.805852 . ISBN   9781450374927S2CID 163294. في السطر الأخير ، استخدمنا حيلة تُسمى "التقسيم الجزئي" (نسبةً إلى عالم المنطق هنري كاري) لحل مشكلة إدخال عملية ثنائية في لغةٍ يجب أن تقبل فيها جميع الدوال وسيطًا واحدًا فقط. (يُشير المُحكِّم إلى أنه على الرغم من أن مصطلح "التقسيم الجزئي" يبدو أكثر جاذبية، إلا أن "التقسيم الجزئي" قد يكون أكثر دقة) .  أُعيد نشرها بعنوان: رينولدز، جون سي. (1998). "المفسرات التعريفية للغات البرمجة عالية الرتبة" . الحوسبة عالية الرتبة والرمزية . 11 (4). بوسطن: دار كلوير للنشر الأكاديمي: 363-397 . doi : 10.1023/A:1010027404223 . 13 - عبر جامعة سيراكيوز: كلية الهندسة وعلوم الحاسوب - الأقسام والمراكز والمعاهد والمشاريع السابقة.
  9. ↑ سلونجر، كينيث؛ كورتز، باري ل. (1995). "الدوال المُقَيَّدة، 5.1: المفاهيم والأمثلة، الفصل 5: حساب لامدا". بناء الجملة الرسمي ودلالات لغات البرمجة: منهج عملي (ملف PDF) . شركة أديسون-ويسلي للنشر. ص 144. ISBN  0-201-65697-3.
  10. 1 2 3 كاري، هاسكل ب. (1980). باروايز، جون؛ كيسلر، هـ. جيروم؛ كونين، كينيث (محررون). "بعض الجوانب الفلسفية للمنطق التوافقي". ندوة كلين: وقائع الندوة التي عُقدت في الفترة من 18 إلى 24 يونيو 1978 في ماديسون، ويسكونسن، الولايات المتحدة الأمريكية (دراسات في المنطق وأسس الرياضيات) . دراسات في المنطق وأسس الرياضيات. 101. شركة نورث هولاند للنشر، بصمة إلسيفير: 85-101 . doi : 10.1016/S0049-237X(08)71254-0 . ISBN 9780444853455ISSN 0049-237X . S2CID 117179133 . يطلق بعض علماء المنطق المعاصرين على هذه الطريقة في النظر إلى الدالة اسم "التقسيم الجزئي"، لأنني استخدمتها على نطاق واسع؛ لكن شونفينكل كان لديه الفكرة قبل حوالي 6 سنوات مني.  
  11. ↑ "Currying Schonfinkelling" . ويكي مستودع أنماط بورتلاند . شركة كونينغهام وكونينغهام، 6 مايو 2012.
  12. ^ باريندريجت ، هينك. باريندسن، إريك (مارس 2000) [ديسمبر 1998]. مقدمة لحساب التفاضل والتكامل لامدا (PDF) ( طبعة منقحة). ص. 8.  
  13. ↑ كاري، هاسكل ؛ فيس، روبرت (1958). المنطق التوافقي . المجلد الأول ( الطبعة الثانية). أمستردام، هولندا: شركة نورث هولاند للنشر.  
  14. ↑ هاتون، غراهام؛ جونز، مارك ب.، محرران. (نوفمبر 2002). "الأسئلة الشائعة حول comp.lang.functional، 3. المواضيع التقنية، 3.2. التخصيص الجزئي" . قسم علوم الحاسوب، جامعة نوتنغهام .
  15. ↑ هايم، إيرين؛ كراتزر، أنجليكا (2 يناير 1998). علم الدلالة في القواعد التوليدية (ملف PDF) . مالدن، ماساتشوستس: بلاكويل للنشر، وهي دار نشر تابعة لدار وايلي. ISBN 0-631-19712-5.
  16. ↑ تيرنر، ديفيد (1 يونيو 1997). "لغة البرمجة، أو التكييف الجزئي، أو التشويه؟، العدد 9 من 14" . منتدى لغات برمجة الحاسوب . مؤرشف من الأصل في 3 مارس 2022. تم الاطلاع عليه في 3 مارس 2022 .
  17. 1-2 مايو، جون بيتر (1999). دورة موجزة في الطوبولوجيا الجبرية (ملف PDF) . محاضرات شيكاغو في الرياضيات . شيكاغو، إلينوي: مطبعة جامعة شيكاغو. الصفحات 39-55 . ISBN  0-226-51183-9. OCLC 41266205 . 
  18. ↑ "الفضاء الطوبولوجي المُولّد بشكل مضغوط" . nLab . 28 مايو 2023.
  19. ↑ تيلوتسون، ج.؛ بوث، بيتر آي. (مارس 1980) [تاريخ الاستلام: 2 أكتوبر 1978، تاريخ المراجعة: 29 يونيو 1979، تاريخ النشر: 1 مايو 1980]. كُتب في جامعة ميموريال في نيوفاوندلاند. "الفئات المغلقة أحادية الشكل، والفئات المغلقة ديكارتية، والفئات الملائمة للفضاءات الطوبولوجية" (ملف PDF) . مجلة المحيط الهادئ للرياضيات . 88 (1). بيركلي، كاليفورنيا: دار نشر العلوم الرياضية: 35-53 . doi : 10.2140/pjm.1980.88.35 . eISSN 1945-5844 . ISSN 0030-8730 .  
  20. ↑ "فئة ملائمة من الفضاءات الطوبولوجية" . nLab . 11 أغسطس 2023.
  21. 1 2 3 روتمان، جوزيف جوناه (1988). "الفصل 11". مقدمة في الطوبولوجيا الجبرية . نصوص الدراسات العليا في الرياضيات؛ 119. نيويورك: سبرينغر-فيرلاغ. ISBN 978-0-387-96678-6. OCLC 17383909 . 
  22. ↑ باريندريخت، هندريك بيتر (1984). "النظريتان 1.2.13 و1.2.14". حساب لامدا: تركيبه ودلالاته . دراسات في المنطق وأسس الرياضيات. المجلد 103 ( طبعة منقحة). نورث هولاند، إحدى مطبوعات إلسيفير. ISBN   978-0-444-87508-2.
  23. ↑ ماك لين، سوندرز ؛ مورديك، إيكي (1992). "الفصل الأول: فئات الدوال؛ الأقسام 7: حساب القضايا، 8: جبر هيتينغ، و9: الكميات كمرافقات" . الحزم في الهندسة والمنطق: مقدمة أولية لنظرية التوبوس . نيويورك: سبرينغر-فيرلاغ، جزء من سبرينغر ساينس آند بيزنس ميديا. الصفحات 48-57 . ISBN  978-0-387-97710-2.
  24. ↑ أبرامسكي، سامسون؛ كويك، بوب (5 مارس 2007). "دلالات فئوية للبروتوكولات الكمومية". المنطق في علوم الحاسوب (LICS 2004): وقائع الندوة السنوية التاسعة عشرة لمعهد مهندسي الكهرباء والإلكترونيات، توركو، فنلندا، 2004] . مطبعة جمعية الحاسوب التابعة لمعهد مهندسي الكهرباء والإلكترونيات. الصفحات 415-425 . arXiv : quant-ph/0402130 . doi : 10.1109/LICS.2004.1319636 . ISBN  978-0-7695-2192-3.
  25. ↑ لي، جي. كاي (15 مايو 2013). "البرمجة الوظيفية في 5 دقائق" . شرائح العرض .