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

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

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

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

Історія

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

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

Явне визначення структурної індукції, яке посилається як на рекурсивну ви́значність, так і на нетерівську індукцію, дав Шаблон:Iw) наприкінці 1960-х роківШаблон:Sfn, і в літературі з інформатики саме до нього відносять уведення методу.

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

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

Визначення

Найзагальніше визначенняШаблон:SfnШаблон:Sfn вводиться для класу структур $𝔖$ (без уточнення природи структур $S\in 𝔖$) з відношенням часткового порядку між структурами $⊑$, з умовою мінімального елемента $S_0$ в $𝔖$ і умовою наявності для кожної $S\in 𝔖$ цілком упорядкованої сукупності зі всіх структур, що суворо передують їй: $▽S=\{T\in 𝔖\mid T⊏S\}$. Принцип структурної індукції в цьому випадку формулюється так: якщо виконання властивості $P$ для $𝔖$ випливає з виконання властивості для всіх структур, що суворо передують їй, то властивість виконано і для всіх структур класу; символічно (в позначеннях Шаблон:Нп):

$\frac{\mathrm{\forall }T\in ▽S:P(T)\Rightarrow P(S)}{\mathrm{\forall }S\in 𝔖:P(S)}$.

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

В літературі з інформатики поширена й інша форма визначення структурної індукції, орієнтована на рекурсію за побудовоюШаблон:Sfn, в ній $𝔖$ розглядається як клас об'єктів, визначених над деякою множиною атомарних елементів $𝒜\in 𝔖$ і набором операцій $\{{ℴ}_i:{𝔖}^{k_i}\to 𝔖\}$, при цьому кожен об'єкт $S\in 𝔖$ — результат послідовного застосування операцій до атомарних елементів. У цьому формулюванні принцип стверджує, що властивість $P$ виконується для всіх об'єктів $S\in 𝔖$, як тільки має місце для всіх атомарних елементів і для кожної операції ${ℴ}_i$ з виконання властивості для елементів $S_1,\dots ,S_{i_k}$ слідує виконання властивості для ${ℴ}_i(S_1,\dots ,S_{i_k})$:

$\frac{\mathrm{\forall }A\in 𝒜:P(A),\mathrm{\forall }i:(P(S_1),\dots P(S_{i_k}\Rightarrow P({ℴ}_i(S_1,\dots ,S_{i_k}))}{\mathrm{\forall }S\in 𝔖:P(S)}$.

Роль відношення часткового порядку $⊑$ з загального визначення тут грає відношення включення за побудовою: ${\mathrm{\forall }}_{j=1\dots i_k}{S}_j⊑{ℴ}_i(S_1,\dots ,S_{i_k})$Шаблон:Sfn.

Приклади

Запровадження принципу в інформатику мотивувалося рекурсивним характером таких структур даних, як списки і дереваШаблон:Sfn. Перший приклад над списком, наведений Берстоллом — твердження про властивості Шаблон:Нп $⊛$ з елементами типу $T$ двомісною функцією $\ast :T^2\to T$ і початковим елементом згортки $t\in T$ у зв'язку з конкатенацією списків $\parallel$:

$(S_1\parallel S_2)⊛t=S_1⊛(S_2⊛t)$.

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

ліва частина, за визначенням конкатенації: $(\mathrm{\perp }\parallel S_2)⊛t=S_2⊛t$,

права частина, за визначенням згортки: $\mathrm{\perp }⊛(S_2⊛t)=S_2⊛t$

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

ліва частина, за визначенням конкатенації та згортки: $((x::S_1)\parallel S_2)⊛t=x\ast ((S_1\parallel S_2)⊛t)$,

права частина, за визначенням згортки і припущенням індукції: $(x::S_1)⊛(S_2⊛t)=x\ast ((S_1\parallel S_2)⊛t)$.

Припущення індукції ґрунтується на істинності твердження $S_1$ і включення $S_1⊑x::S_1$.

В теорії графів структурна індукція часто застосовується для доведення тверджень про багатодольні графи (з використанням переходу від $(k-1)$-дольних до $k$-дольних), у теоремах про Шаблон:Нп, властивостей дерев і лісівШаблон:Sfn. Інші структури в математиці, для яких застосовується структурна індукція — перестановки, матриці і їх тензорні добутки, конструкції з геометричних фігур у комбінаторній геометрії.

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

Література

• Шаблон:Книга
• Шаблон:Стаття
• Шаблон:Книга
• Шаблон:Книга Шаблон:Ref-ru