Dalgalanish - Rippling

Dalgalanish^[1] meta-daraja guruhiga ishora qiladi evristika, asosan Informatika maktabidagi Matematik fikrlash guruhida ishlab chiqilgan Edinburg universiteti va ko'pincha qo'llanma uchun ishlatiladi induktiv dalillar yilda avtomatlashtirilgan teorema isbotlovchi tizimlar. Dalgalanma cheklangan shakl sifatida qaralishi mumkin tizimni qayta yozish, bu erda qayta yozishni tugatgandan so'ng urug'lantirishni ta'minlash uchun maxsus ob'ekt darajasidagi izohlardan foydalaniladi, bu esa har qanday qayta yozish qoidalari va ifodalari uchun to'xtatilishini ta'minlaydigan talabni kamaytiradi.

Tarix

Raymond Aubin 1976 yilda nomzodlik dissertatsiyasi ustida ishlayotganda birinchi bo'lib "to'lqinlanish" atamasini ishlatgan.^[2] Edinburg universitetida. U induktiv dalillarni qayta yozish bosqichida harakatning odatiy naqshini tan oldi. Alan Bandi Keyinchalik bu tushunchani yon ta'sirga emas, balki harakatlanishning ushbu naqshiga aylantirish orqali boshiga burishdi.^{[iqtibos kerak ]}

O'shandan beri "yonboshlab to'lqinlanish", "to'lqinlanish" va "o'tmishdagi o'tmish" degan fikrlar paydo bo'ldi, shuning uchun bu atama to'lqinlanib umumlashtirildi.^{[iqtibos kerak ]} Rippling 2007 yildan boshlab Edinburgda va boshqa joylarda ishlab chiqilmoqda.

Rippling an'anaviy ravishda induktiv teoremani isbotlovchi qiyin deb hisoblangan ko'plab muammolarga, shu jumladan jamoalarga qo'llanilgan Bledsoe chegara teoremalari^{[iqtibos kerak ]} va Gordon mikroprotsessorining isboti,^{[iqtibos kerak ]} tomonidan ishlab chiqarilgan miniatyura kompyuteri Maykl J. C. Gordon va uning jamoasi Kembrijda.

Umumiy nuqtai

Ko'pincha, taklifni isbotlashga urinayotganda, biz faqat bir nechta qo'shimcha sintaktik elementlarni kiritish bilan farq qiladigan manba iborasini va maqsadli ifodani beramiz.

Bu, ayniqsa, induktivda to'g'ri keladi dalillar, bu erda berilgan ifoda induktiv gipoteza va maqsadli ifoda induktiv xulosa. Odatda, gipoteza va xulosa o'rtasidagi farqlar juda oz, ehtimol induksiya o'zgaruvchisi atrofida voris funktsiyani kiritish (masalan, +1).

Dalgalanish boshlanganda, to'lqinli jabhalar deb nomlanuvchi ikki ibora orasidagi farqlar aniqlanadi. Odatda bu farqlar dalilni to'ldirishga to'sqinlik qiladi va ularni "ko'chirish" kerak. Ikkala ibora orasidagi to'lqinlar jabhalarini (farqlari) va skeletini (umumiy tuzilishi) ajratish uchun maqsadli ifoda izohlanadi. Keyinchalik to'lqin qoidalari deb nomlangan maxsus qoidalar a da ishlatilishi mumkin tugatish isboti to'ldirish uchun manba ifodasi ishlatilguncha maqsadli ifodani boshqarish modasi.

Misol

Biz buni qo'shishni ko'rsatishni maqsad qilganmiz natural sonlar bu kommutativ. Bu elementar xususiyat va dalil odatiy induksiya bilan. Shunga qaramay, bunday dalilni qidirish maydoni juda katta bo'lishi mumkin.

Odatda, har qanday induktiv dalilning asosiy ishi to'lqinlanishdan tashqari usullar bilan hal qilinadi. Shu sababli, biz qadam holatiga e'tibor qaratamiz, bizning qadamimiz quyidagi shaklga ega, biz indüksiyon o'zgaruvchisi sifatida x dan foydalanishni tanladik:

Bizda lemmalar, induktiv ta'riflar yoki boshqa joylarda yaratilgan bir nechta qayta yozish qoidalari bo'lishi mumkin, ular to'lqin qoidalarini shakllantirish uchun ishlatilishi mumkin.

keyin quyidagilarni izohlash mumkin:

E'tibor bering, ushbu izohlangan qoidalarning barchasi skeletni saqlaydi (x + y = y + x, birinchi holda va x + y ikkinchi / uchinchi qismida). Endi induktiv qadam holatiga izoh berib, bizga quyidagilarni beradi:

Va barchamiz to'lqinlanishni amalga oshirishga tayyormiz:

E'tibor bering, yakuniy qayta yozish barcha to'lqinli jabhalarni yo'q bo'lishiga olib keladi va endi biz isbotlashni yakunlash uchun o'g'itlashni, induktiv gipotezani qo'llashni qo'llashimiz mumkin.

Adabiyotlar

Qo'shimcha o'qish

• Devid A. Bassin va Tobi Uolsh (1996). "Dalgalanma uchun hisoblash va to'xtatish" (PDF). Avtomatlashtirilgan fikrlash jurnali. 16 (1–2): 147–180. doi:10.1007 / BF00244462. S2CID  14427821.