الحث البنيوي

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

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

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

على سبيل المثال، إذا كانت البنى عبارة عن قوائم، فعادةً ما يُستخدم الترتيب الجزئي "<"، حيث L < M عندما تكون القائمة L هي نهاية القائمة M. في ظل هذا الترتيب، تكون القائمة الفارغة [] هي العنصر الأدنى الوحيد. يتكون برهان الاستقراء البنيوي لقضية ما P ( L ) من جزأين: برهان على صحة P ([]) ، وبرهان على أنه إذا كانت P ( L ) صحيحة لقائمة ما L ، وكانت L هي نهاية القائمة M ، فإن P ( M ) يجب أن تكون صحيحة أيضًا.

في نهاية المطاف، قد يوجد أكثر من حالة أساسية و/أو أكثر من حالة استقرائية، وذلك بحسب كيفية بناء الدالة أو البنية. في هذه الحالات، يتكون برهان الاستقراء البنيوي لبعض القضايا P ( L ) مما يلي:

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

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

على سبيل المثال، يمكن إثبات الخاصية "شجرة الأجداد الممتدة على مدى g جيلاً تُظهر على الأكثر 2 ^g − 1 شخص" عن طريق الاستقراء الهيكلي على النحو التالي:

• في أبسط الحالات، تُظهر الشجرة شخصًا واحدًا فقط وبالتالي جيلًا واحدًا؛ وتكون الخاصية صحيحة لمثل هذه الشجرة، نظرًا لأن 1 ≤ 2 ¹ − 1 .
• بدلاً من ذلك، تُظهر الشجرة شخصًا واحدًا وشجرة والديه. وبما أن كل شجرة من الأشجار الأخيرة تُمثل جزءًا من الشجرة الرئيسية، فيمكن افتراض أنها تُحقق الخاصية المراد إثباتها (المعروفة أيضًا بفرضية الاستقراء ). أي، يمكن افتراض أن p ≤ 2g ⁻ 1 و q ≤ ^2h − 1 ، حيث يُمثل g و h عدد الأجيال التي تمتد عليها الشجرة الفرعية للأب والأم على التوالي، بينما يُمثل p و q عدد الأشخاص الذين تُمثلهم.
  • في حالة g ≤ h ، تمتد الشجرة بأكملها على مدى 1 + h جيلاً وتُظهر p + q + 1 شخصًا، و$${\displaystyle p+q+1\leq (2^{g}-1)+(2^{h}-1)+1\leq 2^{h}+2^{h}-1=2^{1+h}-1,}$$أي أن الشجرة بأكملها تحقق الخاصية.
  • في حالة h ≤ g ، تمتد الشجرة بأكملها على مدى 1 + g جيلاً وتظهر p + q + 1 ≤ 2 ^{g + 1} − 1 شخص من خلال منطق مماثل ، أي أن الشجرة بأكملها تحقق الخاصية في هذه الحالة أيضًا.

وبالتالي، من خلال الاستقراء الهيكلي، فإن كل شجرة سلفية تحقق الخاصية.

كمثال آخر أكثر رسمية، ضع في اعتبارك الخاصية التالية للقوائم  :

${\displaystyle {\text{EQ:}}\quad \operatorname {len} (L+\!+\ M)=\operatorname {len} (L)+\operatorname {len} (M)}$

هنا ++ تشير إلى عملية دمج القوائم، و len() تشير إلى طول القائمة، و L و M هما قائمتان.

لإثبات ذلك، نحتاج إلى تعريفات للطول وعملية الدمج. لنفترض أن ( h : t ) تُمثل قائمة رأسها (أول عنصر) هو h وذيلها (قائمة العناصر المتبقية) هو t ، ولنفترض أن [] تُمثل قائمة فارغة. تعريفات الطول وعملية الدمج هي:

${\displaystyle {\begin{array}{ll}{\text{LEN1:}}&\operatorname {len} ([\ ])=0\\{\text{LEN2:}}&\operatorname {len} (h:t)=1+\operatorname {len} (t)\\&\\{\text{APP1:}}&[\ ]+\!+\ list=list\\{\text{APP2:}}&(h:t)+\!+\ list=h:(t+\!+\ list)\end{array}}}$

تنص فرضيتنا P ( l ) على أن EQ صحيحة لجميع القوائم M عندما تكون L هي l . نريد أن نثبت أن P ( l ) صحيحة لجميع القوائم l . سنبرهن على ذلك بالاستقراء البنيوي على القوائم.

سنثبت أولاً أن P ([]) صحيحة؛ أي أن EQ صحيحة لجميع القوائم M عندما تكون L هي القائمة الفارغة [] . لننظر إلى EQ :

${\displaystyle {\begin{array}{rll}\operatorname {len} (L+\!+\ M)&=\operatorname {len} ([\ ]+\!+\ M)\\&=\operatorname {len} (M)&({\text{by APP1}})\\&=0+\operatorname {len} (M)\\&=\operatorname {len} ([\ ])+\operatorname {لين} (M)&({\text{بواسطة LEN1}})\\&=\اسم المشغل {len} (L)+\اسم المشغل {len} (M)\\\end{صفيف}}}$

