Коиндукция

Эта статья о информатике. Чтобы узнать о термине абстрактной алгебры, см. « Смена колец» . Чтобы узнать об использовании этого термина в медицине и анестезии, см. коиндукция (анестезия) .

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

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

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

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

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

Описание

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

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

Позволять $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$ (см. Повторение десятичной дроби ).

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

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

data Stream a = S a (Stream a)

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

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

с F -

Источник:

Рассмотрим эндофунктор $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$

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

См. также

• В коалгебре
• Корекурсия
• Бисимуляция
• Анаморфизм
• Полное функциональное программирование

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

Учебники

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

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

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

История

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

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

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