| 词条 | Coinduction |
| 释义 |
}}{{about|computer science|the use of this term in medicine and anaesthesia|coinduction (anaesthetics)}} In computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects. Coinduction is the mathematical dual to structural induction. Coinductively defined types are known as codata and are typically infinite data structures, such as streams. As a definition or specification, coinduction describes how an object may be "observed", "broken down" or "destructed" into simpler objects. As a proof technique, it may be used to show that an equation is satisfied by all possible implementations of such a specification. To generate and manipulate codata, one typically uses corecursive functions, in conjunction with lazy evaluation. Informally, rather than defining a function by pattern-matching on each of the inductive constructors, one defines each of the "destructors" or "observers" over the function result. In programming, co-logic programming (co-LP for brevity) "is a natural generalization of logic programming and coinductive logic programming, which in turn generalizes other extensions of logic programming, such as infinite trees, lazy predicates, and concurrent communicating predicates. Co-LP has applications to rational trees, verifying infinitary properties, lazy evaluation, concurrent logic programming, model checking, bisimilarity proofs, etc."[1] Experimental implementations of co-LP are available from The University of Texas at Dallas [2] and in Logtalk (for examples see [3]) and SWI-Prolog. See also
References1. ^http://lambda-the-ultimate.org/node/2513 2. ^http://www.utdallas.edu/~gupta/ 3. ^https://github.com/LogtalkDotOrg/logtalk3/tree/master/examples/coinduction Further reading
5 : Theoretical computer science|Logic programming|Functional programming|Category theory|Mathematical induction |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。