Corécursion

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 répétant jusqu'à atteindre un cas de base, la corécursion fonctionne de manière synthétique, en commençant par un cas de base et en le construisant, en produisant de manière itérative des données plus éloignées d'un cas de base. En termes simples, les algorithmes corécursifs utilisent les données qu'ils produisent eux-mêmes, bit par bit, au fur et à mesure qu'elles deviennent disponibles et nécessaires, pour produire d'autres bits de données. Un concept similaire mais distinct est la récursivité générative , qui peut manquer d'une « direction » définie inhérente à la corécursion et à la récursivité.

Alors que la récursivité permet aux programmes d'opérer sur des données arbitrairement complexes, tant qu'elles peuvent être réduites à des données simples (cas de base), la corécursivité 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 . Alors que la récursivité peut ne pas se terminer, sans jamais atteindre un état de base, la corécursivité démarre à partir d'un état de base et produit ainsi des étapes ultérieures de manière déterministe, bien qu'elle puisse se poursuivre indéfiniment (et donc ne pas se terminer sous une évaluation stricte), ou qu'elle puisse consommer plus qu'elle ne produit et ainsi devenir non productive . De nombreuses fonctions 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 à une étape donnée, par exemple des relations de récurrence telles que la factorielle.

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

La corécursion peut être comprise par opposition à la récursivité, qui est plus familière. Bien que la corécursion soit principalement intéressante en 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 de générateur de Python . Dans ces exemples, des variables locales sont utilisées et des valeurs sont attribuées de manière impérative (de manière destructive), bien que celles-ci ne soient pas nécessaires dans la corécursion en programmation fonctionnelle pure . Dans la programmation fonctionnelle pure, plutôt que d'être attribuées à 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 de la séquence font référence aux valeurs antérieures de 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'exposé.

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 la même chose, à moins que le cas de base n'ait été atteint. Ainsi, une pile d'appels se développe dans le processus. Par exemple, pour calculer fac(3) , cela appelle récursivement à son tour fac(2) , fac(1) , fac(0) ("remontant" la pile), auquel cas la récursivité se termine avec 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 jusqu'au cadre d'appel initial 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 finalement renvoie fac(3) = 6 . Dans cet exemple, une fonction renvoie une valeur unique.

Ce déroulement de pile peut être explicité en définissant la factorielle de manière corécursive , comme un itérateur , où l' on part du cas de , puis à partir de cette valeur de départ on construit des valeurs factorielles pour des nombres croissants 1, 2, 3... comme dans la définition récursive ci-dessus avec la "flèche du temps" inversée, pour ainsi dire, en la lisant à l'envers comme . L'algorithme corécursif ainsi défini produit un flux de toutes les factorielles. Ceci peut être concrètement implémenté comme un générateur . Symboliquement, en notant que le calcul de la valeur factorielle suivante nécessite de garder une trace à la fois de n et de f (une valeur factorielle précédente), cela peut être représenté comme :

ou en Haskell ,

( \ ( n , f ) -> ( n + 1 , f * ( n + 1 ))) ` itérer ` ( 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 construites en avançant à partir du cas de départ, plutôt que d'être calculées après avoir d'abord reculé, jusqu'au 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 peut être sélectionné parmi tous, selon les besoins.

Il existe un lien 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 : 
int ) 
-> 
int : 
Fonction factorielle récursive.""" si n == 0 : renvoie 1 sinon : renvoie n * factorial ( n - 1 )

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

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

def 
factorials (): 
Générateur corécursif.""" n , f = 0 , 1 tant que True : rendement 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 ( n : 
int ): 
k , 
f 
= 
0 , 
1 
tant que 
k 
<= 
n : 
rendement 
f 
k , 
f 
= 
k 
+ 
1 , 
f 
* 
( k 
+ 
1 )

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

pour 
f 
dans 
n_factorielles ( 5 ): 
print ( f )

