Коиндукция - Coinduction

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

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

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

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

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

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

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

использованная литература

  1. ^ http://lambda-the-ultimate.org/node/2513
  2. ^ http://www.utdallas.edu/~gupta/
  3. ^ https://github.com/LogtalkDotOrg/logtalk3/tree/master/examples/coinduction

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

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