Перегляд вихідного коду сторінки Структурна індукція

'''Структу́рна інду́кція'''&nbsp;— [[Конструктивне доведення|конструктивний]] метод [[Доведення|математичного доведення]], який узагальнює [[Математична індукція|математичну індукцію]] (застосовувану над натуральним рядом) на довільні [[Рекурсивне означення|рекурсивно означені]] [[Частково впорядкована множина|частково впорядковані]] сукупності. '''Структурна рекурсія'''&nbsp;— реалізація структурної індукції у формі визначення, процедури доведення або [[Комп'ютерна програма|програми]], що забезпечує індукційний перехід над частково впорядкованою сукупністю.

Спочатку{{Перехід|#Історія}} метод використовувався в [[Математична логіка|математичній логіці]], також знайшов застосування{{Перехід|#Приклади}} в [[Теорія графів|теорії графів]], [[Комбінаторика|комбінаториці]], [[Абстрактна алгебра|загальній алгебрі]], [[Математична лінгвістика|математичній лінгвістиці]], але найбільшого поширення як самостійно досліджуваний метод набув у [[Теоретична інформатика|теоретичній інформатиці]]{{Sfn|Штеффен, Рютинг, Хут|2018|с=179}}, де застосовується в питаннях [[Семантика мов програмування|семантики мов програмування]], [[Формальна верифікація|формальної верифікації]], [[Теорія складності обчислень|обчислювальної складності]], [[Функційне програмування|функційного програмування]].

На відміну від [[Фундована множина|нетерівської індукції]]&nbsp;— найзагальнішої форми математичної індукції, застосовуваної над довільними [[Фундована множина|фундованими множинами]],&nbsp;— в понятті про структурну індукцію мається на увазі конструктивний характер, обчислювальна реалізація. При цьому [[Фундована множина|фундованість]] сукупності&nbsp;— властивість, необхідна для рекурсивної ви́значності<ref>{{Із|МЕ|Рекурсия}}</ref>, таким чином, структурну рекурсію можна вважати частковим варіантом нетерівської індукції{{Sfn|Штеффен, Рютинг, Хут|2018|с=179}}.

== Історія ==
Використання методу зустрічається принаймні від 1950-х років, зокрема, в доведенні [[Ультрадобуток|теореми Лоша про ультрадобутки]] застосовується індукція побудови формули, при цьому сам метод особливим чином явно не називався<ref>{{Стаття|author={{iw|Лось, Ежи|J. Loś|pl|Jerzy Łoś (logik)}}|title=Quelques remarques, théorèmes et problèmes sur les classes définissables d'algèbres|видання=Studies in Logic and the Foundations of Mathematics|volume=16|date=1955|pages=98—113|doi=10.1016/S0049-237X(09)70306-4}}</ref>. У ті ж роки метод застосовувався в [[Теорія моделей|теорії моделей]] для доведень над ланцюгами моделей, вважається, що поява терміна «структурна індукція» пов'язана саме з цими доведеннями{{Sfn|Гундерсон|2011|с=48}}. [[Гаскелл Каррі|Карі]] поділив усі види застосування індукції в математиці на два типи&nbsp;— дедуктивну індукцію і структурну індукцію, класичну індукцію над натуральними числами вважаючи підтипом останньої{{Sfn|Карри|1969|місце=при цьому зазначаючи: «Звичайна математична індукція зі справжньої точки зору є структурною індукцією...; вона так часто зустрічається <...> що варто вважати її третім видом - натуральною індукцією»|с=}}.

З іншого боку, не пізніше початку 1950-х років метод [[Трансфінітна індукція|трансфінітної індукції]] вже поширювався на довільні частково впорядковані множини, що задовольняють [[Частково впорядкована множина|умову обриву ростучих ланцюгів]] (що еквівалентно фундованості<ref>{{Книга
|автор = [[Курош Олександр Генадійович|А. Г. Курош]]
|заголовок = Лекции по общей алгебре
|місце = М.
|видавництво = Физматлит
|рік = 1962
|сторінки = 21—22 (§5. Условие минимальности)
|сторінок = 399
}}</ref>), в той же час {{Нп|Леон Генкін|Генкін|ru|Хенкин, Леон}} відсилав до можливості індукції «в деяких типах частково впорядкованих систем»<ref>{{Книга
|автор = Л. Генкин
|заголовок = О математической индукции
|місце = М.
|видавництво = [[Физматгиз]]
|рік = 1962
|сторінок = 36
|сторінки = 36 (заключение)
}}</ref>. У 1960-х роках метод закріпився під назвою нетерівська індукція (за аналогією з [[Кільце Нетер|нетерівським кільцем]], у якому виконано умову обриву ростучих ланцюгів [[Ідеал (алгебра)|ідеалів]])<ref> {{Книга
|автор = [[Пол Моріц Кон|П. Кон]]
|заголовок = 
|місце = М.
|видавництво = [[Мир (видавництво)|Мир]]
|рік = 1969
|сторінок = 351
|сторінки = 33—34
|назва = Универсальная алгебра
}}</ref>.

Явне визначення структурної індукції, яке посилається як на рекурсивну ви́значність, так і на нетерівську індукцію, дав {{Iw|Род Берстолл|Берстолл|en|Rod Burstall}}) наприкінці 1960-х років{{Sfn|Бёрстолл|1969}}, і в літературі з інформатики саме до нього відносять уведення методу<ref>{{Книга
|заголовок = Tools and Notions for Program Construction. An Advanced Course
|відповідальний = D. Néel (ed.)
|видавництво = Cambridge University Press
|рік = 1982
|ISBN = 0-512-24801-9
|сторінок = 400
|сторінки = 196
}}</ref><ref>{{Книга
|автор = О. А. Ильичёва
|заголовок = Формальное описание семантики языков программирования
|місце = Ростов-на-Дону
|видавництво = ЮФУ
|рік = 2007
|сторінок = 223
|сторінки = 99—100
}}</ref>.

Надалі в інформатиці утворилося декілька напрямів, які ґрунтуються на структурній індукції як базовому принципі, зокрема, такими є [[структурна операційна семантика]] мов програмування {{Iw|Гордон Плоткін|Плоткіна|en|Gordon Plotkin}})<ref>{{Стаття|author=G. Plotkin|title=The origins of structural operational semantics|видання=The Journal of Logic and Algebraic Programming|date=2004|pages=3—15|doi=10.1016/j.jlap.2004.03.009}}</ref>, серія індуктивних методів формальної верифікації<ref>{{Стаття|author=Z. Manna, S. Ness, J. Vuillemin|date=1973|title=Inductive methods for proving properties of programs|видання=[[Communications of the ACM]]|volume=16|номер=8|pages=491—502|doi=10.1145/355609.362336}}</ref><ref>{{Стаття|author=C. Reynolds, R. Yeh|date=1976|title=Induction as the basis for program verification|видання=Proceedings of the 2<sup>nd</sup> international conference on Software engineering (ICSE ’76)|publisher=IEEE Computer Society Press|place=Los Alamitos|pages=389}}</ref>, структурно-рекурсивна мова запитів [[UnQL]]<ref>{{Стаття|author=P. Buneman, M. Fernandez, D. Suciu|date=2000|title=UnQL: a query language and algebra for semistructured data based on structural recursion|видання=The VLDB Journal|volume=9|номер=1|pages=76—110|doi=10.1007/s007780050084}}</ref>. У 1990-х роках у теоретичній інформатиці поширився метод [[Коіндукція|коіндукції]], застосовуваний над нефундованих (як правило, нескінченних) структурах, який вважають [[Дуальність|дуальним]] для структурної індукції<ref>{{Стаття|author=[[Робін Мілнер|R. Milner]], M. Tofte|title=Co-induction in relational semantics|видання=[[Theoretical Computer Science]]|volume=87|номер=1|pages=209—220}}</ref>.

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

== Визначення ==
Найзагальніше визначення{{Sfn|Бёрстолл|1969|с=42}}{{Sfn|Гундерсон|2011|с=42}} вводиться для класу [[Математичні структури|структур]] <math>\mathfrak S</math> (без уточнення природи структур <math>S \in \mathfrak S</math>) з відношенням часткового порядку між структурами <math>\sqsubseteq</math>, з умовою мінімального елемента <math>S_0</math> в <math>\mathfrak S</math> і умовою наявності для кожної <math>S \in \mathfrak S</math> [[Цілком впорядкована множина|цілком упорядкованої]] сукупності зі всіх структур, що суворо передують їй: <math>\triangledown S = \{ T \in \mathfrak S \mid T \sqsubset S \}</math>. Принцип структурної індукції в цьому випадку формулюється так: якщо виконання властивості <math>P</math> для <math>\mathfrak S</math> випливає з виконання властивості для всіх структур, що суворо передують їй, то властивість виконано і для всіх структур класу; символічно (в позначеннях {{нп|Натуральне виведення|систем натурального виведення|en|natural deduction}}):

: <math>\frac {\forall T \in \triangledown S : P(T) \Rightarrow P(S)}
{\forall S \in \mathfrak S : P(S)}</math>.

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

В літературі з інформатики поширена й інша форма визначення структурної індукції, орієнтована на рекурсію за побудовою{{Sfn|Штеффен, Рютинг, Хут|2018|сторінки=177—178}}, в ній <math>\mathfrak S</math> розглядається як клас об'єктів, визначених над деякою множиною атомарних елементів <math>\mathcal {A} \in \mathfrak S</math> і набором операцій <math>\left \{ \mathcal o_i : \mathfrak S^{k_i} \to \mathfrak S \right \}</math>, при цьому кожен об'єкт <math>S \in \mathfrak S</math>&nbsp;— результат послідовного застосування операцій до атомарних елементів. У цьому формулюванні принцип стверджує, що властивість <math>P</math> виконується для всіх об'єктів <math>S \in \mathfrak S</math>, як тільки має місце для всіх атомарних елементів і для кожної операції <math>\mathcal o_i</math> з виконання властивості для елементів <math>S_1, \dots, S_{i_k}</math> слідує виконання властивості для <math>\mathcal o_i (S_1, \dots, S_{i_k})</math>:

: <math>\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)}</math>.

Роль відношення часткового порядку <math>\sqsubseteq</math> з загального визначення тут грає відношення включення за побудовою: <math>\forall_{j = 1\dots i_k} S_j \sqsubseteq \mathcal o_i (S_1, \dots, S_{i_k})</math>{{Sfn|Штеффен, Рютинг, Хут|2018|сторінки=178}}.

== Приклади ==
Запровадження принципу в інформатику мотивувалося рекурсивним характером таких структур даних, як [[Список (абстрактний тип даних)|списки]] і [[Дерево (структура даних)|дерева]]{{Sfn|Бёрстолл|1969|с=43, 45}}. Перший приклад над списком, наведений Берстоллом&nbsp;— твердження про властивості {{Нп|Згортка списку|згортки списків|ru|Свёртка списка}} <math>\circledast</math> з елементами типу <math>T</math> двомісною функцією <math>\ast : T^2 \to T</math> і початковим елементом згортки <math>t \in T</math> у зв'язку з [[Конкатенація|конкатенацією]] списків <math>\shortparallel</math>:

: <math>(S_1 \shortparallel S_2) \circledast t = S_1 \circledast (S_2 \circledast t) </math>.

Структурна індукція в доведенні цього твердження ведеться від порожніх списків&nbsp;— якщо <math>S_1 = \bot</math>, то:

: ліва частина, за визначенням конкатенації: <math>(\bot \shortparallel S_2) \circledast t = S_2 \circledast t</math>,
: права частина, за визначенням згортки: <math>\bot \circledast (S_2 \circledast t) = S_2 \circledast t</math>

і в разі, якщо список непорожній, і починається елементом <math>x</math>, то:

: ліва частина, за визначенням конкатенації та згортки: <math>((x::S_1) \shortparallel S_2) \circledast t = x \ast ((S_1 \shortparallel S_2) \circledast t)</math>,
: права частина, за визначенням згортки і припущенням індукції: <math>(x::S_1) \circledast (S_2 \circledast t) = x \ast ((S_1 \shortparallel S_2) \circledast t)</math>.

Припущення індукції ґрунтується на істинності твердження <math>S_1</math> і включення <math>S_1 \sqsubseteq x::S_1</math>.

В теорії графів структурна індукція часто застосовується для доведення тверджень про [[Багатодольний граф|багатодольні графи]] (з використанням переходу від <math>(k-1)</math>-дольних до <math>k</math>-дольних), у теоремах про {{нп|амальгамування графів||en|graph amalgamation}}, властивостей [[Дерево (теорія графів)|дерев]] і [[Дерево (теорія графів)|лісів]]{{Sfn|Гундерсон|2011|с=49, 257, 384, 245}}. Інші структури в математиці, для яких застосовується структурна індукція&nbsp;— [[Перестановка|перестановки]], [[Матриця (математика)|матриці]] і їх [[Тензорний добуток|тензорні добутки]], конструкції з геометричних фігур у [[Комбінаторна геометрія|комбінаторній геометрії]].

Типове застосування в математичній логіці та [[Універсальна алгебра|універсальній алгебрі]]&nbsp;— структурна індукція побудови формул з атомарних термів, наприклад, показується, що виконання необхідної властивості <math>P</math> для термів <math>A</math> і <math>B</math> тягне <math>P(A \vee B)</math>, <math>P(A \wedge B)</math>, <math>P (\lnot A)</math> і так далі. Також за побудовою формул виконуються багато структурно-індуктивних доведень у [[Теорія автоматів|теорії автоматів]], математичній лінгвістиці; для доведення синтаксичної коректності комп'ютерних програм широко використовується структурна індукція за [[Нотація Бекуса — Наура|БНФ-визначенням]] мови (іноді навіть виділяється в окремий підтип&nbsp;— БНФ-індукція{{Sfn|Штеффен, Рютинг, Хут|2018|с=214}}).

== Примітки ==
{{примітки|2}}

== Література ==
* {{Книга
|автор = B. Steffen, O. Rüthing, M. Huth
|заголовок = Mathematical Foundations of Advanced Informatics
|том = 1. Inductive Approaches
|видавництво = [[Springer International Publishing|Springer]]
|рік = 2018
|ISBN = 978-3-319-68396-6
|ref = Штеффен, Рютинг, Хут
}}
* {{Стаття|author=R. M. Burstall|title=Proving properties of programs by structural induction|видання={{iw|The Computer Journal}}|volume=12|номер=1|date=1969|pages=41–48|doi=10.1093/comjnl/12.1.41|ref=Бёрстолл}}
* {{Книга
|автор = D. Gunderson
|заголовок = Handbook of Mathematical Induction. Theory and Applications
|місце = Boca Raton
|видавництво = CRC
|рік = 2011
|сторінок = 893
|ISBN = 978-1-4200-9364-3
|ref = Гундерсон
}}
* {{Книга
|автор = [[Гаскелл Каррі|Х. Карри]]
|заголовок = Основания математической логики
|місце = М.
|видавництво = Мир
|рік = 1969
|сторінок = 567
|ref = Карри
}} {{ref-ru}}

{{Математична логіка|state=collapsed}}

[[Категорія:Математична індукція]]
[[Категорія:Фундованість]]