Si nous ne nous intéressons qu'à 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 ( n : 
int ): 
k , 
f 
= 
0 , 
1 
tant que 
k 
< 
n : 
k , 
f 
= 
k 
+ 
1 , 
f 
* 
( k 
+ 
1 ) 
renvoie 
f

Comme on peut le voir ici, cela est pratiquement équivalent (en remplaçant simplement returnle only yieldthere) à la technique de l'argument accumulateur pour la récursivité terminale , déroulée dans une boucle explicite. On peut donc dire que le concept de corecursion est une explication de l'incarnation des processus de calcul itératifs par des définitions récursives, le cas échéant.

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

Comme la suite de Fibonacci est une relation de récurrence d'ordre 2, la relation corécursive doit suivre deux termes successifs, le correspondant au décalage d'un pas en avant et le correspondant au calcul du terme suivant. Ceci peut alors être implémenté comme suit (en utilisant l'affectation parallèle ) :

def 
fibonacci_sequence (): 
a , 
b 
= 
0 , 
1 
tant que 
Vrai : 
renvoie 
a 
a , 
b 
= 
b , 
a 
+ 
b

En Haskell,

carte fst ( ( \ ( a , b ) -> ( b , a + b )) ` itérer ` ( 0 , 1 ) )

La traversée d'arbres via une approche en profondeur est un exemple classique de récursivité. De même, la traversée en largeur peut être très naturellement mise en œuvre via la corécursion.

De manière itérative, on peut parcourir un arbre en plaçant son nœud racine dans une structure de données, puis en itérant avec cette structure de données alors qu'elle n'est pas vide, en supprimant à chaque étape le premier nœud de celle-ci et en replaçant les nœuds enfants du nœud supprimé dans cette structure de données. Si la structure de données est une pile (LIFO), cela donne une traversée en profondeur d'abord, et si la structure de données est une file d'attente (FIFO), cela donne une traversée en largeur d'abord :

En utilisant la récursivité, une traversée en profondeur d'un arbre est implémentée simplement en traversant récursivement chacun des nœuds enfants du nœud racine à tour de rôle. Ainsi, le deuxième sous-arbre enfant n'est pas traité tant que le premier sous-arbre enfant n'est pas terminé. La valeur du nœud racine est gérée séparément, que ce soit avant que le premier enfant ne soit traversé (résultant en une traversée pré-ordre), après que le premier soit terminé et avant le deuxième (dans l'ordre), ou après que le deuxième nœud enfant soit terminé (post-ordre) - en supposant que l'arbre soit binaire, pour simplifier l'exposition. La pile d'appels (des invocations de fonction de traversée récursive) correspond à la pile sur laquelle serait itérée avec la manipulation explicite de la structure LIFO mentionnée ci-dessus. Symboliquement,

Le terme « récursivité » a ici deux significations. Tout d'abord, il s'agit des invocations récursives des fonctions de parcours d'arbre . Plus précisément, nous devons nous intéresser à la manière dont la liste de valeurs résultante est construite ici. La création de sortie récursive de bas en haut entraînera le parcours d'arbre de droite à gauche. Pour qu'il soit réellement exécuté dans l'ordre de gauche à droite prévu, le séquençage devrait être appliqué par des moyens externes, ou il serait automatiquement réalisé si la sortie devait être construite de manière descendante, c'est-à-dire de manière corécursive .

Un parcours en largeur d'abord créant sa sortie dans l'ordre descendant, de manière co-cursive, peut également être implémenté en commençant au nœud racine, en sortant sa valeur, puis en parcourant en largeur d'abord les sous-arbres - c'est-à-dire en passant toute la liste des sous-arbres à l'étape suivante (pas un seul sous-arbre, comme dans l'approche récursive) - à l'étape suivante en sortant les valeurs de tous leurs nœuds racines, puis en passant leurs sous-arbres enfants, etc. Dans ce cas, la fonction génératrice, 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 (à quelle étape se trouvait l'un, 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ées vers l'avant, en plus de la sortie réelle. Symboliquement,

