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

استقرای ساختاری روشی است که برای اثبات کردن قضایا از آن استفاده می شود که در منطق ریاضی ( به عنوان مثال، در اثبات قضیه لس ) ، علوم کامپیوتر، نظریه گراف، و برخی دیگر از زمینه های ریاضی کاربرد دارد. این استقرا یک تعمیم از استقراء ریاضی روی اعداد طبیعی است، و می تواند به طور قراردادی به استقرای 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 نیز باید درست باشد، می شود.