Структурна індукція

Структу́рна інду́кція — конструктивний метод математичного доведення, який узагальнює математичну індукцію (застосовувану над натуральним рядом) на довільні рекурсивно означені частково впорядковані сукупності. Структурна рекурсія — реалізація структурної індукції у формі визначення, процедури доведення або програми, що забезпечує індукційний перехід над частково впорядкованою сукупністю.

Спочатку^[⇨] метод використовувався в математичній логіці, також знайшов застосування^[⇨] в теорії графів, комбінаториці, загальній алгебрі, математичній лінгвістиці, але найбільшого поширення як самостійно досліджуваний метод набув у теоретичній інформатиці, де застосовується в питаннях семантики мов програмування, формальної верифікації, обчислювальної складності, функційного програмування.

На відміну від нетерівської індукції — найзагальнішої форми математичної індукції, застосовуваної над довільними фундованими множинами, — в понятті про структурну індукцію мається на увазі конструктивний характер, обчислювальна реалізація. При цьому фундованість сукупності — властивість, необхідна для рекурсивної ви́значності, таким чином, структурну рекурсію можна вважати частковим варіантом нетерівської індукції.

Історія

Використання методу зустрічається принаймні від 1950-х років, зокрема, в доведенні застосовується індукція побудови формули, при цьому сам метод особливим чином явно не називався. У ті ж роки метод застосовувався в теорії моделей для доведень над ланцюгами моделей, вважається, що поява терміна «структурна індукція» пов'язана саме з цими доведеннями. Карі поділив усі види застосування індукції в математиці на два типи — дедуктивну індукцію і структурну індукцію, класичну індукцію над натуральними числами вважаючи підтипом останньої.

З іншого боку, не пізніше початку 1950-х років метод трансфінітної індукції вже поширювався на довільні частково впорядковані множини, що задовольняють умову обриву ростучих ланцюгів (що еквівалентно фундованості), в той же час ^[ru] відсилав до можливості індукції «в деяких типах частково впорядкованих систем». У 1960-х роках метод закріпився під назвою нетерівська індукція (за аналогією з нетерівським кільцем, у якому виконано умову обриву ростучих ланцюгів ідеалів).

Явне визначення структурної індукції, яке посилається як на рекурсивну ви́значність, так і на нетерівську індукцію, дав ^[en]) наприкінці 1960-х років, і в літературі з інформатики саме до нього відносять уведення методу.

Надалі в інформатиці утворилося декілька напрямів, які ґрунтуються на структурній індукції як базовому принципі, зокрема, такими є мов програмування ^[en]), серія індуктивних методів формальної верифікації, структурно-рекурсивна мова запитів . У 1990-х роках у теоретичній інформатиці поширився метод коіндукції, застосовуваний над нефундованих (як правило, нескінченних) структурах, який вважають дуальним для структурної індукції.

Через широке застосування в теоретичній інформатиці і нечисленність згадок у математичній літературі, станом на 2010-ті роки вважається, що виділення структурної індукції як особливого методу більшою мірою характерне для інформатики, ніж для математики.

Визначення

Найзагальніше визначення вводиться для класу структур ${\displaystyle {\mathfrak {S}}}$ (без уточнення природи структур ${\displaystyle S\in {\mathfrak {S}}}$) з відношенням часткового порядку між структурами ${\displaystyle \sqsubseteq }$, з умовою мінімального елемента ${\displaystyle S_{0}}$ в ${\displaystyle {\mathfrak {S}}}$ і умовою наявності для кожної ${\displaystyle S\in {\mathfrak {S}}}$ цілком упорядкованої сукупності зі всіх структур, що суворо передують їй: ${\displaystyle \triangledown S=\{T\in {\mathfrak {S}}\mid T\sqsubset S\}}$. Принцип структурної індукції в цьому випадку формулюється так: якщо виконання властивості ${\displaystyle P}$ для ${\displaystyle {\mathfrak {S}}}$ випливає з виконання властивості для всіх структур, що суворо передують їй, то властивість виконано і для всіх структур класу; символічно (в позначеннях ^[en]):

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

