Corécursion - Corecursion

En informatique , la corécursion est un type d'opération qui est double de la récursivité . Alors que la récursivité fonctionne de manière analytique, en commençant par des données plus éloignées d'un cas de base et en les décomposant en données plus petites et en se répétant jusqu'à ce que l'on atteigne un cas de base, la corécursion fonctionne de manière synthétique, à partir d'un cas de base et en le construisant, produisant de manière itérative des données plus éloignées cas de base. En termes simples, les algorithmes corécursifs utilisent les données qu'ils produisent eux-mêmes, petit à petit, au fur et à mesure qu'ils deviennent disponibles et nécessaires, pour produire d'autres bits de données. Un concept similaire mais distinct est la récursion générative qui peut manquer d'une «direction» définie inhérente à la corécursion et à la récursivité.

Là où la récursivité permet aux programmes d'opérer sur des données arbitrairement complexes, du moment qu'elles peuvent être réduites à de simples données (cas de base), la corécursion permet aux programmes de produire des structures de données arbitrairement complexes et potentiellement infinies, telles que des flux , tant qu'elles peuvent être produites à partir de données simples (cas de base) dans une séquence d' étapes finies . Là où la récursivité peut ne pas se terminer, n'atteignant jamais un état de base, la corécursion commence à partir d'un état de base, et produit ainsi des étapes ultérieures de manière déterministe, bien qu'elle puisse continuer indéfiniment (et donc ne pas se terminer sous une évaluation stricte), ou elle peut consommer plus qu'elle ne produit et deviennent ainsi non productifs . De nombreuses fonctions qui sont traditionnellement analysées comme récursives peuvent alternativement, et sans doute plus naturellement, être interprétées comme des fonctions corécursives qui se terminent à un stade donné, par exemple des relations de récurrence telles que la factorielle.