ce qui signifie qu'à chaque étape, on génère la liste des valeurs des nœuds de ce niveau, puis on passe aux nœuds du niveau suivant. Pour générer uniquement les valeurs des nœuds de cette séquence, il suffit de supprimer les données auxiliaires de l'arbre enfant, puis d'aplatir la liste des listes (les valeurs sont initialement regroupées par niveau (profondeur) ; l'aplatissement (dégroupage) produit une liste linéaire plate). Ceci est équivalent en termes d'extension à la spécification ci-dessus. En Haskell,

concatMap fst ( ( \ ( v , ts ) -> ( rootValues ​​ts , childTrees ts )) ` itérer ` ( [] , [ fullTree ]) )

Notamment, étant donné un arbre infini, le parcours corécursif en largeur traversera tous les nœuds, tout comme pour un arbre fini, tandis que le parcours récursif en profondeur descendra d'une branche et ne traversera pas tous les nœuds, et en effet, s'il traverse après l'ordre, comme dans cet exemple (ou dans l'ordre), il ne visitera aucun nœud du tout, car il n'atteint jamais une feuille. Cela montre l'utilité de la corécursivité plutôt que de la récursivité pour traiter des structures de données infinies. Une mise en garde demeure pour les arbres avec le facteur de ramification infini, qui nécessitent un entrelacement plus attentif pour mieux explorer l'espace. Voir dovetailing .

En Python, cela peut être implémenté comme suit. Le parcours en profondeur post-ordre habituel peut être défini comme :

def 
df ( node ) : 
Traversée en profondeur post-commande en premier . " " " si le noeud n'est pas None : df ( node.left ) df ( node.right ) print ( node.value )

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

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

def 
bf ( tree ): 
Générateur corécursif en largeur d'abord.""" tree_list = [ tree ] while tree_list : new_tree_list = [] for tree in tree_list : si tree n'est pas None : renvoie 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 de largeur d'abord :

pour 
i 
dans 
bf ( t ): 
print ( i )

Les types de données initiaux peuvent être définis comme étant le plus petit point fixe ( à isomorphisme près ) d'une équation de type ; l' isomorphisme est alors donné par une algèbre initiale . De manière dualiste, les types de données 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 coalgèbre 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 fondées , alors que les types initiaux ne le font pas. D'autre part, si le domaine du discours est la catégorie des ordres partiels complets et des fonctions continues , ce qui correspond approximativement au langage de programmation Haskell , alors les types finaux coïncident avec les types initiaux, et la coalgèbre finale et l'algèbre initiale correspondantes forment un isomorphisme.

La corécursion est alors une technique permettant de définir de manière récursive des fonctions dont la plage (codomaine) est un type de données final, de manière duale à la manière dont la récursivité ordinaire définit de manière récursive des fonctions dont le domaine est un type de données initial.

La discussion ci-dessous fournit plusieurs exemples en Haskell qui distinguent la corécursion. En gros, si l'on devait transférer ces définitions à 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 corécursion et d'explication de ce qu'elle est.

La règle de la corecursion primitive sur les codata est la même que celle de la récursion primitive sur les data. Au lieu de descendre sur l'argument en faisant correspondre les motifs de ses constructeurs (qui ont été appelés avant , quelque part, de sorte que nous recevions une donnée toute faite et obtenions ses sous-parties constitutives, c'est-à-dire les "champs"), nous remontons sur le résultat en remplissant ses "destructeurs" (ou "observateurs", qui seront appelés après , quelque part - donc nous appelons en fait un constructeur, créant un autre morceau du résultat à observer plus tard). Ainsi, la corecursion crée des codata (potentiellement infinies), tandis que la récursion ordinaire analyse des données (nécessairement finies). La récursion ordinaire peut ne pas être applicable aux codata car elle peut ne pas se terminer. Inversement, la corecursion n'est pas strictement nécessaire si le type de résultat est data, car data doit être fini.