Рекурсивність у цьому визначенні реалізується сукупністю вкладених структур: як тільки є спосіб виводити властивості структури виходячи зі властивостей усіх попередніх їй, можна говорити про рекурсивну визначність структури.

В літературі з інформатики поширена й інша форма визначення структурної індукції, орієнтована на рекурсію за побудовою, в ній ${\displaystyle {\mathfrak {S}}}$ розглядається як клас об'єктів, визначених над деякою множиною атомарних елементів ${\displaystyle {\mathcal {A}}\in {\mathfrak {S}}}$ і набором операцій ${\displaystyle \left\{{\mathcal {o}}_{i}:{\mathfrak {S}}^{k_{i}}\to {\mathfrak {S}}\right\}}$, при цьому кожен об'єкт ${\displaystyle S\in {\mathfrak {S}}}$ — результат послідовного застосування операцій до атомарних елементів. У цьому формулюванні принцип стверджує, що властивість ${\displaystyle P}$ виконується для всіх об'єктів ${\displaystyle S\in {\mathfrak {S}}}$, як тільки має місце для всіх атомарних елементів і для кожної операції ${\displaystyle {\mathcal {o}}_{i}}$ з виконання властивості для елементів ${\displaystyle S_{1},\dots ,S_{i_{k}}}$ слідує виконання властивості для ${\displaystyle {\mathcal {o}}_{i}(S_{1},\dots ,S_{i_{k}})}$:

${\displaystyle {\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)}}}$.

Роль відношення часткового порядку ${\displaystyle \sqsubseteq }$ з загального визначення тут грає відношення включення за побудовою: ${\displaystyle \forall _{j=1\dots i_{k}}S_{j}\sqsubseteq {\mathcal {o}}_{i}(S_{1},\dots ,S_{i_{k}})}$.

Приклади

Запровадження принципу в інформатику мотивувалося рекурсивним характером таких структур даних, як списки і дерева. Перший приклад над списком, наведений Берстоллом — твердження про властивості ^[ru] ${\displaystyle \circledast }$ з елементами типу ${\displaystyle T}$ двомісною функцією ${\displaystyle \ast :T^{2}\to T}$ і початковим елементом згортки ${\displaystyle t\in T}$ у зв'язку з конкатенацією списків ${\displaystyle \shortparallel }$:

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

Структурна індукція в доведенні цього твердження ведеться від порожніх списків — якщо ${\displaystyle S_{1}=\bot }$, то:

ліва частина, за визначенням конкатенації: ${\displaystyle (\bot \shortparallel S_{2})\circledast t=S_{2}\circledast t}$,

права частина, за визначенням згортки: ${\displaystyle \bot \circledast (S_{2}\circledast t)=S_{2}\circledast t}$

і в разі, якщо список непорожній, і починається елементом ${\displaystyle x}$, то:

ліва частина, за визначенням конкатенації та згортки: ${\displaystyle ((x::S_{1})\shortparallel S_{2})\circledast t=x\ast ((S_{1}\shortparallel S_{2})\circledast t)}$,

права частина, за визначенням згортки і припущенням індукції: ${\displaystyle (x::S_{1})\circledast (S_{2}\circledast t)=x\ast ((S_{1}\shortparallel S_{2})\circledast t)}$.

Припущення індукції ґрунтується на істинності твердження ${\displaystyle S_{1}}$ і включення ${\displaystyle S_{1}\sqsubseteq x::S_{1}}$.

В теорії графів структурна індукція часто застосовується для доведення тверджень про багатодольні графи (з використанням переходу від ${\displaystyle (k-1)}$-дольних до ${\displaystyle k}$-дольних), у теоремах про ^[en], властивостей дерев і лісів. Інші структури в математиці, для яких застосовується структурна індукція — перестановки, матриці і їх тензорні добутки, конструкції з геометричних фігур у комбінаторній геометрії.

