التكرار المشترك

في علوم الحاسوب ، يُعدّ الاستدعاء المشترك نوعًا من العمليات يُقابل الاستدعاء ( البنيوي) . فبينما يستهلك الاستدعاء بنية البيانات بمعالجة الطبقة العليا أولًا قبل النزول إلى أجزائها الداخلية، يُنتج الاستدعاء المشترك بنية البيانات بتعريف الطبقة العليا أولًا قبل تعريف أجزائها الداخلية. ويكتسب الاستدعاء المشترك أهمية خاصة في اللغات الشاملة ، إذ يسمح بترميز العمليات الحسابية التي قد لا تنتهي في سياقٍ يجب فيه إنهاء كل دالة. وهو مدعوم من قِبل مُثبتي النظريات Agda ^{[ 1 ]} وRocq ^{[ 2 ]} .

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

في لغات البرمجة الكلية، يمكن تعريف الأعداد الطبيعية على النحو التالي (باستخدام صيغة هاسكل ^{[ a ]} ):

بيانات طبيعية = صفر | طبيعية متتابعة

ينص هذا على أن كل عدد طبيعي إما أن يكون صفرًا أو العدد التالي لعدد طبيعي موجود. على سبيل المثال، يُرمز للعدد واحد بالرمز 1/2، وللعدد Succ Zeroاثنين بالرمز 2/3 Succ (Succ Zero)، وللعدد ثلاثة بالرمز 3/4، Succ (Succ (Succ Zero))وهكذا.

إذا فسرنا التصريح أعلاه بطريقة استقرائية ، فإن جميع الأعداد الطبيعية تُولّد بهذه الطريقة، فنحصل على مجموعتنا المألوفة من الأعداد الطبيعية. والأهم من ذلك، يمكننا استخدام الاستدعاء الذاتي ^{[ b ]} على هذه المجموعة: على سبيل المثال، يمكننا استخدامها لإنشاء قائمة تتكرر فيها قيمة معينة nعددًا من المرات.

كرر :: أ -> طبيعي -> [ أ ] كرر س صفر = [] -- الحالة الأساسية كرر س ( متتالي ن ) = س : كرر س ن -- خطوة استقرائية

لاحظ أن استخدام ` repeat x nthis` أمرٌ بالغ الأهمية، إذ لم يكن بإمكاننا كتابة `this` repeat x (Succ n)، لأنها الدالة التي نحاول تعريفها، وبالتالي ستدخل في حلقة لا نهائية. وبشكلٍ أدق، يجب أن يقل حجم المدخلات - أو بالأحرى أن تتعمق، إذا نظرنا إليها كبنية بيانات - في كل مرة نستدعي فيها الدالة بشكلٍ متكرر.

يمكن أيضاً تفسير الإعلان بطريقة استقرائية ، والتي يمكن الإشارة إليها على النحو التالي:

كوداتا CoNat = صفر | سوك كونات

CoNatتحتوي على جميع الأعداد الطبيعية التي Natتحتوي عليها تلقائيًا. ولكن نظرًا لأن البيانات المشتركة يمكن أن تكون عميقة بلا حدود، فإنها تحتوي على حد إضافي Succ (Succ (Succ (Succ …)))يستمر إلى ما لا نهاية - وغالبًا ما يُرمز إليه بـ ∞. ^{[ 3 ]} هذا خاص بالأعداد الطبيعية المشتركة، لذلك لا يمكن بناؤه إلا باستخدام الاستدعاء الذاتي المشترك:

اللانهاية :: CoNat اللانهاية = Succ اللانهاية

بينما يتطلب الاستدعاء التكراري أن يصغر مُدخل الاستدعاء التكراري في كل مرة، يتطلب الاستدعاء التكراري المشترك أن يكبر مُخرج الاستدعاء التكراري في كل مرة. لهذا السبب يجب علينا كتابة Succ infinity; لأن infinity = infinityاستخدام غير مسموح به لأنه يُكرر العملية إلى ما لا نهاية.

