kantien a écrit 1198 commentaires

Effectivement, tu as bien compris comment fonctionnaient ces tableaux persistants. En interne il y a des effets de bords sur un véritables tableaux à la mode impératif. Cela vient en partie de la conception de la persistance des deux auteurs de l'ouvrage sus-mentionné :

Cela ne signifie pas pour autant qu'une structure de données persistantes soit nécessairement codée sans aucun effet de bord. La bonne définition de persistant est :

persistant = observationnellement immuable

et non purement applicatif (au sens de l'absence d'effet de bord). On a seulement l'implication dans un sens :

purement applicatif => persistant

La réciproque est fausse, à savoir qu'il existe des structures de données persistantes faisant usage d'effets de bord. Cet ouvrage contient plusieurs exemples de telles structures.

Dans cet exemple, on utilise les effets de bords pour avoir des opérations de lecture et d'écriture en temps constant tant qu'on utilise pas la persistance (sinon, il faut prendre en compte le temps de se rebaser sur le bon tableau via reroot en appliquant les patchs).

Pour ce qui est du fonctionnement des shared_ptr, en lisant ton explication, il me semble bien que c'est ce que j'en avais déjà compris. La discussion avec freem sur le sujet commence à ce commentaire et il pensait qu'en programmation fonctionnelle on privilégiait la copie alors que l'on favorise le partage de la mémoire (là où je voyais un rapport avec les shared_ptr, qui apportent aussi une gestion automatique de la mémoire à la manière des GC). Je prenais cet exemple de représentation en mémoire de deux listes qui partagent leur queue :

let l = [1; 2; 3];;
(* la représentation mémoire de celle-ci est une chaîne :

| 1 | -|-->| 2 | -|-->| 3 | -|-->| |

*)

let l1 = 4 :: l and l2 = 5 :: l;;
(* ce qui en mémoire donne :

| 4 | \|
       \
        -->| 1 | -|-->| 2 | -|-->| 3 | -|-->| |
       /
| 5 | /|
*)

De ce que je comprends de ta gestion mémoire pour tes graphes, c'est que tu évites les effets de bords et tu gères tes pointeurs comme le feraient les compilateurs Haskell et OCaml pour les types inductifs. Ai-je tort ? La liste l qui est partagée entre l1 et l2 n'est-elle pas proche d'un shared_ptr ?

Dans le cas de mes tableaux persistants :

type 'a t = 'a data ref
and 'a data = |Arr of 'a array 
              |Diff of int * 'a * 'a t

ce n'est pas avec le type paramétrique 'a t des tableaux que je crois voir une analogie avec les shared_ptr, mais avec le type 'a data. Pour ce qui du type 'a t, c'est une simple référence comme on en trouve en C++. Suis-je à côté de la plaque ?

Pour la note historique, d'après les auteurs du livre, cette structure de tableaux persistants serait due à Henry Baker qui l'utilisait pour représenter efficacement les environnements dans des clôtures LISP. (Henry G. Baker. Shallow binding makes functionnal array fast).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

En moyenne chaque copie du graph coûte O(log(n)) en mémoire, ce qui est négligeable et permet de conserver une grande quantité d'étape d'undo/redo. On peut même les sauvegarder avec le fichier. C'est gratuit à faire avec des structures persistantes, modulo qu'en C++ je dois me balader avec des shared_ptr de partout, mais cela fonctionne.

Ton exemple me rappelle un commentaire que j'avais écrit sur une dépêche C++. Freem se demandait à quoi pouvait bien servir les shared_ptr, et de ce que j'en avais compris je lui avais soumis comme idée une structure de tableaux persistants. J'avais bien compris le fonctionnement des shared_ptr ? Le principe consisté à conserver toutes les opérations de transformations effectuées sur une structure modifiables à la manière d'un gestionnaire de version. C'est ce que tu fais aussi avec tes graphes ? D'ailleurs l'exemple des tableaux persistants est tiré du livre de mon commentaire précédent.

Le bouquin est bien fait, toute la seconde partie est consacrée aux structures de données : modifiables ou persistantes avec analyse de la complexité. Une structure que je trouve particulièrement élégante est le zipper de Gérard Huet pour se déplacer facilement à l'intérieur d'un type inductif (listes, arbres…). Le zipper sur les listes a pour type :

type 'a zipper = { left : 'a list ; right : 'a list }

c'est l'exemple des Queues que Okasaki¹ étudie dans la troisième partie de sa thèse. Gérard Huet en propose une version plus détaillée dans la présentation de The Zen Computational Linguistics Toolkit, voir la troisième partie : Top-down structures vs bottom-up structures.

Pour ce qui est du coût mémoire, qui reste acceptable, même avec des structures impératives on peut difficilement faire sans dès que l'on veut pouvoir annuler des opérations. Prenons un exemple idiot et sans grand intérêt : un pointeur sur un int. Si une opération de modification consiste à lui ajouter un int quelconque, il faudra bien conserver cette valeur quelque part au cas où on voudrait annuler l'addition avec une soustraction : la valeur finale contenue dans le pointeur ne contenant aucune information sur la quantité qui lui a été ajoutée. Autant encapsuler toute cette mécanique dans une structure persistante : cela simplifie son usage et le risque de bugs dans le code client de la structure.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai voulu cependant introduire un peu le concept et fournir une bonne ressource car je trouve que on néglige trop souvent les structures de donnée dans l'apprentissage de l'informatique, et on néglige encore plus les structures non mutables qui offrent des propriétés très intéressantes.

C'est dommage que les structures persistantes soient négligées : la persistance, c'est le bien ! :-)

Dans leur ouvrage Apprendre à programmer avec OCaml, Sylvain Cochon et Jean-Christophe Filliâtre consacrent un paragraphe sur l'utilité et les avantages de la persistance :

Les intérêts pratiques de la persistance sont multiples. De manière immédiate, on comprend qu'elle facilite la lecture du code et sa correction. En effet, on peut alors raisonner sur les valeurs manipulées par le programme en termes « mathématiques », puisqu'elles sont immuables, de manière équationnelle et sans même se soucier de l'ordre d'évaluation. Ainsi est-il facile de se persuader de la correction de la fonction append précédente une fois qu'on a énoncé ce qu'elle est censé faire (i.e append l1 l2 construit la liste formée des éléments de l1 suivis des éléments de l2) : une simple récurrence sur la structure de l1 suffit. Avec des listes modifiables en place et une fonction append allant modifier le dernier pointeur de l1 pour le faire pointer sur l2, l'argument de correction est nettement plus difficile. L'exemple est encore plus flagrant avec le renversement d'une liste. La correction d'un programme n'est pas un aspect négligeable et doit toujours l'emporter sur son efficacité : qui se soucie en effet d'un programme rapide mais incorrect ?

Le code de la fonction append en question est :

let rec append l1 l2 = match l1 with
  | [] -> l2
  | x :: xs -> x :: append xs l2

et effectivement un simple raisonnement par récurrence sur la structure de l1 suffit à prouver sa correction. On peut même facilement formaliser un tel résultat dans un assistant de preuve comme Coq pour certifier le code. Là où avec des structures impératives se sera une toute autre paire de manches.

Ils continuent en prenant un exemple de problématiques de backtracking : parcourir un labyrinthe pour trouver une sortie. La position dans le labyrinthe est modélise par un état e dans un type de donnés persistants. On suppose qu'on a une fonction is_exit qui prend un état et renvoie un booléen pour savoir si on est à une sortie. On a également une fonction possible_moves qui renvoie la liste de tous les déplacements possibles à partir d'un état donné et une fonction move pour effectuer un tel déplacement. La recherche d'une sortie s'écrit alors trivialement à l'aide de deux fonctions mutuellement récursives :

let rec find e =
  is_exit e || try_move (possible_moves e)
and try_move e = function
  | [] -> false
  | d :: r -> find (move d e) || try_move e r

Avec des structures impératives il faudrait, après chaque déplacement, annuler celui-ci avant d'en faire un autre : ce genre de code est un vrai nid à bugs.

let rec find () =
  is_exit () || try_move (possible_moves ())
and try_move = function
  | [] -> false
  | d :: r -> (move d; find ()) || (undo_move d; try_move r)

ici il faudrait s'assurer que la fonction undo_move annule bien correctement le déplacement d effectué via l'appel à move d. Non seulement cela complique le code, mais en plus cela ouvre la porte à des erreurs potentielles.

Dans le même ordre d'idées, on peut prendre le cas de la mise à jour d'une base de données. Avec un structure de donnés modifiables, on aurait un code du style :

