Coinduction - Coinduction
Inom datavetenskap är saminduktion en teknik för att definiera och bevisa egenskaper hos system för samtidiga interagerande objekt .
Coinduction är den matematiska dubbla till strukturell induktion . Coinduktivt definierade typer är kända som kodata och är vanligtvis oändliga datastrukturer , såsom strömmar .
Som en definition eller specifikation beskriver coinduction hur ett objekt kan "observeras", "brytas ned" eller "destrueras" till enklare objekt. Som bevisteknik kan den användas för att visa att en ekvation uppfylls av alla möjliga implementeringar av en sådan specifikation.
För att generera och manipulera kodata använder man vanligtvis corecursive -funktioner, i samband med lat utvärdering . Informellt, snarare än att definiera en funktion genom mönstermatchning på var och en av de induktiva konstruktörerna, definierar man var och en av "destruktorerna" eller "observatörerna" över funktionsresultatet.
I programmering är co-logic programmering (co-LP för korthet) "en naturlig generalisering av logisk programmering och koinduktiv logisk programmering, som i sin tur generaliserar andra utökningar av logisk programmering, såsom oändliga träd, lata predikat och samtidiga kommunicerade predikat. Co-LP har applikationer för rationella träd, verifiering av oändliga egenskaper, lat utvärdering, samtidig logikprogrammering, modellkontroll, likvärdighetsbevis , etc. " Experimentella implementeringar av co-LP är tillgängliga från University of Texas i Dallas och i Logtalk (för exempel se) och SWI-Prolog .
Se även
Referenser
Vidare läsning
- Läroböcker
- Davide Sangiorgi (2012). Introduktion till bisimulering och koinduktion . Cambridge University Press.
- Davide Sangiorgi och Jan Rutten (2011). Avancerade ämnen inom bisimulering och koinduktion . Cambridge University Press.
- Inledande texter
-
Andrew D. Gordon (1994). "En handledning om saminduktion och funktionell programmering". 1994: 78–95. CiteSeerX 10.1.1.37.3914 . Citera journal kräver
|journal=( hjälp ) - matematiskt orienterad beskrivning - Bart Jacobs och Jan Rutten (1997). En handledning om (Co) Algebras och (Co) Induction ( alternativ länk ) - beskriver induktion och coinduction samtidigt
- Eduardo Giménez och Pierre Castéran (2007). "En handledning om [co-] induktiva typer i Coq"
- Coinduction - kort introduktion
- Historia
- Davide Sangiorgi . " On the Origins of Bisimulation and Coinduction ", ACM Transactions on Programming Language and Systems, Vol. 31, Nb 4, maj 2009.
- Diverse
- Co-Logic Programming: Extending Logic Programming with Coinduction- beskriver ko-logisk programmeringsparadigm