لتوضيح الازدواجية بين الاستدعاء الذاتي والاستدعاء الذاتي المشترك، يمكننا تغليفهما في دالتين، recو corec. إن وجود هاتين الدالتين، بالإضافة إلى المُنشئين العاديين لـ Natو CoNat، يُحدد نوعيهما بشكل فريد، وبالتالي يسمح بإعادة كتابة جميع أشكال الاستدعاء الذاتي والاستدعاء الذاتي المشترك باستخدامهما. ^{[ 4 ]}

rec :: Nat -> ( Maybe c -> c ) -> c rec Zero f = f Nothing rec ( Succ n ) f = f ( Just ( rec n f ))corec :: ( c -> Maybe c ) -> c -> CoNat corec f base = case f base of Nothing -> Zero Just x -> Succ ( corec f x )

من الناحية النظرية، CoNatيمكن اعتبارها آلة حالة ، حيث cيمثل نوعًا يغلف "الحالة الحالية". الدالة c -> Maybe cهي دالة انتقال حالة تؤدي إما إلى إنهاء العملية بـ Zeroأو استمرارها بـ Succ. يمكننا إعادة كتابة الأمثلة أعلاه باستخدام الدوال التالية:

كرر x n = rec n ( \ s -> case s of Nothing -> [] Just a -> x : a ) infinity = corec ( \ () -> Just () ) ()

ومن الأمثلة الأكثر تعقيدًا على البيانات المشفرة مثال الأشجار الثنائية ، حيث تكون كل عقدة إما عقدة طرفية تحمل بعض البيانات، أو عقدة فرعية لها طفلان بالضبط:

codata BinaryTree a = Leaf a | Branch ( BinaryTree a ) ( BinaryTree a )

يحتوي هذا المثال على العديد من الحدود ذات العمق اللانهائي التي لا يمكن إنشاؤها إلا عن طريق الاستدعاء الذاتي المشترك. على سبيل المثال، يمكن أن يكون العمق لانهائيًا فقط على الجانب الأيسر، أو على كلا الجانبين، أو بالتناوب بين اليسار واليمين.

infiniteLeft :: a -> BinaryTree a infiniteLeft x = Branch ( infiniteLeft x ) ( Leaf x )infiniteBoth :: BinaryTree a infiniteBoth = Branch infiniteBoth infiniteBothinfiniteAlternating :: a -> Bool -> BinaryTree a infiniteAlternating x False = Branch ( infiniteAlternating x True ) ( Leaf x ) infiniteAlternating x True = Branch ( Leaf x ) ( infiniteAlternating x False )

مرة أخرى، يتخذ التكرار المشترك على الأشجار الثنائية شكلاً أكثر عمومية يعتمد على مُنشئ يشبه "آلة الحالة":

corec :: ( c -> Either a ( c , c )) -> c -> BinaryTree a corec f base = case f base of Left x -> Leaf x Right ( x , y ) -> Branch ( corec f x ) ( corec f y )

codata M a ( b :: a -> * ) = M { root :: a , branch :: b root -> M a b } corec :: ( c -> ( root :: a , b root -> c )) -> c -> M a b corec f base = let ( root , branch ) = f base in M ​​{ root = root , branch = \ i -> corec f ( branch i ) }

f :: Bool -> * f False = Void -- حالة الصفر (لا توجد فروع) f True = () -- حالة النجاح (فرع واحد)Nat = W Bool f CoNat = M Bool f

أظهر القسم السابق وجود ارتباط وثيق بين الأعداد الطبيعية والمجاورة الطبيعية Maybe c، وكذلك بين الأشجار الثنائية Either a (c, c). ويتضح هذا الارتباط من خلال إثبات أن Natتقابل تقابلي مع Maybe Nat، CoNatومع Maybe CoNat؛ وبشكل أدق، يرتبط هذا التقابل التقابلي Zeroبـ Nothingو Succ nبـ Just n. بعبارة أخرى، Natو CoNatهما نقطتان ثابتتان ( حتى التشاكل ) للدالة${\displaystyle X\mapsto X+1}$.