try
 (* effectuer l'opération de mise à jour *)
with e ->
 (* rétablir la base dans un état cohérent *)
 (* traiter ensuite l'erreur *)

Avec un structure persistante, c'est plus simple et moins propice aux bugs.

(* on stocke la base dans une référence *)
let bd = ref base_initale

try
  bd := (* opération de mise à jour de !bd *)
with e ->
  (* traitement de l'erreur *)

Ici la mise à jour construit une nouvelle base qui est ensuite affectée à l'ancienne via une opération atomique qui ne peut échouer. Si il y a une erreur lors de l'opération de mise à jour alors l'ancienne base n'a pas été modifiée et il n'est pas nécessaire de la remettre dans un état cohérent avant de traiter l'erreur proprement dite.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il me semble que Octachron voulait utiliser les notations bra et ket de la physique quantique. En , cela devrait ressembler à quelque chose comme :

$\sum_{k} \bra{\psi{(k)}} \ket{\psi{(k)}} =  \mathbb{1}$

soit :

Cela étant, j'aimerais bien voir un extrait du .XCompose de Octachron. Le parser $\LaTeX$ de linuxfr semble avoir des problèmes (hier la plupart de mes formules en ligne n'était pas traitées et j'ai du écrire N au lieu de , et ici le deuxième LaTeX de mon texte n'est pas traité), et même quand on utilise cela crée un décalage stylistique avec la police du reste du texte.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai hésité avant de te répondre pour plusieurs raisons. Tout d'abord il y a des questions d'ordre historique sur lesquelles je ne sais pas tout, ensuite je craignais de faire encore une réponse à rallonge assez rebutante, et enfin je n'ai pas compris ta dernière question sur les littéraux. Je vais essayer de répondre comme je le peux, sans faire trop long.

Sur le plan historique, les paradoxes de Burali-Forti et Russell dans la théorie des ensembles de Cantor-Frege ont donné naissance à l'axiomatique de Zermelo-Fraenkel. C'est plutôt dans ce cadre axiomatique (avec quelques variantes) que l'on pratique de nos jours la théorie des ensembles.

De leur côté, Russel et Withehead écrivirent les Principia Mathematica pour tenter de fonder l'édifice mathématique sur la seule logique. C'est leur notation utilisée pour les fonctions propositionnelles qui inspira Church pour son lambda-calcul. Ils notaient la proposition f appliquée à un objet singulier a : fa, et la fonction qui à un objet a indéterminé faisait correspondre la valeur de vérité fa ainsi : fâ. Ils avaient aussi une notation du type : âfa. Comme l'éditeur de Church ne pouvait pas mettre d'accents circonflexes sur toutes les lettres, ils ont remplacer l'accent circonflexe par un lambda majuscule qui est ensuite devenu un lambda minuscule. Et l'on note depuis la fonction x -> f x ainsi : .

La théorie des catégories fut introduite originellement dans le cadre de la topologie algébrique. Elle avait pour but d'étudier les relations entres structures mathématiques qui préservent certaines propriétés des dites structures : les morphismes. Ce n'est qu'ensuite qu'un lien a été fait avec la logique et la sémantique des langages de programmation.

En ce qui concerne le lien entre typage et logique, cela concerne la théorie de la démonstration. Il y a un bon ouvrage de vulgarisation sur la logique : La logique ou l'art de raisonner qui expose simplement les différents point de vue sur la logique. Le plan de l'ouvrage est en quatre parties :

• Formaliser : des objets aux énoncés
• Interpréter : des énoncés aux objets
• Prouver : des énoncés aux énoncés
• Axiomatiser : des objets aux ensembles

La notion de vérité relève de la seconde partie, celle sur l'interprétation, et fait intervenir la notion de modèles dont s'occupe la théorie des modèles. Pour prendre un exemple simple. Si on prend un langage qui dispose d'une fonction binaire (disons +) et de deux constantes I et II. Alors si on interprète l'énoncé II + II = I dans l'ensemble N des entiers naturels, munis de son addition et en associant 1 à I et II à 2, alors cet énoncé sera faux. En revanche si on fait de même dans le groupe Z/3Z alors il sera vrai. Dans cette branche de la logique, on développe la notion de modèle d'une théorie et celle de conséquence sémantique : si un énoncé est vrai dans tout modèle d'une théorie alors on dit qu'il est une conséquence sémantique de la théorie. Dans l'ouvrage sus-cité, ils écrivent une des choses les plus importante à comprendre : « […] quand il existe une structure naturelle pour interpréter les énoncés (par exemple N dans le cas des énoncés arithmétiques), il est nécessaire d'envisager toutes les autres, même celles qui semblent n'avoir aucun rapport intuitif avec les énoncés. C'est en faisant varier les interprétations possibles, et en constatant que certaines notions ne sont pas sensibles à ces variations, que l'on touche à l'essence de la logique ». (Tu pourras penser, par exemple, à mon journal sur l'interprétation avec la méthode tagless final où je faisais plusieurs interprétations pour un même terme syntaxique).

De son côté la théorie de la démonstration avec ses formalismes comme la déduction naturelle ou le calcul des séquents de Gentzen, ou les systèmes à la Hilbert, ne s'occupe pas du rapport que les énoncés entretiennent avec des objets (modèles) mais seulement du rapport que les jugements (ou énoncés) entretiennent entre eux. Son cheval de bataille, c'est l'inférence : à quelles conditions peut-on inférer une conclusion donnée de prémisses données ? On obtient alors la notion de conséquence déductive : un énoncé est une conséquence déductive d'une théorie si on peut l'établir comme conclusion d'une preuve dont les prémisses sont toutes des axiomes de la théorie. Les deux questions qui se posent alors sont :

• si un énoncé est conséquence déductive est-il aussi conséquence sémantique ?
• réciproquement, s'il est conséquence sémantique est-il conséquence déductive ?

La première a trait à la cohérence du système (on ne peut pas trouver tout et n'importe quoi avec) et la seconde a trait à sa complétude (il peut prouver tout ce qui est prouvable) qui renvoie à un théorème fameux de Gödel (moins connus que son théorème d'incomplétude, mais tout aussi important).

C'est cette deuxième branche de la logique qui est en lien avec le typage des langages de programmations, elle donne lieu à la correspondance de Curry-Howard ou correspondance preuve-programme : le type d'un programme est une énoncé dont le programme est une preuve. Ce qui apporte de la sécurité dans l'écriture de code, comme le montre le chapitre sur les systèmes de type du livre de Benjamin C. Pierce : well typed programm never gets stuck, autrement dit un programme bien typé ne se retrouvera jamais dans un état indéfini où aucune transition n'est possible. Puis, selon la richesse d'expressivité du système de type, il permet d'exprimer au mieux la sémantique du code : il limite les interprétations possibles, via la complétude.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je comprends l'appréhension qu'a pu susciter ma réponse, mais dans un premier temps je n'ai pas vu comment faire plus court. Il me fallait poser les termes du problèmes (d'où l'exposition des notions de genres et d'espèces), expliquer comme lire les règles de déduction à la Gentzen et illustrer par des exemples un cas où une classe héritant d'une autre n'en était pourtant pas un sous-type.

Je vais essayer de condenser le cœur de l'argumentaire (le nervus probandi, comme on dit).

Oublions le Gamma et le code OCaml.

Laissons de côté le Gamma, qui n'est nullement essentiel pour comprendre le problème, et le code d'illustration en OCaml. L'essentiel tient déjà dans ce qui était simple à comprendre :

Je pense (du moins je l'espère) que ce que je viens d'exposer doit être facilement compréhensible.

Oui ;)

Ensuite on va considérer deux classes dans une syntaxe de mon invention (c'est proche de mon exemple final).

classe A = {
  attr1 : T1 ;
  meth : A -> A
}

classe B herite A = {
  attr2 : T2 ;
  meth : B -> B
}

Voilà deux classes A et B, où la deuxième dérive de la première, ajoute un attribut et surcharge leur méthode commune meth. Pour que B soit un sous-type de A, il faudrait que les types de leurs composants communs soient des sous-types les uns des autres. Autrement dit, il faudrait que T1 <: T1 (types de attr1) et que B -> B <: A -> A (types de meth).

Tout type étant un sous-type de lui-même, on a bien T1 <: T1, mais la deuxième condition ne peut être vérifiée. En voici la raison :

• les fonctions qui acceptent des animaux en entrée, acceptent des hommes en entrée
• les fonctions qui retournent des chats, retournent des félins.

Or, sur le plan de la subordination des genres et des espèces, on a : homme <: animal et chat <: félin. Donc en condensant les deux principes précédents et en faisant abstraction des concepts impliqués, on aboutit à la règle de déduction suivante :

T1 <: S1    S2 <: T2       homme <: animal    chat <: félin
---------------------      --------------------------------
S1 -> S2 <: T1 -> T2       animal -> chat <: homme -> félin

Ainsi pour pouvoir prouver la condition B -> B <: A -> A, il faudrait satisfaire les deux prémisses de la règle ci-dessus, à savoir : A <: B et B <: A. Ce qui reviendrait à dire que les deux classes sont identiques, ce qui n'est évidemment pas le cas.

Revenons à Gamma et au code OCaml.

Ce n'est vraiment pas un point très important à comprendre, le calcul des séquents est surtout un outil qui sert aux personnes étudiant les preuves (les théoriciens de la démonstration); comme le dit la page wikipédia : « le calcul des séquents doit se penser comme un formalisme pour raisonner sur les preuves formelles plutôt que pour rédiger des preuves formelles ».

La lettre grecque dans les notations à la Gentzen sert à désigner l'ensemble des hypothèses utilisées pour prouver la thèse qui se trouve à droite du symbole . Prenons le problème de géométrie suivant :

Soit ABC un triangle isocèle en A et appelons O le milieu du segment BC. Montrer que la droite (BC) est perpendiculaire à la droite (OA).

Ici le contexte Gamma c'est l'énoncé du problème (auquel il faudra rajouter quelques axiomes de la géométrie euclidienne), et à droite du symbole de thèse on aura le résultat à prouver.

Pour tes questions sur le code OCaml, chimrod t'a en partie répondu. En ce qui concerne le syntaxe let ... in, c'est ainsi que l'on définit des variables locales en OCaml. Exemple dans la boucle interactive :

let i = 1 and j = 2 in i + j;;
- : int = 3

i;;
Error: Unbound value i

Les variables i et j n'existent qu'au sein de l'expression i + j, elles sont locales et n'existent plus une fois cette dernière évaluée. Cela étant la boucle me répond que la somme i + j est de type int et vaut 3. Ce qui en notation de Gentzen revient à dire que le type checker a pu prouver ce séquent :

i : int , j : int , (+) : int -> int -> int |- i + j : int

Vois-tu ce qu'est le contexte Gamma dans cet exemple ?

Pour terminer ma réponse, la règle que tu cites en fin de ton message :

Gamma |- t : S   S <: T
-----------------------
   Gamma |- t : T

n'était pas celle utilisée dans mon exemple. Mon exemple avait pour but de répondre à ta question qu'est-ce que Gamma ? (à savoir un contexte, un environnement), et ensuite je réécrivais cette règle pour pouvoir la traduire en français. C'est néanmoins cette règle qui est utilisée dans un bout de code qui se situe un peu plus loin :

let op' = new point2d 1. 2.;;
val op' : point2d = <obj>

move_x 0.1 (op' :> point);;
- : point = <obj>

Dans ce contexte on sait que op' : point2d, de plus on a bien point2d <: point, et donc le type checker peut conclure qu'on a le droit de considérer op' comme étant de type point.

Reste-t-il des points obscurs dans mon exposé ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Si tu acceptes de m'aider (et probablement en aider d'autres) à mieux comprendre ton exposé, je t'en remercie d'avance.

Effectivement, je me rends compte que ce que j'ai écrit doit paraître abscons pour qui n'est pas habitué à ce genre de questions. Je veux bien essayer de clarifier la chose en étant plus didactique, et compléter ainsi la réponse de Def.

On va partir de la logique et de sa notion de concept, la POO cherchant à procéder à une classification des concepts en genres et espèces comme les biologistes le font pour le règne animal.

Toutes les connaissances c'est-à-dire toutes les représentations rapportées consciemment à un objet sont ou bien des intuitions, ou bien des concepts. L'intuition est une représentation singulière, le concept est une représentation générale ou réfléchie.

La connaissance par concept s'appelle la pensée.

Remarques. 1) Le concept est opposé à l'intuition, car c'est une représentation générale ou une représentation de ce qui est commun à plusieurs objets, donc une représentation en tant qu'elle peut être contenue en différents objets.

Kant, Logique.

On peut voir les types comme signifiant des concepts et les termes d'un langage comme des choses rentrant sous un concept. Par exemple, avec le concept de « verre » on peut dire, en en montrant un, « ceci est un verre ». Dans une telle situation, les logiciens disent que l'on subsume la perception que l'on a (l'intuition) sous le concept de « verrre ». Il en est de même lorsque l'on dit que Socrate est un homme. En théorie des types, un tel jugement est appelé un jugement de typage et on l'écrirait Socrate : homme. Comme dans l'exemple suivant :

let i = 1;;
val i : int = 1

Je définit une variable i, et la boucle REPL OCaml me répond : la valeur i est un int.

Jusque là, c'est ce que tu avais bien compris de la notation t : T. Ensuite dans le pensée, nous hiérarchisons nos concepts en genre et espèce : les hommes sont des mammifères, les mammifères sont des animaux, les animaux sont des êtres vivants…

Les concepts sont dits supérieurs s'ils ont sous eux d'autres concepts, qui par rapport à eux sont dit concepts inférieurs.

Remarque. Les concepts n'étant appelé supérieurs et inférieurs que de façon relative, un seul et même concept peut donc, sous différents rapports, être en même temps supérieur et inférieur.

Le concept supérieur dans son rapport avec son concept inférieur s'appelle genre; le concept inférieur dans son rapport à son concept supérieur s'appelle espèce.

Tout comme les concepts inférieurs et supérieurs, ceux de genre et d'espèce se distinguent dans la subordination logique non par leur nature, mais par leur rapport respectif.

Kant, ibid.

Ainsi, par exemple, un triangle est une espèce de polygone et le concept de polygone constitue le genre dans le rapport de subordination logique entres les deux concepts.

Je pense (du moins je l'espère) que ce que je viens d'exposer doit être facilement compréhensible. Les langages orientés objets prétendent, via leur système de classe et d'héritage, réaliser une telle hiérarchie des concepts en genre et espèce. Sauf que, dans les faits, c'est logiquement faux dans la plupart des langages donc faux.

Ce rapport respectif entre concepts, le rapport entre genre et espèce, est justement ce que l'on appelle la relation de sous-typage que l'on note S <: T pour dire que S est un sous-type de T. En revanche, une sous-classe (si l'on entend par là une classe qui hérite d'une autre) n'est pas nécessairement un sous-type. Comme l'a dit Def dans sa réponse, l'héritage c'est proche d'un simple #include, ça évite le copier-coller : c'est pour cela que je parlais de notion syntaxique.

Venons-en maintenant aux règles qui déterminent la relation de sous-typage. Les deux premières que j'ai données sont issues de la syllogistique aristotélicienne : la première figure. Leur notation est empruntée à la formulation par Gentzen du calcul des séquents. On y sépare verticalement les prémisses et la conclusion de la règle de déduction. Ainsi la règle :

S <: U   U <: T
---------------
    S <: T

se lit : sous les prémisses que S est un sous-type de U et que U est un sous-type de T, on conclue que S est un sous-type de T. C'est la figure Barbara des syllogismes aristotéliciens.

Pour la première règle, dans la prémisse Gamma |- t : S, le signe |- (qui est un T couché) se lit « thèse de ». Il signifie que, dans le contexte des hypothèses que constitue Gamma, on peut prouver la thèse t : S (que le terme t est de type S). D'un point de vue programmation, on peut voir Gamma comme un contexte, une portée lexicale (scope). Ainsi dans l'exemple suivant :

let i = 1;;
val i : int = 1

let j =
 let i = 2. in
 i +. 3.;;
val j : float = 5.

Dans le contexte global, la REPL infère que i : int. En revanche, dans le contexte de définition de j, elle inférera que i : float. Ainsi la règle :

Gamma |- t : S   S <: T
-----------------------
   Gamma |- t : T

peut se lire : dans un contexte où on peut prouver que le terme t est de type S et que S est un sous-type de T, on peut alors prouver, dans le même contexte, que t est de type T.

Voyons un peu maintenant ce qui se passe avec des objets (au sens du paradigme orienté objet), l'héritage et la relation de sous-typage. Les objets peuvent être vus comme des enregistrement extensibles (extension obtenue via l'héritage).

Prenons par exemple ces deux types OCaml :

type pt2d = { x : float; y : float };;
type pt3d = { x : float; y : float; z : float };;

let p = {x = 1.; y = 3.};;
val p : pt2d = {x = 1.; y = 3.}
let p' = {x = 1.; y = 3.; z = 4.};;
val p' : pt3d = {x = 1.; y = 3.; z = 4.}

Bien que le type des pt3d contiennent les champs x et y, on ne peut pas, en OCaml, utiliser p' là où le système attend un objet de type pt2d.

let move dx (p : pt2d ) = {p with x = p.x +. dx};;
val move : float -> pt2d -> pt2d = <fun>

move 0.1 (p' :> pt2d);;
Error: Type pt3d is not a subtype of pt2d

Les enregistrements OCaml ne possèdent pas cette relation de sous-typage <:. Pour cela, il faut passer par les enregistrements extensibles que sont les objets.

let op = object method x = 1. method y = 3. end;;
val op : < x : float; y : float > = <obj>
let op' = object method x = 1. method y = 3. method z = 4. end;;
val op' : < x : float; y : float; z : float > = <obj>

type obj_pt2D = <x : float; y : float>;;
let move dx (p : obj_pt2D) : obj_pt2D = object method x = p#x +.dx method y = p#y end;;
val move : float -> obj_pt2D -> obj_pt2D = <fun>

move 0.1 op;;
- : obj_pt2D = <obj>

move 0.1 (op' :> obj_pt2D);;
- : obj_pt2D = <obj>

On peut noter au passage que la coercition entre types doit être explicite (il n'y a pas de cast implicite en OCaml) et qu'elle est notée comme la « symétrique » de la relation de sous-typage : :>.

Les règles qui dictent la relation de sous-typages entre enregistrements sont données dans la section records du chapitre de l'ouvrage de Benjamin C. Pierce. En gros, pour être un sous-type, il faut avoir au moins les mêmes champs (ici x et y) et que les types de ces champs soient des sous-types des champs correspondant (ici ce sont les même, à savoir float).

C'est ici qu'il peut y avoir des soucis entre héritage et sous-typage. Pour l'instant nos méthodes n'étaient pas des fonctions. Lorsque l'on a une classe qui possèdent des fonctions comme méthodes, au moment de l'héritage il faut contrôler le sous-typage entre ces fonctions. D'où la règle de sous-typage entre fonctions et les problématiques de contravariance et de convariance.

Commençons avec deux classes simples à la mode fonctionnel : des points à une ou deux dimensions avec des méthodes pour les déplacer.

class point x_init = object
val x = x_init
method get_x = x
method move_x dx = {< x = x +. dx >}
end;;
class point : 
  float ->
  object('a)
   val x : float
    method get_x : float
    method move_x : float -> 'a
  end

class point2d x_init y_init = object
inherit point x_init
val y = y_init
method get_y = y
method move_y dy = {< y = y +. dy >}
end;;
class point2d : 
  float ->
  float ->
  object ('a)
    val x : float
    val y : float
    method get_x : float
    method get_y : float
    method move_x : float -> 'a
    method move_y : float -> 'a
  end

Ici les méthodes move_x (ou move_y) font référence au types de l'objet ('a) : elle retourne un objet de même type que l'objet sur lesquelles on les utilise. Comme ce type apparaît en position covariante (sortie), l'héritage est aussi un sous-typage.

let move_x dx (p : point) = p#move_x dx;;
val move_x : float -> point -> point = <fun>

let op = new point 1.;;
val op : point = <obj>

let op' = new point2d 1. 2.;;
val op' : point2d = <obj>

move_x 0.1 op;;
- : point = <obj>

move_x 0.1 (op' :> point);;
- : point = <obj>

Maintenant, au lieu de considérer des points, considérons des vecteurs à une ou deux dimensions disposant d'une méthode pour les ajouter entre eux (opérateur binaire).

class virtual vect = object ( _ : 'a)
method virtual get_x : float
method virtual add : 'a -> 'a
end;;
class virtual vect :
  object('a)
    method virtual add : 'a -> 'a 
    method virtual get_x : float
  end

Ici la méthode add n'ont seulement renvoie un objet du type de la classe (position covariante) mais en prend également un en entrée (position contravariante). Ici l'héritage ne sera pas identique au sous-typage.

class vect1d x_init = object
inherit vect
val x = x_init
method get_x = x
method add v = {< x = x +. v#get_x >}
end;;
class vect1d :
  float -> 
  object ('a)
    val x : float
    method add : 'a -> 'a
    method get_x : float
  end

class vect2d x_init y_init = object
inherit vect1d x_init
val y = y_init
method get_y = y
method add v = {< x = x +. v#get_x ; y = y +. v#get_y >}
end;;
class vect2d : 
  float -> 
  float ->
  object ('a)
    val x : float
    val y : float
    method add : 'a -> 'a
    method get_x : float
    method get_y : float
  end

((new vect2d 1. 2.) :> vect1d);;
Error:
  Type vect2d = < add : vect2d -> vect2d; get_x : float;
  get_y : float >  is not a subtype of
  vect1d = < add : vect1d -> vect1d; get_x : float >
  Type vect1d = < add : vect1d -> vect1d; get_x : float > is
  not a subtype of vect2d = < add : vect2d -> vect2d; get_x : float; get_y : float >

Pour que le type vect2d soit un sous-type du type vect1d, il faudrait que sa méthode add : vect2d -> vect2d soit un sous-type de la méthode add : vect1d -> vect1d du type vect1d. Ce qui, d'après la règle de sous-typage des fonctions, nécessiterait que vect2d soit à la fois un sous-type et un sur-type de vetc1d, ce qui est impossible.

Pour rappel, la règle en question était :

T1 <: S1    S2 <: T2
---------------------
S1 -> S2 <: T1 -> T2

autrement dit, avec les prémisses que T1 est un sous-type de S1 et que S2 est un sous-type de T2, on en conclue que le type des fonctions de S1 vers S2 (noté S1 -> S2) est un sous-type de celui des fonctions de T1 vers T2. La règle se comprend intuitivement ainsi : si j'ai une fonction qui prend un S1, je peux bien lui donner également un T1 étant donné que T1 <: S1 (si j'ai besoin d'un animal, prendre un homme convient aussi); et si je renvoie un S2 alors a fortiori je renvoie aussi un T2 (si je renvoie un chat, je renvoie aussi un félin).

Dans le cas de la méthode add de la classe vect2d, on voit bien le problème : pour fonctionner elle a besoin d'un attribut y sur son entrée, ce que ne peut lui fournir un objet de la classe vect1d.

J'espère avoir été plus clair sur la distinction entre héritage et sous-typage. Si ce n'est pas le cas, et que tu as encore des questions, n'hésite pas. Pour plus d'information, voir aussi la page du manuel OCaml sur les objets.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

la sémantique objet est totalement différente entre Java et OCaml par exemple, car en OCaml, une classe héritant d'un autre n'est pas forcément son sous type.

Ce qui est conforme à la nature des choses : l'héritage est une notion syntaxique et le sous-typage une notion sémantique.

Par exemple, lorsque l'on écrit le syllogisme suivant:

• tous les animaux sont mortels
• or les hommes sont des animaux
• donc les hommes sont mortels

le concept « homme » est un sous-type du concept « animal » (ce qu'exprime la mineure). Malheureusement, les adeptes de la POO présentent souvent les concept de classes et d'héritage ainsi, ce qui est une erreur.

Oleg Kyseliov a illustré, sur sa page Subtyping, Subclassing, and Trouble with OOP, le genre de bugs difficiles à détecter que cette confusion peut engendrer. Son exemple est en C++ (mais ça marche aussi en Java, Python…) et traite des ensembles (Set) comme sous-classe des multi-ensembles (Bag).

Il faut prendre soin, dans la relation de sous-typage, des problématiques de covariance et de contravariance. Les règles de la relation de sous-typage sont exposées dans ce chapitre de Software Foundations de Benjamin C. Pierce. La première règle, par exemple, dite règle de subsomption :

Gamma |- t : S   S <: T
-----------------------
   Gamma |- t : T

est celle que l'on utilise dans le syllogisme :

• tous le hommes sont mortels (homme <: mortel)
• or Socrate est un homme (Socrate : homme)
• donc Socrate est mortel (Socrate : mortel).

La règle suivante, la règle structurelle, est celle qui est utilisée dans mon premier syllogisme avec les types animal, mortel et homme.

S <: U   U <: T
---------------
    S <: T

Les problèmes de covariance et de contravariance arrivent lorsqu'il faut sous-typer des fonctions (méthodes dans les objets), dont la règle est :

T1 <: S1    S2 <: T2
---------------------
S1 -> S2 <: T1 -> T2

autrement dit la flèche inverse la relation de sous-typage sur ses domaines (T1 <: S1), elle y est contravariante; tandis qu'elle la conserve sur ses codomaines (S2 <: T2), elle y est covariante.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ce commentaire est là pour indiquer la solution (workaround) retenue par l'équipe en charge du développement du compilateur OCaml afin de maintenir des optimisations du niveau -O2 de GCC, sans pour autant risquer de soulever les bugs des CPU. Elle pourra intéresser des développeurs de logiciels C qui ne veulent pas prendre ce risque.

Elle est expliquée dans cette PR sur github et consiste à passer l'option -fno-tree-vrp à GCC. Il semblerait que ce soit cette passe d'optimisation qui génère le code assembleur « coupable », d'après les investigations réalisées par les gens de chez Ahref et rapportées dans leur article Skylake bug: a detective story.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'en ai trouvé d'autres :

• un bug dans un de leur logiciel ses (leurs ?) logiciels
• le client offre un accès à leur sa (leur ?) machine

mais là je ne sais si je dois mettre le possessif au singulier ou au pluriel. C'est un peu comme la discussion sur la construction un des : l'adjectif renvoie à un sujet singulier (le client) mais celui-ci désigne une personne morale derrière laquelle se trouve une multitude de personnes physiques. Alors, singulier ou pluriel ? Les deux sont acceptables ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

L'idée serait ici de passer non pas sur l'hyperplan mais sur l'hypersphère, je n'ai pas bien compris comment on se place sur une hypersphère. Visiblement c'est via la notion de "normal deviate" mais j'ai encore un peu de mal à bien saisir le principe. C'est ce qui remplace l'opération de gradient, mais sa construction me semble encore obscure.

C'est comme se déplacer sur une courbe de même latitude sur la surface terrestre (un cercle sur une sphère). Cela doit convoquer les opérateurs de la géométrie différentielle qui permet de faire du calcul différentiel dans des espaces non euclidiens (comme une sphère) à la manière de la relativité générale de tonton Albert.

Sinon jolie dépêche ! :-) Je n'en ai pas encore approfondi la lecture, mais comme tu abordes tant Planton et sa caverne, que Kant et son épistémologie dans ton introduction, je me sens dans l'obligation de répondre. Cependant, je différerai mon commentaire sur le sujet (j'ai beaucoup à dire dessus) et espère pouvoir le faire d'ici la fin de semaine. En tout cas, je suis heureux de voir qu'un laboratoire de physique s'y intéresse (j'avais quelque peu perdu espoir sur la question ;-).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Avec Intel on a même un grand exemple avec le bogue de la division du Pentium.

Oui, c'est le premier exemple qui me soit venu à l'esprit quand j'ai lu l'article de Xavier Leroy. Je ne sais pas si tu l'as lu, mais il a tout de suite envisagé un problème matériel et le cas de l'hyperthreading lui a été inspiré par un autre problème sur l'arithémtique vectorielle et les instructions AVX pour la famille Skylake.

Cela n'empêche pas que le code de ces choses là devraient être libres, mais on a un exemple que la solution de fondre le firmware sous forme de transistors directement n'est pas idéale.

Effectivement, ce qui montre aussi toute l'utilité des projets comme ceux que développent vejmarie sur le matériel Open Source. Cet exemple montre aussi l'intérêt des échanges publiques. Le premier bug fut identifié et résolu en privé, et Xavier Leroy ne savait pas comment contacter Intel en précisant « Intel doesn't have a public issue tracker like the rest of us » dans son article. Le second qui avait la même cause fut discuté publiquement sur le tracker OCaml et quelques mois plus tard il y a un correctif, même s'il reste fermé, grâce à l'intervention de Mark Shinwell.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il y en a d'autres :

• les derniers porcesseurs processeurs Intel
• ce qui ce se comprend, ce dernier utilisant Clang

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Mais pourquoi ? C’est quoi le problème avec Jack ? C’est quoi le problème avec ces outils qui font très bien leur boulot ?

Le problème est peut-être que ceux qui parlent de Jack ne savent pas ce qu'il fait et à quoi il sert ? Je dirais que si une personne prend peur devant un tel objet physique :

alors Jack n'est pas fait pour elle et elle peut passer son chemin.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Merci pour les liens.

De rien.

Grew est intéressant, mais ça ne peut pas servir tel quel: c’est du Ocaml et rien n’est apparemment prévu pour Windows.

C'est pas tant le logiciel Grew en lui-même que je voulais signaler, mais sa méthode d'analyse grammaticale. Sinon du code OCaml ça se compile sous Windows, ou mieux, ça se transcompile en javascript via js_of_ocaml (c'est comme ça que l'on peut tester OCaml dans son navigateur avec la boucle REPL compilée en javascript).

Ce que fait Grew c'est de la réécriture de graphe (en) pour, par exemple, produire une analyse en grammaire de dépendance (en) dans la lignée des travaux de Lucien Tesnière. En réalité c'est un moteur qui prend en entrée un système de réécriture (une grammaire pour le français dans notre cas) comme Hunspell prend un dictionnaire. L'intérêt étant de pouvoir développer sa grammaire à part de façon modulaire.

Je fais par exemple :

$ echo "le chat mange la souris" | MElt -L -t > chat.melt
$ grew -grs ~/src/POStoSSQ/grs/surf_synt_main.grs -seq full -gr chat.melt

pour analyser la phrase le chat mange la souris, la grammaire du français se trouvant dans le fichier surf_synt_main.grs.

Il y a d'autres formalismes comme les TAG, ou grammaire d'arbres adjoints, qui sont très répandues et qui utilisent des métagrammaires pour leur mise au point à la manière du logiciel FRMG.

Toutes ces grammaires fonctionnent comme ton DAG (graphe orienté acyclique) pour le lexique, sauf qu'elles reconnaissent des langages légèrement sensibles au contexte (et non seulement des langages réguliers). Il y a des cycles dans le graphe, et l'opération d'adjonction dans les TAG permet de formaliser certains phénomènes récursifs des langues naturelles, comme dans la phrase Quel cadeau crois-tu que Jean offre à Marie ? :

J’imagine que Grew part du principe qu’une phrase est (à peu près) correctement formée et que les erreurs potentielles sont des raretés. En cas d’aberration, ça envoie juste une analyse brute des mots, mais on ne peut pas le lui reprocher, ce n’est pas ce pour quoi ça a été fait.

Non, Grew (comme FRMG) produit une analyse partielle si la phrase n'est pas reconnue par la grammaire. À l'inverse, l'ancien logiciel leopar fonctionnait comme un dictionnaire : l'entrée était reconnue ou non par la grammaire, dans ce dernier cas elle était tout simplement rejetée. Néanmoins, l'un comme l'autre ne fonctionne pas comme un correcteur orthographique (ou plutôt grammaticale) et ne propose pas une solution pour rendre l'entrée conforme à la grammaire. Il faudrait rajouter, pour cela, un autre traitement en aval du leur pour essayer de comprendre quelle peut être la source du problème (traitement qui est propre à un correcteur grammaticale comme l'est grammalecte), en tirant partie du travail d'analyse de la phase précédente.

Pour ma part, j'ai un faible pour le formalisme des MCG (grammaires minimalistes catégorielles) parce qu'il s'inscrit, de manière large, dans le cadre de la correspondance de Curry-Howard (ou correspondance preuve-programme) à la base du lambda-calcul statiquement typé, c'est-à-dire la programmation fonctionnelle avec typage statique comme Haskell, OCaml ou Coq. Et dans ce formalisme, on voit clairement la correspondance entre analyse grammaticale et typage statique avec inférence de type comme je l'ai déjà souligné précédemment. :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai un peu joué avec Grew et son fonctionnement n'est pas identique à celui de leur ancien outil leopar et ne s'inscrit pas de la même manière dans la chaîne de traitement.

Il se situe en aval de l'étiqueteur morphosyntaxique et calcul l'arbre de dépendances selon un technique de réécriture de graphes (d'où son nom Grew pour Graph Rewriting) décrite dans cet article (en anglais) permettant l'écriture d'une grammaire de façon modulaire et d'effectuer des analyses partielles. L'étiquetage des mots est, quant à lui, effectué par le logiciel MElt. C'est ce dernier qui arrive à gérer les mots absents du lexiques (comme « moldus » dans mon exemple précédent) et, étant écrit en perl et python, ce dernier pourrait peut être t'intéresser.

À la base de MElt, il y a le lexique lefff (lexique des formes fléchies du français) développé initialement au sein de l'ancienne équipe ALPAGE (Analyse Linguistique Profonde À Grande Échelle). Il est disponible sous deux formes :

• lexique intensionnel, qui décrit pour chaque entrée lexicale son lemme (forme canonique + table de flexion) et des informations de syntaxe profonde (cadre de sous-catégorisation en fonctions syntaxiques profondes et réalisations possibles + constructions/reformulations/diathèses admissibles)
• lexique extensionnel, compilé automatiquement à partir du lexique intensionnel ; ce processus de génération comporte une phase de flexion, en fonction de la classe morphologique associée à l’entrée intensionnelle, puis une phase de construction de la structure syntaxique associée à chacune des formes fléchie obtenues (les informations syntaxiques variant d’une forme à une autre, en particulier pour les formes infinitives et participiales, et en fonction de chaque construction associée à l'entrée).

et fût constitué par des méthodes tant automatisées que manuelles. Son auteur principal, Benoît Sagot, le présente dans cet article (en anglais). À la lecture de l'article, j'ai appris l'existence d'un phénomène bien connu des linguistes et qu'ils nomment sandhi d'après les grammairiens indiens. C'est ce phénomène qui est à l'origine de la discussion que nous avons eue sur la subdivision des verbes du premier groupe :

• ajout du « e » entre le « g » et le « a » ou le « o », ou transformation du « c » en « ç » ;
• accentuation du « e » ou doublement des consonnes « l » et « t » ;
• transformation du « y » en « i ».

C'est l'occasion de rectifier une légère erreur que j'avais commise alors : le doublement de la consonne correspond à un accent grave et non aigu (le suffixe -ette se prononce comme -ète et non -éte). Ce genre de changement dans la graphie renvoie à des raisons phonétiques appelées euphonie et ne sont pas propres, en français, à la conjugaison des verbes. Dans la version intentionnelle du lefff, on trouve par exemple ces règles :

<letterclass name="aou" letters="a à â ä o ô ö u û ü ù"/>
<letterclass name="ou" letters="o ô ö u û ü ù"/>
<sandhi source="g_[:aou:]" target="ge_[:aou:]"/>
<sandhi source="[:ou:]y_es$" target="[:ou:]i_es$"/>
<sandhi source="et_2e$" target="ett_e$"/>

Pour installer l'outil MElt, il faut suivre les instructions sur sa page mais le traditionnel ./configure ; make ; make install ne fonctionnera pas de suite. Le script ./configure génère une cible pour la documentation dans le dossier /doc mais il manque un fichier latex pour le faire fonctionner; il faudra simplement éditer le fichier make du répertoire en question et ensuite tout fonctionne. Il faudra de plus installer les bibliothèques Perl pour la gestion de sqlite et la bibliothèque numpy pour Python. Puis dans un shell :

echo "les moldus et les cracmols" | MElt -L -t
les/DET/le moldus/NC/*moldu et/CC/et les/DET/le cracmols/NC/*cracmol

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Bonjour Olivier,

Ces derniers jours, suite à ta dépêche, j'ai fait quelques recherches pour savoir ce qui se faisait dans le monde du TALN, et je suis tombé sur le site de l'équipe sémagramme. C'est un laboratoire affilié INRIA-LORIA qui travaille sur des modèles, méthodes et outils pour l'analyse sémantique des énoncés et discours en langue naturelle, le tout basé sur la logique.

Parmi leurs ressources, on trouve le site deep-sequoia qui contient un riche corpus de phrases en français avec annotations grammaticales sous licence LGPL-LR. Cela pourra sans doute t'être utile pour tester ton correcteur et repérer les bonnes formations qui lui échappent.

Ils ont aussi développé un outil Grew (testable en ligne) d'analyse syntaxique de phrase en français. Sa sortie ressemble à ceci :

Comme grammalecte il semble vouloir enfermer la république, mais il gère les mots absents du lexique et identifie leur catégorie grammaticale.

Sur le wiki dédié à leur ancien outil léopar, ils expliquent le principe à la base de la construction de leur arbre d'analyse. Cela te donnera peut être des idées.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Liens intéressants mais aucun ne fournit, ou plutôt n'explique, le principe qui va régir la bonne formation grammaticale des phrases avec ce type de construction.

Tentons la chose ! L'article « de » prend deux groupes (ou syntagmes) nominaux et forme un groupe nominal; exemples : la sœur de ma mère, un de ceux j'ai vu, le premier de la liste… On peut le voir comme un opérateur binaire infixe, et le groupe nominal produit hérite du genre et du nombre du paramètre de gauche; féminin singulier, masculin singulier et masculin singulier pour les exemples précédents.

Viens maintenant la question de l'analyse d'une telle construction lorsqu'apparaît une subordonnée relative : à qui se réfère le pronom relatif « qui » ou « que » ? Il peut aussi bien se référer au groupe complet « x de y » que faire partie de la construction du groupe nominal qui constitue l'argument de droite de l'article « de ».

Prenons, en exemple, la phrase du journal qui à soulever la question : « un des points auxquels je n’avais pas beaucoup réfléchi et qui m’a le plus surpris »; elle est grammaticalement erronée, mais peut donner naissance à celle-ci en supprimant le « et » :

• un des (points auxquels je n’avais pas beaucoup réfléchi) qui m’a le plus surpris

Ici, le groupe « points auxquels je n'avais pas beaucoup réfléchi » est bien formé (le verbe ne s'accorde pas, le syntagme « points » étant un COI). Ce groupe étant au pluriel l'article est mis à sa forme plurielle ( « de » devient « des »). Ensuite le sujet de l'auxiliaire avoir est le pronom relatif « qui » qui se réfère au syntagme nominal complet formé par la construction « un des … » : il est donc masculin singulier, et l'auxiliaire est bien conjugué.

En revanche, la proposition de lecteur devrait se décomposer ainsi :

• un des (points auxquels je n’avais pas beaucoup réfléchis et qui m’ont le plus surpris)

ici, la subordonnée relative fait partie de la construction du syntagme nominal qui joue le rôle du second argument de l'article « de ». Le pronom relatif « qui » se réfère aux « points », le sujet est donc pluriel et l'auxiliaire est bien conjugué.

Voilà les raisons pour lesquelles l'accord dépendra de ce que veut exprimer l'auteur. Selon le contexte dans lequel est employé la construction, il y a deux sujets possibles dont le choix dépend de la pensée à exprimer. D'où les trois constructions possibles suivantes :

• un des (points auxquels je n’avais pas beaucoup réfléchis et qui m’ont le plus surpris)
• un des (points auxquels je n’avais pas beaucoup réfléchi) qui m’a le plus surpris
• (un des points) auquel je n’avais pas beaucoup réfléchi et qui m’a le plus surpris

il semblerait que ce soit la dernière que voulait exprimer Olivier.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

On n’est déjà pas d’accord ça. Les radicaux du 1ᵉʳ sont souvent modifiés. Sinon je n’aurais pas eu besoin d’autant de règles pour gérer ça.

C'est effectivement là que nous ne sommes pas d'accord : il ne s'agit pas là pour moi de ce que j'entendais par altération du radical.

Dans tes exemples, on trouve d'abord les verbes en « -ger » et « -cer » qui n'altère pas le radical mais rajoute un « e » entre le « g » et le « a » ou le « o » de la terminaison pour conserver le phonème « ge » dans le premier cas, et transforme le « c » en « ç » pour conserver le phonème « ce » dans le second. Ces deux situations relèvent de l'orthographe lexicale et de la correspondance grapho-phonique de ces deux consonnes selon la voyelle qui les suit (cf p.14 du programme de primaire).

Pour d'autres cas, le radical n'est pas altéré : sa voyelle « e » subie différentes accentuations, mais c'est toujours la même voyelle et le même radical. Ce qu'il y a, avec l'accentuation de cette voyelle, c'est qu'elle peut se signifier aussi bien par un accent graphique que par un doublement de la consonne qui la suit dans le cas de l'accent aigu et des consonnes « l » et « t » (on écrit, par exemple, « elle » et non « éle »). Là ce sont, à nouveau, certaines règles étranges de la correspondance graphico-phonique qui sont à l'origine de cette subdivison du premier groupe.

Enfin il reste le cas des verbes en « -oyer » pour lesquelles le recours au « y » dans la graphie intervient pour la liaison phonétique entre les phonèmes « oi » et « er » (comme pour « noyais ») mais qui est substitué par un « i » lorsque la liaison n'est pas nécessaire (comme pour « noierait »). Connaissant peu l'histoire de notre langue, je ne saurai dire d'où vient un tel usage du « y ».

En revanche, le verbe « aller » subit une totale altération du radical. Otachron en a donné la raison : il emprunte trois radicaux distincts issus de trois verbes latins différents (WTF !). Pour le cas des verbes « renvoyer » et « envoyer », je n'ai aucune idée de la raison de la disparition du phonème « oi » dans son radical à certain temps contrairement au verbe comme « noyer ».

On pourrait toujours rajouter un quatrième groupe des verbes tordus, seuls de leur espèce, plutôt que de les ranger dans le troisième groupe, mais le seul rapport que je leur vois avec les autres verbes du premier groupe reste leur terminaison en « -er » et non les principes de leur conjugaison.

Bref, comme je l’ai dit, en grammaire, l’unanimité n’a pas encore été trouvée.

Il y a peu de chance qu'elle le soit un jour. Quand notre langue sera morte ?

Pour le reste, ce n'est pas d'une grande importance (quoique ?); j'aurais pas mal de choses à dire mais je n'ai pas le temps d'écrire un long commentaire. Pour faire court, l'analyse lexical et les informations du dictionnaire permettent de passer de la phrase :

• le chat mange la souris

à une situation du genre :

• (le : art. m. sg.) (chat : nm. sg.) (mange : vb. tr.) (la : art. f. sg.) (souris : nf. sg.)

dans laquelle chaque mot reçoit son type grammatical (ou ses types possibles en cas d'homonymie), et ensuite les règles de la grammaire française permettent de montrer que la construction syntaxique est grammaticalement correcte et a le type d'une phrase. C'est dans cette phase qu'interviennent les problématiques algorithmiques liées à l'inférence et à la vérification de type.

Traiter cette phase à la manière des compilateurs permettrait, par exemple, dans le cas d'une telle phrase :

• les moldus et les cracmols ne maîtrisent pas l'art de la legilimancie

d'inférer que les mots « moldu », « cracmol » et « legilimancie » doivent être des noms communs quand bien même ils ne se trouveraient pas dans le dictionnaire (raisonnement que tout lecteur de cette phrase, connaissant la grammaire française, fait de lui-même). Ce qui pourrait offrir la possibilité de suggérer l'ajout de ces mots avec ces catégories au dictionnaire, quand l'ajout de mot sera possible. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Fil intéressant sur la classification des verbes, en particulier celle du verbe « aller ». Le sujet dont on parle dans ce journal étant la grammaire, j'ai choisi de répondre à ce commentaire en particulier car j'y ai détecté une erreur fréquente qui passe inaperçue auprès de grammalecte. Je commencerai donc ma réponse par une petite digression, bien que je te rejoigne entièrement sur la classification de « aller » dans le troisième groupe (ainsi que sur celle de « envoyer » dans le troisième également).

Voici la faute :

N'oublie pas que le français reste une langue avec un historique important dont pour uniformiser les usages on a conçu l'Académie Française pour rationaliser cet historique.

un mauvais usage du pronom relatif « dont », pourtant bien utilisé dans la phrase qui suit :

ce qui peut faire rire étant donné la quantité d'exceptions dont bénéficient notre langue

même si ici le verbe est mal conjugué, son sujet étant « notre langue » qui est singulier. ;-)

Le pronom relatif « dont » introduit un groupe nominal objet, normalement introduit par la préposition « de », lorsque celui est placé avant le groupe verbal. La deuxième utilisation (celle qui est correcte) correspondant à : « notre langue bénéficie de quantité d'exceptions ». Une telle construction est souvent utilisée pour élaborer un groupe nominal sujet afin d'éviter l'usage d'une subordonnée relative (introduite par « qui »). Exemples :

• notre langue bénéficie de quantité d'exceptions qui peuvent faire rire.
• la quantité d'exceptions dont bénéficie notre langue peuvent faire rire.

Revenons maintenant à la classification du verbe « aller ». Olivier a écrit dans un de ces commentaires :

Pour ma part, je juge discutable la classification, et quand ça sort de nulle part sans explication crédible, je me demande qui, quoi, pourquoi, s’il y a une meilleure explication que « c’est comme ça ».

et pourtant tu lui as donné le principe déterminant la classification dans le premier groupe : verbe dont l'infinitif est en « er » dont (:-P¹) le radical ne subit pas d'altération lors de sa conjugaison. On peut toujours vouloir choisir un autre principe de classification (chacun est libre de choisir les principes qu'il veut après tout), mais qualifier celui-ci d'explication qui sort de nulle part est un peu fort de café, me semble-t-il.

En ce qui concerne le verbe « aller », son radical subit une transformation dans plusieurs temps ce qui le disqualifie (selon ce principe) pour appartenir au premier groupe. Exemples : je vais, tu vas, il va, ils vont, j'irai, tu iras, il ira, nous irons, vous irez, ils iront…

Les soient disantes irrégularités du premier groupe ne concernent jamais une altération du radical, mais des adaptations de la terminaison pour des raisons de sonorité comme le « e » dans « nous mangeons » ou le « ç » dans « nous lançons ».

Pour ce qui est du verbe « renvoyer », la stricte parenté de conjugaison avec le verbe « voir » (en dehors du participe passé dérivé en conformité avec sa terminaison en « er ») me semble être un bon principe pour le classifier dans le troisième groupe. Prendre, par exemple, son comportement au futur (où le radical est altéré) :

• j’enverrai
• tu enverras
• il enverra
• nous enverrons
• vous enverrez
• ils enverront

et le comparer à celui d'un verbe du premier groupe avec la même terminaison comme « louvoyer » :

• je louvoierai
• tu louvoieras
• il louvoiera
• nous louvoierons
• vous louvoierez
• ils louvoieront

Pour répondre au principe d'Olivier qui invoquait le nombre de règles dont se sert grammalecte entre le premier et le troisième groupe. D'une manière générale, comme je l'avais déjà dit dans ton autre dépêche, je considère que les problèmes algorithmiques liés à la correction grammaticale sont analogues à ceux que l'on rencontre dans la vérification et l'inférence de types dans l'écriture de compilateur de langages de programmation. Je salue la performance de ton logiciel ainsi que ton travail mais, si les expressions régulières sont fort utiles pour de l'analyse lexicale, le choix de construire un moteur entier d'analyse grammaticale autour des expressions régulières est déjà, en soi, une option discutable². Mais si, de plus, tu te fondes sur un tel choix pour justifier ta classification des verbes alors là je ne peux absolument plus te suivre; et il y a peu de chance que tu arrives à faire des émules chez les grammairiens (ce que je ne suis pas, mais je n'en ai jamais lu un qui classifiait « aller » dans le premier groupe).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Le problème de cette solution, c’est que tu multiplies le temps d’examen de chaque mot par le nombre de dictionnaires que tu as. Pour chaque mot, tu lances la recherche à partir de zéro dans un graphe de mots. Très coûteux en ressources donc.

J'ai pensé aux problèmes de complexité après avoir posté mon message, mais n'y a-t-il pas non plus moyen de le résoudre en utilisant autre chose qu'une liste de dictionnaires ? Ton dictionnaire a apparemment un format binaire indexable de ton propre cru qui exige une phase de compilation. Dans ton moteur tu le charges en mémoire ou tu vas lire le dictionnaire sur le disque ? Peux-tu envisager une fusion-compilation de plusieurs dictionnaires (à la volée en fonction d'une option) avant d'entamer l'analyse proprement dite ?

Je pose ces questions car, au-delà des néologismes et autres bizarreries, se joue la possibilité pour l'utilisateur de personnaliser son dictionnaire en fonction de ses besoins.

L’autre problème est culturel. Vouloir refuser « les néologismes et autres bizarreries », c’est une chose; se mettre d’accord sur la place du curseur sur ces questions en est une autre. Les gens sont très divisés sur l’acceptable et l’inacceptable… Il suffit de voir tout le barouf sur “ognon”… “Ognon”, c’est un sacrilège. “Fake news”, non. Ou l’inverse. Ça dépend des personnes.

Je prends un exemple. De nos jours, presque tout le monde ou presque écrit “décrédibiliser”… Pourtant, il existait un mot plus court que tout le monde semble avoir oublié en quelques années: “discréditer”. À mes yeux, “décrédibiliser” est néologisme superflu. Mais ça a fini par rentrer dans les dictionnaires. Ai-je eu tort de céder?

D'où mes questions sur la possibilité d'intégrer la gestion de plusieurs dictionnaires, et les adaptations nécessaires à apporter au code. Pour l'instant, tu te retrouves à devoir arbitrer un consensus pour tous les utilisateurs, là où avec la gestion de dictionnaires multiples chacun arbitrera pour lui-même car, comme tu le dis, sur ces questions « ça dépend des personnes ».

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Malheureusement, les dictionnaires n’acceptent que 2 possibilités: un mot est présent ou absent. Bref, c’est compliqué, et même si c’était faisable, ce serait un travail de titan.

Je ne connais pas l'architecture interne de ton moteur, mais pour la présence des mots ne peux tu pas avoir deux dictionnaires (disons D1 et D2) puis, suivant une option, tu testes la présence du mot dans D1 ou bien dans un des dico de la liste [D1; D2] ? Cela demanderait trop de changement de code que le test de présence se fasse sur une liste plutôt qu'un dico fixe donné ?

Sinon, merci pour ton logiciel que je l'utilise régulièrement via l'extension de firefox. Je vais voir pour participer à la campagne.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Mais une question que j'avais posée est : qu'est-ce qui peut pousser un développeur à utiliser cette fonction en dehors des bornes 0 .. 63 ?

A cette question je pourrais répondre bêtement en disant que je veux que la fonction suivante calcule le quotient de n par 2^a pour toutes les valeurs de la plage des types de ses arguments.

function quo_power2 (n, a: natural) return natural;

Ça m'intriguait cette histoire, et je n'arrivais pas à admettre qu'un informaticien comme Xavier Leroy ait pu faire un tel choix sans une bonne raison. Pour faire de l'arithmétique entière, il y a une bibliothèque dédiée (écrite en collaboration) : Zarith qui ne fait pas partie de la distribution officielle ni de la bibliothèque standard (elle est volontairement minimaliste).

#require "zarith";;
#install_printer Z.pp_print;;

Z.shift_right Z.one 64;;
- : Z.t = 0

Z.(shift_right (shift_left one 65) 1);;
- : Z.t = 18446744073709551616

Z.(shift_right (shift_left one 64) 128);;
- : Z.t = 0

Z.(shift_right (shift_left one 65) (-1));;
Exception: Invalid_argument "Z.shift_right: count argument must be positive".

Son objectif est de faire de l'arithmétique sur Z de manière efficace, et la doc de la fonction shift_right précise qu'elle a bien le comportement souhaité :

external shift_right: t -> int -> t = shift_right@ASM
(** Shifts to the right. 
    This is an arithmetic shift, 
    equivalent to a division by a power of 2 with rounding towards -oo.
    The second argument must be non-negative.
*)

Le module Int64 (et son compagnon Int32) ne doivent pas spécialement être fait pour cela :

This module provides operations on the type int64 of signed 64-bit integers. Unlike the built-in int type, the type int64 is guaranteed to be exactly 64-bit wide on all platforms. All arithmetic operations over int64 are taken modulo 264

Performance notice: values of type int64 occupy more memory space than values of type int, and arithmetic operations on int64 are generally slower than those on int. Use int64 only when the application requires exact 64-bit arithmetic.

Ici comme la précision est fixe et que la performance n'est pas déjà au top, on laisse l'appelant se charger des vérifications s'il pense que cela est nécessaire, l'appelé ne fournissant que la garantie du bon résultat dans les bornes 0 .. 63 (du moins je suppute que c'est ce genre de considération qui a du influencer le choix de cette implémentation).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Afr, mon compilateur interne vient d'émettre un warning : risque de boucle sans fin, abort envisageable au prochain tour. ;-)

C'est ce que j'expliquais dans un ancien post.

Je le sais bien c'est le premier commentaire de ce sous-fil : on boucle !!! Qu'est-ce que tu n'as pas compris dans ma réponse ? Tu m'as pourtant répondu que j'avais était très clair, là c'est moi qui ne te comprends plus.

Si OCaml disposait de la notion de sous types (contraints) alors il disposerait de deux fonctions shr.

J'espère que tu me pardonneras la familiarité de l'expression mais j'ai envie de te répondre : « si ma tante en avait, on l'appellerait mon oncle ». J'avais pourtant précisé dans ma réponse que les systèmes de typage était une question distincte, bien qu'elle puisse être utilisée dans le cas de Ada pour traiter le problème. Mais jusqu'à preuve du contraire, un langage doit faire avec le système de type dont il dispose. À ma connaissance il n'y a aucun plan pour intégrer cette sorte de type dans le langage, ce que je peux comprendre pour des raisons théoriques liées aux fondements du langage qu'ils seraient trop longs de développer (il y a néanmoins des sous-types contraints en OCaml, mais pas de la sorte des types range comme en Ada).

Connais tu la théorie des types ? J'avais pourtant donner un lien vers un dossier de la gazette des mathématiciens sur le sujet, l'as-tu lu ? Outre son utilité pour le typage statique des langages fonctionnelles, le système F (qui est le fondement des système de type de Haskell et OCaml) a été inventé au début des années 70 par le mathématicien et logicien français Jean-Yves Girard pour des questions liées aux fondements des mathématiques. Je cite ici sa nécrologie à la page 14 :

En 1953, Takeuti remarquait que la logique du second ordre permettait de formuler sans axiomes toutes les mathématiques courantes, et il proposait un procédé effectif d’élimination des coupures pour étendre le théorème de Gentzen : c’est la conjecture de Takeuti. En 1965, Tait démontrait l’existence de démonstrations sans coupure pour le calcul des séquents de Takeuti, mais l’essentiel manquait, à savoir la convergence du procédé d’élimination proposé par Takeuti. C’est ce que j’ai démontré en 1970, dans l’article [1], résultat amélioré dans [2] et [3]. En fait, ce résultat se présentait comme un système de calcul fonctionnel typé, (le système F), dans lequel on pouvait définir un type nat des entiers (i.e. dont les objets sont les entiers), avec deux théorèmes principaux :

Théorème 1
Le procédé de calcul dans F converge (normalisation).

Théorème 2
Tout algorithme fonctionnel (envoyant les entiers dans les entiers) dont on peut établir la terminaison au moyen des mathématiques courantes, se représente dans F au moyen d’un objet de type nat ⇒ nat.

Le système F est par exemple utilisé par Haskell comme représentation intermédiaire pour son compilateur. Ce système a connu depuis différentes extensions, ou il y a eu d'autres système du même genre comme la théorie des types de Per Martin-Löf, le Calcul des Constructions (CoC) à la base de Coq qui devint le Calcul des Constructions Inductives, puis on a tout récemment la théorie homotopique des types. Ces théories tournent toutes autour d'une problématique : la recherche d'un système de formalisation unifié de l'ensemble de l'édifice mathématique, ainsi que la réponse à la question : « les mathématiques sont-elles cohérentes ? ». Parce que l'on parle d'arithmétique depuis le début, mais l'arithmétique est-elle une théorie cohérente ?

Pour revenir sur la question initiale du journal : le décalage bit à bit vers la droite. Dans un autre commentaire, tu as écris :

Haskel, Python, Ada, Eiffel le proposent. D'autres langages de haut niveau ne font rien de plus que le jeu d'instruction X86 et je trouve que c'est une faiblesse (générateur de bugs).

Premièrement ce que fait Haskell, la bibliothèque standard OCaml aurait pu tout aussi bien le faire : je l'ai expliqué précédemment; cela n'a pas été l'option retenue (j'ignore, néanmoins, les raisons qui ont déterminé un tel choix). Ce n'est pas lié au possibilité du langage mais à un choix d'implémentation pour la bibliothèque standard fournie avec le compilateur. Mais ce n'est pas la seule existante, elle a des concurrentes certains développeurs ne la jugeant pas assez fournie.

Deuxièmement mettre Python dans la liste sur des questions de sécurités de code : c'est une blague ou tu es sérieux ?

Troisièmement, vu que tu viens de rajouter une exigence à ton cahier des charges : ne pas avoir de types cycliques pour le paramètre déterminant le degré du décalage, tu viens de les perdre tous sauf Ada. La liste des langages qui trouve grâce à tes yeux s'amenuise de plus en plus au fur et à mesure que progresse la discussion. ;-)

Pour le cas de Haskell, je l'ai déjà illustré. Pour celui de Eiffel, si je lis la documentation

infix "|>>" (s: INTEGER_8): INTEGER_64
    Shift by s positions right (sign bit copied) bits falling off the end are lost.
bit_shift_right (s: INTEGER_8): INTEGER_64
    Shift by s positions right (sign bit copied) bits falling off the end are lost.

Déjà le paramètre est sur 8 bit, donc ton exercice n'est pas réalisable en Eiffel avec cette version de shift_right. Et si je lis la documentation sur les INTEGER_8, dans le résumé je vois : 8 bits signed integer. J'ai comme le pressentiment qu'il est cyclique lui aussi : si un développeur Eiffel pouvait confirmer mon intuition ?

Et pour le langage de départ du projet de tes élèves, FreePascal, outre le comportement du shr inattendu, il me semble bien d'après cette documentation que le type en question est lui aussi cyclique :

function isBitSet(AValue, ABitNumber:integer):boolean;
begin
   result:=odd(AValue shr ABitNumber);
end;

Ai-je raison de supposer que le type integer est cyclique en Pascal ?

Comme de tout le fil de discussion et de tous les commentaires je suis le seul à avoir pointé du doigt l'importance de la nature du type de ce paramètre, je suis au regret de devoir émettre une nouvelle hypothèse qui me chagrine en espérant me tromper. Le « bug » n'était pas anticipé et a été découvert par hasard, et malgré son apparente solution tu en es au même point d'incompréhension que tes élèves : la source fondamentale du problème c'est la différence de géométrie entre un tore et un cylindre. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

De rien. Je suis content de voir qu'il y a au moins une personne qui apprécie mon humour.

Mais cette lecture peut au moins répondre partiellement à la question : que peut-on vouloir modéliser avec cela ? Une piste serait alors la modélisation de l'Odysée d'Ulysse dans une vision Homérique où il n'aurait fait que voyager sur un beignet. Les grecs anciens ayant été le premier peuple à émettre l'hypothèse que la terre ne serait ni plate ni sphérique mais aurait la forme d'un beignet ! :-P

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.