Strukturna indukcija
Strukturna indukcija je primer metoda koja se koristi u matematičkoj logici(npr., primer Łoś-ove teoreme), računarskoj nauci, teoriji grafa, i nekim ostalim poljima matematike. To je generalizacija matematičke indukcije nad prirodnim brojevima, i može biti još generalizovana do proizvoljne Noeteričke indukcije. Strukturna rekurzije je rekurzivni metod snošenja istog odnosa prema strukturnoj indukciji kao obična rekruzija koja nosi običnu matematičku indukciju.
Strukturni indukcija se koristi da dokaže da neki predlozi P(k) važe za svako h neke vrste rekurzivno definisane strukture, kao što su liste ili stabla. Dobro osnovani delimični redovi bi se definisali na objektima ("podlista" za liste i "podstabla" za stabla). Dokaz strukturne indukcije je dokaz da predlog važi za sve minimalne strukture, i da ako se drži za neposredne podstrukture određene strukture S, onda mora se držati i za S takođe. (Formalno, onda ovo zadovoljava premise aksioma dobro osnovane indukcije, što tvrdi da su dovoljni za predlog da se održi za svako h ova dva uslova.)
Strukturno rekurzivna funkcija koristi istu ideju da definiše rekurzivnu funkciju: "klasični slučajevi" se bave svakom minimalnom strukturom i pravilima za rekurzije. Strukturna rekurzija se obično pokazala tačnom strukturom indukcije; u posebno lakim slučajevima, induktivni korak je često izostavljen. Dužina i ++ funkcije u primeru ispod su strukturno rekurzivne.
Na primer, ako su strukture liste, obično se uvodi delimičnan redosled '<' u kojima je L <M kad god je lista L rep liste M. Prema ovom redosledu, prazna lista [] je jedinstven minimalni elemenat. Dokaz strukturne indukcije nekog predloga P (L) se zatim sastoji iz dva dela: A dokaz da je P ([]) istinito, i dokaz da ako je P (L) tačnp za neku listu L, a ako je repliste M, onda P (P) takođe mora biti istinit.
Na kraju, može da postoji više od jednog osnovnog slučaja, i / ili više od jednog induktivnog slučaa, u zavisnosti kako je izgrađena funkcija ili struktura. U tim slučajevima, dokaz strukturne indukcije nekog predloga P (L) i zatim se sastoji od:A) dokaza da je P (BC) istinito za svaki osnovni slučaj BC, i B): dokaz da ako je P (I) istina za neke primere I, i M se može dobiti iz I primenom bilo kog rekurzivnog pravila jedanput, tada P (M) mora takođe biti istina.
Primeri[uredi | uredi izvor]
Drvo predaka je često poznata struktura podataka; pokazuje roditelje, babe i dede, itd. osobe poznate do sad (videti sliku za primer). Rekurzivno je definisano:
- u najjednostavnijem slučaju, drvo predaka pokazuje jednu osobu (ako ništa nije poznato o njegovim/njenim roditeljima);
- alternativno, drvo predaka pokazuje jednu osobu, i povezana je sa granama, dve podrgrane predaka njegovih/njenih roditelja (korišćen za kratkoću pojednostavljenja pretpostavke da je jedan od njih poznat, oboje su) .
Kao primer, imovina"Drvo predaka raste preko g generacija pokazuje najviše 2g-1 osoba" može biti dokazano strukturnom indukcijom koja sledi:
- Pri najjednostavnijem slučaju, drvo prikazuje samo jednu osobu i samim tim jednu generaciju, imovina je tačna za takvo drvo, još od 1 ≤ 21-1.
- Alternativno, drvo pokazuje jednu osobu i drva njegovih/njenih roditelja. Pošto skai od njih je podstruktura celog drveta, može se prepostaviti da vlasništo bude dokazano (iliti hipoteza indukcije). To je, p ≤ 2g-1 i q ≤ 2h-1 može biti pretpostavljeno, gde g i h označavaju broj generacija očeve i majčine podgrane koja raste, repsektivno, i p i q označavaju broj osoba koje prikazuju.
- U slučaju g ≤ h, celo drvo raste preko 1+h generacija i prikazuje p+q+1 osoba, i p+q+1 ≤ (2g-1) + (2h-1) + 1 ≤ 2h + 2h - 1 = 21+h - 1, npr.. celo drvo zadovoljava imovinu.
- U slučaju h ≤ g, celo drvo raste preko 1+g generacija i pokazuje p+q+1 ≤ 21+g - 1 osoba po sličnom obrazloženju, odnosno celo drvo zadovoljava imovinu i u ovom slučaju.
Dakle, pomoću strukturne indukcije, svaki predak drveta zadovoljava imovinu.
Kao još jedan, formalniji primer, razmotriti sledeće osobine liste:
length (L ++ M) = length L + length M [EQ]
Ovde ++ označava operaciju nadovezivanja liste i L i M su liste.
Kako bismo dokazali ovo, potrebne su nam definicije za dužinu i za operaciju nadovezivanja. Pustimod (h:t) oznaku liste čija je glava (prvi element) h i čiji je rep (lista preostalih elemenata) t, i pustimo [] da označava praznu listu. Definicije za dužinu i nadovezivanje su:
length [] = 0 [LEN1]
length (h:t) = 1 + length t [LEN2]
[] ++ list = list [APP1]
(h:t) ++ list = h : (t ++ list) [APP2]
Naša pozicija P(l)je ta da je EQ tačno za sve liste M kada jeL l. Želimo da pokažemo da je P(l) tačno za sve liste l. Dokazaćemo ovo preko strukturne indukcije na listama
Prvo ćemo dokazati da je P([])tačno;da je, EQ tačno za sve liste M kada L postane prazna lista []. Razmotriti EQ:
length (L ++ M) = length ([] ++ M)
= length M (by APP1)
= 0 + length M
= length [] + length M (by LEN1)
= length L + length M
Ovaj deo teoreme je dokazan; EQ je tačan za sve M, kada je L [], zato što leva i desna strana ruke su jednake.
Sledeće, razmotriti bilo koju nepraznu listu I. Pošto I nije prazna, ima glavni član, x, i rep liste, xs, tako da ga možemo izraziti kao (x:xs). Hipoteza indukcija je ta da je EQ za sve vrednosti M kada je L xs:
length (xs ++ M) = length xs + length M (hypothesis)
Želeli bismo da pokažemo da ako je ovo slučaj, onda je EQ takođe tačan za sve vrednosti M kada je L = I = (x:xs). Nastavljamo kao i pre:
length L + length M = length (x:xs) + length M
= 1 + length xs + length M (by LEN2)
= 1 + length (xs ++ M) (by hypothesis)
= length (x: (xs ++ M)) (by LEN2)
= length ((x:xs) ++ M) (by APP2)
= length (L ++ M)
Tako, iz struktrune indukcije, zaključujemo da je P(L) tačan za sve liste L.
Dobro naručivanje[uredi | uredi izvor]
Baš kao što je standardna matematička indukcija ekvivalentna principu dobrog naručivanja, strukturna indukcija je takođe jednako dobro principu naručivanja. Ako je skup svih struktura određene vrste priznanja dobro osnovan parcijalni red, onda svaki neprazni podskup mora imati najmanji element. (Ovo je definicija "utemeljenja".) Značaj leme u ovom kontekstu je da nam dozvoljava da zaključimo da, ako postoje kontra primeri do teoreme koju želimo da dokažemo, onda mora postojati minimalni kontra primer. Ako možemo da pokažemo postojanje minimalnog kontra primera koji podrazumeva još manji kontra primer, imamo kontradikciju (jer minimalni kontra primer nije minimalni) pa skup kontra primera mora biti prazan.
Kao primer ove vrste argumenata, razmotriti skup svih binarnih stabala. Mi ćemo pokazati da je broj listova u punom binarnom stablu za jedan više od broja unutrašnjih čvorova. Pretpostavimo da postoji kontra primer; onda mora postojati jedan sa minimalnim mogućem brojem unutrašnjih čvorova. Ovaj kontra primer S, ima n unutrašnjih čvorova i I lišća, gde je n+1 ≠ l. Pored toga, S mora biti netrivijalan, jer trivijalno drvo ima n = 0 i I = 1 i stoga, nije kontraprimer. S dakle ima najmanje jedan list čiji je roditelj čvor koji je unutrašnji čvor. Brisanjem ovog lista i njegovog roditelja od drveta, promovisanje lista brata čvor na poziciji ranije zauzetog roditelja. Ovo smanjuje ova n i I sa 1, tako da novo drvo ima takođe n+1 ≠ l i zbog toga ima manje kontra primera. Ali hipotezom, S je već najmanji kontra primer; dakle, pretpostavka da postoje kontra primeri za početak, je lažna . Delimičan redosled podrazumeva preko 'manjeg' ovde je onaj koji kaže da je S <T kad god S ima manje čvorova od T.
Vidi još[uredi | uredi izvor]
Literatura[uredi | uredi izvor]
- Hopcroft, John E.; Rajeev Motwani; Jeffrey D. Ullman Introduction to Automata Theory, Languages, and Computation . Reading Mass: Addison-Wesley. (2nd изд.). 2001. ISBN 978-0-201-44124-6.
Ranija izdavanja o struktrunoj indukciji uključuju:
- 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. Tekst „journal” ignorisan (pomoć); Nedostaje ili je prazan parametar
|title=(pomoć). - 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.