Strukturální indukce

Strukturální indukce je konstruktivní metoda matematického důkazu , která zobecňuje matematickou indukci (aplikovanou na přirozené řady) na libovolné rekurzivně definované částečně uspořádané kolekce. Strukturální rekurze je implementace strukturální indukce ve formě definice, důkazní procedury nebo programu , který poskytuje indukční přechod přes částečně uspořádanou množinu.

Zpočátku se metoda používala v matematické logice , nalezla uplatnění také v teorii grafů , kombinatorice , obecné algebře , matematické lingvistice , ale nejvíce se používala jako samostatně studovaná metoda v teoretické informatice [1] , kde se používá v otázkách sémantiky programovacích jazyků , formální verifikace , výpočetní složitosti , funkcionálního programování .

Na rozdíl od noetherovské indukce – nejobecnější formy matematické indukce aplikované na libovolné dobře podložené množiny – koncept strukturální indukce implikuje konstruktivní povahu, výpočetní implementaci. Opodstatněnost množiny je zároveň vlastností nezbytnou pro rekurzivní definovatelnost [2] , takže strukturální rekurzi lze považovat za konkrétní verzi noetherovské indukce [1] .

Historie

Využití metody se vyskytuje minimálně od 50. let 20. století, zejména v důkazu Losovy věty o ultraproduktech se používá indukce na konstrukci vzorce, přičemž samotná metoda nebyla výslovně nazývána zvláštním způsobem [3]. . Ve stejných letech byla metoda používána v teorii modelů pro důkazy nad řetězci modelů, má se za to, že právě s těmito důkazy souvisí výskyt termínu "strukturální indukce" [4] . Curry rozdělil všechny typy aplikací indukce v matematice do dvou typů – deduktivní indukce a strukturální indukce, přičemž klasickou indukci na přirozených číslech považoval za podtyp druhého zmíněného [5] .

Na druhou stranu, nejpozději počátkem 50. let 20. století byla metoda transfinitní indukce již rozšířena na libovolné částečně uspořádané množiny splňující podmínku přerušování rostoucích řetězců (což se rovná opodstatněnosti [6] ), přičemž Genkin odkazoval na možnost indukce „u některých typů, částečně uspořádaných systémů“ [7] . V 60. letech 20. století byla metoda zafixována pod názvem noetherovská indukce (analogicky s noetherovským prstencem , ve kterém je splněna podmínka přerušení rostoucích řetězců ideálů ) [8] .

Explicitní definici strukturální indukce, odkazující jak na rekurzivní definovatelnost, tak na noetherovskou indukci, podal koncem 60. let 20. století Rod Burstall [9] a v počítačové literatuře je označována jako zavedení metody [10] [ 11 ] .

Následně se v informatice objevilo několik směrů založených na strukturální indukci jako základním principu, zejména taková je strukturální operační sémantika programovacích jazyků Plotkin ( angl. Gordon Plotkin ) [12] , série induktivních metod formální verifikace. [13] [14] , strukturální rekurzivní dotazovací jazyk UnQL [15] . V 90. letech 20. století se v teoretické informatice rozšířila metoda koindukce , aplikovaná na nepodložené (obvykle nekonečné) struktury a považovaná za duální ke strukturální indukci [16] .

Vzhledem k širokému uplatnění v teoretické informatice a nedostatku odkazů v matematické literatuře se od 10. let 20. století má za to, že přidělení strukturální indukce jako speciální metody je typičtější pro informatiku než pro matematiku [17] .

Definice

Nejobecnější definice [18] [19] je zavedena pro třídu struktur (bez objasnění podstaty struktur ) s částečným řádovým vztahem mezi strukturami , s podmínkou minimálního prvku v a podmínkou přítomnosti pro každou zcela uspořádanou množinu všech přísně předcházející struktury: . Princip strukturální indukce je v tomto případě formulován následovně: jestliže splnění vlastnosti pro vyplývá z naplnění vlastnosti pro všechny struktury, které jí přesně předcházejí, pak je vlastnost splněna i pro všechny struktury třídy; symbolicky (v zápisu přirozených inferenčních systémů ): ${\mathfrak S}$ $S\in {\mathfrak {S}}$ $\sqsubseteq$ $S_{0}$ ${\mathfrak S}$ $S\in {\mathfrak {S}}$ $\triangledown S=\{T\in {\mathfrak {S}}\mid T\sqsubset S\}$ $P$ ${\mathfrak S}$

