Структурная индукция: различия между версиями

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску
Интерактивная навигация по истории
[отпатрулированная версия][отпатрулированная версия]
← Предыдущая правкаСледующая правка →
Содержимое удалено Содержимое добавлено
ВизуальныйВики-текст
уточнения, буде продолжать
м +ещё книга
Строка 3: Строка 3:
'''Структурная индукция''' — [[Конструктивное доказательство|конструктивный]] метод [[Математическое доказательство|математического доказательства]], обобщающий [[Математическая индукция|математическую индукцию]] (применяемую над натуральным рядом) на произвольные [[Рекурсивное определение|рекурсивно определённые]] [[Частично упорядоченное множество|частично упорядоченные]] совокупности. '''''Структурная рекурсия''''' — реализация структурной индукции в форме определения, процедуры доказательтва или [[Компьютерная программа|программы]], обеспечивающая индукционный переход над частично упорядоченной совокупностью.
'''Структурная индукция''' — [[Конструктивное доказательство|конструктивный]] метод [[Математическое доказательство|математического доказательства]], обобщающий [[Математическая индукция|математическую индукцию]] (применяемую над натуральным рядом) на произвольные [[Рекурсивное определение|рекурсивно определённые]] [[Частично упорядоченное множество|частично упорядоченные]] совокупности. '''''Структурная рекурсия''''' — реализация структурной индукции в форме определения, процедуры доказательтва или [[Компьютерная программа|программы]], обеспечивающая индукционный переход над частично упорядоченной совокупностью.


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