الفرق بين البيانات والبيانات المساعدة هو أن البيانات تمثل أصغر نقطة ثابتة، بينما تمثل البيانات المساعدة أكبر نقطة ثابتة. وبهذا المعنى، يمكن تلخيص الاستدعاء الذاتي بأنه "تم توليد كل عنصر من النوع فقط بواسطة المُنشئات المُعطاة ( Zeroو Succفي حالة Nat/ CoNat)"، بينما ينص الاستدعاء الذاتي المشترك على أن "كل قيمة يمكن تحليلها باستخدام المُنشئات كحالات موجودة".

من منظور نظرية الفئات، CoNatيمكن تعريفها بدقة على أنها الجبر المشترك النهائي للدالة الداخلية${\displaystyle X\mapsto X+1}$[ ^{4 ]} عند تفكيك هذا التعريف، نجد ما يلي ^:

• توجد دالة . "Pred" اختصار لـ "predecessor" (السلف)، وبديهيًا، تطرح هذه الدالة واحدًا من العدد الطبيعي المقابل أو تعطي قيمة أخرى. بعبارة أخرى، و . هذا يُظهر أن الدالة هي جبر مشترك للدالة، ولكن ليس بالضرورة الجبر النهائي.pred :: CoNat -> Maybe CoNatNothingpred Zero = Nothingpred (Succ n) = Just nCoNat
• لكل نوع cودالة ، توجد دالة بحيث . بتفصيل هذا أكثر، إذا كان ، فإن ، بينما إذا كان ، فإن — وهذا يطابق تعريف الدالة الذي نعرفه.f :: c -> Maybe ccorec f :: c -> CoNatpred (corec f x) = fmap (corec f) (f x)f x = Just ycorec f x = Succ (corec f y)f x = Nothingcorec f x = Zerocorec
• corecفريد من نوعه بالمعنى التالي: لأي دالة أخرى تحقق أيضًا ، . وهذا يضمن أن يكون جبرًا مشتركًا نهائيًا .g :: c -> CoNatpred (g x) = fmap g (f x)g x = corec f xCoNat

Maybe cيمكن استبدالها بأي دالة أخرى في الوصف أعلاه للحصول على تعريف أي نوع استقرائي مشترك آخر.

لا تمتلك جميع الدوال جبرًا مشتركًا نهائيًا. على سبيل المثال، تنص نظرية كانتور على أنه لا يمكن لأي مجموعة أن تكون تقابل مجموعة القوى الخاصة بها، وبالتالي فإن دالة مجموعة القوىa -> Bool لا تمتلك جبرًا مشتركًا نهائيًا. ومع ذلك، في حالة الدوال متعددة الحدود أو دوال القسمة متعددة الحدود ^{[ 6 ]} ، توجد دائمًا جبر مشترك نهائي؛ فالدوال متعددة الحدود هي دوال يمكن التعبير عنها بالشكل التالي:${\displaystyle \textstyle X\mapsto \sum _{a:\alpha }X^{\beta (a)}}$بالنسبة للنوع α وعائلة الأنواع المفهرسة β ( a ). النوع M هو بالضبط بناء هذه الجبر المشترك النهائي. ^{[ 5 ]}

