Strukturális indukció

A strukturális indukció a matematikai bizonyítás konstruktív módszere , amely a matematikai indukciót (természetes sorozatokra alkalmazva) tetszőleges, rekurzívan meghatározott , részben rendezett gyűjteményekre általánosítja. A strukturális rekurzió a strukturális indukció megvalósítása definíció, bizonyítási eljárás vagy program formájában , amely induktív átmenetet biztosít egy részben rendezett halmazon.

módszert kezdetben a matematikai logikában használták, a gráfelméletben , a kombinatorikában , az általános algebrában , a matematikai nyelvészetben is alkalmazták , de legszélesebb körben az elméleti számítástechnikában önállóan tanulmányozott módszerként alkalmazták [1] , ahol a programozási nyelvek szemantikája , formális ellenőrzés , számítási összetettség , funkcionális programozás terén használják .

A Noether-indukcióval ellentétben - a matematikai indukció legáltalánosabb formája, amelyet tetszőleges jól megalapozott halmazokon alkalmaznak - a strukturális indukció fogalma konstruktív természetet, számítási megvalósítást foglal magában. Ugyanakkor a halmaz megalapozottsága a rekurzív definiálhatósághoz szükséges tulajdonság [2] , így a strukturális rekurzió a Noether-indukció egy sajátos változatának tekinthető [1] .

Történelem

A módszer alkalmazása legalább az 1950-es évektől előfordul, különösen a Los-tétel ultratermékekre vonatkozó bizonyítása során , a képlet felépítésére indukciót alkalmaznak, míg magát a módszert nem nevezték kifejezetten speciális módon [3] . Ugyanebben az években a modellelméletben is alkalmazták a módszert a modellláncokon átívelő bizonyításokra; úgy vélik, hogy a "strukturális indukció" kifejezés megjelenése pontosan ezekhez a bizonyításokhoz kapcsolódik [4] . Curry az indukció minden alkalmazási típusát a matematikában két típusra osztotta – a deduktív indukcióra és a strukturális indukcióra, a természetes számokon végzett klasszikus indukciót az utóbbi altípusának tekintve [5] .

Másrészt, legkésőbb az 1950-es évek elején a transzfinit indukció módszerét már kiterjesztették tetszőleges, részben rendezett halmazokra, amelyek kielégítik a növekvő láncok megszakításának feltételét (ami egyenértékű a megalapozottsággal [6] ), míg Genkin utalt az indukció lehetőségére „bizonyos típusú, részben rendezett rendszerekben” [7] . Az 1960-as években a módszert Noether-indukció néven rögzítették (a Noether-gyűrű analógiájára , amelyben teljesül a növekvő ideálláncok megszakításának feltétele ) [8] .

A rekurzív definiálhatóságra és a Noether-indukcióra egyaránt utaló strukturális indukció explicit definícióját Rod Burstall adta meg az 1960 - as évek végén [9] , a számítástechnikai szakirodalom pedig a módszer bevezetéseként említi [10] [11 ]. ] .

A későbbiekben a strukturális indukcióra mint alapelvre épülő számítástechnikában több irány is megjelent, különösen ilyen a Plotkin programozási nyelvek strukturális működési szemantikája ( Gordon Plotkin ) [ 12] , a formális verifikáció induktív módszereinek sorozata. [13] [14] , UnQL strukturális rekurzív lekérdező nyelv [15] . Az 1990-es években az elméleti számítástechnikában elterjedt az alaptalan (általában végtelen) struktúrákon alkalmazott, a szerkezeti indukcióval kettősnek tekintett koindukciós módszer [16] .

Az elméleti számítástechnikában való széleskörű alkalmazás és a matematikai irodalomban található hivatkozások szűkössége miatt a 2010-es évektől úgy vélik, hogy a strukturális indukció, mint speciális módszer kijelölése inkább a számítástechnikára, mint a matematikára jellemző [17] .

Definíció

A legáltalánosabb definíciót [18] [19] a struktúrák egy osztályára vezetjük be (a struktúrák természetének tisztázása nélkül ), ahol a struktúrák között részleges sorrendi kapcsolat van , a minimális elemfeltétel és a jelenléti feltétel minden egyes teljesen rendezett halmazhoz. szigorúan megelőző szerkezetek: . A szerkezeti indukció elve ebben az esetben a következőképpen fogalmazódik meg: ha egy tulajdonság teljesülése következik az azt szigorúan megelőző összes szerkezetre vonatkozó tulajdonság teljesüléséből, akkor a tulajdonság az osztály összes szerkezetére is teljesül; szimbolikusan (a természetes következtetési rendszerek jelölésével ): ${\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)))