Dans « Programmation avec des flux en Coq : une étude de cas : le crible d'Eratosthène » nous trouvons

hd ( conc a s ) = a tl ( conc a s ) = s
( tamis p s ) = si div p ( hd s ) alors tamis p ( tl s ) sinon conc ( hd s ) ( tamis p ( tl s ))
hd ( nombres premiers s ) = ( hd s ) tl ( nombres premiers s ) = nombres premiers ( tamis ( hd s ) ( tl s ))

où les nombres premiers « sont obtenus en appliquant l'opération des 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 progressivement tamisés, peuvent être représentés comme

ou en Haskell,

( \ ( p , s @ ( h : t )) -> ( h , tamis h t )) ` itérer ` ( 0 , [ 2 .. ])

Les auteurs expliquent que la définition de sieven'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 en Haskell. La définition suivante produit la liste des nombres de Fibonacci en temps linéaire :

fibs = 0 : 1 : zipAvec ( + ) fibs ( queue fibs )

Cette liste infinie dépend d'une évaluation paresseuse ; les éléments sont calculés selon les besoins et seuls les préfixes finis sont explicitement représentés en mémoire. Cette fonctionnalité permet aux algorithmes de terminer des parties de codata ; de telles techniques constituent une partie importante de la programmation Haskell.

Cela peut également être fait en Python :

>>> depuis 
itertools 
import 
tee , 
chain , 
islice 
>>> def 
fibonacci (): 
... 
def 
deferred_output (): 
... 
rendement depuis 
la sortie 
... 
... 
résultat , 
c1 , 
c2 
= 
tee ( deferred_output (), 
3 ) 
... 
paired 
= 
( x 
+ 
y 
pour 
x , 
y 
dans 
zip ( c1 , 
islice ( c2 , 
1 , 
None ))) 
... 
sortie 
= 
chain ( [ 0 , 
1 ], 
paired ) 
... 
résultat de retour 
>>> print ( * islice ( fibonacci (), 20 ), sep = ', ' ) 0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181

La définition de zipWithpeut être intégrée, ce qui donne ceci :

fibs = 0 : 1 : prochain fibs où prochain ( a : t @ ( b : _ )) = ( a + b ) : prochain t

Cet exemple utilise une structure de données autoréférentielle . La récursivité ordinaire utilise des fonctions autoréférentielles , mais ne prend pas en charge les données autoréférentielles. Cependant, cela n'est pas essentiel à l'exemple de Fibonacci. Il peut être réécrit comme suit :

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

Cette méthode utilise uniquement une fonction autoréférentielle pour construire le résultat. Si elle était utilisée avec un constructeur de liste strict, ce serait un exemple de récursivité incontrôlable, mais avec un constructeur de liste non strict , cette récursivité protégée produit progressivement une liste indéfiniment définie.