بينما يمكن الاستدلال على أنواع البيانات المشتركة باستخدام خاصية التفرد corecمباشرةً، إلا أنه غالبًا ما يكون من الأنسب استخدام الاستقراء المشترك ، الذي يمكنه إثبات تساوي البيانات المشتركة. لنفترض وجود جبر مشترك نهائي A لدالة متعددة الحدود F — أي${\displaystyle \textstyle F(X)=\sum _{a:\alpha }X^{\beta (a)}}$— نقول إن العلاقة${\displaystyle R\subseteq A\times A}$تكون ثنائية التماثل إذا، لكل${\displaystyle (a,b)\in R}$،${\displaystyle {\text{root}}(a)={\text{root}}(b)}$و${\displaystyle {\text{branch}}(a,i)R{\text{branch}}(b,i)}$للجميع${\displaystyle i:B({\text{root}}(a))}$. هنا،${\displaystyle {\text{root}}}$و${\displaystyle {\text{branch}}}$راجع الخرائط:

${\displaystyle {\begin{aligned}{\text{root}}&:A\rightarrow \alpha \\{\text{branch}}&:\prod _{a:A}\beta ({\text{root}}(a))\rightarrow A\end{aligned}}}$

ينص مبدأ الاستقراء المشترك على أنه بالنسبة لجميع عمليات المحاكاة الثنائية R على A و${\displaystyle (a,b)\in R}$،${\displaystyle a=b}$.

وبشكل أعم، بالنسبة لخريطة الجبر المشترك${\displaystyle {\text{get}}:A\rightarrow F(A)}$تكون العلاقة R على A علاقة ثنائية التماثل إذا وُجدت دالة${\displaystyle f:R\rightarrow F(R)}$مُرضٍ للجميع${\displaystyle (a,b)\in R}$،

• ${\displaystyle {\text{get}}(a)=F(\pi _{1})(f(a,b))}$و
• ${\displaystyle {\text{get}}(b)=F(\pi _{2})(f(a,b))}$،

حيث π ₁ و π ₂ هما خريطتا الإسقاط الأولى والثانية${\displaystyle R\rightarrow A}$ويمكن اعتبار هذا مكافئًا لحالة كثير الحدود عن طريق وضع${\displaystyle f(a,b)=({\text{root}}(a),i\mapsto ({\text{branch}}(a,i),{\text{branch}}(b,i)))}$ويمكن أيضًا التعبير عن المتساويات المطلوبة كمخطط تبادلي:

يسهل إثبات الاستقراء المشترك من خلال تفرد corec: فكل من π₁ و π₂ يحققان الخاصية المطلوبة للمساواة corec f، وبالتالي فهما متساويان، مما يدل على أن${\displaystyle a=\pi _{1}(a,b)=\pi _{2}(a,b)=b}$[ ^{4 ]​}

إضافة :: CoNat -> CoNat - > CoNat أضف صفر = أ أضف أ ( Succ b ) = Succ ( أضف أ ب )

أضف صفرًا صفر = صفر أضف ( لاحق أ ) صفر = لاحق ( أضف أ صفرًا ) أضف أ ( لاحق ب ) = لاحق ( أضف أ ب )

تكرار :: ( CoNat , CoNat ) -> ربما ( CoNat , CoNat ) تكرار صفر صفر = لا شيء تكرار ( Succ a ) صفر = فقط ( a , صفر ) تكرار a ( Succ b ) = فقط ( a , b )أضف a b = corec iterate ( a , b )

إذا كان مجال الخطاب هو فئة المجموعات والدوال الكلية (كما هو الحال في برامج إثبات النظريات مثل أغدا وروك)، فإن الأنواع النهائية (البيانات المشتركة) قد تحتوي على قيم لا نهائية وغير مؤسسة ، بينما لا تحتوي الأنواع الأولية (البيانات) على ذلك. ^{[ 8 ] [ 9 ]} من ناحية أخرى، إذا كان مجال الخطاب هو فئة الترتيبات الجزئية الكاملة والدوال المتصلة ، والتي تتوافق تقريبًا مع لغة البرمجة هاسكل ، فإن الأنواع النهائية تتطابق مع الأنواع الأولية، ويشكل الجبر المشترك النهائي والجبر الأولي المقابلان تماثلًا. ^{[ 10 ]}

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

• المحاكاة الثنائية
• عملية التوليد النقدي
• التكرار
• التشوه البصري