Коиндукция

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

Коиндукция — это математический аналог структурной индукции . ^{[ нужна ссылка ]} Коиндуктивно определенные типы данных известны как кодаты и обычно представляют собой бесконечные структуры данных , такие как потоки .

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

Для генерации кодовых данных и управления ими обычно используются коркурсивные функции в сочетании с ленивыми вычислениями . Неформально, вместо того, чтобы определять функцию путем сопоставления с образцом каждого из индуктивных конструкторов, определяется каждый из «деструкторов» или «наблюдателей» над результатом функции.

В программировании кологическое программирование (для краткости co-LP) «является естественным обобщением логического программирования и коиндуктивного логического программирования, которое, в свою очередь, обобщает другие расширения логического программирования, такие как бесконечные деревья, ленивые предикаты и параллельные взаимодействующие предикаты. Co-LP имеет приложения к рациональным деревьям, проверке бесконечных свойств, ленивым вычислениям, параллельному логическому программированию , проверке моделей , биподобия и т. д.». доказательствам ^[1] Экспериментальные реализации совместного LP доступны в Техасском университете в Далласе. ^[2] и на языке Logtalk (примеры см. ^[3]) и SWI-Пролог .

Описание

В ^[4] дается краткое изложение как принципа индукции , так и принципа коиндукции . в первую очередь не рассматривается Хотя в данной статье индукция , полезно сразу рассмотреть их несколько обобщенные формы. Чтобы сформулировать принципы, необходимо сделать несколько предварительных сведений.

Предварительные сведения

Позволять $U$ быть набором и $F$ быть монотонной функцией $2^{U}\rightarrow 2^{U}$ , то есть:

X\subseteq Y\Rightarrow F(X)\subseteq F(Y)

Если не указано иное, $F$ будем считать монотонным.

X является F-замкнутым, если

F(X)\subseteq X

X является F-согласованным, если

X\subseteq F(X)

X является неподвижной точкой, если

X=F(X)

Эти термины можно интуитивно понять следующим образом. Предположим, что $X$ представляет собой набор утверждений, и $F(X)$ операция, приводящая к последствиям $X$ . Затем $X$ является F-замкнутым, когда вы не можете сделать вывод больше, чем вы уже утверждали, в то время как $X$ является F-непротиворечивым , когда все ваши утверждения поддерживаются другими утверждениями (т. е. нет «не- F -логических предположений»).

Теорема Кнастера -Тарского говорит нам, что наименьшая неподвижная точка $F$ (обозначается $\mu F$ ) задается пересечением всех F-замкнутых множеств, а наибольшая неподвижная точка (обозначается $\nu F$ ) задается объединением всех F-согласованных множеств. Теперь мы можем сформулировать принципы индукции и коиндукции.

Определение

Принцип индукции : если

X

является F-замкнутым , то

\mu F\subseteq X

Принцип коиндукции : если

X

является F-согласованным , то

X\subseteq \nu F

Обсуждение

Как уже говорилось, принципы несколько неясны, но их можно с пользой представить следующим образом. Предположим, вы хотите доказать свойство $\mu F$ . По принципу индукции достаточно представить F-замкнутое множество $X$ на который удерживается имущество. Предположим, вы хотите показать, что $x\in \nu F$ . Тогда достаточно показать F-согласованное множество, что $x$ известно, что он является членом.

Примеры

Определение набора типов данных

Рассмотрим следующую грамматику типов данных:

T=\bot \;|\;\top \;|\;T\times T

То есть в набор типов входит "нижний тип" $\bot$ , "высший тип" $\top$ и (неоднородные) списки. Эти типы можно идентифицировать по строкам в алфавите. $\Sigma =\{\bot ,\top ,\times \}$ . Позволять $\Sigma ^{\leq \omega }$ обозначают все (возможно, бесконечные) строки над $\Sigma$ . Рассмотрим функцию $F:2^{\Sigma ^{\leq \omega }}\rightarrow 2^{\Sigma ^{\leq \omega }}$ :