A rekurzivitást ebben a definícióban egymásba ágyazott struktúrák halmaza valósítja meg: amint mód nyílik egy struktúra tulajdonságainak származtatásának meghatározására az azt megelőző összes tulajdonság alapján, beszélhetünk a struktúra rekurzív definiálhatóságáról.

A számítástechnikai szakirodalomban a szerkezeti indukció egy másik definíciós formája is elterjedt, amely a konstrukciós rekurzióra fókuszál [20] , ezt olyan objektumok osztályának tekintik, amelyek meghatározott atomi elemek halmazán és műveletek halmazán definiálhatók . az objektum az atomelemekre végrehajtott szekvenciális műveletek eredménye. Ebben a megfogalmazásban az elv kimondja, hogy egy tulajdonság minden objektumra végrehajtódik , amint az összes atomi elemre bekövetkezik, és minden egyes műveletnél az elemekre vonatkozó tulajdonság végrehajtása követi a tulajdonság végrehajtását : ${\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},\dots ,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}),\dots P(S_{i_{k} } \Rightarrow P({\mathcal {o}}_{i}(S_{1},\dots ,S_{i_{k))))}{\forall S\in {\mathfrak {S}}:P ( S)}}

A részleges sorrendi reláció szerepét az általános definícióból itt a konstrukciós befogadás viszonya játssza: [21] . $\sqsubseteq$ $\forall _{j=1\dots i_{k}}S_{j}\sqsubseteq {\mathcal {o}}_{i}(S_{1},\dots ,S_{i_{k}} )$

Példák

Az elv számítástechnikába való bevezetését az adatstruktúrák, például listák és fák rekurzív jellege motiválta [22] . Burstall első példája a listákon egy kijelentés a listák hajtásainak tulajdonságairól diadikus függvény típusú elemekkel és kezdeti hajtási elemekkel a lista összefűzésével kapcsolatban : $\circledast$ $T$ $\ast :T^{2}\to T$ $t\in T$ $\shortparallel$

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

A strukturális indukció ennek az állításnak a bizonyításában üres listákból történik - ha , akkor: $S_{1}=\bot$

bal oldal, az összefűzés definíciója szerint: ,

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

a jobb oldal a konvolúció meghatározása szerint:

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

és ha a lista nem üres, és az elemmel kezdődik , akkor: $x$

a bal oldal, az összefűzés és hajtogatás definíciói szerint: ,

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

a jobb oldal a konvolúció definíciója és az indukció feltevése szerint: .

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

Az indukciós hipotézis a for állítás és a befogadás igazságosságán alapul . $S_{1}$ ${\displaystyle S_{1}\sqsubseteq x::S_{1))$

A gráfelméletben a strukturális indukciót gyakran használják a többrészes gráfokra vonatkozó állítások bizonyítására (a -partiteról a -partitera), a gráfösszevonási tételekben a fák és erdők tulajdonságaira [23] . A matematikában további olyan struktúrák , amelyekre strukturális indukciót alkalmaznak , a permutációk , mátrixok és tenzorszorzataik , a kombinatorikus geometriában a geometriai alakzatokból származó konstrukciók . $(k-1)$ $k$

A matematikai logikában és az univerzális algebrában egy tipikus alkalmazás a strukturális indukció a képletek atomi tagokból való felépítésére, például megmutatjuk, hogy a kifejezések és a kifejezések megkívánt tulajdonságának teljesülése magában foglalja a , és így tovább. Ezenkívül számos strukturális-induktív bizonyítás az automataelméletben , a matematikai nyelvészetben a képletek felépítésén dolgozik; a számítógépes programok szintaktikai helyességének bizonyítására széles körben alkalmazzák a nyelv BNF definícióján a strukturális indukciót (néha még külön altípusként is kiemelkedik - BNF indukció [24] ). $P$ $A$ $B$ $P(A\vee B)$ $P(A\wedge B)$ $P(\lnot A)$

Jegyzetek