وهكذا تم إثبات هذا الجزء من النظرية؛ EQ صحيح لجميع M ، عندما يكون L هو [] ، لأن الجانب الأيسر والجانب الأيمن متساويان.

بعد ذلك، لنفترض أي قائمة غير فارغة I. بما أن I غير فارغة، فإنها تحتوي على عنصر رأس، x ، وقائمة ذيل، xs ، لذا يمكننا التعبير عنها على النحو التالي : ( x : xs ) . تنص فرضية الاستقراء على أن EQ صحيحة لجميع قيم M عندما تكون L هي xs :

${\displaystyle {\text{HYP:}}\quad \operatorname {len} (xs+\!+\ M)=\operatorname {len} (xs)+\operatorname {len} (M)}$

نريد أن نبين أنه إذا كان هذا هو الحال، فإن المعادلة EQ صحيحة أيضًا لجميع قيم M عندما L = I = ( x : xs ) . نتابع كما في السابق:

${\displaystyle {\begin{array}{rll}\operatorname {len} (L)+\operatorname {len} (M)&=\operatorname {len} (x:xs)+\operatorname {len} (M)\\&=1+\operatorname {len} (xs)+\operatorname {len} (M)&({\text{by LEN2}})\\&=1+\operatorname {len} (xs+\!+\ M)&({\text{by HYP}})\\&=\operatorname {len} (x:(xs+\!+\ M))&({\text{by LEN2}})\\&=\operatorname {len} ((x:xs)+\!+\ M)&({\text{by APP2}})\\&=\operatorname {len} (L+\!+\ M)\end{array}}}$

وبالتالي ، من خلال الاستقراء الهيكلي، نحصل على أن P ( L ) صحيح لجميع القوائم L.

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

كمثال على هذا النوع من الحجج، لننظر إلى مجموعة جميع الأشجار الثنائية . سنُبين أن عدد الأوراق في شجرة ثنائية كاملة يزيد بواحد عن عدد العقد الداخلية. لنفترض وجود مثال مضاد؛ عندها لا بد من وجود مثال آخر بأقل عدد ممكن من العقد الداخلية. هذا المثال المضاد، C ، يحتوي على n عقدة داخلية و l ورقة، حيث n + 1 ≠ l . علاوة على ذلك، يجب أن يكون C غير تافه، لأن الشجرة التافهة تحتوي على n = 0 و l = 1 ، وبالتالي فهي ليست مثالًا مضادًا. لذلك، يحتوي C على ورقة واحدة على الأقل يكون عقدها الأب عقدة داخلية. احذف هذه الورقة وعقدتها الأب من الشجرة، مع ترقية العقدة الشقيقة للورقة إلى الموضع الذي كانت تشغله عقدتها الأب. هذا يُقلل كلاً من n و l بمقدار 1، لذا فإن الشجرة الجديدة تحتوي أيضًا على n + 1 ≠ l ، وبالتالي فهي مثال مضاد أصغر. ولكن بحسب الفرضية، كان C بالفعل أصغر مثال مضاد؛ لذا، فإن افتراض وجود أي أمثلة مضادة في البداية كان خاطئًا. الترتيب الجزئي الذي يُشير إليه مصطلح "أصغر" هنا هو الذي ينص على أن S < T عندما يكون عدد عقد S أقل من عدد عقد T.

• عملية التوليد النقدي
• الجبر الابتدائي
• ثابت في الحلقة ، مماثل لحلقات for

• هوبكروفت، جون إي.؛ راجيف موتاني؛ جيفري د. أولمان (2001). مقدمة في نظرية الأوتوماتا واللغات والحوسبة (الطبعة الثانية  ). ريدينغ، ماساتشوستس: أديسون-ويسلي. ISBN 978-0-201-44124-6.
• "المنطق الرياضي - الفيديو 01.08 - الاستقراء المعمم (البنيوي)" على يوتيوب

تشمل المنشورات المبكرة حول الاستقراء البنيوي ما يلي:

• بورستال، آر إم (1969). "إثبات خصائص البرامج بالاستقراء البنيوي". مجلة الحاسوب . 12 (1): 41-48 . doi : 10.1093/comjnl/12.1.41 .
• أوبين، ريموند (1976)، ميكنة الاستقراء البنيوي ، EDI-INF-PHD، المجلد 76-002 ، جامعة إدنبرة، hdl : 1842/6649 
• هويه، جي؛ وهولو، جي إم (1980). "البراهين بالاستقراء في النظريات المعادلة مع المُنشئات" (ملف PDF) . المؤتمر السنوي الحادي والعشرون حول أسس علوم الحاسوب . معهد مهندسي الكهرباء والإلكترونيات. الصفحات 96-107 . 
• Rózsa Péter , Über die Verallgemeinerung der Theorie der rekursiven Funktionen für abstrakte Mengen geeigneter Struktur als Definitionsbeeiche , Symposium International, Varsovie septembre (1959) ( حول تعميم نظرية الوظائف العودية للكميات المجردة مع الهياكل المناسبة كمجالات ) .