عملية التوليد النقدي

يترك${\displaystyle U}$كن مجموعة و${\displaystyle F}$لتكن دالة رتيبة${\displaystyle 2^{U}\rightarrow 2^{U}}$، إنه:

$${\displaystyle X\subseteq Y\Rightarrow F(X)\subseteq F(Y)}$$

ما لم يُنص على خلاف ذلك،${\displaystyle F}$سيفترض أن يكون رتيبًا.

• تكون X مغلقة من النوع F إذا${\displaystyle F(X)\subseteq X}$
• يكون X متسقًا مع F إذا${\displaystyle X\subseteq F(X)}$
• تكون النقطة X نقطة ثابتة إذا${\displaystyle X=F(X)}$

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

تنص نظرية كناستر-تارسكي على أن أصغر نقطة ثابتة لـ${\displaystyle F}$(يشار إليه)${\displaystyle \mu F}$يُعطى ) بتقاطع جميع المجموعات المغلقة من النوع F ، بينما تُعطى أكبر نقطة ثابتة (يرمز لها بـ${\displaystyle \nu F}$يُعطى ) باتحاد جميع المجموعات المتسقة مع F. يمكننا الآن ذكر مبادئ الاستقراء والاستقراء المشترك.

• مبدأ الاستقراء : إذا${\displaystyle X}$إذا كانت F مغلقة ، فـ${\displaystyle \mu F\subseteq X}$
• مبدأ الاستقراء المشترك : إذا${\displaystyle X}$إذا كان متسقًا مع F ، فـ${\displaystyle X\subseteq \nu F}$

ضع في اعتبارك قواعد أنواع البيانات التالية:

$${\displaystyle T=\bot \;|\;\top \;|\;T\times T}$$

أي أن مجموعة الأنواع تتضمن "النوع الأدنى".${\displaystyle \bot }$، النوع "الأعلى"${\displaystyle \top }$وأنواع المنتجات. ويمكن تحديد هذه الأنواع باستخدام سلاسل نصية فوق الأبجدية.${\displaystyle \Sigma =\{\bot ,\top ,\times \}}$. يترك${\displaystyle \Sigma ^{\leq \omega }}$تشير إلى جميع السلاسل (التي قد تكون لانهائية) على${\displaystyle \Sigma }$ضع في اعتبارك الدالة${\displaystyle F:2^{\Sigma ^{\leq \omega }}\rightarrow 2^{\Sigma ^{\leq \omega }}}$:

$${\displaystyle F(X)=\{\bot ,\top \}\cup \{x\times y:x,y\in X\}}$$

في هذا السياق،${\displaystyle x\times y}$يعني "تسلسل السلسلة"${\displaystyle x}$، الرمز${\displaystyle \times }$، وسلسلة${\displaystyle y}$ينبغي لنا الآن تعريف مجموعة أنواع البيانات لدينا كنقطة ثابتة لـ${\displaystyle F}$لكن الأمر يختلف باختلاف ما إذا كنا نختار نقطة ثابتة صغيرة أم كبيرة .

لنفترض أننا نأخذ${\displaystyle \mu F}$باعتبارها مجموعة أنواع البيانات لدينا. باستخدام مبدأ الاستقراء ، يمكننا إثبات الادعاء التالي:

جميع أنواع البيانات في${\displaystyle \mu F}$محدودة​

للوصول إلى هذه النتيجة، ضع في اعتبارك مجموعة جميع السلاسل المنتهية على${\displaystyle \Sigma }$من الواضح${\displaystyle F}$لا يمكن أن ينتج سلسلة لانهائية، لذلك اتضح أن هذه المجموعة مغلقة من النوع F، ويترتب على ذلك النتيجة.

لنفترض الآن أننا نأخذ${\displaystyle \nu F}$كمجموعة من أنواع البيانات لدينا. نود استخدام مبدأ الاستقراء المشترك لإثبات الادعاء التالي:

النوع${\displaystyle \bot \times \bot \times \cdots \in \nu F}$

هنا${\displaystyle \bot \times \bot \times \cdots }$يشير إلى السلسلة اللانهائية${\displaystyle (\bot ,\times ,\bot ,\times ,\ldots )}$لاستخدام مبدأ الاستقراء المشترك ، ضع في اعتبارك المجموعة التالية:

$${\displaystyle S=\{\bot ,\;\bot \times \bot \times \cdots \}}$$

هذه المجموعة متسقة مع F. أولاً،${\displaystyle \bot \in \{\bot ,\top \}\subseteq F(S)}$ثانيًا، بما أن${\displaystyle \bot \in S}$و${\displaystyle \bot \times \bot \times \cdots \in S}$لدينا${\displaystyle \bot \times (\bot \times \bot \times \cdots )\in F(S)}$تفسير السلاسل النصية كمتواليات (دوال من${\displaystyle \mathbb {N} \rightarrow \Sigma }$), إضافة البادئة المحدودة${\displaystyle \bot \times }$إلى السلسلة اللانهائية${\displaystyle \bot \times \bot \times \cdots }$العائد${\displaystyle \bot \times \bot \times \cdots }$لذا، بنفسها${\displaystyle \bot \times \bot \times \cdots \in F(S)}$. لذلك${\displaystyle S\subseteq F(S)}$وبحسب مبدأ الاستقراء المشترك ،${\displaystyle \bot \times \bot \times \cdots \in \nu F}$.