La corécursion peut produire des structures de données finies et infinies en tant que résultats, et peut employer des structures de données autoréférentielles . La corécursion est souvent utilisée en conjonction avec l' évaluation paresseuse , pour produire seulement un sous-ensemble fini d'une structure potentiellement infinie (plutôt que d'essayer de produire une structure infinie entière à la fois). La corécursion est un concept particulièrement important en programmation fonctionnelle , où la corecursion et les codata permettent à des langages totaux de travailler avec des structures de données infinies.

Exemples

La corécursion peut être comprise par contraste avec la récursivité, qui est plus familière. Alors que la corécursion est principalement intéressante dans la programmation fonctionnelle, elle peut être illustrée à l'aide de la programmation impérative, qui est effectuée ci-dessous à l'aide de la fonction générateur de Python. Dans ces exemples, des variables locales sont utilisées et assignées des valeurs de manière impérative (destructive), bien que celles-ci ne soient pas nécessaires en corecursion en programmation fonctionnelle pure. Dans la programmation fonctionnelle pure, plutôt que d'assigner à des variables locales, ces valeurs calculées forment une séquence invariable, et les valeurs antérieures sont accessibles par auto-référence (les valeurs ultérieures dans la séquence font référence aux valeurs antérieures dans la séquence à calculer). Les affectations expriment simplement cela dans le paradigme impératif et spécifient explicitement où les calculs ont lieu, ce qui sert à clarifier l'exposition.

Factorielle

Un exemple classique de récursivité est le calcul de la factorielle , qui est définie récursivement par 0! : = 1 et n! : = n × (n - 1)! .

Pour calculer récursivement son résultat sur une entrée donnée, une fonction récursive s'appelle (une copie de) elle-même avec une entrée différente ("plus petite" en quelque sorte) et utilise le résultat de cet appel pour construire son résultat. L'appel récursif fait de même, sauf si le cas de base a été atteint. Ainsi, une pile d'appels se développe dans le processus. Par exemple, pour calculer fac (3) , cela appelle à son tour fac (2) , fac (1) , fac (0) ("liquidation" de la pile), à ​​quel point la récursivité se termine par fac (0) = 1 , puis la pile se déroule dans l'ordre inverse et les résultats sont calculés sur le chemin du retour le long de la pile d'appels vers la trame d'appel initiale fac (3) qui utilise le résultat de fac (2) = 2 pour calculer le résultat final comme 3 × 2 = 3 × fac (2) =: fac (3) et enfin retourner fac (3) = 6 . Dans cet exemple, une fonction renvoie une valeur unique.

Ce déroulement de la pile peut être expliqué, en définissant la factorielle corécursivement , comme un itérateur , où l'on commence par le cas de , puis à partir de cette valeur de départ construit des valeurs factorielles pour des nombres croissants 1, 2, 3 ... comme dans la définition récursive ci-dessus avec "time arrow" inversé, pour ainsi dire, en le lisant à l' envers comme . L'algorithme corécursif ainsi défini produit un flux de toutes les factorielles. Cela peut être concrètement implémenté en tant que générateur . Symboliquement, en notant que le calcul de la valeur factorielle suivante nécessite de suivre à la fois n et f (une valeur factorielle précédente), cela peut être représenté par: ${\ displaystyle 1 =: 0!}$${\ Displaystyle n! \ fois (n + 1) = :( n + 1)!}$

${\ Displaystyle n, f = (0,1) :( n + 1, f \ fois (n + 1))}$

ou à Haskell ,

  (\(n,f) -> (n+1, f*(n+1))) `iterate` (0,1)

signifiant, "à partir de , à chaque étape, les valeurs suivantes sont calculées comme ". Ceci est mathématiquement équivalent et presque identique à la définition récursive, mais souligne que les valeurs factorielles sont en cours de construction en , va vers l' avant du boîtier de départ, au lieu d'être calculé après la première marche arrière, vers le bas pour le cas de base, avec un décrément. La sortie directe de la fonction corécursive ne contient pas simplement les valeurs factorielles , mais inclut également pour chaque valeur les données auxiliaires de son index n dans la séquence, de sorte que n'importe quel résultat spécifique puisse être sélectionné parmi tous, au fur et à mesure des besoins. ${\ Displaystyle n, f = 0,1}$${\ Displaystyle n + 1, f \ fois (n + 1)}$${\ displaystyle +1}$${\ displaystyle -1}$${\ Displaystyle n!}$

Il y a une connexion avec la sémantique dénotationnelle , où les dénotations des programmes récursifs sont construites de manière corécursive de cette manière.

En Python, une fonction factorielle récursive peut être définie comme:

def factorial(n):
    """Recursive factorial function."""
    if n == 0:
        return 1
    else:
        return n * factorial(n - 1)

Cela pourrait alors être appelé par exemple factorial(5) pour calculer 5! .

Un générateur corecursif correspondant peut être défini comme:

def factorials():
    """Corecursive generator."""
    n, f = 0, 1
    while True:
        yield f
        n, f = n + 1, f * (n + 1)

Cela génère un flux infini de factorielles dans l'ordre; une partie finie de celui-ci peut être produite par:

def n_factorials(k):
    n, f = 0, 1
    while n <= k:
        yield f
        n, f = n + 1, f * (n + 1)

Cela pourrait alors être appelé pour produire les factorielles jusqu'à 5! via:

for f in n_factorials(5):
    print(f)

Si nous ne sommes intéressés que par une certaine factorielle, seule la dernière valeur peut être prise, ou nous pouvons fusionner la production et l'accès en une seule fonction,

def nth_factorial(k):
    n, f = 0, 1
    while n < k:
        n, f = n + 1, f * (n + 1)
    yield f

Comme on peut le voir facilement ici, c'est pratiquement équivalent (juste en remplaçant return le seul yield là-bas) à la technique de l'argument d'accumulateur pour la récursivité de queue , déroulée en une boucle explicite. Ainsi, on peut dire que le concept de corécursion est une explication de la réalisation des processus de calcul itératifs par des définitions récursives, le cas échéant.

Séquence de Fibonacci

De la même manière, la séquence de Fibonacci peut être représentée par:

${\ Displaystyle a, b = (0,1) :( b, a + b)}$

Parce que la séquence de Fibonacci est une relation de récurrence d'ordre 2, la relation corécursive doit suivre deux termes successifs, avec le correspondant pour avancer d'un pas, et le correspondant pour calculer le terme suivant. Cela peut ensuite être implémenté comme suit (en utilisant l' affectation parallèle ): ${\ displaystyle (b, -)}$${\ displaystyle (-, a + b)}$

def fibonacci_sequence():
    a, b = 0, 1
    while True:
        yield a
        a, b = b, a + b

À Haskell,

 map fst ( (\(a,b) -> (b,a+b)) `iterate` (0,1) )

Traversée d'arbre

La traversée d'arbres via une approche de profondeur d'abord est un exemple classique de récursivité. La traversée en largeur d'abord peut très naturellement être implémentée via corecursion.

Sans utiliser spécifiquement la récursivité ou la corécursion, on peut traverser un arbre en commençant au nœud racine, en plaçant ses nœuds enfants dans une structure de données, puis en itérant en supprimant nœud après nœud de la structure de données tout en replaçant les enfants de chaque nœud supprimé dans cette structure de données . Si la structure de données est une pile (LIFO), cela donne un parcours en profondeur d'abord, et si la structure de données est une file d'attente (FIFO), cela donne un parcours en largeur d'abord.

En utilisant la récursivité, une traversée en profondeur (post-ordre) en premier peut être implémentée en commençant au nœud racine et en parcourant de manière récursive chaque sous-arbre enfant à son tour (le sous-arbre basé sur chaque nœud enfant) - le deuxième sous-arbre enfant ne commence pas le traitement tant que le le premier sous-arbre enfant est terminé. Une fois qu'un nœud feuille est atteint ou que les enfants d'un nœud de branche ont été épuisés, le nœud lui-même est visité (par exemple, la valeur du nœud lui-même est sortie). Dans ce cas, la pile d'appels (des fonctions récursives) agit comme la pile qui est itérée.

En utilisant la corecursion, une traversée en largeur d'abord peut être implémentée en commençant au nœud racine, en sortant sa valeur, puis en traversant d'abord en largeur les sous-arbres - c'est-à-dire en passant la liste complète des sous-arbres à l'étape suivante (pas un seul sous-arbre, comme dans l'approche récursive) - à l'étape suivante, sortie de la valeur de tous leurs nœuds racines, puis transmission de leurs sous-arbres enfants, etc. Dans ce cas, la fonction de générateur, en fait la séquence de sortie elle-même, agit comme la file d'attente. Comme dans l'exemple factoriel (ci-dessus), où les informations auxiliaires de l'index (à quel pas un était, n ) ont été poussées vers l'avant, en plus de la sortie réelle de n !, Dans ce cas les informations auxiliaires des sous-arbres restants sont poussé vers l'avant, en plus de la sortie réelle. Symboliquement:

${\ displaystyle v, t = ([], [FullTree]) :( RootValues ​​(v, t), ChildTrees (t))}$

ce qui signifie qu'à chaque étape, on sort la liste des valeurs des nœuds racines, puis on passe aux sous-arbres enfants. Générer uniquement les valeurs de nœud à partir de cette séquence nécessite simplement de supprimer les données de l'arborescence enfant auxiliaire, puis d'aplatir la liste des listes (les valeurs sont initialement regroupées par niveau (profondeur); l'aplatissement (dégroupage) donne une liste linéaire plate). À Haskell,

 concatMap fst ( (\(v, t) -> (rootValues v t, childTrees t)) `iterate` ([], fullTree) )

Ceux-ci peuvent être comparés comme suit. Le parcours récursif gère un nœud feuille (en bas ) comme cas de base (lorsqu'il n'y a pas d'enfants, affichez simplement la valeur), et analyse un arbre en sous-arbres, traversant chacun à son tour, aboutissant finalement à seulement des nœuds feuilles - feuille réelle nœuds, et les nœuds de branche dont les enfants ont déjà été traités (coupés ci-dessous ). En revanche, le parcours corecursif gère un nœud racine (en haut ) comme cas de base (étant donné un nœud, commencez par afficher la valeur), traite un arbre comme étant synthétisé d'un nœud racine et de ses enfants, puis produit comme sortie auxiliaire une liste des sous-arbres à chaque étape, qui sont alors l'entrée pour l'étape suivante - les nœuds enfants de la racine d'origine sont les nœuds racine à l'étape suivante, car leurs parents ont déjà été traités (coupés ci-dessus ). Dans le parcours récursif, il y a une distinction entre les nœuds feuilles et les nœuds de branche, tandis que dans le parcours corécursif il n'y a pas de distinction, car chaque nœud est traité comme le nœud racine du sous-arbre qu'il définit.

Notamment, étant donné un arbre infini, le parcours corecursif largeur-premier traversera tous les nœuds, tout comme pour un arbre fini, tandis que le parcours récursif profondeur-premier descendra d'une branche et ne traversera pas tous les nœuds, et même s'il traverse un ordre postérieur. , comme dans cet exemple (ou dans l'ordre), il ne visitera aucun nœud, car il n'atteint jamais une feuille. Cela montre l'utilité de la corécursion plutôt que de la récursivité pour traiter des structures de données infinies.

En Python, cela peut être implémenté comme suit. Le parcours habituel de profondeur d'abord après ordre peut être défini comme suit:

def df(node):
    """Post-order depth-first traversal."""
    if node is not None:
        df(node.left)
        df(node.right)
        print(node.value)

Cela peut ensuite être appelé par df(t) pour imprimer les valeurs des nœuds de l'arbre dans l'ordre de profondeur post-ordre.

Le générateur corécursif en largeur peut être défini comme suit:

def bf(tree):
    """Breadth-first corecursive generator."""
    tree_list = [tree]
    while tree_list:
        new_tree_list = []
        for tree in tree_list:
            if tree is not None:
                yield tree.value
                new_tree_list.append(tree.left)
                new_tree_list.append(tree.right)
        tree_list = new_tree_list

Cela peut ensuite être appelé pour imprimer les valeurs des nœuds de l'arbre dans l'ordre en largeur:

for i in bf(t):
    print(i)

Définition

Les types de données initiaux peuvent être définis comme étant le plus petit point fixe ( jusqu'à l'isomorphisme ) d'une équation de type; l' isomorphisme est alors donné par une algèbre initiale . Les types de données bimensuels, finaux (ou terminaux) peuvent être définis comme étant le plus grand point fixe d'une équation de type; l'isomorphisme est alors donné par une gèbre charbonnière finale .

Si le domaine du discours est la catégorie des ensembles et des fonctions totales, alors les types de données finaux peuvent contenir des valeurs infinies et non bien fondées , contrairement aux types initiaux. En revanche, si le domaine du discours est la catégorie des ordres partiels complets et des fonctions continues , ce qui correspond à peu près au langage de programmation Haskell , alors les types finaux coïncident avec les types initiaux, et la charbonnière finale et l'algèbre initiale correspondantes forment un isomorphisme.

La corécursion est alors une technique pour définir récursivement des fonctions dont la plage (codomaine) est un type de données final, duel à la façon dont la récursivité ordinaire définit récursivement des fonctions dont le domaine est un type de données initial.

La discussion ci-dessous fournit plusieurs exemples dans Haskell qui distinguent la corecursion. En gros, si l'on portait ces définitions dans la catégorie des ensembles, elles seraient toujours corécursives. Cet usage informel est cohérent avec les manuels existants sur Haskell. Les exemples utilisés dans cet article sont antérieurs aux tentatives de définition de la corecursion et expliquent de quoi il s'agit.

Discussion

La règle de la corécursion primitive sur les codata est la double de celle de la récursivité primitive sur les données. Au lieu de descendre sur l'argument par pattern-matching sur ses constructeurs (qui ont été appelés avant , quelque part, donc nous recevons une donnée prête à l'emploi et obtenons ses sous-parties constitutives, c'est-à-dire les "champs"), nous montons sur le résultat en remplissant ses "destructeurs" (ou "observateurs", qui seront appelés par la suite , quelque part - donc nous appelons en fait un constructeur, créant un autre morceau du résultat à observer plus tard). Ainsi, la corécursion crée des codonnées (potentiellement infinies), tandis que la récursivité ordinaire analyse des données (nécessairement finies). La récursivité ordinaire peut ne pas être applicable aux codata car elle peut ne pas se terminer. Inversement, la corécursion n'est pas strictement nécessaire si le type de résultat est data, car les données doivent être finies.

Dans "Programmation avec des flux en Coq: une étude de cas: le tamis d'Eratosthène", nous trouvons

hd (conc a s) = a               
tl (conc a s) = s

(sieve p s) = if div p (hd s) then sieve p (tl s)
              else conc (hd s) (sieve p (tl s))

hd (primes s) = (hd s)          
tl (primes s) = primes (sieve (hd s) (tl s))

où les nombres premiers "sont obtenus en appliquant l'opération nombres premiers au flux (Enu 2)". En suivant la notation ci-dessus, la séquence de nombres premiers (avec un 0 jetable préfixé) et les flux de nombres étant tamisés progressivement, peuvent être représentés comme

${\ displaystyle p, s = (0, [2 ..]) :( hd (s), tamis (hd (s), tl (s)))}$

ou à Haskell,

(\(p, s@(h:t)) -> (h, sieve h t)) `iterate` (0, [2..])

Les auteurs discutent de la façon dont la définition de sieve n'est pas toujours garantie d'être productive , et pourrait rester bloquée, par exemple si elle est appelée avec [5,10..] comme flux initial.

Voici un autre exemple dans Haskell. La définition suivante produit la liste des nombres de Fibonacci en temps linéaire:

fibs = 0 : 1 : zipWith (+) fibs (tail fibs)

Cette liste infinie dépend de l'évaluation paresseuse; les éléments sont calculés au besoin, et seuls les préfixes finis sont toujours explicitement représentés en mémoire. Cette fonction permet aux algorithmes sur des parties de codata de se terminer; ces techniques sont une partie importante de la programmation Haskell.

Cela peut également être fait en Python:

from itertools import tee, chain, islice, imap

def add(x, y):
    return x + y

def fibonacci():
    def deferred_output():
        for i in output:
            yield i
    result, c1, c2 = tee(deferred_output(), 3)
    paired = imap(add, c1, islice(c2, 1, None))
    output = chain([0, 1], paired)
    return result

for i in islice(fibonacci(), 20):
    print(i)

La définition de zipWith peut être intégrée, conduisant à ceci:

fibs = 0 : 1 : next fibs
  where
    next (a: t@(b:_)) = (a+b):next t

Cet exemple utilise une structure de données autoréférentielle . Marques de récursion ordinaires utilisent des autoréférentielles fonctions , mais ne peuvent pas accueillir des données auto-référentiel. Cependant, ce n'est pas essentiel pour l'exemple de Fibonacci. Il peut être réécrit comme suit:

fibs = fibgen (0,1)
fibgen (x,y) = x : fibgen (y,x+y)

Cela n'utilise que la fonction auto-référentielle pour construire le résultat. S'il était utilisé avec un constructeur de liste stricte, ce serait un exemple de récursivité incontrôlable, mais avec un constructeur de liste non stricte, cette récursivité surveillée produit progressivement une liste indéfiniment définie.

La corécursion n'a pas besoin de produire un objet infini; une file d'attente corécursive est un exemple particulièrement bon de ce phénomène. La définition suivante produit une traversée en largeur d'abord d'un arbre binaire en temps linéaire:

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 : gen 1 queue

    gen  0   p                 =         []           
    gen len (Leaf   _     : s) =         gen (len-1) s 
    gen len (Branch _ l r : s) = l : r : gen (len+1) s

Cette définition prend un arbre initial et produit une liste de sous-arbres. Cette liste sert à la fois de file d'attente et de résultat ( gen len p produit ses len encoches de sortie après son pointeur arrière d'entrée,, le p long de queue ). Il est fini si et seulement si l'arbre initial est fini. La longueur de la file d'attente doit être explicitement suivie afin d'assurer la terminaison; cela peut être éludé en toute sécurité si cette définition n'est appliquée qu'aux arbres infinis.

Un autre exemple particulièrement bon donne une solution au problème de l'étiquetage en largeur d'abord. La fonction label visite chaque nœud dans un arbre binaire de manière large en premier, et remplace chaque étiquette par un entier, chaque entier suivant étant plus grand que le dernier par un. Cette solution utilise une structure de données autoréférentielle, et l'arbre binaire peut être fini ou infini.

label :: Tree a b -> Tree Int Int 
label t = t′
    where
    (t′, ns) = go t (1:ns)

    go :: Tree a b    -> [Int]  -> (Tree Int Int, [Int])
    go   (Leaf   _    ) (n:ns) = (Leaf   n       , n+1 : ns  )
    go   (Branch _ l r) (n:ns) = (Branch n l′ r′ , n+1 : ns′′)
                                where
                                  (l′, ns′ ) = go l ns
                                  (r′, ns′′) = go r ns′

Un apomorphisme (tel qu'un anamorphisme , tel que déplier ) est une forme de corécursion de la même manière qu'un paramorphisme (tel qu'un catamorphisme , tel qu'un pli ) est une forme de récursivité.

L' assistant de preuve Coq prend en charge la corecursion et la coinduction à l'aide de la commande CoFixpoint.

L'histoire

La corécursion, appelée programmation circulaire, remonte au moins à ( Bird 1984 ), qui crédite John Hughes et Philip Wadler ; des formes plus générales ont été développées dans ( Allison 1989 ) . Les motivations originales comprenaient la production d'algorithmes plus efficaces (permettant 1 passage sur les données dans certains cas, au lieu de nécessiter plusieurs passes) et la mise en œuvre de structures de données classiques, telles que des listes et des files d'attente à double chaînage, dans des langages fonctionnels. erreur harv: pas de cible: CITEREFAllison1989 ( aide )

Voir également

• Bisimulation
• Coinduction
• Récursion
• Anamorphisme

Remarques

Références