{\frac {\forall T\in \triangledown S:P(T)\Rightarrow P(S)}{\forall S\in {\mathfrak {S}}:P(S)))

Rekurzivita v této definici je implementována množinou vnořených struktur: jakmile existuje způsob, jak určit odvození vlastností struktury na základě vlastností všech předcházejících, můžeme mluvit o rekurzivní definovatelnosti struktury.

V informatické literatuře je také běžná jiná forma definice strukturální indukce, zaměřená na rekurzi pomocí konstrukce [20] , je považována za třídu objektů definovaných nad určitou množinou atomárních prvků a množinou operací , přičemž každá objekt je výsledkem sekvenční aplikace operací na atomové prvky. V této formulaci princip říká, že vlastnost je vykonána pro všechny objekty , jakmile nastane pro všechny atomární prvky a pro každou operaci , provedení vlastnosti pro prvky následuje provedení vlastnosti pro : ${\mathfrak S}$ ${\mathcal {A}}\in {\mathfrak {S}}$ $\left\{{\mathcal {o}}_{i}:{\mathfrak {S}}^{k_{i}}\to {\mathfrak {S}}\right\}$ $S\in {\mathfrak {S}}$ $P$ $S\in {\mathfrak {S}}$ ${\mathcal {o}}_{i}$ $S_{1},\tečky ,S_{i_{k}}$ ${\mathcal {o}}_{i}(S_{1},\dots ,S_{i_{k}})$

