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

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

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

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

История

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

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

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

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

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

Определение

Наиболее общее определение вводится для класса структур S {displaystyle {mathfrak {S}}} (без уточнения природы структур S ∈ S {displaystyle Sin {mathfrak {S}}} ) с отношением частичного порядка между структурами ⊑ {displaystyle sqsubseteq } , с условием минимального элемента S 0 {displaystyle S_{0}} в S {displaystyle {mathfrak {S}}} и условием наличия для каждой S ∈ S {displaystyle Sin {mathfrak {S}}} вполне упорядоченной совокупности из всех строго предшествующих ей структур: ▽ S = { T ∈ S ∣ T ⊏ S } {displaystyle riangledown S={Tin {mathfrak {S}}mid Tsqsubset S}} . Принцип структурной индукции в этом случае формулируется следующим образом: если выполнение свойства P {displaystyle P} для S {displaystyle {mathfrak {S}}} следует из выполнения свойства для всех строго предшествующих ей структур, то свойство выполнено и для всех структур класса; символически (в обозначениях систем натурального вывода):

∀ T ∈ ▽ S : P ( T ) ⇒ P ( S ) ∀ S ∈ S : P ( S ) {displaystyle {frac {forall Tin riangledown S:P(T)Rightarrow P(S)}{forall Sin {mathfrak {S}}:P(S)}}} .

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

В литературе по информатике распространена и другая форма определения структурной индукции, ориентированная на рекурсию по построению, в ней S {displaystyle {mathfrak {S}}} рассматривается как класс объектов, определённых над некоторым множеством атомарных элементов A ∈ S {displaystyle {mathcal {A}}in {mathfrak {S}}} и набором операций { o i : S k i → S } {displaystyle left{{mathcal {o}}_{i}:{mathfrak {S}}^{k_{i}} o {mathfrak {S}} ight}} , при этом каждый объект S ∈ S {displaystyle Sin {mathfrak {S}}} — результат последовательного применения операций к атомарным элементам. В этой формулировке принцип утверждает, что свойство P {displaystyle P} выполняется для всех объектов S ∈ S {displaystyle Sin {mathfrak {S}}} , как только имеет место для всех атомарных элементов и для каждой операции o i {displaystyle {mathcal {o}}_{i}} из выполнения свойства для элементов S 1 , … , S i k {displaystyle S_{1},dots ,S_{i_{k}}} следует выполнение свойства для o i ( S 1 , … , S i k ) {displaystyle {mathcal {o}}_{i}(S_{1},dots ,S_{i_{k}})} :

∀ A ∈ A : P ( A ) , ∀ i : ( P ( S 1 ) , … P ( S i k ⇒ P ( o i ( S 1 , … , S i k ) ) ∀ S ∈ S : P ( S ) {displaystyle {frac {forall Ain {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 Sin {mathfrak {S}}:P(S)}}} .

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

Примеры

Введение принципа в информатику мотивировалось рекурсивным характером таких структур данных, как списки и деревья. Первый пример над списком, приводимый Бёрстоллом — утверждение о свойствах свёртки списков ⊛ {displaystyle circledast } с элементами типа T {displaystyle T} двухместной функцией ∗ : T 2 → T {displaystyle ast :T^{2} o T} и начальным элементом свёртки t ∈ T {displaystyle tin T} в связи с конкатенацией списков ∥ {displaystyle shortparallel } :

( S 1 ∥ S 2 ) ⊛ t = S 1 ⊛ ( S 2 ⊛ t ) {displaystyle (S_{1}shortparallel S_{2})circledast t=S_{1}circledast (S_{2}circledast t)} .

Структурная индукция в доказательстве этого утверждения ведётся от пустых списков — если S 1 = ⊥ {displaystyle S_{1}=ot } , то:

левая часть, по определению конкатенации: ( ⊥ ∥ S 2 ) ⊛ t = S 2 ⊛ t {displaystyle (ot shortparallel S_{2})circledast t=S_{2}circledast t} , правая часть, по определению свёртки: ⊥ ⊛ ( S 2 ⊛ t ) = S 2 ⊛ t {displaystyle ot circledast (S_{2}circledast t)=S_{2}circledast t}

и в случае, если список непуст, и начинается элементом x {displaystyle x} , то:

левая часть, по определениям конкатенации и свёртки: ( ( x :: S 1 ) ∥ S 2 ) ⊛ t = x ∗ ( ( S 1 ∥ S 2 ) ⊛ t ) {displaystyle ((x::S_{1})shortparallel S_{2})circledast t=xast ((S_{1}shortparallel S_{2})circledast t)} , правая часть, по определению свёртки и предположению индукции: ( x :: S 1 ) ⊛ ( S 2 ⊛ t ) = x ∗ ( ( S 1 ∥ S 2 ) ⊛ t ) {displaystyle (x::S_{1})circledast (S_{2}circledast t)=xast ((S_{1}shortparallel S_{2})circledast t)} .

Предположение индукции основывается на истинности утверждения для S 1 {displaystyle S_{1}} и включении S 1 ⊑ x :: S 1 {displaystyle S_{1}sqsubseteq x::S_{1}} .

В теории графов структурная индукция часто применяется для доказательств утверждений о многодольных графах (с использованием перехода от ( k − 1 ) {displaystyle (k-1)} -дольных к k {displaystyle k} -дольным), в теоремах об амальгамировании графов, свойств деревьев и лесов. Другие структуры в математике, для которых применяется структурная индукция — перестановки, матрицы и их тензорные произведения, конструкции из геометрических фигур в комбинаторной геометрии.

Типичное применение в математической логике и универсальной алгебре — структурная индукция по построению формул из атомарных термов, например, показывается, что выполнение требуемого свойства P {displaystyle P} для термов A {displaystyle A} и B {displaystyle B} влечёт P ( A ∨ B ) {displaystyle P(Avee B)} , P ( A ∧ B ) {displaystyle P(Awedge B)} , P ( ¬ A ) {displaystyle P(lnot A)} и так далее. Также по построению формул работают многие структурно-индуктивные доказательства в теории автоматов, математической лингвистике; для доказательства синтаксической корректности компьютерных программ широко используется структурная индукция по БНФ-определению языка (иногда даже выделяется в отдельный подтип — БНФ-индукция).