WikiSort.ru - Не сортированное

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

Изначально^[⇨] метод использовался в математической логике, также нашёл применение^[⇨] в теории графов, комбинаторике, общей алгебре, математической лингвистике, но наибольшее распространение как самостоятельно изучаемый метод получил в теоретической информатике^[1], где применяется в вопросах семантики языков программирования, формальной верификации, вычислительной сложности, функционального программирования.

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

История

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

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

Явное определение структурной индукции, ссылающееся как на рекурсивную определимость, так и на нётерову индукцию, дано Бёрстоллом (англ. Rod Burstall) в конце 1960-х годов^[9], и в литературе по информатике именно к нему относят введение метода^[10][11].

В дальнейшем в информатике возникло несколько направлений, основывающихся на структурной индукции как базовом принципе, в частности, таковы структурная операционная семантика языков программирования Плоткина (англ. Gordon Plotkin)^[12], серия индуктивных методов формальной верификации^[13][14], структурно-рекурсивный язык запросов UnQL^[15]. В 1990-е годы в теоретической информатике получил распространение метод коиндукции, применяемый над нефундированными (как правило, бесконечными) структурами и считающийся двойственным структурной индукции^[16].

В связи с широким применением в теоретической информатике и немногочисленностью упоминаний в математической литературе, по состоянию на 2010-е годы считается, что что выделение структурной индукции как особого метода более характерно именно для информатики, нежели для математики^[17].

Определение

Наиболее общее определение^[18][19] вводится для класса структур ${\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)}}}$ .

Рекурсивность в этом определении реализуется совокупностью вложенных структур: как только есть способ определять выводить свойства структуры исходя из свойств всех предшествующих ей, можно говорить о рекурсивной определимости структуры.

В литературе по информатике распространена и другая форма определения структурной индукции, ориентированная на рекурсию по построению^[20], в ней ${\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}})}$ ^[21].

Примеры

Введение принципа в информатику мотивировалось рекурсивным характером таких структур данных, как списки и деревья^[22]. Первый пример над списком, приводимый Бёрстоллом — утверждение о свойствах свёртки списков ${\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], свойств деревьев и лесов^[23]. Другие структуры в математике, для которых применяется структурная индукция — перестановки, матрицы и их тензорные произведения, конструкции из геометрических фигур в комбинаторной геометрии.

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

Примечания

Литература

• B. Steffen, O. Rüthing, M. Huth. Mathematical Foundations of Advanced Informatics. — Springer, 2018. — Vol. 1. Inductive Approaches. — ISBN 978-3-319-68396-6.
• R. M. Burstall. Proving properties of programs by structural induction // The Computer Journal^[en]. — 1969. — Vol. 12, № 1. — P. 41–48. — DOI:10.1093/comjnl/12.1.41.
• D. Gunderson. Handbook of Mathematical Induction. Theory and Applications. — Boca Raton: CRC, 2011. — 893 с. — ISBN 978-1-4200-9364-3.
• Х. Карри. Основания математической логики. — М.: Мир, 1969. — 567 с.