↑ 1 2 Steffen, Rüting, Huth, 2018 , p. 179.
↑ Recursion - Encyclopedia of Mathematics cikk . N. V. Belyakin
↑ J. Loś Quelques remarques, théorèmes et problèmes sur les classes définissables d'algèbres // Studies in Logic and the Foundations of Mathematics. - 1955. - 1. évf. 16. - P. 98-113. - doi : 10.1016/S0049-237X(09)70306-4 .
↑ Gunderson, 2011 , p. 48.
↑ Curry, 1969 , miközben rámutat: „A közönséges matematikai indukció jelen nézőpontból strukturális indukció sams rendszeren; annyira elterjedt <...>, hogy harmadik fajtának – természetes indukciónak – kell tekinteni.
↑ A. G. Kurosh . Előadások az általános algebráról. - M. : Fizmatlit, 1962. - S. 21-22 (§5. Minimális feltétel). — 399 p.
↑ L. Genkin. A matematikai indukcióról. - M .: Fizmatgiz , 1962. - S. 36 (következtetés). — 36 s.
↑ P. Cohn . Univerzális algebra. - M . : Mir , 1969. - S. 33-34. — 351 p.
↑ Burstall, 1969 .
↑ Eszközök és fogalmak a programkészítéshez. Advanced Course / D. Neel (szerk.). - Cambridge University Press, 1982. - S. 196. - 400 p. - ISBN 0-512-24801-9 .
↑ O. A. Iljicseva. A programozási nyelvek szemantikájának formális leírása. - Rostov-on-Don: SFU, 2007. - S. 99-100. — 223 p.
↑ G. Plotkin. A strukturális műveleti szemantika eredete // The Journal of Logic and Algebraic Programming. - 2004. - P. 3-15. - doi : 10.1016/j.jlap.2004.03.009 .
↑ Z. Manna, S. Ness, J. Vuillemin. Induktív módszerek a programok tulajdonságainak bizonyítására // Az ACM kommunikációja . - 1973. - 1. évf. 16., 8. sz . - P. 491-502. - doi : 10.1145/355609.362336 .
↑ C. Reynolds, R. Yeh. Bevezetés, mint a programellenőrzés alapja // A 2. nemzetközi szoftverfejlesztési konferencia (ICSE '76) előadásai. - Los Alamitos: IEEE Computer Society Press, 1976. - 389. o .
↑ P. Buneman, M. Fernandez, D. Suciu. UnQL: lekérdezési nyelv és algebra félig strukturált adatokhoz szerkezeti rekurzión alapuló // The VLDB Journal. - 2000. - Vol. 9, 1. sz . - P. 76-110. - doi : 10.1007/s007780050084 .
↑ R. Milner , M. Tofte. Koindukció a relációs szemantikában // Theoretical Computer Science . — Vol. 87, 1. sz . - P. 209-220.
↑ Gunderson, 2011 , p. 48: „A matematika többi részében a „strukturális indukció” kifejezést ritkán használják a számítástechnikai alkalmazásokon kívül – ahogy egy barátom mondta egyszer: „az egész csak indukció”.
↑ Burstall, 1969 , p. 42.
↑ Gunderson, 2011 , p. 42.
↑ Steffen, Rüting, Huth, 2018 , pp. 177-178.
↑ Steffen, Rüting, Huth, 2018 , pp. 178.
↑ Burstall, 1969 , p. 43, 45.
↑ Gunderson, 2011 , p. 49, 257, 384, 245.
↑ Steffen, Rüting, Huth, 2018 , p. 214.

Irodalom

B. Steffen, O. Ruthing, M. Huth. A haladó informatika matematikai alapjai. - Springer , 2018. - Vol. 1. Induktív megközelítések. - ISBN 978-3-319-68396-6 .
RM Burstall. Programok tulajdonságainak bizonyítása strukturális indukcióval // The Computer Journal . - 1969. - 1. évf. 12, 1. sz . — P. 41–48. - doi : 10.1093/comjnl/12.1.41 .
D. Gunderson. Matematikai indukció kézikönyve. Elmélet és alkalmazások. - Boca Raton: CRC, 2011. - 893 p. — ISBN 978-1-4200-9364-3 .
H. Curry . A matematikai logika alapjai. — M .: Mir, 1969. — 567 p.