{\frac {\forall A\in {\mathcal {A):P(A),\,\forall i:(P(S_{1}),\tečky P(S_{i_{k} } \Rightarrow P({\mathcal {o}}_{i}(S_{1},\tečky ,S_{i_{k))))}{\forall S\in {\mathfrak {S}}:P ( S)}}

Roli relace dílčího řádu z obecné definice zde hraje relace inkluze konstrukcí: [21] . $\sqsubseteq$ $\forall _{j=1\dots i_{k}}S_{j}\sqsubseteq {\mathcal {o}}_{i}(S_{1},\tečky ,S_{i_{k}} )$

Příklady

Zavedení principu do informatiky bylo motivováno rekurzivní povahou datových struktur, jako jsou seznamy a stromy [22] . První Burstallův příklad nad seznamem je prohlášení o vlastnostech skládání seznamu s prvky typu dyadická funkce a prvek počátečního skládání ve spojení se zřetězením seznamu : $\circledast$ $T$ $\ast :T^{2}\to T$ $v T$ $\shortparallel$

(S_{1}\shortparallel S_{2})\circledast t=S_{1}\circledast (S_{2}\circledast t)

Strukturální indukce v důkazu tohoto tvrzení se provádí z prázdných seznamů - if , pak: $S_{1}=\bot$

levá strana podle definice zřetězení: ,

(\bot \shortparallel S_{2})\circledast t=S_{2}\circledast t

pravá strana podle definice konvoluce:

\bot \circledast (S_{2}\circledast t)=S_{2}\circledast t

a pokud seznam není prázdný a začíná prvkem , pak: $X$

levá strana, podle definic zřetězení a skládání: ,

((x::S_{1})\shortparallel S_{2})\circledast t=x\ast ((S_{1}\shortparallel S_{2})\circledast t)

pravá strana, podle definice konvoluce a předpokladu indukce: .

(x::S_{1})\circledast (S_{2}\circledast t)=x\ast ((S_{1}\shortparallel S_{2})\circledast t)

Indukční hypotéza je založena na pravdivosti tvrzení pro a inkluze . $S_{1}$ ${\displaystyle S_{1}\sqsubseteq x::S_{1))$

V teorii grafů se strukturální indukce často používá k dokazování tvrzení o vícedílných grafech (pomocí přechodu z -partite na -partite), ve větách o amalgamaci grafů , vlastnostech stromů a lesů [23] . Dalšími strukturami v matematice, pro které se uplatňuje strukturální indukce, jsou permutace , matice a jejich tenzorové produkty , konstrukce z geometrických útvarů v kombinatorické geometrii . $(k-1)$ $k$

Typickou aplikací v matematické logice a univerzální algebře je strukturální indukce na konstrukci vzorců z atomárních členů, například se ukazuje, že splnění požadované vlastnosti pro členy a implikuje , , a tak dále. Také, mnoho strukturální-induktivní důkazy v teorii automatů , matematická lingvistika pracuje na konstrukci rovnic; k prokázání syntaktické správnosti počítačových programů se hojně používá strukturální indukce na BNF definici jazyka (někdy dokonce vystupuje jako samostatný podtyp - BNF indukce [24] ). $P$ $A$ $B$ $P(A\vee B)$ $P(A\wedge B)$ $P(\lnot A)$

Poznámky

↑ 1 2 Steffen, Rüting, Huth, 2018 , str. 179.
↑ Rekurze – článek z encyklopedie matematiky . N. V. Beljakin
↑ J. Loś Quelques remarques, théorèmes et problèmes sur les class définissables d'algèbres // Studium logiky a základů matematiky. - 1955. - Sv. 16. - S. 98-113. - doi : 10.1016/S0049-237X(09)70306-4 .
↑ Gunderson, 2011 , str. 48.
↑ Curry, 1969 , přičemž zdůrazňuje: „Obyčejná matematická indukce je ze současného pohledu strukturální indukce na systému sams; je tak běžná <...>, že by měla být považována za třetí druh - přirozenou indukci.
↑ A. G. Kurosh . Přednášky o obecné algebře. - M. : Fizmatlit, 1962. - S. 21-22 (§5. Podmínka minimalizace). — 399 s.
↑ L. Genkin. O matematické indukci. - M .: Fizmatgiz , 1962. - S. 36 (závěr). — 36 s.
↑ P. Cohn . Univerzální algebra. - M .: Mir , 1969. - S. 33-34. — 351 s.
↑ Burstall, 1969 .
↑ Nástroje a pojmy pro konstrukci programu. Kurz pro pokročilé / D. Neel (ed.). - Cambridge University Press, 1982. - S. 196. - 400 s. - ISBN 0-512-24801-9 .
↑ O. A. Iljičeva. Formální popis sémantiky programovacích jazyků. - Rostov na Donu: SFU, 2007. - S. 99-100. — 223 s.
↑ G. Plotkin. Počátky strukturální operační sémantiky // The Journal of Logic and Algebraic Programming. - 2004. - S. 3-15. - doi : 10.1016/j.jlap.2004.03.009 .
↑ Z. Manna, S. Ness, J. Vuillemin. Indukční metody pro dokazování vlastností programů // Komunikace ACM . - 1973. - Sv. 16, č. 8 . - S. 491-502. - doi : 10.1145/355609.362336 .
↑ C. Reynolds, R. Yeh. Indukce jako základ pro ověření programu // Sborník příspěvků z 2. mezinárodní konference softwarového inženýrství (ICSE '76). - Los Alamitos: IEEE Computer Society Press, 1976. - S. 389 .
↑ P. Buneman, M. Fernandez, D. Suciu. UnQL: dotazovací jazyk a algebra pro semistrukturovaná data založená na strukturální rekurzi // The VLDB Journal. - 2000. - Sv. 9, č. 1 . - S. 76-110. - doi : 10.1007/s007780050084 .
↑ R. Milner , M. Tofte. Koindukce v relační sémantice // Theoretical Computer Science . — Sv. 87, č. 1 . - S. 209-220.
↑ Gunderson, 2011 , str. 48: „Ve zbytku matematiky se termín „strukturální indukce“ mimo aplikace informatiky používá jen zřídka – jak jednou řekl přítel, „všechno je to jen indukce“.
↑ Burstall, 1969 , str. 42.
↑ Gunderson, 2011 , str. 42.
↑ Steffen, Rüting, Huth, 2018 , pp. 177-178.
↑ Steffen, Rüting, Huth, 2018 , pp. 178.
↑ Burstall, 1969 , str. 43, 45.
↑ Gunderson, 2011 , str. 49, 257, 384, 245.
↑ Steffen, Rüting, Huth, 2018 , str. 214.

Literatura

B. Steffen, O. Ruthing, M. Huth. Matematické základy pokročilé informatiky. - Springer , 2018. - Sv. 1. Indukční přístupy. - ISBN 978-3-319-68396-6 .
RM Burstall. Dokazování vlastností programů strukturální indukcí // The Computer Journal . - 1969. - Sv. 12, č. 1 . — S. 41–48. - doi : 10.1093/comjnl/12.1.41 .
D. Gunderson. Příručka matematické indukce. Teorie a aplikace. - Boca Raton: CRC, 2011. - 893 s. — ISBN 978-1-4200-9364-3 .
H. Kari . Základy matematické logiky. — M .: Mir, 1969. — 567 s.