Коиндукция

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

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

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

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

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

Описание

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

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

Пусть будет множеством и будет монотонной функцией , то есть: У {\displaystyle U} Ф {\displaystyle F} 2 У → 2 У {\displaystyle 2^{U}\rightarrow 2^{U}}

Х ⊆ И ⇒ Ф ( Х ) ⊆ Ф ( И ) {\displaystyle X\subseteq Y\Стрелка вправо F(X)\subseteq F(Y)}

Если не указано иное, предполагается, что сигнал монотонный. Ф {\displaystyle F}

X является F-закрытым, если Ф ( Х ) ⊆ Х {\displaystyle F(X)\subseteq X}
X является F-консистентным, если Х ⊆ Ф ( Х ) {\displaystyle X\subseteq F(X)}
X является неподвижной точкой, если Х = Ф ( Х ) {\displaystyle X=F(X)}

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

Теорема Кнастера –Тарского гласит, что наименьшая неподвижная точка ( обозначается ) задается пересечением всех F-замкнутых множеств, тогда как наибольшая неподвижная точка (обозначается ) задается объединением всех F-согласованных множеств. Теперь мы можем сформулировать принципы индукции и коиндукции. Ф {\displaystyle F} μ Ф {\displaystyle \мю Ф} ν Ф {\displaystyle \nu F}

Определение

Принцип индукции : Если F -замкнуто , то Х {\displaystyle X} μ Ф ⊆ Х {\displaystyle \mu F\subseteq X}
Принцип коиндукции : Если F -непротиворечиво , то Х {\displaystyle X} Х ⊆ ν Ф {\displaystyle X\subseteq \nu F}

Обсуждение

Принципы, как указано, несколько непрозрачны, но их можно с пользой рассматривать следующим образом. Предположим, вы хотите доказать свойство . По принципу индукции достаточно продемонстрировать F-замкнутое множество , для которого выполняется свойство. Двойственно, предположим, что вы хотите показать, что . Тогда достаточно продемонстрировать F-согласованное множество, которое, как известно, является членом. μ Ф {\displaystyle \мю Ф} Х {\displaystyle X} х ∈ ν Ф {\displaystyle x\in \nu F} х {\displaystyle x}

Примеры

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

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

Т = ⊥ | ⊤ | Т × Т {\displaystyle T=\bot \;|\;\top \;|\;T\times T}

То есть, набор типов включает "нижний тип" , "верхний тип" и (неоднородные) списки. Эти типы можно идентифицировать со строками над алфавитом . Пусть обозначает все (возможно бесконечные) строки над . Рассмотрим функцию : ⊥ {\displaystyle \bot} ⊤ {\displaystyle \top} Σ = { ⊥ , ⊤ , × } {\displaystyle \Sigma =\{\bot ,\top ,\times \}} Σ ≤ ω {\displaystyle \Сигма ^{\leq \омега }} Σ {\displaystyle \Сигма} Ф : 2 Σ ≤ ω → 2 Σ ≤ ω {\displaystyle F:2^{\Сигма ^{\leq \omega }}\rightarrow 2^{\Сигма ^{\leq \omega }}}

Ф ( Х ) = { ⊥ , ⊤ } ∪ { х × у : х , у ∈ Х } {\displaystyle F(X)=\{\bot ,\top \}\cup \{x\times y:x,y\in X\}}

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

Предположим, что мы берем в качестве нашего набора типов данных. Используя принцип индукции , мы можем доказать следующее утверждение: μ Ф {\displaystyle \мю Ф}

Все типы данных конечны μ Ф {\displaystyle \мю Ф}

Чтобы прийти к этому выводу, рассмотрим множество всех конечных строк над . Очевидно, что не может создать бесконечную строку, поэтому оказывается, что это множество F-замкнуто , и отсюда следует вывод. Σ {\displaystyle \Сигма} Ф {\displaystyle F}

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

Тип ⊥ × ⊥ × ⋯ ∈ ν Ф {\displaystyle \bot \times \bot \times \cdots \in \nu F}

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