Типове застосування в математичній логіці та універсальній алгебрі — структурна індукція побудови формул з атомарних термів, наприклад, показується, що виконання необхідної властивості ${\displaystyle P}$ для термів ${\displaystyle A}$ і ${\displaystyle B}$ тягне ${\displaystyle P(A\vee B)}$, ${\displaystyle P(A\wedge B)}$, ${\displaystyle P(\lnot A)}$ і так далі. Також за побудовою формул виконуються багато структурно-індуктивних доведень у теорії автоматів, математичній лінгвістиці; для доведення синтаксичної коректності комп'ютерних програм широко використовується структурна індукція за БНФ-визначенням мови (іноді навіть виділяється в окремий підтип — БНФ-індукція).

Примітки

1. Штеффен, Рютинг, Хут, 2018, с. 179.
2. [Рекурсия Структурна індукція] — стаття з Математичної енциклопедії
3. ^[pl]. 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. — Т. 16 (16 червня). — С. 98—113. — DOI:10.1016/S0049-237X(09)70306-4.
4. Гундерсон, 2011, с. 48.
5. Карри, 1969, при цьому зазначаючи: «Звичайна математична індукція зі справжньої точки зору є структурною індукцією...; вона так часто зустрічається <...> що варто вважати її третім видом - натуральною індукцією».
6. . Лекции по общей алгебре. — М. : Физматлит, 1962. — С. 21—22 (§5. Условие минимальности).
7. Л. Генкин. О математической индукции. — М. : , 1962. — С. 36 (заключение).
8. . Универсальная алгебра. — М. : Мир, 1969. — С. 33—34.
9. Бёрстолл, 1969.
10. Tools and Notions for Program Construction. An Advanced Course / D. Néel (ed.). — Cambridge University Press, 1982. — С. 196. — .
11. О. А. Ильичёва. Формальное описание семантики языков программирования. — Ростов-на-Дону : ЮФУ, 2007. — С. 99—100.
12. G. Plotkin. The origins of structural operational semantics // The Journal of Logic and Algebraic Programming. — 2004. — 16 червня. — С. 3—15. — DOI:10.1016/j.jlap.2004.03.009.
13. Z. Manna, S. Ness, J. Vuillemin. Inductive methods for proving properties of programs // Communications of the ACM. — 1973. — Т. 16, № 8 (16 червня). — С. 491—502. — DOI:10.1145/355609.362336.
14. C. Reynolds, R. Yeh. Induction as the basis for program verification // Proceedings of the 2^nd international conference on Software engineering (ICSE ’76). — Los Alamitos : IEEE Computer Society Press, 1976. — 16 червня. — С. 389.
15. P. Buneman, M. Fernandez, D. Suciu. UnQL: a query language and algebra for semistructured data based on structural recursion // The VLDB Journal. — 2000. — Т. 9, № 1 (16 червня). — С. 76—110. — DOI:10.1007/s007780050084.
16. R. Milner, M. Tofte. Co-induction in relational semantics // Theoretical Computer Science. — Т. 87, № 1. — С. 209—220.
17. Бёрстолл, 1969, с. 42.
18. Гундерсон, 2011, с. 42.
19. Штеффен, Рютинг, Хут, 2018, с. 177—178.
20. Штеффен, Рютинг, Хут, 2018, с. 178.
21. Бёрстолл, 1969, с. 43, 45.
22. Гундерсон, 2011, с. 49, 257, 384, 245.
23. Штеффен, Рютинг, Хут, 2018, с. 214.

Література

• B. Steffen, O. Rüthing, M. Huth. Mathematical Foundations of Advanced Informatics. — , 2018. — Т. 1. Inductive Approaches. — .
• R. M. Burstall. Proving properties of programs by structural induction // ^[en]. — 1969. — Т. 12, № 1 (16 червня). — С. 41–48. — DOI:10.1093/comjnl/12.1.41.
• D. Gunderson. Handbook of Mathematical Induction. Theory and Applications. — Boca Raton : CRC, 2011. — 893 с. — .
• Х. Карри. Основания математической логики. — М. : Мир, 1969. — 567 с. (рос.)