ملاحظة. تمثيل الأنواع كسلاسل نصية على${\displaystyle \Sigma }$لا يلتزم ببنية الشجرة الأساسية. السلاسل المحدودة مثل${\displaystyle \bot \times \top \times \bot }$تكون غامضة بدون استخدام الأقواس، ولأي سلسلة لا نهائية${\displaystyle s}$التسلسل${\displaystyle s\times t=s}$للجميع${\displaystyle t}$وبالتالي، يمكن تحديد أشجار متميزة. لا يؤثر هذا على الحجة المذكورة أعلاه، والتي توضح فقط مبدأ الاستقراء المشترك عبر الاتساق F ، ولكنه سيكون مهمًا في الحالات التي يجب فيها الحفاظ على بنية المُنشئ. يُمثل المعالجة الهيكلية القياسية الأنواع عبر التماثل.${\displaystyle T\cong 1+1+(T\times T)}$انظر إلى الجبر F لمزيد من التفاصيل.

لنأخذ تعريف التدفق التالي في لغة هاسكل : ^{[ 5 ]}

بيانات التدفق أ = S أ ( التدفق أ )-- رأس "المدمرات" للتدفق :: التدفق أ -> أ رأس ( S أ astream ) = أ ذيل :: التدفق أ -> التدفق أ ذيل ( S أ astream ) = أstream

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

ضع في اعتبارك الوظيفة الداخلية${\displaystyle F}$في فئة المجموعات :

$${\displaystyle {\begin{align}F(x)&=A\times x\\F(f)&=\langle \mathrm {id} _{A},f\rangle \end{محاذاة}}}$$

الجبر المشترك النهائي F${\displaystyle \nu F}$يرتبط بها التشاكل التالي:

$${\displaystyle \mathrm {out}$$ :\nu F\rightarrow F(\nu F)=A\times \nu F}

وهذا يؤدي إلى جبر مشترك آخر${\displaystyle F(\nu F)}$مع التشكل المرتبط${\displaystyle F(\mathrm {out} )}$. لأن${\displaystyle \nu F}$نهائي ، يوجد تشاكل فريد

$${\displaystyle {\overline {F(\mathrm {out} )}}:F(\nu F)\rightarrow \nu F}$$

بحيث

$${\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ F(\mathrm {out} )=F\left({\overline {F(\mathrm {out} )}}\circ \mathrm {out} \right)}$$

التركيب${\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} }$يُنتج تشاكلًا آخر في الجبر المشترك F${\displaystyle \nu F\rightarrow \nu F}$. منذ${\displaystyle \nu F}$إذا كان هذا التشاكل نهائيًا، فهو فريد، وبالتالي${\displaystyle \mathrm {id} _{\nu F}}$إجمالاً لدينا:

$${\displaystyle {\begin{aligned}{\overline {F(\mathrm {out} )}}\circ \mathrm {out} &=\mathrm {id} _{\nu F}\\[0.5ex]\mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F {\bigl (}{\overline {F(\mathrm {out} )}}\circ \mathrm {out} {\bigr )}&=\mathrm {id} _{F(\nu F)}\end{محاذاة}}}$$

وهذا يشهد على التماثل${\displaystyle \nu F\simeq F(\nu F)}$وهذا يشير بشكل قاطع إلى أن${\displaystyle \nu F}$هي نقطة ثابتة لـ${\displaystyle F}$ويبرر هذا الترميز. ^{[ 6 ]}

out astream = ( head astream , tail astream ) out' ( a , astream ) = S a astream

سنوضح كيف يشمل مبدأ الاستقراء الاستقراء الرياضي.${\displaystyle P}$لنفترض أن لدينا خاصية من خواص الأعداد الطبيعية . سنعتمد التعريف التالي للاستقراء الرياضي:

$${\displaystyle 0\in P\land (n\in P\Rightarrow n+1\in P)\Rightarrow \mathbb {N} \subseteq P}$$

والآن لننظر في الدالة${\displaystyle F:2^{\mathbb {N} }\rightarrow 2^{\mathbb {N} }}$:

$${\displaystyle F(X)=\{0\}\cup \{x+1:x\in X\}}$$

لا ينبغي أن يكون من الصعب رؤية ذلك${\displaystyle \mu F=\mathbb {N} }$لذلك، وفقًا لمبدأ الاستقراء ، إذا أردنا إثبات خاصية ما${\displaystyle P}$ل${\displaystyle \mathbb {N} }$يكفي أن نبين أن${\displaystyle P}$مغلق من النوع F. بالتفصيل، نحتاج إلى:

$${\displaystyle F(P)\subseteq P}$$

إنه،

$${\displaystyle \{0\}\cup \{x+1:x\in P\}\subseteq P}$$

هذا هو الاستقراء الرياضي كما هو مذكور.