В отличие от [[нётерова индукция|нётеровой индукции]] — наиболее общей формы математической индукции, применяемой над произвольными [[Фундированное множество|фундированными множествами]], в понятии о структурной индукции подразумевается конструктивный характер, вычислительная реализация. При этом фундированность{{Переход|#Фундированность}} совокупности — свойство, необходимое для рекурсивной определяемости<ref>{{Из|МЭ|заглавие=Рекурсия|автор=Н. В. Белякин}}</ref>, таким образом, структурную рекурсию можно считать конструктивным вариантом нётеровой индукции.
В отличие от [[нётерова индукция|нётеровой индукции]] — наиболее общей формы математической индукции, применяемой над произвольными [[Фундированное множество|фундированными множествами]], в понятии о структурной индукции подразумевается конструктивный характер, вычислительная реализация. При этом фундированность{{Переход|#Фундированность}} совокупности — свойство, необходимое для рекурсивной определяемости<ref>{{Из|МЭ|заглавие=Рекурсия|автор=Н. В. Белякин}}</ref>, таким образом, структурную рекурсию можно считать частным вариантом нётеровой индукции{{Sfn|Штеффен, Рютинг, Хут|2018|p=179}}.


== История ==
== История ==
Использование метода встречается, по крайней мере, с 1950-х годов, в частности, в доказательстве [[теорема Лося об ультрапроизведениях|теоремы Лося об ультрапроизведениях]] применяется индукция по построению формулы, при этом сам метод особым образом явно не назывался<ref>{{Статья | автор = {{iw|Лось, Ежи|J. Loś|pl|Jerzy Łoś (logik)}} | заглавие = Quelques remarques, théorèmes et problèmes sur les classes définissables d'algèbres | издание = Studies in Logic and the Foundations of Mathematics | том = 16 | год = 1955 | страницы = 98—113 | doi = 10.1016/S0049-237X(09)70306-4}}</ref>. [[Карри, Хаскелл|Карри]] делил все виды применения [[Индуктивное умозаключение|индукции]] в математике на два типа — дедуктивную индукцию и структурную индукцию, классическую индукцию над натуральными числами считая её подтипом{{Sfn|Карри|1967|loc=при этом указывая: «Обычная математическая индукция с настоящей точки зрения является структурной индукцией по системе самов; она так часто встречается <…> что стоит считать её третьим видом — натуральной индукцией»}}, [[Генкин, Леон|Генкин]] отсылал к возможности индукции «в некоторых типах частично-упорядоченных систем»<ref>{{книга | автор = Л. Генкин | заглавие = О математической индукции | место = М. | издательство = [[Физматгиз]] | год = 1962 | страниц = 36 | страницы = 36 (заключение)}}</ref>. С другой стороны, не позднее начала 1950-х годов метод [[Трансфинитная индукция|трансфинитной индукции]] уже распространялся на произвольные частично упорядоченные множества, удовлетворяющие [[Условие обрыва возрастающих цепей|условию обрыва возрастающих цепей]] (что эквивалентно фундированности<ref>{{Книга | автор = [[Курош, Александр Геннадиевич|А. Г. Курош]] | заглавие = Лекции по общей алгебре |место = М. | издательство = Физматлит | год = 1962 | страницы = 21—22 (§5. Условие минимальности) | страниц = 399}}</ref>), и метод закрепился под наименованием нётеровой индукции (по аналогии с [[Нётерово кольцо|нётеровым кольцом]], в котором выполнено условие обрыва возрастающих цепей [[Идеал кольца|идеалов]]).
Использование метода встречается, по крайней мере, с 1950-х годов, в частности, в доказательстве [[теорема Лося об ультрапроизведениях|теоремы Лося об ультрапроизведениях]] применяется индукция по построению формулы, при этом сам метод особым образом явно не назывался<ref>{{Статья | автор = {{iw|Лось, Ежи|J. Loś|pl|Jerzy Łoś (logik)}} | заглавие = Quelques remarques, théorèmes et problèmes sur les classes définissables d'algèbres | издание = Studies in Logic and the Foundations of Mathematics | том = 16 | год = 1955 | страницы = 98—113 | doi = 10.1016/S0049-237X(09)70306-4}}</ref>. [[Карри, Хаскелл|Карри]] делил все виды применения [[Индуктивное умозаключение|индукции]] в математике на два типа — дедуктивную индукцию и структурную индукцию, классическую индукцию над натуральными числами считая её подтипом{{Sfn|Карри|1967|loc=при этом указывая: «Обычная математическая индукция с настоящей точки зрения является структурной индукцией по системе самов; она так часто встречается <…> что стоит считать её третьим видом — натуральной индукцией»}}, [[Генкин, Леон|Генкин]] отсылал к возможности индукции «в некоторых типах частично-упорядоченных систем»<ref>{{книга | автор = Л. Генкин | заглавие = О математической индукции | место = М. | издательство = [[Физматгиз]] | год = 1962 | страниц = 36 | страницы = 36 (заключение)}}</ref>. С другой стороны, не позднее начала 1950-х годов метод [[Трансфинитная индукция|трансфинитной индукции]] уже распространялся на произвольные частично упорядоченные множества, удовлетворяющие [[Условие обрыва возрастающих цепей|условию обрыва возрастающих цепей]] (что эквивалентно фундированности<ref>{{Книга | автор = [[Курош, Александр Геннадиевич|А. Г. Курош]] | заглавие = Лекции по общей алгебре |место = М. | издательство = Физматлит | год = 1962 | страницы = 21—22 (§5. Условие минимальности) | страниц = 399}}</ref>), и метод закрепился под наименованием нётеровой индукции (по аналогии с [[Нётерово кольцо|нётеровым кольцом]], в котором выполнено условие обрыва возрастающих цепей [[Идеал кольца|идеалов]]).


Явное определение структурной индукции, ссылающееся как на рекурсивную определимость, так и на нётерову индукцию, дано {{нп2|Бёрстолл, Род|Бёрстоллом|en|Rod Burstall}} в середине 1960-х годов{{Sfn|Бёрстолл|1969}}, и в литературе по информатике именно к нему относят введение метода<ref>{{книга | автор = О. А. Ильичёва | заглавие = Формальное описание семантики языков программирования | место = Ростов-на-Дону | издательство = ЮФУ | год = 2007 | страниц = 223 | страницы = 99—100}}</ref><!--ещё из программирования<ref></ref>; про SOS Плоткина-->.
Явное определение структурной индукции, ссылающееся как на рекурсивную определимость, так и на нётерову индукцию, дано {{нп2|Бёрстолл, Род|Бёрстоллом|en|Rod Burstall}} в середине 1960-х годов{{Sfn|Бёрстолл|1969}}, и в литературе по информатике именно к нему относят введение метода<ref>{{книга | автор = О. А. Ильичёва | заглавие = Формальное описание семантики языков программирования | место = Ростов-на-Дону | издательство = ЮФУ | год = 2007 | страниц = 223 | страницы = 99—100}}</ref><!--ещё из программирования<ref></ref>; про SOS Плоткина-->.
{{раздел не завершён}}
{{раздел не завершён}}


Строка 26: Строка 26:


== Литература ==
== Литература ==
* {{книга | автор = B. Steffen, O. Rüthing, M. Huth | заглавие = Mathematical Foundations of Advanced Informatics | том = Volume 1. Inductive Approaches | издательство = [[Springer International Publishing|Springer]] | год = 2018 | isbn = 978-3-319-68396-6 | ref = Штеффен, Рютинг, Хут}}
* {{статья | автор = R. M. Burstall | заглавие = Proving properties of programs by structural induction | издание = {{iw|The Computer Journal}} | том = 12 | номер = 1 | год = 1969 | страницы = 41–48 | doi = 10.1093/comjnl/12.1.41|ref=Бёрстолл}}
* {{статья | автор = R. M. Burstall | заглавие = Proving properties of programs by structural induction | издание = {{iw|The Computer Journal}} | том = 12 | номер = 1 | год = 1969 | страницы = 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 = Гундерсон}}
* {{книга | автор = D. Gunderson | заглавие = Handbook of Mathematical Induction. Theory and Applications | место = Boca Raton | издательство = CRC | год = 2011 | страниц = 893 | isbn = 978-1-4200-9364-3 | ref = Гундерсон}}

Версия от 11:48, 10 мая 2018

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

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

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

История

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

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

Определение

Примеры

Фундированность

Примечания

  1. ↑ 1 2 Штеффен, Рютинг, Хут, 2018, p. 179.
  2. ↑ Рекурсия — статья из Математической энциклопедии. Н. В. Белякин
  3. ↑ J. Loś[пол.]. Quelques remarques, théorèmes et problèmes sur les classes définissables d'algèbres // Studies in Logic and the Foundations of Mathematics. — 1955. — Т. 16. — С. 98—113. — doi:10.1016/S0049-237X(09)70306-4.
  4. ↑ Карри, 1967, при этом указывая: «Обычная математическая индукция с настоящей точки зрения является структурной индукцией по системе самов; она так часто встречается <…> что стоит считать её третьим видом — натуральной индукцией».
  5. ↑ Л. Генкин. О математической индукции. — М.: Физматгиз, 1962. — С. 36 (заключение). — 36 с.
  6. ↑ А. Г. Курош. Лекции по общей алгебре. — М.: Физматлит, 1962. — С. 21—22 (§5. Условие минимальности). — 399 с.
  7. ↑ Бёрстолл, 1969.
  8. ↑ О. А. Ильичёва. Формальное описание семантики языков программирования. — Ростов-на-Дону: ЮФУ, 2007. — С. 99—100. — 223 с.

Литература

  • B. Steffen, O. Rüthing, M. Huth. Mathematical Foundations of Advanced Informatics. — Springer, 2018. — Т. Volume 1. Inductive Approaches. — ISBN 978-3-319-68396-6.
  • R. M. Burstall. Proving properties of programs by structural induction // The Computer Journal[англ.]. — 1969. — Т. 12, № 1. — С. 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 с.
Источник — https://ru.wikipedia.org/w/index.php?title=Структурная_индукция&oldid=92570510