Minecraft
Passer en vue forum1 2 3 4 5 6 7 8 9 10 11 12 13 14 | type BinaryTree_accu($A,$T) : accu ( $T -> $T neutral, ($A,$T) -> $T accumulate, ).define $T accu (BinaryTree($A) t,$T acc,BinaryTree_accu($A,$T) d) =if t is{ empty then neutral(d)(acc), binary_tree(l,a,r) then accu(l,accumulate(d)(a,accu(r,acc,d)),d)}. |
Derniers articles 
Version d'archive
- Ce site est en lecture seule. Certains liens dynamiques peuvent ne pas fonctionner correctement.
Revenge of MoonLib
Ce brouillon d'article est destiné à mettre au clair (comprendre : pour des logiciens) certaines des idées algorithmiques développées dans ma bibliothèque MoonLib .
Les problèmes ne sont pas classés par ordre d'importance mais par ordre d'arrivée (ordre dans lequel j'arrive à les exprimer dans les catégories bi-cartésiennes fermées).
Ma bibliothèque MoonLib donne des solutions algorithmiques à ces problèmes. J'espère que les exprimer à l'aide des catégories bi-cartésiennes fermées aidera à formaliser les solutions catégoriques correspondantes.
1. Monoïdes et transformations naturelles
Typiquement, un programmeur Anubis a l'habitude des définitions suivantes :
1 2 3 4 5 6 7 | type List($A) : [], [$A . List($A)].type BinaryTree($A) : empty, binary_tree(BinaryTree($A),$A,BinaryTree($A)). |
On veut une transformation naturelle de type BinaryTree($A) → List($A).
Cette transformation naturelle conserve la structure de monoïde.
Il s'ensuit qu'on l'on va utiliser l'opérateur List($A) + List($A) alors même que cet opérateur de concaténation est une fonction de complexité temporelle linéaire. Pour résoudre le problème on pourrait utiliser une structure de listes concaténables en temps constant.
1 2 3 4 | type CatenableList($A) : [], singleton($A), CatenableList($A) + CatenableList($A). |
La structure des listes concaténables est tout à fait semblable à la structure des arbres binaires dont les données sont placées aux feuilles (au lieu d'être placées aux nœuds).
1 2 3 4 | type LeafTree($A) : [], singleton($A), LeafTree($A) + LeafTree($A). |
MoonLib
résout le problème autrement, en fournissant un récurseur
accu
.
Le récurseur
accu
se comporte et s'utilise différemment du récurseur primitif. Au lieu de rendre explicite la structure monoïdale sous-jacente, il utilise la définition du programmeur pour implanter une transformation naturelle efficace.
Définition algorithmique de accu pour BinaryTree :
Spoiler
Afficher/Masquer
Utlisation de accu sur un BinaryTree :
1 2 3 4 5 6 7 8 9 10 11 12 | define List($A) to_list (BinaryTree($A) t) =accu( t, [], accu ( (List($A) l) |-> l, ($A a,List($A) l) |-> [a . l] )). |
Le cardinal d'un arbre binaire (en entier de Peano) pose un problème similaire :
1 2 3 | type Nat : zero, succ(Nat). |
On devrait utiliser l'opérateur Nat + Nat alors même que cet opérateur est une fonction de complexité temporelle linéaire. Même maladie, même remède.
1 2 3 4 5 6 7 8 9 10 11 12 | define Nat to_nat (BinaryTree($A) t) =accu( t, zero, accu ( (Nat n) |-> n, ($A a,Nat n) |-> succ(n) )). |
2. Encore + avec les bi-récurseurs
Pour implanter Nat + Nat on peut accumuler au choix sur le 1ier ou le 2nd argument.
Même chose avec un arbre binaire ordonné. Pour implanter l'union ( + ) on peut déconstruire indifféremment le 1ier ou le 2nd argument.
Cependant, parfois il arrive que pour implanter
+
on ne puisse déconstruire ni le 1ier ni le 2nd argument. Dans ces cas, la récursion primitive n'est pas juste inefficace (comme au chapitre précédent) elle est carrément impuissante / inexpressive 
MoonLib utilise le bi-récurseur fuse pour :
Réaliser le tri-fusion d'une liste (le récurseur primitif est inefficace).
Réaliser la fusion de 2 tas tournoi.
Réaliser la fusion de 2 pagodes.
© Copyright 2002-2024 Aeriesguard.com - Mentions légales
Aerie's Guard V 7.0 réalisé par Ertaï, designé par Ivaldir, illustré par Izual et Sophie Masure
