In computer science, corecursion is a type of operation that is dual to recursion. Corecursion is typically used (in conjunction with lazy evaluation) to generate infinite data structures. The rule for primitive corecursion on codata is the dual to that for primitive recursion on data. Instead of descending on the argument by pattern-matching on its constructors, we ascend on the result by filling-in its "destructors" (or "observers").

PropertyValue
dbpprop:abstract
  • In computer science, corecursion is a type of operation that is dual to recursion. Corecursion is typically used (in conjunction with lazy evaluation) to generate infinite data structures. The rule for primitive corecursion on codata is the dual to that for primitive recursion on data. Instead of descending on the argument by pattern-matching on its constructors, we ascend on the result by filling-in its "destructors" (or "observers"). Notice that corecursion creates (potentially infinite) codata, whereas ordinary recursion analyses (necessarily finite) data. Ordinary recursion is not applicable to the codata because it might not terminate. Conversely, corecursion is not applicable if the result type is data, because data must be finite. Here is an example in Haskell. The following definition produces the list of Fibonacci numbers in linear time: fibs = 0 : 1 : zipWith (+) fibs (tail fibs) The infinite list is produced by corecursion — the latter values of the list are computed on demand starting from the initial two items 0 and 1. This kind of definition is possible only because of lazy evaluation, which allows algorithms on parts of codata to terminate; such techniques are an important part of Haskell programming. Corecursion can produce finite objects as well; a corecursive queue is a particularly good example of this phenomenon. The following definition produces a breadth-first traversal of a binary tree in linear time: data Tree a b = Leaf a | Branch b (Tree a b) (Tree a b) bftrav :: Tree a b -> [Tree a b] bftrav tree = queue where queue = tree : trav 1 queue trav 0 q = trav len = trav (len-1) q trav len = l : r : trav (len+1) q This definition takes an initial tree and produces list of subtrees. This list is finite if and only if the initial tree is finite. Lazy evaluation is still needed, even if the result happens to be finite. This is due to the use of self-reference. The list serves a dual purpose as both the queue and the result. The length of the queue must be explicitly tracked in order to ensure termination; this can safely be elided if this definition is applied only to infinite trees. An anamorphism is a form of corecursion in the same way that a catamorphism is a form of recursion. The Coq proof assistant supports corecursion and coinduction using the CoFixpoint command.
  • In de informatica is corecursie een operatie type dat een duale is van een recursie. Corecursie wordt typisch in samenhang met luie evaluatie gebruikt om oneindige datastructuren te genereren. De regel voor primitieve corecursie op codata is de duale van de regel voor primitieve recursie op data. In plaats van de argumenten van boven naar beneden te bekijken, lopen we de resultaten van beneden naar boven door. Mark op dat de corecursie (mogelijk oneindige) codata creëert, terwijl de gewone recursie (noodzakelijkerwijs eindige) data analyseert. Gewone recursie is niet toepasbaar op de codata, omdat de recursie mogelijk niet eindigt. Omgekeerd is corecursie niet toepasbaar als het resultaattype van de data eindig moet zijn. Een anamorfisme is op dezelfde manier een vorm van corecursie als een catamorfisme een vorm van recursie is. De Coq bewijsassistent ondersteunt corecursie en coinductie en maakt daarbij gebruik van het CoFixpoint commando.
  • Кореку́рсия — в теории категорий и информатике тип операции, дуальный к рекурсии. Обычно корекурсия используется (совместно с механизмом ленивых вычислений) для генерации бесконечных структур данных.
dbpprop:hasPhotoCollection
rdfs:comment
  • In computer science, corecursion is a type of operation that is dual to recursion. Corecursion is typically used (in conjunction with lazy evaluation) to generate infinite data structures. The rule for primitive corecursion on codata is the dual to that for primitive recursion on data. Instead of descending on the argument by pattern-matching on its constructors, we ascend on the result by filling-in its "destructors" (or "observers").
  • In de informatica is corecursie een operatie type dat een duale is van een recursie. Corecursie wordt typisch in samenhang met luie evaluatie gebruikt om oneindige datastructuren te genereren. De regel voor primitieve corecursie op codata is de duale van de regel voor primitieve recursie op data. In plaats van de argumenten van boven naar beneden te bekijken, lopen we de resultaten van beneden naar boven door.
  • Кореку́рсия — в теории категорий и информатике тип операции, дуальный к рекурсии. Обычно корекурсия используется (совместно с механизмом ленивых вычислений) для генерации бесконечных структур данных.
rdfs:label
  • Corecursion
  • Corecursie
  • Корекурсия
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of