F(X)=\{\bot ,\top \}\cup \{x\times y:x,y\in X\}

В этом контексте $x\times y$ означает «объединение строк $x$ , символ $\times$ и строка $y$ .» Теперь нам следует определить наш набор типов данных как фиксированную точку $F$ , но важно, возьмем ли мы наименьшую или наибольшую фиксированную точку.

Предположим, мы возьмем $\mu F$ как наш набор типов данных. Используя принцип индукции , мы можем доказать следующее утверждение:

Все типы данных в

\mu F

конечны

Чтобы прийти к этому выводу, рассмотрим множество всех конечных строк над $\Sigma$ . Четко $F$ не может создать бесконечную строку, поэтому оказывается, что это множество F-замкнуто , из чего следует вывод.

Теперь предположим, что мы берем $\nu F$ как наш набор типов данных. Мы хотели бы использовать принцип коиндукции, чтобы доказать следующее утверждение:

Тип

\bot \times \bot \times \cdots \in \nu F

Здесь $\bot \times \bot \times \cdots$ обозначает бесконечный список, состоящий из всех $\bot$ . Чтобы использовать принцип коиндукции , рассмотрим набор:

\{\bot \times \bot \times \cdots \}

Это множество оказывается F-согласованным , и поэтому $\bot \times \bot \times \cdots \in \nu F$ . Это зависит от подозрительного заявления, которое

\bot \times \bot \times \cdots =(\bot \times \bot \times \cdots )\times (\bot \times \bot \times \cdots )

Формальное обоснование этого является техническим и зависит от интерпретации строк как последовательностей , т.е. функций из $\mathbb {N} \rightarrow \Sigma$ . Интуитивно этот аргумент аналогичен аргументу о том, что $0.{\bar {0}}1=0$ (см. Повторение десятичной дроби ).

Коиндуктивные типы данных в языках программирования

Рассмотрим следующее определение потока : ^[5]

data Stream a = S a (Stream a)

-- Stream "destructors"
head (S a astream) = a
tail (S a astream) = astream

Казалось бы, это определение недостаточно обосновано , но, тем не менее, оно полезно в программировании и о нем можно рассуждать. В любом случае поток — это бесконечный список элементов, из которого вы можете наблюдать первый элемент или помещать элемент перед ним, чтобы получить другой поток.

Связь с F -коалгебрами

Источник: ^[6]

Рассмотрим эндофунктор $F$ в категории наборы :

F(x)=A\times x

F(f)=\langle \mathrm {id} _{A},f\rangle

Последняя F-коалгебра $\nu F$ имеет связанный с ним следующий морфизм:

\mathrm {out} :\nu F\rightarrow F(\nu F)=A\times \nu F

Это порождает еще одну коалгебру $F(\nu F)$ с ассоциированным морфизмом $F(\mathrm {out} )$ . Потому что $\nu F$ является окончательным , существует единственный морфизм

{\overline {F(\mathrm {out} )}}:F(\nu F)\rightarrow \nu F

такой, что

\mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ F(\mathrm {out} )=F\left({\overline {F(\mathrm {out} )}}\circ \mathrm {out} \right)

Состав ${\overline {F(\mathrm {out} )}}\circ \mathrm {out}$ индуцирует другой F -коалгебры гомоморфизм $\nu F\rightarrow \nu F$ . С $\nu F$ окончателен, этот гомоморфизм единственен и, следовательно, $\mathrm {id} _{\nu F}$ . Итого имеем:

{\overline {F(\mathrm {out} )}}\circ \mathrm {out} =\mathrm {id} _{\nu F}

\mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ \mathrm {out} )=\mathrm {id} _{F(\nu F)}

Это свидетельствует об изоморфизме $\nu F\simeq F(\nu F)$ , что категорически указывает на то, что $\nu F$ является фиксированной точкой $F$ и оправдывает обозначения.

Поток как конечная коалгебра

Мы покажем это

Stream A

является конечной коалгеброй функтора $F(x)=A\times x$ . Рассмотрим следующие реализации:

out astream = (head astream, tail astream)
out' (a, astream) = S a astream

Легко увидеть, что они взаимно обратны, что свидетельствует об изоморфизме. Более подробную информацию смотрите в ссылке.

Связь с математической индукцией

Мы покажем, как принцип индукции включает в себя математическую индукцию. Позволять $P$ быть некоторым свойством натуральных чисел . Примем следующее определение математической индукции:

0\in P\land (n\in P\Rightarrow n+1\in P)\Rightarrow P=\mathbb {N}

Теперь рассмотрим функцию $F:2^{\mathbb {N} }\rightarrow 2^{\mathbb {N} }$ :

F(X)=\{0\}\cup \{x+1:x\in X\}

Это не должно быть трудно увидеть $\mu F=\mathbb {N}$ . Следовательно, по принципу индукции , если мы хотим доказать какое-то свойство $P$ из $\mathbb {N}$ , достаточно показать, что $P$ является F-замкнутым . Подробно нам потребуется:

F(P)\subseteq P

То есть,

\{0\}\cup \{x+1:x\in P\}\subseteq P

Как уже говорилось, это именно математическая индукция .

См. также

Ссылки

^ «Со-логическое программирование | Lambda the Ultimate» .
^ «Домашняя страница Гопала Гупты» .
^ «Logtalk3/Examples/Coinduction у мастера · LogtalkDotOrg/Logtalk3» . Гитхаб .
^ Бенджамин С. Пирс . «Типы и языки программирования» . Массачусетский технологический институт Пресс .
^ Декстер Козен , Александра Сильва . «Практическая коиндукция». CiteSeerX 10.1.1.252.3961 .
^ Ральф Хинце (2012). «Общее программирование с дополнениями» . Общее и индексированное программирование . Конспекты лекций по информатике. Том. 7470. Спрингер. стр. 47–129. дои : 10.1007/978-3-642-32202-0_2 . ISBN 978-3-642-32201-3 .

Дальнейшее чтение

Учебники

Давиде Санджорджи (2012). Введение в бисимуляцию и коиндукцию . Издательство Кембриджского университета.
Давиде Санджорджи и Ян Руттен (2011). Продвинутые темы по бисимуляции и коиндукции . Издательство Кембриджского университета.

Вводные тексты

Эндрю Д. Гордон (1994). «Учебник по коиндукции и функциональному программированию». 1994. стр. 78–95. CiteSeerX 10.1.1.37.3914 . — математически ориентированное описание
Барт Джейкобс и Ян Руттен (1997). Учебник по (Co)алгебрам и (Co)индукции ( альтернативная ссылка ) — одновременно описывает индукцию и коиндукцию.
Эдвард Хименес и Питер Кастеран (2007). «Учебное пособие по [ко-]индуктивным типам в Coq»
Коиндукция — краткое введение

История

Давиде Санджорджи . « О происхождении бисимуляции и коиндукции », Транзакции ACM по языкам и системам программирования , Vol. 31, № 4, май 2009 г.

Разнообразный

Кологическое программирование: расширение логического программирования с помощью коиндукции - описывает парадигму кологического программирования.

[1] «Со-логическое программирование | Lambda the Ultimate» .

[2] «Домашняя страница Гопала Гупты» .

[3] «Logtalk3/Examples/Coinduction у мастера · LogtalkDotOrg/Logtalk3» . Гитхаб .

[4] Бенджамин С. Пирс . «Типы и языки программирования» . Массачусетский технологический институт Пресс .

[5] Декстер Козен , Александра Сильва . «Практическая коиндукция». CiteSeerX 10.1.1.252.3961 .

[6] Ральф Хинце (2012). «Общее программирование с дополнениями» . Общее и индексированное программирование . Конспекты лекций по информатике. Том. 7470. Спрингер. стр. 47–129. дои : 10.1007/978-3-642-32202-0_2 . ISBN 978-3-642-32201-3 .

[1]

[2]

[3]

[4]

[5]

[6]