La corécursion ne produit pas nécessairement un objet infini ; une file d'attente corécursive est un exemple particulièrement pertinent de ce phénomène. La définition suivante produit une traversée en largeur d'un arbre binaire de manière descendante , en temps linéaire (incorporant déjà l'aplatissement mentionné ci-dessus) :

données Arbre a b = Feuille a | Branche b ( Arbre a b ) ( Arbre a b )
bftrav :: Arbre a b -> [ Arbre a b ] bftrav arbre = arbre : ts où ts = gen 1 ( arbre : ts )
gen 0 p = [] gen len ( Feuille _ : p ) = gen ( len - 1 ) p gen len ( Branche _ l r : p ) = l : r : gen ( len + 1 ) p -- ----lecture---- ----écriture anticipée---
-- arbre bfvalues ​​= [v | (Branche v _ _) <- arbre bftrav]

Cette définition prend un arbre et produit une liste de ses sous-arbres (nœuds et feuilles). Cette liste a une double fonction, à la fois comme file d'attente d'entrée et comme résultat ( gen len pelle produit sa sortie lenquelques crans avant son pointeur arrière d'entrée, ple long de la liste). Elle est finie si et seulement si l'arbre initial est fini. La longueur de la file d'attente doit être explicitement suivie afin de garantir la terminaison ; cela peut être élidé en toute sécurité si cette définition est appliquée uniquement aux arbres infinis.

Ce code Haskell utilise une structure de données autoréférentielle, mais ne dépend pas essentiellement d'une évaluation paresseuse. Il peut être traduit directement en Prolog, par exemple, qui n'est pas un langage paresseux. Ce qui est essentiel, c'est la capacité à construire une liste (utilisée comme file d'attente) de manière descendante . Pour cela, Prolog a une récursivité de queue modulo cons (c'est-à-dire des listes ouvertes). Ce qui est également émulable dans Scheme, C, etc. en utilisant des listes chaînées avec un pointeur sentinelle de queue mutable :

bftrav ( 
Arbre , 
[ Arbre | TS ]) 
:- 
bfgen ( 
1 , 
[ Arbre | TS ], 
TS ).
bfgen ( 
0 , 
_ , 
[ ] ) 
: - 
!. 
% 0 entrées dans la file d'attente -- arrêter et fermer la liste 
bfgen ( 
N , 
[ leaf ( _ ) 
| P ], 
TS 
) 
: - 
N2 
est 
N - 1 , 
bfgen ( 
N2 , 
P , 
TS ). 
bfgen ( 
N , 
[ branch ( _ , L , R )| P ], 
[ L , R | TS ] ) 
: - 
N2 
est 
N + 1 , 
bfgen ( 
N2 , 
P , 
TS ). 
%% ----lecture----- --écriture anticipée--

Un autre exemple particulier donne une solution au problème de l'étiquetage en largeur. La fonction labelvisite chaque nœud d'un arbre binaire de manière à ce que la largeur soit la première, en remplaçant chaque étiquette par un entier, chaque entier suivant étant plus grand que le dernier de 1. Cette solution utilise une structure de données autoréférentielle et l'arbre binaire peut être fini ou infini.

étiquette :: Arbre a b -> Arbre Int Int étiquette t = tn où ( tn , ns ) = go t ( 1 : ns )
go :: Arbre a b -> [ Int ] -> ( Arbre Int Int , [ Int ]) go ( Feuille _ ) ( i : a ) = ( Feuille i , i + 1 : a ) go ( Branche _ l r ) ( i : a ) = ( Branche i ln rn , i + 1 : c ) où ( ln , b ) = go l a ( rn , c ) = go r b

Ou en Prolog, à titre de comparaison,

étiquette ( 
Arbre , 
Tn ) 
:- 
étiquette ( 
Arbre , 
[ 1 | Ns ], 
Tn , 
Ns ).
étiquette ( 
feuille ( _ ), 
[ I | A ], 
feuille ( 
I ), 
[ I + 1 | A ]). 
étiquette ( 
branche ( _ , L , R ), [ I | A ], 
branche ( I , Ln , Rn ), [ I + 1 | C ]) 
:- 
étiquette ( 
L , 
A , 
Ln , 
B ), 
étiquette ( 
R , 
B , 
Rn , 
C ).

Un apomorphisme (comme un anamorphisme , tel que unfold ) est une forme de corécursion de la même manière qu'un paramorphisme (comme un catamorphisme , tel que fold ) 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.

La corecursion, appelée programmation circulaire, remonte au moins à (Bird 1984), qui attribue son existence à John Hughes et Philip Wadler ; des formes plus générales ont été développées en (Allison 1989). Les motivations initiales comprenaient la production d'algorithmes plus efficaces (permettant un seul passage sur les données dans certains cas, au lieu de nécessiter plusieurs passages) et la mise en œuvre de structures de données classiques, telles que des listes et des files d'attente doublement chaînées , dans des langages fonctionnels.