Strukturální indukce

Strukturální indukce nebo strukturální indukce je způsob definice z funkce nebo vlastnost na konstrukci, to znamená, že na objektech (matematické nebo počítač) strukturovaných jako seznamy , na strom nebo stromy binární , ale obecněji se používá na jakoukoli matematickou strukturu, která má rekurzivní definici . Tím, že stejný princip umožňuje definovat celkový predikát, tj. Který je definován všude, je strukturální indukce také metodou demonstrace vlastnosti na struktuře.

Strukturální indukce je zobecněním tradiční recidivy i konkrétním případem opodstatněné rekurence .

Příklady

Funkce definované strukturální indukcí zobecňují funkce definované indukcí na celá čísla .

Seznamy

Seznamy jsou definovány jako

• buď prázdný seznam [],
• je seznam získaný nastavení čele seznamu prvku je , dávat a: .ℓ{\ displaystyle \ ell}ℓ{\ displaystyle \ ell}

Funkce délky, která definuje délku seznamu, je definována strukturální indukcí:

• délka ([]) = 0
• délka (a :) = 1 + délka ( )ℓ{\ displaystyle \ ell}ℓ{\ displaystyle \ ell} .

Funkce concat, která spojuje dva seznamy aℓ1{\ displaystyle \ ell _ {1}}ℓ2{\ displaystyle \ ell _ {2}}

• concat ([], ) =ℓ2{\ displaystyle \ ell _ {2}}ℓ2{\ displaystyle \ ell _ {2}}
• concat (a: , ) = a: (concat ( , ))ℓ1{\ displaystyle \ ell _ {1}}ℓ2{\ displaystyle \ ell _ {2}}ℓ1{\ displaystyle \ ell _ {1}}ℓ2{\ displaystyle \ ell _ {2}}

Můžeme dokázat strukturální indukcí následující tvrzení:

délka ( concat ( )) = délka ( ) + délka ( ).ℓ1,ℓ2{\ displaystyle \ ell _ {1}, \ ell _ {2}}ℓ1{\ displaystyle \ ell _ {1}}ℓ2{\ displaystyle \ ell _ {2}}

První etapa

délka (concat ([], )) = délka ( ) = 0 + délka ( ) = délka ([]) + délka ( )ℓ2{\ displaystyle \ ell _ {2}}ℓ2{\ displaystyle \ ell _ {2}}ℓ2{\ displaystyle \ ell _ {2}}ℓ2{\ displaystyle \ ell _ {2}}

Druhý krok Důkaz využívá hypotézu strukturní indukce

Délka (concat (a: , )) = délka (A: concat ( , )) = 1 + délka (concat ( , ))ℓ1{\ displaystyle \ ell _ {1}}ℓ2{\ displaystyle \ ell _ {2}}ℓ1{\ displaystyle \ ell _ {1}}ℓ2{\ displaystyle \ ell _ {2}}ℓ1{\ displaystyle \ ell _ {1}}ℓ2{\ displaystyle \ ell _ {2}} = (strukturální indukční hypotézou) 1+ délka ( ) + délka ( ) = délka (a :) + délka ( )ℓ1{\ displaystyle \ ell _ {1}}ℓ2{\ displaystyle \ ell _ {2}}ℓ1{\ displaystyle \ ell _ {1}}ℓ2{\ displaystyle \ ell _ {2}}

Binární stromy

Zvažte binární stromy definované takto:

• ◻{\ displaystyle \ Box} pro prázdný strom,
• B B pro non-prázdné strom, jehož levý podstrom B a pravý podstrom B .1{\ displaystyle _ {1}} ∙{\ displaystyle \ bullet}2{\ displaystyle _ {2}}1{\ displaystyle _ {1}}2{\ displaystyle _ {2}}

Můžeme definovat velikostní funkci (počet vnitřních uzlů binárního stromu):

• size ( ) = 0◻{\ displaystyle \ Box}
• velikost (B B ) = velikost (B ) + velikost (B ) + 11{\ displaystyle _ {1}} ∙{\ displaystyle \ bullet}2{\ displaystyle _ {2}}1{\ displaystyle _ {1}}2{\ displaystyle _ {2}}

Zásady

Zvažte strukturu definovanou konstruktory arity . Konstruktory arity 0 jsou konstanty. F1,...,Fne{\ displaystyle f_ {1}, ..., f_ {n}}na1,...,nane{\ displaystyle a_ {1}, ..., a_ {n}}

Definice strukturální indukcí

Definice strukturní indukce funkce je napsána pro každý konstruktorG{\ displaystyle g}Fi{\ displaystyle f_ {i}}

• G(Fi(X1,..Xnai),y1,...yne)=Ei(G(X1),...,G(Xnai),y1,...,yne){\ displaystyle g (f_ {i} (x_ {1}, .. x_ {a_ {i}}), y_ {1}, ... y_ {n}) = E_ {i} (g (x_ {1 }), ..., g (x_ {a_ {i}}), y_ {1}, ..., y_ {n})}

kde je výraz, který závisí na i '. Všimněte si, že pokud je konstanta, je definice základního případu:Ei{\ displaystyle E_ {i}}Fi{\ displaystyle f_ {i}}

• G(Fi,y1,...yne)=Ei(y1,...,yne){\ displaystyle g (f_ {i}, y_ {1}, ... y_ {n}) = E_ {i} (y_ {1}, ..., y_ {n})}

Odůvodnění strukturální indukcí

Demonstrační diagram, že vlastnost P je platná pro celou strukturu, je prezentován ve formě pravidla odvození pro každý konstruktorFi{\ displaystyle f_ {i}}

P(X1)...P(Xnai)P(Fi(X1,...,Xnai)){\ displaystyle {\ frac {P (x_ {1}) ... P (x_ {a_ {i}})} {P (f_ {i} (x_ {1}, ..., x_ {a_ {i }}))}}}

Je proto nutné provést demonstraci „dědičnosti“ pro každého konstruktéra.

Případ přirozených čísel

Případ přirozených celých čísel je takový, kde existují dva konstruktory: 0 arity 0 (tedy konstanta) a succ (jinými slovy +1 ) arity 1 . Tradiční opakování se proto u těchto dvou výrobců snižuje na strukturální opakování.

Bibliografie

• (en) John E. Hopcroft , Rajeev Motwani a Jeffrey D. Ullman, Úvod do teorie automatů, jazyků a výpočtů , četba, Addison-Wesley ,2001, 2.  vyd. , 521  str. ( ISBN  0-201-44124-1 )
• (en) RM Burstall , „  Proving Properties of Programs by Structural Induction  “ , The Computer Journal , sv.  12, n o  1,Únor 1968, str.  41–48 ( DOI  10.1093 / comjnl / 12.1.41 , číst online )
• Niklaus Wirth , Algoritmy a datové struktury , Prentice Hall ,1985( číst online )
• Horst Reichel, Strukturální indukce parciálních algeber , Akademie-Verlag,1984
• Jason Filippou, "  Strukturální indukce  " ,7. května 2016
• Rozsa Peter , Über die Verallgemeinerung der Theorie der rekursiven Funktionen für abstrakte Mengen geeigneter Struktur als Definitionsbereiche , Symposium International, Varšava (Září 1959) ( Zobecnění teorie rekurzivních funkcí na abstraktní množiny s, jako doménami, přizpůsobenými strukturami ) .

Podívejte se také

• Definice indukcí
• Opodstatněný řád
• Odůvodnění opakováním
• Transfinitní opakování
• Termín (logický)

<img src="https://fr.wikipedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" title="" width="1" height="1" style="border: none; position: absolute;">