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

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

ИзначальноШаблон:Переход метод использовался в математической логике, также нашёл применениеШаблон:Переход в теории графов, комбинаторике, общей алгебре, математической лингвистике, но наибольшее распространение как самостоятельно изучаемый метод получил в теоретической информатикеШаблон:Sfn, где применяется в вопросах семантики языков программирования, формальной верификации, вычислительной сложности, функционального программирования.

В отличие от нётеровой индукции — наиболее общей формы математической индукции, применяемой над произвольными фундированными множествами, — в понятии о структурной индукции подразумевается конструктивный характер, вычислительная реализация. При этом фундированность совокупности — свойство, необходимое для рекурсивной определяемости, таким образом, структурную рекурсию можно считать частным вариантом нётеровой индукцииШаблон:Sfn.

История

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

С другой стороны, не позднее начала 1950-х годов метод трансфинитной индукции уже распространялся на произвольные частично упорядоченные множества, удовлетворяющие условию обрыва возрастающих цепей (что эквивалентно фундированности), в то же время Генкин отсылал к возможности индукции «в некоторых типах частично-упорядоченных систем». В 1960-е годы метод закрепился под наименованием нётеровой индукции (по аналогии с нётеровым кольцом, в котором выполнено условие обрыва возрастающих цепей идеалов).

Явное определение структурной индукции, ссылающееся как на рекурсивную определимость, так и на нётерову индукцию, дано Шаблон:Нп2 в конце 1960-х годовШаблон:Sfn, и в литературе по информатике именно к нему относят введение метода.

В дальнейшем в информатике возникло несколько направлений, основывающихся на структурной индукции как базовом принципе, в частности, таковы структурная операционная семантика языков программирования Шаблон:Нп2, серия индуктивных методов формальной верификации, структурно-рекурсивный язык запросов 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$-дольным), в теоремах об Шаблон:Iw, свойств деревьев и лесовШаблон:Sfn. Другие структуры в математике, для которых применяется структурная индукция — перестановки, матрицы и их тензорные произведения, конструкции из геометрических фигур в комбинаторной геометрии.

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

Литература

• Шаблон:Книга
• Шаблон:Статья
• Шаблон:Книга
• Шаблон:Книга