{ ⊥ × ⊥ × ⋯ } {\displaystyle \{\bot \times \bot \times \cdots \}}

Этот набор оказывается F-консистентным , и поэтому . Это зависит от подозрительного утверждения, что ⊥ × ⊥ × ⋯ ∈ ν Ф {\displaystyle \bot \times \bot \times \cdots \in \nu F}

⊥ × ⊥ × ⋯ = ( ⊥ × ⊥ × ⋯ ) × ( ⊥ × ⊥ × ⋯ ) {\displaystyle \bot \times \bot \times \cdots =(\bot \times \bot \times \cdots )\times (\bot \times \bot \times \cdots )}

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

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

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

Поток данных a = S a ( Поток a )       -- Поток "деструкторов" head ( S a astream ) = a tail ( S a astream ) = astream

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

Отношения сF -коалгебры

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

Рассмотрим эндофунктор в категории множеств : Ф {\displaystyle F}

Ф ( х ) = А × х {\displaystyle F(x)=A\times x}
Ф ( ф ) = ⟨ я г А , ф ⟩ {\displaystyle F(f)=\langle \mathrm {id} _{A},f\rangle }

С конечной F-коалгеброй связан следующий морфизм: ν F {\displaystyle \nu F}

o u t : ν F → F ( ν F ) = A × ν F {\displaystyle \mathrm {out} :\nu F\rightarrow F(\nu F)=A\times \nu F}

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

F ( o u t ) ¯ : F ( ν F ) → ν F {\displaystyle {\overline {F(\mathrm {out} )}}:F(\nu F)\rightarrow \nu F}

такой что

o u t ∘ F ( o u t ) ¯ = F ( F ( o u t ) ¯ ) ∘ F ( o u t ) = F ( F ( o u t ) ¯ ∘ o u t ) {\displaystyle \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)}

Композиция индуцирует другой гомоморфизм F -коалгебры . Поскольку является конечным, этот гомоморфизм единственен и, следовательно , . Всего имеем: F ( o u t ) ¯ ∘ o u t {\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} } ν F → ν F {\displaystyle \nu F\rightarrow \nu F} ν F {\displaystyle \nu F} i d ν F {\displaystyle \mathrm {id} _{\nu F}}

F ( o u t ) ¯ ∘ o u t = i d ν F {\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} =\mathrm {id} _{\nu F}}
o u t ∘ F ( o u t ) ¯ = F ( F ( o u t ) ¯ ) ∘ o u t ) = i d F ( ν F ) {\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ \mathrm {out} )=\mathrm {id} _{F(\nu F)}}

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

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

Мы покажем, что

Поток А

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

из потока = ( голова потока , хвост потока ) из потока ( а , поток ) = S а поток

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

Отношения сматематическая индукция

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

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

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

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

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

F ( P ) ⊆ P {\displaystyle F(P)\subseteq P}

То есть,

{ 0 } ∪ { x + 1 : x ∈ P } ⊆ P {\displaystyle \{0\}\cup \{x+1:x\in P\}\subseteq P}

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

Смотрите также

Ссылки

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

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

Учебники
  • Давиде Санджорджи (2012). Введение в бисимуляцию и коиндукцию . Cambridge University Press.
  • Davide Sangiorgi и Jan Rutten (2011). Advanced Topics in Bisimulation and Coinduction . Cambridge University Press.
Вводные тексты
  • Эндрю Д. Гордон (1994). «Учебник по коиндукции и функциональному программированию». 1994. С.  78–95 . CiteSeerX 10.1.1.37.3914 . — математически ориентированное описание
  • Барт Якобс и Ян Раттен (1997). Учебник по (Ко)алгебрам и (Ко)индукции (альтернативная ссылка) — описывает индукцию и коиндукцию одновременно
  • Эдуардо Хименес и Пьер Кастеран (2007). «Учебное пособие по [ко-] индуктивным типам в Coq»
  • Коиндукция — краткое введение
История
Разнообразный
  • Co-Logic Programming: расширение логического программирования с помощью Coinduction — описывает парадигму co-logic-программирования.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Coinduction&oldid=1220174979"