Структурна индукција

(преусмерено са Structural induction)

Структурна индукција је пример метода која се користи у математичкој логици(нпр., пример Łoś-ове теореме), рачунарској науци, теорији графа, и неким осталим пољима математике. То је генерализација математичке индукције над природним бројевима, и може бити још генерализована до произвољне Ноетеричке индукције. Структурна рекурзије је рекурзивни метод сношења истог односа према структурној индукцији као обична рекрузија која носи обичну математичку индукцију.

Структурни индукција се користи да докаже да неки предлози P(k) важе за свако х неке врсте рекурзивно дефинисане структуре, као што су листе или стабла. Добро основани делимични редови би се дефинисали на објектима ("подлиста" за листе и "подстабла" за стабла). Доказ структурне индукције је доказ да  предлог важи за све минималне структуре, и да ако се држи за непосредне подструктуре одређене структуре С, онда мора се држати и за С такође. (Формално, онда ово задовољава премисе аксиома добро основане индукције, што тврди да су довољни за предлог да се одржи за свако х ова два услова.)

Структурно рекурзивна функција користи исту идеју да дефинише рекурзивну функцију: "класични случајеви" се баве сваком минималном структуром и правилима за рекурзије. Структурна рекурзија се обично показала тачном структуром индукције; у посебно лаким случајевима, индуктивни корак је често изостављен. Дужина и ++ функције у примеру испод су структурно рекурзивне.

На пример, ако су структуре  листе, обично се уводи делимичнан редослед '<' у којима је L <M кад год је листа L  реп листе М. Према овом редоследу, празна листа [] је јединствен минимални елеменат. Доказ структурне индукције  неког предлога P (L) се затим  састоји из два дела: А доказ да је P ([])  истинито, и доказ да ако је P (L) тачнп за неку листу L, а ако је реплисте М, онда  P (P) такође мора бити истинит.

На крају, може да постоји више од једног основног случаја, и / или више од једног индуктивног случаа, у зависности како је изграђена функција или структура. У тим случајевима, доказ структурне индукције неког предлога P (L) и затим се састоји од:А) доказа да је P (BC)  истинито за сваки основни случај BC, и Б): доказ да ако је P (I) истина за неке примере I, и М се може добити из I применом било ког рекурзивног правила једанпут, тада P (М) мора такође бити истина.

Примери уреди

 
Старо дрво предака, показује 31 особу у 5 генерација.

Дрво предака је често позната структура података; показује родитеље, бабе и деде, итд. особе познате до сад (видети слику за пример). Рекурзивно је дефинисано:

  • у најједноставнијем случају, дрво предака показује једну особу (ако ништа није познато о његовим/њеним родитељима);
  • алтернативно, дрво предака показује једну особу, и повезана је са гранама, две подргране предака његових/њених родитеља (коришћен за краткоћу поједностављења претпоставке да је један од њих познат, обоје су) .

Као пример, имовина"Дрво предака расте преко g генерација показује највише 2g-1 особа" може бити доказано структурном индукцијом која следи:

  • При најједноставнијем случају, дрво приказује само једну особу и самим тим једну генерацију, имовина је тачна за такво дрво, још од 1 ≤ 21-1.
  • Алтернативно, дрво показује једну особу и дрва његових/њених родитеља. Пошто скаи од њих је подструктура целог дрвета, може се препоставити да власништо буде доказано (илити хипотеза индукције). То је,  p ≤ 2g-1 и q ≤ 2h-1 може бити претпостављено, где g и h означавају број генерација очеве и мајчине подгране која расте, репсективно, и p и q означавају број особа које приказују.
    • У случају gh, цело дрво расте преко 1+h генерација и приказује p+q+1 особа, и p+q+1 ≤ (2g-1) + (2h-1) + 1 ≤ 2h + 2h - 1 = 21+h - 1, нпр.. цело дрво задовољава имовину.
    • У случају hg, цело дрво расте преко 1+g генерација и показује p+q+1 ≤ 21+g - 1 особа по сличном образложењу, односно цело дрво задовољава имовину и у овом случају.

Дакле, помоћу структурне индукције, сваки предак дрвета задовољава имовину.

Као још један, формалнији пример, размотрити следеће особине листе:

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

Овде ++ означава операцију надовезивања листе и L и M су листе.

Како бисмо доказали ово, потребне су нам дефиниције за дужину и за операцију надовезивања. Пустимод (h:t) ознаку листе чија је глава (први елемент) h и чији је реп (листа преосталих елемената) t, и пустимо [] да означава празну листу. Дефиниције за дужину и надовезивање су:

    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. Пошто I није празна, има главни члан, 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     (by LEN2)
                              = 1 + length (xs ++ M)         (by hypothesis)
                              = length (x: (xs ++ M))        (by LEN2)
                              = length ((x:xs) ++ M)         (by APP2)
                              = length (L ++ M) 

Тако, из структруне индукције, закључујемо да је P(L) тачан за све листе L.

Добро наручивање уреди

Баш као што је стандардна математичка индукција еквивалентна принципу доброг наручивања, структурна индукција је такође једнако добро принципу наручивања. Ако је скуп свих структура одређене врсте признања добро основан парцијални ред, онда сваки непразни подскуп мора имати најмањи елемент. (Ово је дефиниција "утемељења".) Значај леме у овом контексту је да нам дозвољава да закључимо да, ако постоје контра примери до теореме коју желимо да докажемо, онда мора постојати минимални контра пример. Ако можемо да покажемо постојање минималног контра примера који  подразумева још мањи контра пример, имамо контрадикцију (јер  минимални контра пример није минимални) па скуп контра примера мора бити празан. 

Као пример ове врсте аргумената, размотрити скуп свих бинарних стабала. Ми ћемо показати да је број листова у пуном бинарном стаблу за један више од броја унутрашњих чворова. Претпоставимо да постоји контра пример; онда мора постојати један са минималним могућем бројем унутрашњих чворова. Овај контра пример С, има n унутрашњих чворова и I лишћа, где је n+1 ≠ l. Поред тога, С мора бити нетривијалан, јер тривијално дрво има n = 0 и I = 1 и  стога, није контрапример. С дакле има најмање један лист чији  је родитељ чвор који је унутрашњи чвор. Брисањем овог листа и његовог родитеља од дрвета, промовисање листа  брата чвор на позицији раније заузетог родитеља. Ово смањује ова n и I са 1, тако да ново дрво има такође n+1 ≠ l  и због тога има мање контра примера. Али хипотезом, С је већ најмањи контра пример; дакле, претпоставка да постоје контра примери за почетак, је лажна . Делимичан редослед  подразумева  преко 'мањег' овде је онај који каже да је S <Т кад год S има мање чворова од Т.

Види још уреди

Литература уреди

  • 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. 

Ранија издавања о структруној индукцији укључују:

  • 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.  Текст „journal” игнорисан (помоћ); Недостаје или је празан параметар |title= (помоћ).
  • 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.