Le blog de SpiceGuid

Profil Contributions

Vous l'ignorez sans doute : LEGO®-group fait énormément de crowdsourcing .

Pour des pièces, des boîtes, des thèmes, c'est sans limite.

Avant qu'il y ait un site dédié pour ça j'avais même reçu un courriel qui me demandait de proposer une idée de thème original visant les 8/10 ans (jamais fait chez LEGO, à décrire en 5 lignes !) pour l'année suivante.

Grosso-modo, à l'époque, j'avais pensé à un cyber-univers, rebelles contre machines, Matrix-like (le courriel demandait explicitement de s'inspirer ou de parodier un film à succès).

Le temps a passé, la limite des 5 lignes a perdu son sens, et voici aujourd'hui le synopsis tel qu'il a évolué :

• La planète terre a été envahie par une forme de vie artificielle holistique baptisée Narcissus.
• Narcissus a abondamment dispersé dans l'atmosphère une toxine baptisée Némésis.
• Cette toxine diffuse fait pourrir la chair des femmes et des hommes qui la respirent. Toutefois certaines femmes, les Neva, y survivent et acquièrent ainsi de nouveaux pouvoirs. De même certains hommes, les Numa, y survivent et acquièrent ainsi de nouveaux talents.
• Alors que l'humanité est décimée par Némésis, Narcissus a envoyé ses CompuTrix pour entamer la phase de terraformation. Désormais la surface de la terre n'est plus une BioSphère mais une CompuSphère. Les dernières Neva et les derniers Numa se sont réfugiés sous la surface, dans les entrailles du CompuGlobe, un immense dédale de béton et d'acier, terraformé par les infatigables CompuTrix de Narcissus. Apparemment sans limites, le CompuGlobe est parcouru par les CompuWires qui relient entre-eux les CompuCores du Computron principal.
• Le Computron principal est un réseaux hypercubique qui permet la conversion des CompuBits en CompuWare et vice-versa. De cette façon Narcissus peut déplacer ses CompuBots à volonté. Où il veut. Quand il veut. En nombre voulu.
• Nairu est un puissant Numa captif des CompuBots. Après son évasion, il décide d'entamer une longue ascension vers la CompuSphère où il espère trouver Naira, la Neva de lumière dont il a rêvé.
• Ysus est un autre puissant Numa captif des CompuBots. Après son évasion, il décide d'entamer une longue descente au cœur du CompuGlobe où il espère trouver Ysis, la Neva de fertilité dont il a rêvé.

Ça me paraît assez simple. Du coup je soupçonne que ça a déjà été fait (en mieux). Dites-le moi. Ou sinon dites-moi pourquoi il ne faudrait pas conserver ceci, ou cela, ou même le tout.

À vos plûmes.

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.

Alors comme ça vous envisagez un doctorat ?

Dès que j'ai lu le titre une envie irrésistible m'a prise de faire le test .

Question 1. When you finished your undergraduate degree, you ...

Manque d'assiduité, je n'ai pas terminé ma licence Je n'ai pas le niveau / diplôme pour postuler à un doctorat. Bon, je le reconnais, ça démarre mal pour moi.

Mais je ne me laisse pas décourager. Je ne pourrai pas répondre à la Question 1 mais je vais quand-même poursuivre le test pour voir si j'ai le mental, le profil, l'état d'esprit, what it takes , pour un doctorat.  

 
Question 2. réponse A
Question 3. réponse A
Question 4. réponse A
Question 5. réponse A
Question 6. réponse D
Question 7. réponse A
Question 8. réponse A
Question 9. réponse B
Question 10.  réponse C (un tournoi FIFA 2013, c'est vraiment du n'importe quoi !)
Question 11. réponse A

Suite et fin de l' Introduction express aux types dépendants .

Prérequis.

Il est entendu que vous avez lu attentivement Introduction express aux types dépendants et qu'éventuellement vous êtes allé un peu plus loin. Par exemple en lisant le manuel Coq ainsi que d'autres tutoriels sur le net.

De la Turing complétude et de la misère de la condition humaine.

On pourrait penser qu'avec un langage aussi sérieux que OCaml on est à l'abri des turpitudes qui empoissent la vie des pauvres mortels que nous sommes.

 Hélas ça n'est qu'une illusion dont je vais rapidement vous délivrer.

OCaml est Turing-complet. D'un côté c'est rassurant. Au premier abord c'est même un avantage :

D'après la thèse de Church cela ne limite pas vos ambitions en matière de calculabilité.

Et de l'ambition vous en avez à revendre. Par exemple pourquoi ne pas créer une intelligence supérieure et la lancer à la conquête de l'univers ? Ou bien transformer le plomb en or ?

Bon, on va commencer par quelque chose de simple, on va se contenter de transformer le plomb en or.

(* 1Kg de plomb et 1Kg d'or *)
type lead_1Kg = Lead_1Kg
type gold_1Kg = Gold_1Kg

(* une fonction magique *)
let rec magic abracadabra = magic abracadabra

(* une fonction qui utilise la magie pour transformer 1Kg de plomb en 1Kg d'or *)
# let transmute : lead_1Kg -> gold_1Kg = magic;;
val transmute : lead_1Kg -> gold_1Kg = <fun>

Et nous voilà virtuellement riches comme Nicolas Flamel, car pour produire 1Kg d'or il nous suffit de transmuter 1Kg de plomb transmute Lead_1Kg .

On est bien parti. Pourquoi s'arrêter en si bon chemin ? Être riche c'est bien mais à la longue on s'y habitue.

Alors on va se lancer un nouveau défi, plus grandiose : conquérir l'univers à l'aide d'une simple cacahuète.

(* une cacahuète *)
type peanut = Peanut

(* un plan diabolique qui utilise la magie pour transformer une cacahuète *)
(* en une super-intelligence qu'on va lancer à la conquête de l'univers   *)
# let my_space_conquest_plan : peanut -> <conquer_the_universe:unit> = magic;;
val my_space_conquest_plan : peanut -> <conquer_the_universe:unit> = <fun>

Zut, j'ai mangé tout le paquet de cacahuètes.

Ha oui. J'ai oublié de vous dire. La fonction magic ne termine pas

C'est un des désagréments de la Turing-complétude.

Moins de promesses, plus de preuves !

Et si on abandonnait carrément la Turing-complétude ?

On perdrait (éventuellement) quelques possibilités délirantes (ou pas, mais là n'est pas la question qui nous préoccupe ici). C'est l'inconvénient.

Cependant l'avantage est considérable :

Si notre programme n'est pas Turing-complet on peut vérifier sa terminaison.

Si notre programme n'est pas Turing-complet on peut rédiger sa spécification et prouver qu'il la respecte en tous points.

Le peuple réclame un exemple concret !

Soit. On va abandonner OCaml.

On passe en Coq, et on revoit nos classiques.
Par exemple l'indémodable arbre binaire de recherche .

On va y stocker des entiers naturels, certes on y perd en généricité mais le code sera plus lisible et le principe reste le même :

Ou bien l'arbre est vide.

Ou bien l'arbre possède une racine qui contient un élément pivot, les éléments strictement plus petits sont dans la branche gauche, les éléments strictement plus grands sont dans la branche droite.

L'arbre est un ensemble et pas un multi-ensemble, chaque élément est inclus une fois et une seule.

On ne va pas se prendre la tête : notre arbre binaire de recherche ne sera pas équilibré .

On envoie la sauce en Coq :

(* c'est là qu'est définie nat_compare *)
Require Import Arith.Arith_base.

(* un arbre est soit vide soit une séparation en deux *)
Inductive tree : Type :=
  | Empty: tree
  | Split: tree -> nat -> tree -> tree.

(* recherche d'un entier n dans un arbre t *)
Fixpoint find t n :=
  match t with
  | Empty => false     (* absent *)
  | Split l m r =>
      match nat_compare n m with
      | Eq => true     (* on l'a trouvé *)
      | Lt => find l n (* on cherche à gauche *)
      | Gt => find r n (* on cherche à droite *)
      end
  end.

(* insertion d'un entier n dans un arbre t *)
Fixpoint insert t n :=
  match t with
  | Empty => Split Empty n Empty     (* on crée un singleton *)
  | Split l m r =>
      match nat_compare n m with
      | Eq => t                      (* déjà présent *)
      | Lt => Split (insert l n) m r (* on insère à gauche *)
      | Gt => Split l m (insert r n) (* on insère à droite *)
      end
  end.

Quelle différence avec une source équivalente en OCaml ?

Hé bien très peu sinon qu'ici il n'y a pas d'arnaque, on est certain que les fonctions find et insert terminent bien. Coq nous l'annonce par les messages suivants :

find is recursively defined (decreasing on 1st argument)
insert is recursively defined (decreasing on 1st argument)

Néanmoins nous ne baissons pas la garde. Nos fonctions terminent mais jusque là rien ne nous garantie qu'elles se comportent selon nos attentes.

Foin de la démagogie ! Le peuple réclame une politique de transparence !

Soit. Examinons en détail le programme de notre candidat au statut d'arbre totalement ordonné :

L'évidence voudrait qu'on puisse retrouver un élément une fois qu'il a été inséré.

La politesse voudrait qu'un élément admis dans l'ensemble n'entraine pas l'expulsion d'un ou plusieurs éléments déjà présents.

Le protocole exige que l'insertion d'un élément laisse l'arbre dans son état ordonné qui précédait l'insertion.

Qu'est-ce que vous en pensez ? Ça paraît honnête, non ?

Bon, après vous me direz : c'est de la politique, il va nous dire 'héritage désastreux légué par mon prédécesseur', 'crise', 'croissance molle'...

Il dit ce qu'il fait.

Parce que jusque là le programme est un peu vague. C'est sujet à interprétation. Et puis il ne va pas appliquer toutes ses mesures mais seulement les moins coûteuses et celles qui arrangent ses partisans.

Alors on va réécrire tout ça plus proprement.
En commençant par la propriété d'appartenance d'un entier à un arbre ordonné :

Inductive member : tree -> nat -> Prop :=
  | root_member :
      forall l n r,
      member (Split l n r) n
  | left_member :
      forall m n l r,
      member l n ->
      member (Split l m r) n 
  | right_member :
      forall m n l r,
      member r n ->
      member (Split l m r) n. 

Il y a comme qui dirait de la redite. Malgré une nouvelle syntaxe, dans l'esprit ça ressemble furieusement à la fonction find . Attendez une minute ! J'ai un mot d'excuse. find est une fonction, alors que member est une proposition (d'où son type Prop ). find est faite pour s'exécuter, alors que member ne s'exécutera jamais. Pour faire nos démonstrations nous n'exécutons rien, nous avons besoin de propositions.

À commencer par member que nous allons mettre au charbon pas plus tard que tout de suite :

La première mesure de notre candidat peut maintenant se reformuler comme ceci : 

forall t n, member (insert t n) n .

La seconde mesure de notre candidat peut maintenant se reformuler comme ceci : 

forall t m n, member t m -> member (insert t n) m .

La troisième mesure de notre candidat peut maintenant se reformuler comme ceci est reportée au prochain mandat.

Il a la tactique.

La tactique principale c'est l' induction .

Il s'agit d'une généralisation du raisonnement par récurrence .

Soit une propriété P à démontrer sur un type T :

Démontrez cette propriété pour les constructeurs non récursifs ( O pour ℕ, Empty pour une liste ou un ensemble,...).

Faites l'hypothèse d'induction que P est vraie pour les composantes récursives ( P(n) pour S n , P(t) pour Cons h t ,...) et démontrez qu'alors P est vraie pour les constructeurs récursifs ( P(S n) , P(Cons h t) ,...).

Il fait ce qu'il dit.

On peut retrouver un élément une fois qu'il a été inséré :

Theorem insert_is_inclusive :
  forall t n, member (insert t n) n.
Proof.
  intros t n. induction t.
  (* Empty *)
  simpl.
    apply root_member.
  (* Split *)
  simpl. remember (nat_compare n n0) as cmp.
  destruct cmp.
    (* Eq *)
    symmetry in Heqcmp.
    apply (nat_compare_eq n n0) in Heqcmp.
    subst n0. apply root_member.
    (* Lt *)
    apply left_member. exact IHt1.
    (* Gt *)
    apply right_member. exact IHt2.
Qed.

Un élément inséré dans l'ensemble n'entraine pas l'expulsion d'un ou plusieurs éléments déjà présents :

Theorem insert_is_conservative :
  forall t m n, member t m -> member (insert t n) m.
Proof.
  intros t m n H. induction t.  
  (* Empty *)
  simpl.
    apply left_member. exact H.
  (* Split *)
  remember (Split t1 n0 t2) as node.
  destruct H.
  (* root_member *)
  simpl. destruct (nat_compare n n1).
    apply root_member.
    apply root_member.
    apply root_member.
  (* left_member *)
  inversion Heqnode. rewrite H1 in H.
  simpl. destruct (nat_compare n n0).
    apply left_member. exact H.
    apply IHt1 in H. apply left_member. exact H.
    apply left_member. exact H.
  (* right_member *)
  inversion Heqnode. rewrite H3 in H.
  simpl. destruct (nat_compare n n0).
    apply right_member. exact H.
    apply right_member. exact H.
    apply IHt2 in H. apply right_member. exact H.
Qed.

Il termine le travail. 

Merci de m'avoir renouvelé votre confiance.

Il me reste un dernière promesse à tenir : l'insertion d'un élément doit laisser l'arbre dans son état ordonné qui précédait l'insertion.

Pour ça il nous faudrait une proposition tree_ordered qui dirait si un arbre binaire est totalement ordonné ou non.

Votre serviteur avait proposé ceci :

Inductive tree_between : tree -> nat -> nat -> Prop :=
  | leaf_tree_between :
      forall a b,
      tree_between Leaf a b
  | node_tree_between :
      forall l m r, forall a b,
      tree_between l a m -> a < m < b -> tree_between r m b ->
      tree_between (Node l m r) a b
with tree_less : tree -> nat -> Prop :=
  | leaf_tree_less :
      forall b,
      tree_less Leaf b
  | node_tree_less :
      forall l m r, forall b,
      tree_less l m -> m < b -> tree_between r m b ->
      tree_less (Node l m r) b
with tree_more : tree -> nat -> Prop :=
  | leaf_tree_more :
      forall a,
      tree_more Leaf a
  | node_tree_more :
      forall l m r, forall a,
      tree_between l a m -> a < m -> tree_more r m ->
      tree_more (Node l m r) a.
  
Inductive tree_ordered : tree -> Prop :=
  | leaf_tree_ordered :
      tree_ordered Leaf
  | node_tree_ordered :
      forall l m r,
      tree_less l m -> tree_more r m ->
      tree_ordered (Node l m r).

Heureusement que je suis entouré des meilleurs conseillers Il se trouve que ma proposition pour tree_ordered est sous-optimale.

Explication. Il y a deux écueils possibles dans l'activité de spécification :

La sous-spécification. La spécification donne certaines garanties mais pas toutes les garanties qu'on est en droit d'attendre. Tout n'est pas prouvé, il peut rester une ou plusieurs failles.

La sur-spécification. La spécification donne plus de garanties que celles qu'on attend. Le logiciel est correct. Mais la preuve est sans doute plus longue, laborieuse et alambiquée que nécessaire.

Le problème de mon tree_ordered c'est qu'il n'est pas récursif. Il ne fait qu'utiliser tree_between - tree_less - tree_more . C'est un cas de sur-spécification. La preuve serait plus compliquée que strictement nécessaire.

à Ptival et à dividee pour cette remarque pertinente.

en plus de diagnostiquer le problème dividee a également élaboré une solution.

Bravo à lui, c'est un bel exemple de proof-engineering .

Voici la solution proposée par dividee   :

Inductive tree_less : tree -> nat -> Prop :=
  | empty_tree_less :
      forall b, tree_less Empty b
  | split_tree_less :
      forall l m r b,
      tree_less l b -> tree_less r b -> m < b ->
      tree_less (Split l m r) b.

Inductive tree_more : tree -> nat -> Prop :=
  | empty_tree_more :
      forall a, tree_more Empty a
  | split_tree_more :
      forall l m r a,
      tree_more l a -> tree_more r a -> m > a ->
      tree_more (Split l m r) a.

Inductive tree_ordered : tree -> Prop :=
  | empty_tree_ordered :
      tree_ordered Empty
  | split_tree_ordered :
      forall l m r,
      tree_ordered l -> tree_ordered r ->
      tree_less l m -> tree_more r m ->
      tree_ordered (Split l m r).

Avec cette solution la proposition tree_ordered est maintenant récursive. Ça va faciliter la preuve par induction .

Du coup "l'insertion d'un élément doit laisser l'arbre dans son état ordonné" peut maintenant s'écrire ainsi : forall t, tree_ordered t -> forall n, tree_ordered (insert t n) .

à dividee pour avoir développé la preuve qui suit.

dividee commence par caractériser les sous-arbres à gauche : ce sont les arbres majorés par un entier.

Fact tree_less_upper_bound:
  forall t n, tree_less t n <-> forall m, member t m -> m < n.
Proof.
  split.
  (* -> *)
  intros Hless m Hm. induction t.
  inversion Hm.
  inversion Hm; inversion Hless; subst; auto.
  (* <- *)
  intros H. induction t.
    constructor.
    constructor.
      apply IHt1. intros m Hm. apply H. apply left_member. assumption.
      apply IHt2. intros m Hm. apply H. apply right_member. assumption.
      apply H. apply root_member.
Qed.

Et, symétriquement, les sous-arbres à droite sont les arbres minorés par un entier.

Fact tree_more_lower_bound: 
  forall t n, tree_more t n <-> forall m, member t m -> m > n.
Proof.
  split.
  (* -> *)
  intros Hmore m Hm. induction t.
  inversion Hm.
  inversion Hm; inversion Hmore; subst; auto.
  (* <- *)
  intros H. induction t.
    constructor.
    constructor.
      apply IHt1. intros m Hm. apply H. apply left_member. assumption.
      apply IHt2. intros m Hm. apply H. apply right_member. assumption.
      apply H. apply root_member.
Qed.

Puis dividee introduit deux lemmes , l'un dit qu'un élément plus petit que le pivot est présent dans le sous-arbre gauche, l'autre dit qu'un élément plus grand que le pivot est présent dans le sous-arbre droit.

Lemma member_left:
  forall l m r n, tree_ordered (Split l m r) -> member (Split l m r) n -> n < m -> member l n.
Proof.
  intros l m r n Hord Hmem Hlt.
  inversion Hord; subst; clear Hord.
  inversion Hmem; subst; clear Hmem.
    contradict Hlt. apply lt_irrefl.
    assumption.
    apply tree_more_lower_bound with (m:=n) in H5.
      contradict H5. apply gt_asym. assumption.
      assumption.
Qed.

Lemma member_right:
  forall l m r n, tree_ordered (Split l m r) -> member (Split l m r) n -> n > m -> member r n.
Proof.
  intros l m r n Hord Hmem Hlt.
  inversion Hord; subst; clear Hord.
  inversion Hmem; subst; clear Hmem.
    contradict Hlt. apply lt_irrefl.
    apply tree_less_upper_bound with (m:=n) in H4.
      contradict H4. apply lt_asym. assumption. assumption.
    assumption.
Qed.

Ensuite dividee ajoute encore deux lemmes , l'un dit que l'insertion d'un élément plus petit préserve le majorant, l'autre dit que l'insertion d'un élément plus grand préserve le minorant. 

Lemma insert_preserves_less:
  forall t n m, tree_less t n -> m < n -> tree_less (insert t m) n.
Proof.
  induction t; intros; inversion H; subst; clear H.
  repeat constructor. assumption.
  simpl. destruct (nat_compare m n); constructor; auto.
Qed.

Lemma insert_preserves_more:
  forall t n m, tree_more t n -> m > n -> tree_more (insert t m) n.
Proof.
  induction t; intros; inversion H; subst; clear H.
  repeat constructor. assumption.
  simpl. destruct (nat_compare m n); constructor; auto.
Qed.

Finalement dividee prouve que l'insertion préserve un arbre totalement ordonné.

Theorem insert_preserves_order :
  forall t, tree_ordered t ->
  forall n, tree_ordered (insert t n).
Proof.
  induction t; intros.
  (* Empty *)
  simpl. repeat constructor.
  (* Split *)
  simpl. remember (nat_compare n0 n) as cmp. symmetry in Heqcmp.
  destruct cmp.
    assumption.
    inversion H; subst; clear H. constructor; auto.
      apply nat_compare_lt in Heqcmp. apply insert_preserves_less; assumption.
    inversion H; subst; clear H. constructor; auto.
      apply nat_compare_gt in Heqcmp. apply insert_preserves_more; assumption.
Qed.

Il contente même les grognons.

Certains grincheux pourraient penser que les "bons" théorèmes à prouver ne devraient pas utiliser la proposition member mais plutôt la fonction find , par exemple comme ceci :

forall t n, find (insert t n) n = true

forall t m n, (find t m = true) -> (find (insert t n) m = true)

dividee a pensé à eux. Il prouve que member (dans le monde des propositions) est rigoureusement équivalent à find (dans le monde des fonctions).

Theorem find_iff_member :
  forall t, tree_ordered t ->
  forall n, find t n = true <-> member t n.
Proof.
  intros t ord n.
  split; intro H.
    (* -> *)
    induction t.
      (* Empty *)
      inversion H.
      (* Split *)
      inversion_clear ord.
      simpl in H. remember (nat_compare n n0) as cmp.
      symmetry in Heqcmp. destruct cmp.
        (* n = n0 *)
        apply nat_compare_eq in Heqcmp. subst.
        apply root_member.
        (* n < n0 *)
        apply left_member. apply IHt1.
          assumption. assumption.
        (* n > n0 *)
        apply right_member. apply IHt2.
          assumption. assumption.
    (* <- *)
    induction t.
      (* Empty *)
      inversion H.
      (* Split *)
      simpl. remember (nat_compare n n0) as cmp.
      symmetry in Heqcmp. destruct cmp.
        (* n = m *)
        reflexivity.
        (* n < m *)
        apply IHt1.
          inversion ord. assumption.
          apply nat_compare_lt in Heqcmp.
            apply member_left with (n:=n) in ord.
              assumption. assumption. assumption.
        (* n > m *)
        apply IHt2.
          inversion ord. assumption.
          apply nat_compare_gt in Heqcmp.
            apply member_right with (n:=n) in ord.
              assumption. assumption. assumption.
Qed.

Son bilan.

Avantages :

Bye-bye UML. Bye-bye les méthodes agiles. Bye-bye l' extreme programming . Bye-bye les diagrammes de conception. Bye-bye la documentation. Bye-bye le cycle de développement en fontaine, en cascade ou en spirale. Bye-bye stderr . Bye-bye le QA ( Quality Assurance ). Bye-bye le bug-tracker . Bye-bye la maintenance .

Inconvénients :

Le code à prouver fait 25 lignes. La preuve de ce code fait 230 lignes. On n'est pas du tout dans les proportions du principe de Pareto En fait on en est plus éloigné qu'il n'y paraît. Même en utilisant CoqIDE, vous constaterez rapidement qu'une ligne de preuve est bien plus difficile à écrire qu'une ligne de programme.

Dans l'absolu on est pas encore dans la perfection puisqu'on peut encore tomber dans l'erreur de la sous-spécification ou dans la galère de la sur-spécification.

À l'heure d'aujourd'hui cette méthodologie "deluxe" ne s'applique pas encore (partiellement et/ou très difficilement) à des logiciels fortement interactifs / parallélisés / multi-utilisateurs.

Pis encore : même si votre fonction possède une définition simple et rigoureuse il n'est pas garanti que vous puissiez prouver telle ou telle propriété .

Message de test de la coloration du code Anubis.

Commençons par un petit dérivateur formel en Anubis :

// a simple formal derivator

// functions from R to R
public type RtoR :
   x,
   cst(Int),
   ~ RtoR,
   RtoR + RtoR,
   RtoR * RtoR,
   sin(RtoR),
   cos(RtoR),
   exp(RtoR).


// automagically generated
public type RtoR_recu($T) :
   recu
   (
      $T x,
      $T cst,
      ($T) -> $T neg,
      ($T,$T) -> $T add,
      (RtoR,$T,RtoR,$T) -> $T mul,
      (RtoR,$T) -> $T sin,
      (RtoR,$T) -> $T cos,
      (RtoR,$T) -> $T exp
   ).

// automagically generated
public define $T recu (RtoR f,RtoR_recu($T) d)
   =
if f is
{
   x then x(d),
   cst(z) then cst(d),
   ~ u    then neg(d)(recu(u,d)),
   u + v  then add(d)(recu(u,d),recu(v,d)),
   u * v  then mul(d)(u,recu(u,d),v,recu(v,d)),
   sin(u) then sin(d)(u,recu(u,d)),
   cos(u) then cos(d)(u,recu(u,d)),
   exp(u) then exp(d)(u,recu(u,d))
}.


public define RtoR deriv (RtoR f)
   =
recu
(
   f,
   recu
   (
      cst(0),
      cst(1),
      (RtoR du) |-> ~ du,
      (RtoR du,RtoR dv) |-> du + dv,
      (RtoR u,RtoR du,RtoR v,RtoR dv) |-> du * v + u * dv,
      (RtoR u,RtoR du) |-> du * cos(u),
      (RtoR u,RtoR du) |-> ~ du * sin(u),
      (RtoR u,RtoR du) |-> du * exp(u)
   )
).

J'attire l'attention du lecteur sur le fait que la fonction deriv n'est   pas directement récursive, nulle part dans son corps elle appelle la fonction  deriv !

En effet, toute la récursion est encapsulée dans le récurseur recu .

Le second exemple, à savoir les ensembles totalement ordonnés, illustre un ensemble plus complet de récurseurs : accu , fold , cata , recu et para .

// totally ordered set of integers
public type Ordered :
   empty,
   ordered(Ordered,Int,Ordered).


// automagically generated
public type Ordered_accu($T) :
   accu
   (
      $T->$T empty,
      (Int,$T) -> $T cons,
   ).

// automagically generated
public define $T accu (Ordered t,$T acc,Ordered_accu($T) d)
   =
if t is
{
   empty then empty(d)(acc),
   ordered(l,i,r) then accu(l,cons(d)(i,accu(r,acc,d)),d)
}.

// automagically generated
public type Ordered_fold($T) :
   fold
   (
      $T empty,
      ($T,Int,$T) -> $T ordered
   ).

// automagically generated
public define $T fold (Ordered s,Ordered_fold($T) d)
   =
if s is
{
   empty then empty(d),
   ordered(l,i,r) then ordered(d)(fold(l,d),i,fold(r,d)) 
}.

// automagically generated
public type Ordered_cata($T) :
   cata
   (
      $T empty,
      (One->$T,Int,One->$T) -> $T ordered
   ).

// automagically generated
public define $T cata (Ordered s,Ordered_cata($T) d,One _)
   =
if s is
{
   empty then empty(d),
   ordered(l,i,r) then ordered(d)
   ((One u)|->cata(l,d,u),i,(One u)|->cata(r,d,u)) 
}.

// automagically generated
public type Ordered_recu($T) :
   recu
   (
      $T empty,
      (Ordered,$T,Int,Ordered,$T) -> $T ordered
   ).

// automagically generated
public define $T recu (Ordered s,Ordered_recu($T) d)
   =
if s is
{
   empty then empty(d),
   ordered(l,i,r) then ordered(d)(l,recu(l,d),i,r,recu(r,d)) 
}.

// automagically generated
public type Ordered_para($T) :
   para
   (
      $T empty,
      (Ordered,One->$T,Int,Ordered,One->$T) -> $T ordered
   ).

// automagically generated
public define $T para (Ordered s,Ordered_para($T) d,One _)
   =
if s is
{
   empty then empty(d),
   ordered(l,i,r) then ordered(d)
   (l,(One u)|->para(l,d,u),i,r,(One u)|->para(r,d,u)) 
}.


public define Word32 cardinal (Ordered s)
   =
fold
(
   s,
   fold
   (
      0,
      (Word32 l,Int _,Word32 r) |-> l + 1 + r
   )
).

   // an alternative cardinal using 'accu' instead of 'fold'
   public define Word32 cardinal (Ordered s)
   =
accu
(
   s,
   0,
   accu
   (
      (Word32 n) |-> n,
      (Int _,Word32 n) |-> n + 1
   )
).

public define Bool member (Ordered s,Int n)
   =
cata
(
   s,
   cata
   (
      false,
      (One->Bool l,Int i,One->Bool r) |->
         if n < i then l(unique)
         else if n > i then r(unique)
         else true  
   ),
   unique
).

public define Bool forall (Ordered s,(Int)->Bool cond)
   =
cata
(
   s,
   cata
   (
      true,
      (One->Bool l,Int i,One->Bool r) |->
            cond(i) & l(unique) & r(unique)  
   ),
   unique
).

public define Ordered insert (Ordered s,Int n)
   =
para
(
   s,
   para
   (
      ordered(empty,n,empty),
      (Ordered l,One->Ordered dl,Int i,Ordered r,One->Ordered dr) |->
         if n < i then ordered(dl(unique),i,r)
         else if n > i then ordered(l,i,dr(unique))
         else s  
   ),
   unique
).

public define Ordered Ordered s + Int n
   =
insert(s,n).

public define Int minimum (Ordered s,Int n)
   =
para
(
   s,
   para
   (
      n,
      (Ordered l,One->Int dl,Int i,Ordered r,One->Int _) |->
         if l is empty then i else dl(unique)
   ),
   unique
).
      
public define Ordered remove_minimum (Ordered sl,Int n,Ordered sr)
   =
if sl is empty then
   sr
else
   ordered
   (
      para
      (
         sl,
         para
         (
            empty,
            (Ordered l,One->Ordered dl,Int i,Ordered r,One->Ordered _) |->
               if l is empty then r
               else ordered(dl(unique),i,r)
         ),
         unique
      ),
      n,
      sr
   ).
   
// concatenation of sa + sb where max(sa) < min(sb)
public define Ordered concat (Ordered sa,Ordered sb)
   =
if sa is empty then
   sb
else if sb is
   {
      empty then sa
      ordered(lb,nb,rb) then
         ordered(sa,minimum(lb,nb),remove_minimum(lb,nb,rb))
   }.
   
public define Ordered remove (Ordered s,Int n)
   =
para
(
   s,
   para
   (
      empty,
      (Ordered l,One->Ordered dl,Int i,Ordered r,One->Ordered dr) |->
         if n < i then ordered(dl(unique),i,r)
         else if n > i then ordered(l,i,dr(unique))
         else concat(l,r)
   ),
   unique
).
      
// returns (sa,b,sb) where max(sa) < n < min(sb) and b = member(s,n)
public define (Ordered,Bool,Ordered) split (Ordered s,Int n)
   =
para
(
   s,
   para
   (
      (empty,false,empty),
      (Ordered l,One->(Ordered,Bool,Ordered) dl,Int i,Ordered r,One->(Ordered,Bool,Ordered) dr) |->
         if n < i then
            (if dl(unique) is (a,b,c) then (a,b,ordered(c,i,r)))
         else if n > i then
            (if dr(unique) is (a,b,c) then (ordered(l,i,a),b,c))
         else (l,true,r)
   ),
   unique
).

public define Ordered filter (Ordered s,Int->Bool cond)
   =
fold
(
   s,
   fold
   (
      empty,
      (Ordered l,Int i,Ordered r) |->
         if cond(i) then ordered(l,i,r) 
         else concat(l,r)
   )
).

public define Ordered union (Ordered sa,Ordered sb)
   =
fold
(
   sa,
   fold
   (
      (Ordered s) |-> s,
      (Ordered->Ordered l,Int i,Ordered->Ordered r) |->
         (Ordered s) |->
         if s is
         {
            empty then empty,
            ordered(sl,si,sr) then
               if split(s,i) is (a,b,c) then ordered(l(a),i,r(c))
         }
   )
)
(sb).

public define Ordered Ordered sa + Ordered sb
   =
union(sa,sb).

public define Ordered intersection (Ordered sa,Ordered sb)
   =
fold
(
   sa,
   fold
   (
      (Ordered s) |-> empty,
      (Ordered->Ordered l,Int i,Ordered->Ordered r) |->
         (Ordered s) |->
         if s is
         {
            empty then empty,
            ordered(sl,si,sr) then
               if split(s,i) is (a,b,c) then
               if b then ordered(l(a),i,r(c))
               else concat(l(a),r(c))
         }
   )
)
(sb).

public define Ordered difference (Ordered sa,Ordered sb)
   =
recu
(
   sa,
   recu
   (
      (Ordered s) |-> empty,
      (Ordered l,Ordered->Ordered dl,Int i,Ordered r,Ordered->Ordered dr) |->
         (Ordered s) |->
         if s is
         {
            empty then ordered(l,i,r),
            ordered(sl,si,sr) then
               if split(s,i) is (a,b,c) then
               if b then concat(dl(a),dr(c))
               else ordered(dl(a),i,dr(c))
         }
   )
)
(sb).

public define Ordered Ordered sa - Ordered sb
   =
difference(sa,sb).

public define Bool subset (Ordered sa,Ordered sb)
   =
fold
(
   sa,
   fold
   (
      (Ordered s) |-> true,
      (Ordered->Bool l,Int i,Ordered->Bool r) |->
         (Ordered s) |->
         if s is
         {
            empty then true,
            ordered(sl,si,sr) then
               if i < si then l(sl) & member(sl,i) & r(s)
               else if i > si then l(s) & member(sr,i) & r(sr)
               else l(sl) & r(sr)
         }
   )
)
(sb).

public define Bool Ordered sa = Ordered sb
   =
subset(sa,sb) & subset(sb,sa).

public define List(Int) to_ordered_list(Ordered t)   
   =
accu
(
   t,
   [],
   accu
   (
      (List(Int) l) |-> l,
      (Int i,List(Int) l) |-> [i . l]
   )
).

Le dernier exemple, à savoir un tax-maximum fusionnable, illustre le récurseur fuse .

// skew max-heap
public type Skew :
   empty,
   skew(Skew,Int,Skew).

// automagically generated   
public type Skew_fuse :
   fuse
   (
   (Skew,Skew,(Skew,Skew)->Skew,(Skew,Skew)->Skew) -> Skew both_not_empty
   ).

// automagically generated
public define Skew fuse(Skew sa,Skew sb,Skew_fuse d)
   =
if sa is {
   empty then sb
   skew(_,_,_) then
      if sb is
      {
         empty then sa
         skew(_,_,_) then both_not_empty(d)
         (sa,sb,(Skew u,Skew v)|->fuse(u,v,d),(Skew u,Skew v)|->fuse(u,v,d))
      }
}.

public define Skew join(Skew s1,Skew s2)   
   =
fuse
(
   s1,
   s2,
   fuse
   (
      (Skew sa,Skew sb,(Skew,Skew)->Skew fa,(Skew,Skew)->Skew fb) |->
         if sa is {empty then alert,skew(la,na,ra) then
         if sb is {empty then alert,skew(lb,nb,rb) then
         if na > nb then skew(la,na,fa(ra,sb)) 
         else skew(fb(sa,lb),nb,rb)}}
   )
).

public define Skew insert(Skew s,Int n)   
   =
join(s,skew(empty,n,empty)).

public define Skew remove(Skew l,Skew r)
   =   
join(l,r).

Je laisse le soin au lecteur de vérifier que les fonctions (assez avancées) de ces deux derniers exemples ne font appel à aucune récursion ni aucune itération.

au talentueux webmaster qui a implémenté la coloration OCaml , Anubis , Coq ainsi que la citation de code dans le texte, sur ma simple demande.  

Parfois, même avec un langage de programmation très fortement typé, certaines erreurs vont passer alors qu'on saurait très bien comment les éviter. Il est possible d'attraper toutes les erreurs, à la compilation, grâce aux types dépendants .

Langages fortement typés

Pour le besoin de notre discussion OCaml fera très bien l'affaire comme représentant des langages fortement typés.

Après avoir lancé la commande en ligne ocaml on entre ce code dans la console :

type interval = Interval of int * int;;

On peut alors créer des intervalles d'entiers comme l'intervalle [1,2] ou l'intervalle [0,9] :

# Interval(1,2);;
- : interval = Interval (1, 2)
# Interval(0,9);;
- : interval = Interval (0, 9)

Cependant on peut tout aussi bien créer des intervalles invalides comme [2,1] :

# Interval(2,1);;
- : interval = Interval (2, 1)

Et ocaml les accepte comme des intervalles valides !

Alors que faire ?

Programmation par contrat

Il existe une solution que l'on appelle la programmation par contrat et qui consiste à cacher l'implémentation du type interval et à lui associer un constructeur make qui vérifie la validité des paramètres fournis.

module Interval :
sig (* interface *)
  type interval
  val  make : int -> int -> interval
end 
  =
struct (* implémentation *)
  type interval =
    Interval of int * int
  let make a b =  (* constructeur *)
    assert(a<b);  (* assertion *)
    Interval(a,b) (* résultat *)
end;;

On créé l'intervalle [1,2] à l'aide de Interval.make 1 2
Par contre si on créé Interval.make 2 1 on a une erreur à l'exécution :

Exception: Assert_failure ("", 11, 4)
(* 11 et 4 indiquent la ligne et la colonne où l'erreur s'est produite *)

Avantage : le programme ne construit pas d'intervalle invalide.

Inconvénient : l'erreur n'est pas détectée à la compilation.

Maintenant discutons cet avantage. Certes le programme ne commet pas l'erreur de construire un intervalle invalide. Néanmoins le programme produit tout de même une erreur qui s'avère tout aussi fatale. Car il est trop tard pour corriger cette erreur. Il n'y a aucune contre-mesure possible. Vous pouvez toujours remplir un rapport d'erreur cela n'empêchera pas le programme de mal s'exécuter tant que l'erreur ne sera pas corrigée par le programmeur. Car c'est lui le responsable de l'erreur, pas l'utilisateur.

La programmation par contrat ressemble plus à un mécanisme de signalement qu'un à mécanisme de prévention. Pour faire de la prévention le seul bon moment c'est à la compilation. À l'exécution on ne peut plus ni agir ni réagir. À l'exécution il est trop tard.

Un jour un programmeur m'a dit

Un jour pas si lointain, un programmeur expérimenté m'a dit :

Citation :

Hé bien justement ...

Types dépendants

Les types dépendants proposent une approche radicalement différente.

Pour le besoin de notre discussion Coq fera très bien l'affaire comme représentant des langages à types dépendants.

Après avoir lancé la commande en ligne coqtop on entre ce code dans la console :

Inductive interval : nat -> nat -> Prop :=
Interval : forall min max, min < max -> interval min max.

À présent essayons de créer l'intervalle [1,2] :

Coq < Eval compute in Interval 1 2.
     = Interval 1 2
     : 1 < 2 -> interval 1 2

Ce que coq nous dit c'est que Interval 1 2 n'est pas un intervalle mais une fonction du type 1 < 2 vers le type interval 1 2 . Quel est donc ce mystérieux type 1 < 2 ? C'est le type d'une preuve que 1 est < que 2 . C'est le type du paramètre manquant pour la construction pleine et entière d'un intervalle [1,2] valide.
Pour fabriquer cette preuve nous chargeons les capacités arithmétiques de base avec Require Import Arith.Arith_base.

À présent nous disposons de lt_n_Sn , c'est une preuve qu'un entier n est plus petit que son successeur S n .
Nous allons utiliser cet argument à bon escient car 2 est le successeur de 1 . Il s'ensuit que lt_n_Sn 1 est de type 1 < 2 .
Nous pouvons maintenant construire l'intervalle [1,2] :

Coq < Eval compute in Interval 1 2 (lt_n_Sn 1).
     = Interval 1 2 (lt_n_Sn 1)
     : interval 1 2

Cette fois le résultat est bien du type interval .   
Toutefois notre situation est encore précaire, par exemple comment construire [0,9] alors que 9 n'est pas le successeur de 0 ?

Hé bien nous disposons de lt_0_Sn qui est une preuve que 0 est < qu'un successeur quelconque. Or 9 est le successeur de 8. Il s'ensuit que lt_0_Sn 8 est de type 0 < 9 .

Coq < Eval compute in Interval 0 9 (lt_0_Sn 8).
     = Interval 0 9 (lt_0_Sn 8)
     : interval 0 9

Il reste un dernier cas, le cas général, où la borne inférieure n'est pas zéro et où la borne supérieure n'est pas son successeur.

Par exemple [1,9]. Cette fois nous allons devoir faire la preuve à la main.

Commençons par l'énoncer comme un fait lt_1_9 :

Coq < Fact lt_1_9 : 1 < 9.             

Coq entre alors en proof mode , il veut bien accepter ce fait si vous lui en fournissez une démonstration. Ce passage de coq en  proof mode est visible dans l'invite : elle passe de Coq < à lt_1_9 < .

Fournissez-lui l'argumentaire repeat constructor.
Puis affirmez Qed. ( Quod Erat Demonstrandum ) pour quitter le proof mode .

Coq < Fact lt_1_9 : 1 < 9.
1 subgoal

  ============================
   1 < 9

lt_1_9 < repeat constructor.
Proof completed.

lt_1_9 < Qed.
repeat constructor.

lt_1_9 is defined

Coq < Eval compute in Interval 1 9 lt_1_9.
     = Interval 1 9 lt_1_9
     : interval 1 9

Petit théorème

Jusqu'à présent on a utilisé que des intervalles à bornes constantes.

Bien entendu les intervalles peuvent aussi avoir des bornes variables.

Pour l'illustrer on va démontrer un tout petit théorème qui dit dire que b est strictement borné par a et c est équivalent à affirmer l'existence de 3 intervalles [ a,b ] [ b,c ] et [ a,c ].

On va appeler ce petit théorème bounded_iff_intervals :

Theorem bounded_iff_intervals :
  forall a b c, a < b < c <-> interval a b /\ interval b c /\ interval a c.

Puis, pour le prouver, on utilise les 5 tactiques qui suivent :

split qui décompose 1 but a ⇔ b en 2 buts a ⇒ b et a ⇐ b , 1 but a < b < c en 2 buts a < b et b < c ou encore 1 but a ⋀ b en 2 buts a et b .

intro H qui transforme la condition d'un but en une hypothèse H .

destruct H qui décompose une hypothèse H .

apply A qui fait valoir un argumentaire A .

exact H qui fait valoir une hypothèse H .

Proof.
  split.
  (* -> *)
  intro H.
  destruct H as (Hab,Hbc).
  split.
  apply (Interval a b Hab).
  split.
  apply (Interval b c Hbc).
  apply (Interval a c (lt_trans a b c Hab Hbc)).
  (* <- *)
  intro H.
  destruct H as (Hab,(Hbc,Hac)).
  split.
  destruct Hab. exact H.
  destruct Hbc. exact H.
Qed.

Commandes

Comme tout logiciel console, coqtop possède son lot de commandes purement utilitaires.

Les commandes en proof mode :

Restart. Reprendre la preuve à son début.

Undo. Défaire la dernière tactique.

Abort All. Abandonner la preuve et quitter le proof mode .

Les commandes top level :

Quit. Quitter coqtop.

Reset Initial. Réinitialiser coqtop.

Check expr . Affiche le type de l'expression.

Sous GTK2+ coqtop est accompagné de l'environnement graphique Coq IDE.

Récapitulatif du code

Inductive interval : nat -> nat -> Prop :=
Interval : forall min max, min < max -> interval min max.

Require Import Arith.Arith_base.

Eval compute in Interval 1 2 (lt_n_Sn 1).
Eval compute in Interval 0 9 (lt_0_Sn 8).

Fact lt_1_9 : 1 < 9.
  repeat constructor.
Qed.

Eval compute in Interval 1 9 lt_1_9.

Theorem bounded_iff_intervals :
  forall a b c, a < b < c <-> interval a b /\ interval b c /\ interval a c.
Proof.
  split.
  (* -> *)
  intro H.
  destruct H as (Hab,Hbc).
  split.
  apply (Interval a b Hab).
  split.
  apply (Interval b c Hbc).
  apply (Interval a c (lt_trans a b c Hab Hbc)).
  (* <- *)
  intro H.
  destruct H as (Hab,(Hbc,Hac)).
  split.
  destruct Hab. exact H.
  destruct Hbc. exact H.
Qed. 

Pour aller plus loin

Le site officiel .

Le manuel de référence .

La librairie standard .

Le calcul des séquents .

Les types dépendants .

Il s'agit de plusieurs paquets que j'ai réalisés pour Racy Puppy Linux 5 .

Racy Puppy Linux 5 est une distribution légère qui fonctionne aussi bien sur mon Compaq Armada M700 (décembre 2000), sur mon Lenovo R60 (septembre 2006) et sur mon eeePC701.

Racy Puppy Live-CD

Le fichier iso . Le patch de mise à jour. Le fichier développeur .

Vous n'êtes pas obligé de graver un CD, si vous avez une clé USB reformattez-là en clé bootable et copier les fichiers dans l'iso à l'aide de 7-zip . Dans tous les cas vous devrez vous assurer que votre BIOS est bien configuré pour booter d'abord sur le CD / USB avant le HD.

Je vous recommande ce thème GTK .

À part pour le clavier, n' essayez pas de franciser votre installation. De toute façon vous ne trouverez pas les traductions pour les utilitaires.

Le dépôt de paquets compatibles.

Par exemple vous devrez installer vous-même les paquets SDL / SDL-image / SDL-mixer / SDL-ttf / SDL-net .

Installer mes paquets

rdtsc

PyGame

SolarWolf wide edition

OCaml + LablGTK2

Coq 8.3pl5 + CoqIDE

Vous avez des questions sur Racy Puppy Linux ?

Demandez et on vous répondra.

Le forum officiel .

Que cache cette affirmation erronée ? Une question bien plus fondamentale.

Ha ha, démontrer que 1 + 1 = 2, en voilà un exercice qu'il va être rapidement expédié

Alors ça va être strictement incompréhensible mais tant pis.

Il existe un entier naturel initial qu'on va appeler O

On a une notation qui désigne l'entier suivant d'un entier n , c'est S n

On s'accorde sur le fait que 1 c'est l'entier suivant O , c'est-à-dire S O

C'est le cas bâtard où Coq est super docile et va faire la démonstration pour nous.

Rassurez-vous ça ne se reproduira pas.

Copie d'écran :

C:> coqtop
Welcome to Coq 8.3pl2 (avril 2011)

Coq < Eval compute in S O + S O.
     = 2
     : nat

On a bien S O + S O = 2 , ce qu'il fallait démonter.

© Ok, je suis pris en flagrant délit d'étalage gerbant de ma culture, car en fait il y avait beaucoup moins pédant :

Coq < Eval compute in 1 + 1.
     = 2
     : nat

Citation :

Aie Aie Aie. Il y aurait donc une démonstration de 1 + 1 ≠ 2.

Ben alors on est bien dans la ( démonstration de ) merde.

Alors les maths détiennent la vérité ?

En voilà une question plus intéressante.

Je vais essayer de rester très borné donc très technique (zéro philosophie, que du matheux psycho-rigidifié).

Je vais considérer (arbitrairement) que la vérité c'est tout ce que je peux démontrer en Coq.

Remarquez: c'est très très limité comme définition. Par exemple Coq ne me dira jamais si le capitaine Dreyfus était coupable de haute trahison ou non.

Mais bon, bon an mal an, si je me satisfais de cette restriction, est-ce qu'au moins je suis certain de n'atteindre que des vérités vraies aussi dures et froides qu'un rail de chemin de fer en Sibérie ?

Coq admet un axiome (une formule qu'on ne peut pas démontrer en Coq) :

⊥ = ∀ q ∈ Ω, q

En français: il est faux que tous les énoncés sont vrais

Conclusion: il vous suffit d'affirmer que cet axiome c'est du pipeau (parce que pas démontré) pour que toute la crédibilité de Coq s'effondre. En quelque sorte le programmeur Coq a la foi que cet axiome est juste . Dans le cas contraire il n'aurait foi dans aucun résultat que lui fournirait Coq.

En résumé: on ne peut pas concevoir que quelque chose est vrai sans avoir foi en quelque chose qui, aussi évident soit-il, n'est pas démontré.

Ce billet a pour but de tester la coloration du code OCaml sur Aerie's Guard. En grandeur nature.

Certains d'entre vous ont expérimenté avec Haskell .

Certains d'entre vous ont expérimenté avec OCaml ou suivent des cours OCaml .

Peut-être que certains d'entre vous suivent des cours Caml-Light .

Quoiqu'il en soit, avant de me lancer dans le grand bain, j'essaye d'abord le petit bassin.

En OCaml un module peut être un module-fonction , c'est-à-dire qu'il peut être paramétrable par un (ou plusieurs) module-argument (s) d'un certain module-type (s).

Donc la 1ière chose que nous allons faire c'est déclarer un module-type .

Il s'agit du type des ensembles totalement ordonnés implémentés comme des arbres binaires de recherche .

Mais on ne précise pas s'ils sont mutables ou immutables (on le fera plus tard).

(* Totally ordered Sets *)
module type OrderedSet =
   sig
      type 'a set =
         'a non_empty_set option
      and 'a non_empty_set =
         private
         {mutable left: 'a set; item: 'a; mutable right: 'a set}
      val empty : 'a set
      val make : 'a set -> 'a -> 'a set -> 'a non_empty_set
      val with_left  : 'a non_empty_set -> 'a set -> 'a non_empty_set
      val with_right : 'a non_empty_set -> 'a set -> 'a non_empty_set
   end

La 2ième chose c'est que l'on veut 2 modules-valeurs de ce module-type .

On veut un module-argument pour les ensembles totalement ordonnés   immutables .

(* Immutable totally ordered Sets *)
module PureOrderedSet : OrderedSet =
   struct
      type 'a set =
         'a non_empty_set option
      and 'a non_empty_set =
         {mutable left: 'a set; item: 'a; mutable right: 'a set}
      let empty = None
      let make l x r = {left=l; item=x; right=r}
      let with_left  s l = {s with left=l}
      let with_right s r = {s with right=r}
   end

On veut un module-argument pour les ensembles totalement ordonnés   mutables .

(* Mutable totally ordered Sets *)
module MutableOrderedSet : OrderedSet =
   struct
      type 'a set =
         'a non_empty_set option
      and 'a non_empty_set =
         {mutable left: 'a set; item: 'a; mutable right: 'a set}
      let empty = None
      let make l x r = {left=l; item=x; right=r}
      let with_left  s l = s.left  <- l; s
      let with_right s r = s.right <- r; s
   end

La 3ième chose c'est que la récursion c'est compliqué. On peut se tromper et si on se trompe il faudra déboguer, soit parce que le calcul ne termine pas ou bien parce que la valeur retournée est incorrecte.

Déboguer c'est du temps perdu pour rien .

Alors on va régler le problème une fois pour toutes en encapsulant la récursion sur les ensembles totalement ordonnés .

(* Recursing upon totally ordered Sets *)
module OrderedSetRecursors(S:OrderedSet) =
   struct
      include S
      (* strict catamorphism *)
      type ('a,'b) fold =
         <empty: 'a; node: 'a -> 'b -> 'a -> 'a>
      let rec fold s (case:('a,'b) fold) =
         match s with
         | None -> case#empty
         | Some n -> case#node (fold n.left case) n.item (fold n.right case)
      (* lazy catamorphism *)
      type ('a,'b) cata =
         <empty: 'a; node: (unit -> 'a) -> 'b -> (unit -> 'a) -> 'a>
      let rec cata s (case:('a,'b) cata) () =
         match s with
         | None -> case#empty
         | Some n -> case#node (cata n.left case) n.item (cata n.right case)
      (* strict paramorphism *)
      type ('a,'b) recu =
         <empty: 'b;
          node: 'a non_empty_set -> 'b -> 'b -> 'b>
      let rec recu s (case:('a,'b) recu) =
         match s with
         | None ->
               case#empty
         | Some n ->
               case#node n (recu n.left case) (recu n.right case)
      (* lazy paramorphism *)
      type ('a,'b) para =
         <empty: 'b;
          node: 'a non_empty_set -> (unit -> 'b) -> (unit -> 'b) -> 'b>
      let rec para s (case:('a,'b) para) () =
         match s with
         | None ->
               case#empty
         | Some n ->
               case#node n (para n.left case) (para n.right case)
      let para_non_empty n (case:('a,'b) para) () =
         case#node n (para n.left case) (para n.right case)
   end

On veut une dernière chose :

Pouvoir créer des ensembles totalement ordonnés mutables ou immutables

Les équiper de toutes les opérations ensemblistes, à savoir e ∈ S, A ∪ B, A ∩ B, A ⊃ B, A - B, A = B, ∀ e ∈ S on a P(e), {e ∈ S, P(e)}

Que toutes ces opérations soient performantes, qu'elles utilisent le fait que les ensembles sont ordonnées. Par exemple il est hors de question d'ajouter les éléments de A un-par-un à l'ensemble B pour calculer A ∪ B. 

(* Build a concrete totally ordered Set *)
module MakeSet(S:OrderedSet)
   =
   struct
      (* general *)
      include
         OrderedSetRecursors(S)
      let cardinal s =
         fold s (
            object
               method empty = 0
               method node l _ r = l + 1 + r
            end )
      let for_all cond s =
         cata s (
            object
               method empty = true
               method node l y r =
                  l() && cond y && r()
            end ) ()
      (* binary tree set *)
      let member x s =
         cata s (
            object
               method empty = false
               method node l y r =
                  if x < y then l()
                  else if x > y then r()
                  else true
            end ) ()
      let insert x s =
         para s (
            object
               method empty =
                  make None x None
               method node n l r =
                  let y = n.item in
                  if x < y then with_left n (Some (l()))
                  else if x > y then with_left n (Some (r()))
                  else n
            end ) ()
      let minimum s =
         para_non_empty s (
            object
               method empty = s
               method node n l r =
                  if n.left = empty then n
                  else l()
            end ) ()
      let remove_minimum s =
         para_non_empty s (
            object
               method empty = empty
               method node n l r =
                  if n.left = empty then n.right
                  else Some (with_left n (l()))
            end ) ()
      (* concatenation of sa + sb where max(sa) < min(sb) *)            
      let concat sa sb =
         if sa = empty then sb else
         match sb with
         | None -> sa
         | Some n ->
            let m = minimum n
            and r = remove_minimum n
            in Some (with_right (with_left m sa) r)
      let remove x s =
         para s (
            object
               method empty =
                  empty
               method node n l r =
                  let y = n.item in
                  if x < y then Some (with_left n (l()))
                  else if x > y then Some (with_right n (r()))
                  else concat n.left n.right
            end ) ()
      let split x s =
         para s (
            object
               method empty =
                  empty,false,empty
               method node n l r =
                  let y = n.item in
                  if x < y then
                     let a,b,c = l() in
                     a,b,Some (with_left n c)
                  else if x > y then
                     let a,b,c = r() in
                     Some (with_right n a),b,c
                  else
                     n.left,true,n.right
            end ) ()
      let filter cond s =
         recu s (
            object
               method empty =
                  empty
               method node n l r =
                  if cond n.item then
                     Some (with_right (with_left n l) r)
                  else
                     concat l r
            end )
      let union sa sb =
         recu sa (
            object
               method empty s =
                  s
               method node m l r s =
                  Some (
                  match s with
                  | None -> m
                  | Some n ->
                     let a,b,c = split m.item s in
                     with_right (with_left m (l a)) (r c))
            end ) sb
      let intersection sa sb =
         recu sa (
            object
               method empty s =
                  empty
               method node m l r s =
                  match s with
                  | None -> empty
                  | Some n ->
                     let a,b,c = split m.item s in
                     if b then
                        Some (with_right (with_left m (l a)) (r c))
                     else
                        concat (l a) (r c)
            end ) sb
      (* sa - sb *)
      let difference sa sb =
         recu sa (
            object
               method empty s =
                  empty
               method node m l r s =
                  match s with
                  | None ->
                     Some m
                  | Some n ->
                     let a,b,c = split m.item s in
                     if b then
                        concat (l a) (r c)
                     else
                        Some (with_right (with_left m (l a)) (r c))
            end ) sb
      let subset sa sb =
         recu sa (
            object
               method empty s =
                  true
               method node m l r s =
                  match s with
                  | None -> false
                  | Some n ->
                     if m.item < n.item then
                        (l n.left) && member m.item n.left && (r s)
                     else if m.item > n.item then
                        (l s) && member m.item n.right && (r n.right)
                     else
                        (l n.left) && (r n.right)
            end ) sb
      let equal sa sb =
         subset sa sb && subset sb sa
   end

Désormais, pour créer un module ensemble totalement ordonné immutable :

module PSet = MakeSet(PureOrderedSet)

Désormais, pour créer un module ensemble totalement ordonné mutable :

module MSet = MakeSet(MutableOrderedSet)

Les fonctions ont toutes le type approprié. Par exemple il est impossible de retirer un élément d'un ensemble vide parce que la fonction remove est du type :

val remove : 'a -> 'a non_empty_set -> 'a set

Réciproquement, lorsque l'on insère un élément dans un ensemble quelconque, on obtient forcément un ensemble non vide   :

val insert : 'a -> 'a set -> 'a non_empty_set

Ce billet est un brouillon largement inspiré par le Lightning-talk de Benjamin Lorteau (de 30:50 à 35:26). Comme j'ai moi aussi mon lot de projets poubelles, j'ai fouillé ma corbeille afin de vous déterrer quelques pépites de projets merdiques. La vie n'étant qu'un espoir perpétuellement renouvelé j'espère mettre à jour ce billet avec de futurs nouveaux plantages. 

Je ne suis pas un mathématicien, je ne suis pas un logicien, je ne suis qu'un pathétique technicien. Comme tous les autres techniciens j'ai largement appris sur le tas. Comme tous les autres techniciens j'ai mon lot de ratages épiques.

Depuis l'explosion de la bulle internet et le succès d'Harry Potter (qui prouve que la magie est amusante, au contraire de la technologie qui est terriblement ennuyeuse) on sent comme qui dirait une baisse des vocations informatiques. Donc selon toute vraisemblance ce billet ne vous intéresse pas mais ça ne fait rien puisque je le rédige pour moi d'abord.

Petite ontologie de mes plus beaux plantages

Tant va la cruche à l'eau

C'est le fameux "j'ai oublié la conception".

On essaye de compenser avec de la motivation mais ça ne marche pas. Parce que la motivation ne remplace pas l'expérience et la compétence.

Le Frankenstein raté

 sur une suggestion de Ragnarork . Cette fois-ci j'ai écouté les injonctions des ouvrages de conception. Découper le projet en plusieurs composants indépendants communicants avec des protocoles biens définis. Chaque sortie d'un composant est une partie de l'entrée du composant suivant et le tout s'assemble comme un charme. Le hic : le dataflow ne convient pas du tout, de l'information capitale s'est perdue en cours de route parce qu'un composant en amont n'en avait "pas besoin". Du coup en aval c'est la galère pour récupérer ce qui a été "oublié" sans démanteler toute l'encapsulation.

Le lièvre et la tortue

C'est typiquement le projet de compilateur ou de système d'exploitation. Qui part de zéro, avec une équipe d'une personne, et donc qui n'arrivera jamais à rattraper les solutions plus matures déjà bien entrenchées qui ont déjà saturé le marché. De toute façon même si le projet arrivait à maturité, pendant ce temps là la valeur ajoutée se serait évadée vers un autre marché. 

Le One Shot

Le petit projet réalisé en 15 jours , simple comme du Tetris, mais qui n'a jamais de succès ni de descendance.

Le Titanic

Une merveille de beauté conceptuelle et d'élégance technique.

Moi c'était le projet OCaml-Idaho . Jusqu'à ce qu'on me demande de faire des "tests unitaires".

La solution à la recherche d'un problème

Typiquement j'ai résolu un problème algorithmique ment réputé comme étant "difficile". Il ne reste plus qu'à trouver un débouché. J'ai dans les mains une solution abstraite, mais pour quel problème concret ?

Le Phoenix

C'est le projet académique par excellence . Il n'y aura jamais aucun débouché avant le 23ième siècle. Nonobstant l'attrait intellectuel est tel qu'on y revient forcément ou qu'on y repense à chaque fois qu'on s'ennuie.

La grenouille qui voulait devenir aussi grosse que le bœuf

Une sorte de retenue m'a empêché d'avouer celle-ci. Genre : je n'y ai pas touché, ailleurs peut être mais ici non. Et pourtant si, moi aussi je me suis fait avoir. Alors, vous allez être déçus, même pas un petit projet d'IA avec des canons lasers géants pour conquérir le monde ( vous l'avez échappé belle). Par contre une idée m'a effleuré un moment : le fait est que (selon mes estimations) il ne faut pas plus d'environ 300 briques distinctes pour créer un thème lego espace. De plus la conquête spatiale ça n'existe pas donc si c'est pas réaliste on s'en fiche un peu puisque ça ne ressemble à rien de connu. Par conséquent on peut faire n'importe quoi pourvu que ça tienne debout. D'où mon idée génialement naïve :

• cataloguer les volumes et les points d'assemblage pour environ 300 pièces lego "space"

• prototyper un algorithme top-down qui, à partir d'un langage de description, décomposerait un modèle en un assemblage de building-patterns

• prototyper un algorithme bottom-up qui arrangerait un tout solide et cohérent

L'erreur à la base de ce genre de projet c'est de croire qu'on l'on peut concevoir quelque chose d'intelligent sur une base 100% grammaticale. Alors qu'au contraire, tout ce qui est intelligent requière une quantité énorme de connaissances et de créativité.