استقرای ساختاری

استقرای ساختاری

استقرای ساختاری روشی است که برای اثبات کردن قضایا از آن استفاده می‌شود که در منطق ریاضی (به عنوان مثال، در اثبات قضیه لس)، علوم کامپیوتر، نظریه گراف، و برخی دیگر از زمینه‌های ریاضی کاربرد دارد. این استقرا یک تعمیم از استقراء ریاضی روی اعداد طبیعی است، و می‌تواند به‌طور قراردادی به استقرای Noetherian تعمیم داده شود. روش بازگشت ساختاری یک روش بازگشتی است که ارتباط آن با استقرای ساختاری همانند ارتباط یک رابطه بازگشتی ساده با یک رابطه استقرای ریاضی ساده است.

استقرای ساختاری برای اثبات برخی گزاره‌های (P(x، که به ازای همهٔ xهای نوعی از ساختارهای تعریف شده به صورت بازگشتی مانند لیست‌ها یا درختان صحیح است، استفاده می‌شود. یک ترتیب جزئی کامل بر ساختارها ("زیرلیست" برای لیست‌ها و "زیر درخت" برای درختان) تعریف شده‌است. روش اثباتی استقرای ساختاری ثابت می‌کند که گزاره برای تمام ساختارهای مینیمال صحیح است، و در صورتی که این روش برای زیرساخت¬های بلافاصله یک ساختار خاص مانند S برقرار باشد آنگاه می¬بایست برای خود S نیز برقرار باشد. (به زبان رسمی، این مسئله موجب صحت فروض اصل استقرای کامل است که ادعا می‌کند که این دو شرط برای گزاره‌ای با هر مقدار x کافی است.)

یک تابع بازگشتی ساختاری ازهمان ایده که برای تعریف یک تابع بازگشتی به کار برده می‌شود، استفاده میکند: حالات پایه که هر یک از ساختارهای مینیمال را رسیدگی می‌کنند و یک قانون برای بازگشت. رابطه بازگشتی ساختاری معمولاً بوسیله استقرای ساختاری ثابت می‌شود؛ در موارد خاص آسان ،معمولاً از گام استقرا صرف نظر می‌شود. طول(length) و توابع ++ در مثال زیر روابط ساختاری بازگشتی‌اند. برای مثال، اگر ساختارها به صورت لیست باشند، لیستی معمولاً ترتیب جزئی '<' را معرفی می‌کند که در آن L <M است، هر زمان که لیست L دم لیست M باشد. بر اساس این ترتیب، لیست خالی []عنصر خاص مینمال است. اثبات استقرای ساختاری برخی از گزاره‌های (P(l شامل دو بخش است: اثبات این که ([])P درست است، و اثبات این که اگر (P(L برای برخی از لیست‌های L درست باشد، و اگر L دم لیست M باشد، پس (P(M نیز باید درست باشد.

در نهایت، ممکن است بیش از یک حالت پایه و/ یا بیش از یک حالت استقرا، بسته به اینکه چگونه تابع یا ساختار ساخته شده است، وجود داشته باشد. در آن موارد، اثبات استقرای ساختاری برخی از گزاره‌های (P(L شامل: الف) اثبات این که (P(BC، برای هر حالت پایه BC درست است. و ب) اثبات این که اگر (P(l برای برخی از موارد l درست باشد، وM بتواند از l با یک بار امتحان کردن هر یک از قواعد بازگشتی به دست بیاید، پس (P(M نیز باید درست باشد، می‌شود.

مثال‌ها

شجره نامه باستان، نشان دادن 31 نفر در 5 نسل

شجره نامه یک ساختار داده شناخته شده‌است که پدر و مادر، پدربزرگ و مادربزرگ، و اجداد یک فرد را تا آنجا که شناخته شده باشند نشان می دهد و به صورت بازگشتی تعریف می‌شود:

• در ساده‌ترین حالت، یک شجره نامه فقط یک نفر را نشان می دهد (اگر چیزی در مورد پدر و مادر آن شخص مشخص نباشد).
• متناوباً، شجره نامه یک نفر را، که توسط شاخه به دو زیر درخت پدر و مادر خود متصل شده است، نشان می دهد(با استفاده از فرضی ساده که اگر :یکی از آن‌ها شناخته شده باشد، پس هر دو شناخته شده اند).

به عنوان مثال، ویژگی " یک شجره نامه که بیش از g نسل را گسترش می دهد حداکثر 2^g-1 نفر را نشان می دهد" را می‌توان با استقرای ساختاری ثابت کرد که به شرح زیر است:

• در ساده‌ترین حالت، درخت فقط یک نفر را و از این رو یک نسل را نشان می‌دهد. تا زمانی که 1 ≤ 2¹ - 1 ویژگی مذکور برای چنین درختی درست است.
• متناوباً، درخت، درختان یک نفر و والدینش را نشان می‌دهد. از آن جا که هر یک از والدین یک زیرساختار از ساختار درخت هستند، می‌توان صحیح بودن ویژگی مذکور را اثبات شده فرض نمود. که با عنوان فرضیه استقرایی نیز شناخته می‌شود.

پس می‌توان فرض کرد، p ≤ 2^g – 1 و q ≤ 2^h – 1، که در آن g و h نشان دهنده تعداد نسل‌هایی است که زیردرخت‌های پدر و مادر به ترتیب گسترش می دهند، و p و q نشان دهنده تعداد افرادی است که آن‌ها نشان می دهند.

• در صورتی که g ≤ h، کل درخت، بیش از 1 + hنسل گسترش می یابد و p + q + 1 نفر را نشان می‌دهد. و

p + q + 1 ≤ (2^g - 1) + (2^h - 1) + 1 ≤ 2^h + 2^h - 1 = 2^{(1 + h)} – 1؛

یعنی کل درخت ویژگی مذکور را برآورده می‌کند.

• در صورتی که h ≤ g، کل درخت، بیش از 1 + g نسل گسترش می یابد و همینطور p + q + 1 ≤ 2^{(1 + g)} - 1 نفر را با استدلالی مشابه نشان می‌دهد. یعنی کل درخت در این مورد نیز ویژگی مذکور را برآورده می سازد.

از این رو، با استقرای ساختاری، هر شجره نامه ویژگی مذکور را برآورده می‌کند.

به عنوان مثالی رسمی تر، ویژگی مربوط به لیست‌های زیر را در نظر بگیرید:

   [length (L ++ M) = length L + length M          [EQ

در اینجا ++ نشان دهنده عمل الحاق لیست هاست وL و M لیست می‌باشند. به منظور اثبات این ویژگی، ما تعاریف طول(length) و عمل الحاق(++) را نیاز داریم. قرار دهید (h : t) که لیستی را که سر (عنصر اول) آن h و دم (فهرست عناصر باقی مانده) آن T است نشان می دهد، و اجازه دهید [] نشان دهنده ی لیست خالی باشد. تعاریف طول(length) و عمل الحاق(++) عبارتند از:

   [length []     = 0                  [LEN1
   [length (h:t)  = 1 + length t       [LEN2
   
   [list = list               [APP1 ++    []
   [h:t) ++ list = h : (t ++ list)    [APP2)

گزاره (P(l ما برابراست با EQ برای همه لیست‌های M درست است اگر L برابر l باشد. می خواهیم نشان می دهیم که (P(l برای همه لیست‌های l درست است. ما این کار را با استقرای ساختاری بر لیست‌ها ثابت خواهیم کرد. ابتدا ثابت می‌کنیم که ([])P درست است. که در واقع برابر است با، EQ درست است برای همه لیستهای M زمانی که L برابر لیست خالی [] است. EQ را به صورت زیردر نظر بگیرید:

                          (length (L ++ M)  = length ([] ++ M
          (length M               (by APP1 =
                              0 + length M = 
          (length [] + length M   (by LEN1 =
                      length L  + length M = 

بنابراین این بخش از قضیه ثابت شد. EQ برای همه Mها درست است، هنگامی که L برابر [] است، چرا که سمت چپ و سمت راست برابرند. سپس، هر لیست مخالف تهی I را در نظر بگیرید. از آنجا که l مخالف تهی است، پس یک سر، x ، و یک لیست دم، xs ، دارد. بنابراین ما می‌توانیم آن را به عنوان (x: xs) بیان کنیم. فرض استقرا این است که EQ برای تمام مقادیر M زمانی است که L برابر xs است درست باشد:

       (length (xs ++ M) = length xs + length M    (hypothesis

میخواهیم نشان دهیم که در صورت برقراری این شرایط EQ برای تمام مقادیر M هنگامی که (L = I = (x: xs درست است.همانند قبل ادامه می دهیم:

                   length L  + length M      = length (x:xs) + length M
                   1 + length xs + length M =      
                       1 + (length (xs ++ M = 
                       (length (x: (xs ++ M =
                       (length ((x:xs) ++ M = 
                            (length (L ++ M =

بنابراین، ما بوسیله ی استقرای ساختاری، به دست آوردیم که (P(L برای همه لیست‌های L درست است.

خوش ترتیبی

همانگونه که استقرای ریاضی استاندارد معادل "اصل خوش ترتیبی" است، استقرای ساختاری نیز معادل یک "اصل خوش ترتیبی" است. اگر مجموعه ی تمام ساختارهای نوعی خاص یک ترتیب جزئی کامل را بپذیرد ، پس هر زیر مجموعه ناتهی باید دارای یک عنصر مینیمال باشد.(این تعریف کامل است.) اهمیت این لم در این زمینه، آن است که به ما اجازه می دهد تا استنباط کنیم که اگر هر گونه مثال نقضی برای قضیه‌ای که می خواهیم اثباتش کنیم وجود داشته باشد، پس باید یک مثال نقض مینیمم وجود داشته باشد. اگر ما بتوانیم نشان دهیم که وجود مثال نقض مینیمم دلالت می‌کند بر وجود مثال نقض‌های حتی کوچکتر، ما یک تناقض (هنگامی که مثال نقض مینیمم، کوچکترین نیست) داریم و در نتیجه مجموعه مثالهای نقض باید خالی باشد. به عنوان مثالی از این نوع استدلال، مجموعه‌ای از تمام درختان دودویی را در نظربگیرید. ما نشان خواهیم داد که تعداد برگ‌ها در یک درخت دودویی کامل یکی بیشتر از تعداد گره‌های داخلی آن است. فرض کنید یک مثال نقض وجود داشته باشد؛ پس باید یک درخت کامل با حداقل تعداد گره‌های داخلی ممکن وجود داشته باشد. این مثال نقض، C، دارای n گره داخلی وl برگ است، که در آن l ≠ n + 1 . علاوه بر این، C باید غیر بدیهی باشد، چرا که درخت بدیهی دارای n = 0 و L = 1 است و بنابراین، این یک مثال نقض نیست. در نتیجه C حداقل یک برگ که پدر آن یک گره داخلی است، دارد. حذف این برگ و پدر آن از درخت، گره برادر برگ را به موقعیت ای که قبلاً توسط پدر گره اشغال شده بود انتقال می‌دهد. این هر دوی n و l را یک واحد کاهش می دهد ، پس درخت جدید نیز دارای n + 1 ≠ l و بنابراین دارای یک مثال نقض کوچکتر است. اما بنابر فرض، C در حال حاضر کوچکترین مثال نقض بود. لذا این فرض که هرگونه مثال نقضی برای شروع وجود دارد می¬بایست فرض نادرستی باشد. "ترتیب جزئی که توسط 'کوچکتر' در اینجا گفته شد بیان می‌کند که S <T هر گاه S دارای گره‌های کمتر از T باشد.

جستارهای وابسته

• Coinduction
• Initial algebra

منابع

• Hopcroft, John E.; Rajeev Motwani; Jeffrey D. Ullman (2001). Introduction to Automata Theory, Languages, and Computation (2nd ed.). Reading Mass: Addison-Wesley. ISBN 0-201-44124-1.

Early publications about structural induction include

• Burstall, R.M. (1969). "Proving Properties of Programs by Structural Induction". The Computer Journal 12 (1): 41–48. doi:10.1093/comjnl/12.1.41.
• Aubin, Raymond (1976), Mechanizing Structural Induction, EDI-INF-PHD, 76-002, University of Edinburgh
• Huet, G.; Hullot, J.M. (1980). "Proofs by Induction in Equational Theories with Constructors". 21st Ann. Symp. on Foundations of Computer Science. IEEE. pp. 96–107