0 0 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 :

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.

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).

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 :

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)
}.

Utlisation de accu sur un BinaryTree :

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 :

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.

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.