kantien a écrit 1187 commentaires

Pour le code le fonction pred, il faut bien sûr lire

let pred n =
  match n with
  | Zero -> None
  | S n' -> Some n'

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

Au sujet du « faux », ne penses-tu pas que les développeurs OCaml peuvent utiliser le type polymorphe 'a option pour représenter cette notion ? L'idée m'est venue en relisant l'article du programme de Hilbert aux programmes tout court de Jean-Louis Krivine, en particulier ce passage au sujet de la correspondance de Curry-Howard :

Ce sont des logiciens qui l'ont découverte, tout au moins en ce qui concerne la logique intuitionniste. Mais c'est un informaticien, T. Griffin qui a opéré son extension à la logique classique, trente ans après, en 1990. C'est, de nouveau, une découverte capitale et tout à fait inattendue : en effet, le raisonnement par l'absurde est associé à une instruction très sophistiquée du langage SCHEME (une variante de LISP), qui a été inventée pour gérer, entre autres, les exceptions et le multi-tâches.

Or le type 'a option est une manière de gérer les exceptions de manière plus fonctionnelle en OCaml que de lever une exception de type exn. Je m'explique sur l'exemple du calcul du prédécesseur pour les entiers unaires :

type nat = Zero | S of nat

let pred n =
  match n with
  | Zero -> None
  | S n' -> n'

Un entier qui aurait zéro pour successeur est absurde, mais pas pour les autres entiers. Cela se passe comme si lorsque l'hypothèse est absurde on renvoie None, alors que lorsque ce n'est pas le cas on renvoie une conclusion du bon type Some 'a. Ce qui me fait penser à l'interprétation gödelienne de la logique intuitionniste : dans chaque étude de cas, on dispose soit d'une preuve de l'absurdité de l'hypothèse, soit de la prouvabilité du théorème sous l'hypothèse donnée. Cette interprétation te semble-t-elle recevable ? Les leçons de M. Krivine sont trop lointaines pour moi (une dizaine d'années, et déjà à l'époque je n'avais suivi son cours sur le lambda-calcul typé qu'en option) pour que je puisse avancer avec assurance sur ce genre de question.

Autrement, je viens de commencer la lecture de ta thèse et j'apprécie beaucoup ton sens de l'humour :-) En conclusion des remerciements, tu en adresses à Jean-Yves et Jean-Louis, que je suppose être MM. Girard et Krivine. J'aurais aimé me procurer les deux tomes de l'ouvrage Le point aveugle, mais le premier tome est en rupture de stock chez tous les distributeurs que j'ai regardé. Sais tu s'il en est prévu une réédition ?

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

Pour la taille des programmes que les spécialistes de Coq peuvent écrire, je pense que la réponse de Perthmâd est suffisante. Quand je parle de spécialistes, il faut voir que pour le compilateur C il s'agit d'un projet de Xavier Leroy, le Big Boss OCaml.
On pourrait rajouter un micro noyau, mais lui certifié par Isabelle.

Pour le reste de tes questions, je veux bien essayer de répondre, en espérant rester le plus compréhensible possible. En guise d'avertissement, je tiens à préciser que je ne suis ni informaticien, ni développeur, par contre tout comme toi je suis mathématicien de formation, mais également logicien (master Logique Mathématique et Fondements de l'Informatique) porté sur la philosophie (d'où mon pseudonyme).

Tout d'abord, en logique on distingue la partie qui traite des règles de bonne formation des jugements (règles syntaxiques) de celle qui s'occupe des règles par lesquelles on dérive ou infère les jugements les uns des autres (théorie de la démonstration). Les notions de logique propositionnelle ou des prédicats du premier ou second ordre relèvent de la première partie, alors que la distinction entre logique intuitionniste ou classique de la seconde. Je présenterai d'abord quelques notions syntaxiques, puis dans un second temps la différence entre logique classique et intuitionniste, et enfin je tenterai de montrer les liens entre ces notions et le typage de programme.

Lorsque l'on s'intéresse à la forme logique de nos jugements, quelqu'en soit le contenu (il fait beau, mon pseudonyme est kantien, Socrate est mortel, Gödel est le plus grand logicien du vingtième siècle, Kant est le plus grand philosophe de tous les temps…), si l'on fait abstraction du rapport sujet-prédicat (la structure sujet-verbe-complément) on trouve qu'ils se subdivisent en jugements affirmatifs (il fait beau), négatifs (il ne fait pas beau), hypothétiques (s'il fait beau alors je vais me promener), conjonctifs (il fait beau et les oiseaux chantent) ou disjonctifs (il fait beau ou il pleut). Tel est le point de vue de la logique propositionnelle. Usuellement, on représente les propositions non analysées, à partir desquelles on construit toutes les autres, par des lettres majuscules A, B, C… À partir d'elles on peut former, par exemple, les jugements : A et B et C, non A ou B, si A alors B etc. Cela doit paraître clair et évident pour un développeur : ce sont tous les opérateurs agissant sur les booléens. Mais pour l'instant on en reste à la logique propositionnelle dite du premier ordre : on ne se permet pas de quantifier sur les variables propositionnelles (aucun article défini ou indéfini, singulier ou pluriel). Quand on autorise une telle quantification, on parle de logique propositionnelle du second ordre. Dans une telle logique, on peut former des propositions de la forme : Pour toutes propositions A,B si A alors B. On note habituellement la forme des jugements hypothétiques (ou implication) par une flèche ->, et la proposition précédente se réécrit Pour toutes A,B A -> B. En anticipant la partie sur le typage, tu pourras comparer au type OCaml 'a -> 'b ;) (l'apostrophe ' a son importance, c'est le quantificateur universel).
Voilà qui est bien intéressant, mais dans nos phrases nous utilisons des verbes, et la grammaire ne répète-t-elle pas que la phrase minimale est constituée de la structure sujet-verbe-complément ? Les logiciens préfèrent parler de rapport sujet-prédicat ou de rapport prédicatif entre un ou plusieurs sujets. On parle alors de logique des prédicats. Ainsi, dans la phrase « Socrate est mortel » Socrate est le sujet, mortel le prédicat; tandis que dans la phrase « Roméo aime Juliette » aimer est le prédicat Roméo et Juliette en étant les sujets (on parle de prédicat binaire). Tout comme pour la logique propositionnelle, on distingue un premier et un second ordre selon les objets sur lesquels on autorise la quantification : quand on ne quantifie que sur les sujets on est au premier ordre, tandis que si l'on quantifie aussi bien sur les sujets que sur le prédicats on est au second ordre. Je vais tâcher d'illustrer la différence entre ces deux ordres dans la formulation des théories en prenant l'exemple de l'arithmétique.
Lorsque l'on cherche à axiomatiser l'arithmétique (comme il se doit pour toute théorie mathématique), outre les axiomes de bases comme 0 est un entier, tout entier a un successeur, le successeur d'un entier n'est jamais nul… il faut pouvoir exprimer l'essence même des nombres entiers : le principe du raisonnement par récurrence. En première année de licence, on le présente ainsi : si un proposition est vraie de 0 et qu'elle passe au successeur (si elle est vraie pour n alors elle est vraie pour n+1) alors elle est vraie pour tout entier. On pourrait l'écrire aussi : Pour tout P, (P0 et (Pn -> P(n+1))) -> pour tout n, Pn. Dans une telle formulation, la quantification porte aussi bien sur les propositions que sur les entiers : elle est du second ordre. Par contre, dans la logique du premier ordre on ne peut quantifier sur les propositions, il faut s'y prendre autrement. Alors, au lieu d'un unique axiome, on pose une infinité d'axiomes à travers ce que l'on nomme un schéma d'axiomes : à chaque proposition syntaxiquement bien formée (P) portant sur les entiers, on lui associe son axiome de récurrence : si P est vraie de 0 et qu'elle passe au successeur… La théorie a beau avoir une infinité d'axiomes, elle reste récursivement énumérable : il existe un algorithme pour décider si une formule est ou non un axiome. Par contre il n'existe pas d'algorithme pour décider si une formule est une conséquence déductive de la théorie : tel est le premier théorème d'incomplétude de Gödel (qui a pour corollaire l'impossibilité de résoudre le problème de l'arrêt pour une machine de Turing). Ce qui nous amène à la deuxième partie : qu'est-ce qu'être une conséquence déductive ? ou qu'elles sont les règles pour prouver ?

Je n'entrerai pas dans le détail de toutes ces régles, ni dans un exposé exhaustif, mais m'arrêterai sur trois règles qui ont leur importance dans la différence et l'opposition entre logique classique et intuitionniste : le modus ponens, le modus tollens et le tiers exclus. La première peut s'exprimer dans le raisonnement suivant : si A alors B, or A donc B. La seconde dans le raisonnement suivant : si A alors B, or non B donc non A (on parle aussi de raisonnement par contraposition : la contraposée de la proposition si A alors B étant la proposition si non B alors non A, le modus tollens n'est que le modus ponens appliqué à la contraposée). Enfin, la troisième affirme que pour toute proposition A, on peut poser A ou non A (entre une thèse et son antithèse, tout tiers est exclus). Et c'est cette dernière règle que les intuitionnistes rejètent : elle permet de prouver l'existence d'objets sans même exhiber un moyen de les construire (on a pour cela qualifié les intuitionnistes de constructivistes). Illustrons cette propriété étonnante du tiers exclus sur un exemple célèbre.
Théorème : il existe deux nombres irrationnels a et b tels que a^b soit rationnel.
Preuve :
Posons a = b = racine de 2 qui est irrationnel. Selon le tiers exclus, ou bien a^b est rationnel ou bien il ne l'est pas, c'est à dire qu'il est irrationnel. Si le premier cas est vrai, alors on a fini. Supposons donc que a^b soit irrationnel. Alors comme (a^b)a = a^b*a = a² = 2 est rationnel, il suffit de prendre a^b et a pour les deux nombres cherchés.
CQFD.
Voilà une preuve bien étrange : elle affirme l'existence de deux nombres ayant une propriété particulière, mais à la fin de la preuve on ne les connaît pas, ne sachant pas laquelle des deux alternatives fournies par le tiers exclus est la bonne. À dire vrai, on peut prouver sans tiers exclus que la deuxième alternative est vraie… mais la preuve est bien plus longue. ;)
Le principe du tiers exclus est équivalent au principe du raisonnement par l'absurde que l'on peut formuler ainsi : (non A -> A) -> A. Autrement dit : si une antithèse prouve la thèse qu'elle est censée réfuter, alors on peut affirmer la thèse sans hypothèse auxiliaire. Une des conséquence surprenante de la logique intuitionniste est qu'une double négation n'est pas équivalente à une affirmation ( non non A n'est pas équivalente à A). Dans un raisonnement par l'absurde, un intuitionniste conclura à la double négation (non A -> A -> non non A) mais non à l'affirmation comme le ferai un mathématicien « classique ». De même, si le principe du tiers exclus n'est pas prouvable en logique intuitionniste, on peut par contre y prouver la double négation de celui-ci.

J'espère que la réponse sur la traduction des « pour tout » et la nature du second ordre te semble claire : les intuitionnistes traduisent comme tout le monde, le second ordre permet de quantifier sur les prédicats, mais les intuitionnistes ne concluent pas toujours comme le font les mathématiciens « classiques ». C'est dans les liens logico-déductifs entre énoncés, et non dans leur formulation, que se situe la différence entre logique classique et logique intuitionniste.
Venons en enfin aux programmes et à leur typage, et donc à la correspondance de Curry-Howard ou correspondance preuve-programme (là où tu t'es dis « chouette » ;). Les langages fonctionnels comme OCaml (ou Haskell, Lisp…) ont pour modèle théorique le lambda-calcul, là où les langages impératifs s'inspirent du modèle des machines de Turing. Le lambda-calcul d'Alonzo Church avait pour ambition de capturer l'essence de la notion mathématique de fonction ¹. Le lambda-calcul peut être vu comme un langage de programmation, dans lequel les fonctions sont des citoyens de première classe, où les types sont des formules du prédicats du seconde ordre: telle est la correspondance de Curry-Howard. Cela est du au fait que les règles de typage de ce langage sont analogues aux règles de déduction de la logique intuitionniste. Ainsi, en gros, à chaque fois que l'on type un lambda terme on peut construire en parallèle une preuve d'un théorème : le théorème « dit » ce que fait le programme ², et celui-ci est une preuve particulière de celui-là.
Prenons des exemples avec le typage de fonctions en Ocaml. Si l'on définit la fonction let f x = x +1, elle aura pour type int -> int et quand on calcule le terme f 1 on trouve la valeur 2 de type int. Observes bien la forme du type de la fonction ! Ne te rappelle-t-il pas la notation de l'implication logique A -> B (si A alors B) avec ici A = B = int ? C'est bien le cas. Le type int peut être vu comme une constante propositionnelle, et le type de la fonction f comme la tautologie si A alors A. Et quand on l'applique a une valeur du bon type, on applique la règle du modus ponens : si A alors A, or A donc A (1 est de type int, le or A, donc la valeur f 1 = 2 est de type int). La forme générale du modus ponens s'obtient avec la fonction let apply f = fun x -> f x de type ('a -> 'b) - 'a -> 'b que l'on peut paraphraser en : Pour toute proposition A et B, si A alors B or A donc B. On a là une formule du second ordre, et c'est ce second ordre qui confère le polymorphisme au langage. Les fonctions et leur application permettent donc de retrouver les formules hypothétiques. Pour ce qui est des formules disjonctives et conjonctives, elles sont fournies respectivement par les variants et les enregistrements (les variants sont des « ou », les enregistrements des « et »). Comme il manque la négation logique, on retrouve un sous-ensemble de la logique propositionnelle du second ordre. Ainsi, si on regarde les fonctions OCaml comme des preuves et leur type comme des théorèmes, le compilateur vérifie que l'on applique les théorèmes à des prémisses dont la forme est conforme à l'énoncé du théorème : autrement dit, on n'utilise pas les théorèmes n'importe comment, comme quelqu'un qui voudrait appliquer le théorème de Pythagore à un triangle équilatéral.
Malheureusement, ce système est limité quand à son expressivité sémantique : il n'y a pas de prédicats. C'est là que Coq entre en jeu. Pour un programmeur, y avoir recours peut être disproportionné (sortir un char d'assaut pour tuer une mouche), mais dans des logiciels critiques où le droit à l'erreur n'est pas permis (comme le pilote automatique d'un avion ;) cela peut s'avérer être une solution recevable. Je vais illustrer son principe en utilisant un exemple donné par Perthmâd dans son article sur coq 8.5. Il y définit une fonction qui calcule le nombre d'occurrence d'un entier dans une liste, et prouve que si on concatène deux listes on ajoute le nombre d'occurrence.

(* import de modules pour les listes et l'arithmétique *)
Require Import List Arith.
Fixpoint multiplicity (n : nat) (l : list nat) : nat  :=
    (* filtrage par motifs sur la liste "l" *)
    match l with       
    (* cas où la liste est vide *)
    | nil     => 0  
    (* cas où on a un élément "a" en tête de liste, "l'" le reste *)  
    | a :: l' => 
        (* test d'égalité de "n" avec l'élément "a" *)       
        if eq_nat_dec n a             
        (* appel récursif suivi de la fonction successeur d'un entier *)
        then S (multiplicity n l')  
        else multiplicity n l'         
    end.

Lemma multiplicity_app (n : nat) (l1 l2 : list nat) : 
  multiplicity n (l1 ++ l2) = multiplicity n l1 + multiplicity n l2.
Proof.
  induction l1. reflexivity.
  simpl. destruct eq_nat_dec; auto.
  rewrite IHl1. auto.
Qed.

En OCaml, cela ressemblerai à ceci :

(* représentation unaire des entiers naturels *)
type nat = Zero | S of nat;;

(* prédicat d'égalité décidable entre deux entiers *)
let rec eq_nat_dec n m =
  match n, m with
  | Zero, Zero -> true
  | Zero, _ | _, Zero -> false
  | S n', S m' -> eq_nat_dec n' m'
;;

(* la fonction multiplicity définie comme en Coq *)
let rec multiplicity n l =
  match l with
  | [] -> Zero
  | a :: l' ->
     if eq_nat_dec a n
     then S (multiplicity n l')
     else multiplicity n l'
;;

(* définition de l'addition sur le type nat *)
let rec plus_nat n m =
  match n, m with
  | Zero, _ -> m
  | _, Zero -> n
  | S n', S m' -> S (S (plus_nat n' m'))
;;

(* morphisme du type int vers le type nat *)
let rec nat_of_int n =
  match n with
  | 0 -> Zero
  | _ -> S (nat_of_int (n-1))
;;

(* morphisme du type nat vers le type int *)
let rec int_of_nat n =
  let rec loop m acc =
    match m with
    | Zero -> acc
    | S m' -> loop m' (acc + 1)
  in loop n 0
;;

On remarque déjà que le théorème ne porte pas sur le type int mais sur le type nat. D'ailleurs, le type int muni de l'addition est un groupe cyclique isomorphe à un Z/nZ où la valeur de n dépend de l'architecture de la machine (2³¹ sur 32-bit et 2⁶³ sur 64-bit), et ne représente qu'imparfaitement le concept de nombre entier. Toutefois, en utilisant les morphismes entre les deux types on pourrait le « traduire » pour le type int.
Et dans une boucle interactive :

(* on représente 2 en unaire *)
# let n = nat_of_int 2;;
val n : nat = S (S Zero)

(* on crée deux listes d'entiers unaires qu'on concatène *)
# let l1 = List.map (nat_of_int) [2; 3; 4; 2; 5];;
val l1 : nat list =
  [S (S Zero); S (S (S Zero)); S (S (S (S Zero))); S (S Zero);
   S (S (S (S (S Zero))))]
# let l2 = List.map (nat_of_int) [2; 3; 4; 2; 2];;
val l2 : nat list =
  [S (S Zero); S (S (S Zero)); S (S (S (S Zero))); S (S Zero); S (S Zero)]
# let l3 = l1 @ l2;;
val l3 : nat list =
  [S (S Zero); S (S (S Zero)); S (S (S (S Zero))); S (S Zero);
   S (S (S (S (S Zero)))); S (S Zero); S (S (S Zero)); S (S (S (S Zero)));
   S (S Zero); S (S Zero)]

(* le théorème est bien vérifié sur ce cas particulier *)
# multiplicity n l3 = plus_nat (multiplicity n l1) (multiplicity n l2);;
- : bool = true

Là où pour vérifier la correction sémantique de la fonction un développeur OCaml ferai des tests unitaires (qui ne seront jamais exhaustifs étant donné qu'il faudrait tester une infinité de cas), la preuve en Coq nous garantie qu'elle est correcte. Comme dit plus haut, avoir recours à Coq pour cet exemple est sans doute disproportionné par rapport au besoin. Un cas plus proche de la pratique est, par exemple, cette structure de données union-find persistante.

Si tu as eu la patience de rester en ma compagnie jusqu'au bout, et que je n'ai pas fait trop d'erreurs ou contresens (ces cours sont loin pour moi, Perthmâd me corrigera sans doute sur quelques points), j'espère t'avoir fait entrevoir les théories mathématiques qui se cachent aux fondements de OCaml. Pour la correspondance de Curry-Howard, comme référence accessible en ligne tu as Lambda-calculus, types and models de Jean-Louis Krivine. En ce qui concerne le système Coq, il y a un ouvrage collaboratif Homotopy Type Theory (sous creatives-commons, écrit en utilisant git) ou cet article sur le site Images des Maths du CNRS.

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

Effectivement, la force des langages comme OCaml ou Haskell est la puissance sémantique de leur système de types. Outre la garantie qu'il n'y aura pas d'erreurs de typage à l'exécution (ce qui était ici reproché à python, mais ne les distingue pas de langage comme le C si l'on passe sous silence l'absence d'effets de bord), le système est un sous-ensemble riche du calcul propositionnel du second ordre : ce qui offre de plus un bon contrôle sémantique sur le code, mais ne dispense pas des tests unitaires.
Pour se dispenser complètement de ces derniers, il faut passer à Coq qui lui à tout le calcul des prédicats du second ordre avec logique intuitionniste (sans raisonnement par l'absurde, quoi que on peut même activer ce dernier mais là…).
Pour ceux qui ne connaissent pas ces notions, disons qu'on peut par exemple exprimer dans le système de types de Coq que l'on définit une fonction qui prend un entier et renvoie son double. Autrement dit on peut exprimer complètement la sémantique du code, et le système vérifie que le code correspond bien à sa sémantique. D'une certaine façon, un code Coq qui compile est garantie sans bugs.

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

Pour le web que reproches tu à Ocsigen et pour le xml à la bibliothèque xmlm ?
Il me semble d'ailleurs que Ocsigen utilise cette dernière pour la production du code html, dont la bonne formation est garantie par le système de type de OCaml (pas de besoin du html validator).
Le projet Ocsigen développe aussi js_of_ocaml pour compiler du code Ocaml vers javascript (et qui tourne des fois plus vite que du bytecode OCaml), ce qui permet par exemple de faire tester des programmes OCaml dans un navigateur comme le font OCaml Pro avec leur logiciel alt-ergo.

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

Tu as parfaitement raison de le souligner. En fait je reprenais dans mon message les termes même du message que je citais, pour des raisons de continuité; je n'aurai peut être pas du.

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

Je te remercie d'avoir porté cet ouvrage à ma connaissance.
On y croise du beau monde selon la présentation bien que Russell se mange la part du lion sur la couverture française, ce qui n'est pas très juste à mon avis.
Je m'en vais le commander, et ferait peut être un journal dessus suite à ma lecture.

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

Je n'ai pas trop d'avis au sujet de ta modélisation du risque de panne dans un raid, si ce n'est que le recours à la loi binomiale est peut être effectivement discutable (non indépendance du risque de panne conjointe). Mais quoi qu'il en soit, le modèle en question était volontairement simplifié (c'était clairement affiché de ta part) et dans tous les cas, pour toute modélisation physique c'est la confrontation avec l'expérience et l'observation qui a le dernier mot. ;)
Pour ce qui est de Nicolas Boulay, il ne semble pas savoir ce que c'est que de la théorie : modéliser c'est faire de la théorie (la réciproque n'est pas nécessairement vraie, bien entendu). À moins qu'il est pour projet d'inventer le triangle à quatre côtés.

En revanche, tu n'as peut être pas bien saisi la signification du passage du texte de Kant que tu cites. Il est vraie que si l'on n'est pas familier avec la partie théorique de sa philosophie (théorie de la connaissance), ce passage peut prêter à confusion. Il veut dire par là que si un concept contient bien un règle, il est souvent impossible de fournir une règle pour dire comment l'appliquer, car alors cette dernière règle exigerai à son tour un autre règle pour savoir quand et comment l'appliquer, et cela à l'infini. Telle est l'utilité de la jurisprudence dans le domaine juridique : donner des cas d'affaires singulières qui tombent sous le coup de telle ou telle loi. La loi fournit l'universel (la règle) et la jurisprudence contient des cas particuliers qui tombent sous elle (appliquer une règle à un cas, c'est cela que Kant nomme « subsomption »). Lorsque notre faculté de juger remplit cette fonction, elle est qualifié de déterminante : elle détermine un cas particulier selon un règle générale.
Or dans le cas de la recherche et de la construction d'un modèle, le particulier est connu mais non la règle. Au contraire c'est cette règle que l'on cherche à trouver. Dans ce cas, notre même faculté de juger (qui précédemment était déterminante) devient réfléchissante : c'est ce que l'on appelle tout bonnement réfléchir. Et ce processus consiste justement à modéliser, et son produit est un modèle. Ce qui correspond plutôt à ce passage du texte

c'est de là que le médecin qui sort de son école, ou l’agriculteur, ou le financier, peut et doit abstraire de nouvelles règles pour compléter sa théorie. Ce n’est pas alors la faute de la théorie, si elle n’a encore que peu de valeur pour la pratique; cela vient de ce qu’on n’a pas assez de théorie, de celle que l’homme aurait dû apprendre de l’expé­rience, et qui est la véritable théorie

Mais bien sûr, pour faire cela il faut savoir théoriser et donc connaître des théories (c'est en forgeant que l'on devient forgeron).

Pour finir, il y a un passage qui m'a fort étonné dans ton journal sur le raid :

Je sais, les maths, blah blah blah blah… l'informatique, l'IT, ce ne sont pas des maths, blah blah blah blah…

Alors je ne sais si c'est ton ressenti d'une pensée ambiante en ces lieux, ou si elle est réelle, mais je peux te rassurer : l'informatique et l'IT c'est des mathématiques !
Comme mon message est déjà bien long je ne vais pas trop m'appesantir, mais l'informatique est une science dont l'algorithmique et la logique mathématique sont des composantes essentielles (ce n'est pas pour rien qu'existe le master Logique Mathématique et Fondements de l'Informatique ). On y apprend, par exemple, qu'un algorithme ou un programme n'est rien d'autre qu'un preuve d'un théorème mathématique, ce résultat est connu sous le nom de « correspondance ou isomoprhisme de Curry-Howard ». Cela relève du lambda calcul fortement typé : c'est de là que vient, entre autre, le système de type algébrique de langages comme Haskell ou OCaml (Haskell était le prénom de Curry). Un exemple classique sur le sujet est le théorème d'Euclide qui affirme l'existence d'une infinité de nombre premier, c'est à dire que pour tout entier n il existe un entier p tel que n < p et p est premier. Et bien toute preuve de ce théorème est un programme qui prend un entier en entrée et renvoie en sortie un nombre premier plus grand que son entrée. ;)
Le langage de type des GADT ne permet pas d'exprimer cela, on peut juste dire qu'on à une fonction qui prend un entier et renvoie un entier, mais le langage Coq le permet.

Les lecteurs désireux dans connaître plus sur le sujet pourront par exemple lire ces deux textes:
À propos de la théorie des démonstrations il relate bien l'histoire de la découverte des paradoxes de Russell, en passant par les résultats de Gödel, jusqu'aux travaux contemporains. De plus, il comporte une touche d'humour en comparant les mathématiciens à des drogués à un jeu en réseau.
Fonctions, programmes et démonstrations

P.S : on peut aussi étendre ce système de typage aux protocoles réseaux

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

Ayant lu ça et là, à travers les différents commentaires, que l'apprentissage de la théorie était une chose dont l'on pouvait se dispenser, voire ne servait à rien dans la pratique, je voudrais citer ici l'introduction d'un essai de Kant intitulé : « Sur le proverbe : cela peut être bon en théorie, mais ne vaut rien pratique ». Le choix de l'auteur n'est pas complètement étranger au sujet présent (l'informatique), mais cela sera expliqué après la citation.

On appelle théorie un ensemble même de règles pratiques, lorsque ces règles sont conçues comme des principes ayant une certaine généralité, et que l'on y fait abstraction d'une foule de conditions qui pourtant exercent nécessairement de l'influence sur leur application. Réciproquement on ne donne pas le nom de pratique à toute espèce d'œuvre, mais seulement à la poursuite d'un but, quand on le considère comme l'observation de certains principes de conduite conçue d'une manière générale.

Il est évident qu'entre la théorie et la pratique il doit y avoir encore un intermédiaire qui forme le lien et le passage de l'une à l'autre, quelque complète d'ailleurs que puisse être la théorie. En effet, au concept de l'entendement, qui contient la règle, doit se joindre un acte du Jugement par lequel le praticien dis­cerne si la règle s'applique ou non au cas présent ; et, comme on ne saurait toujours fournir au jugement des règles qui lui servent à se diriger dans ses subsomptions (puisque cela irait à l'infini), on conçoit qu'il y ait des théoriciens qui ne puissent jamais de­venir praticiens de leur vie, parce qu'ils manquent de jugement : par exemple des médecins ou des jurisconsultes, qui ont fait d'excellentes études, mais qui, lorsqu'ils ont à donner un conseil, ne savent comment s'y prendre. En revanche, chez ceux qui possèdent ce don de la nature, il peut y avoir défaut de prémisses, c'est-à-dire que la théorie peut être incomplète, car peut-être a-t-elle besoin, pour être complétée, d'essais et d'ex­périences qui restent encore à faire; c'est de là que le médecin qui sort de son école, ou l’agriculteur, ou le financier, peut et doit abstraire de nouvelles règles pour compléter sa théorie. Ce n’est pas alors la faute de la théorie, si elle n’a encore que peu de valeur pour la pratique; cela vient de qu’on n’a pas assez de théorie, de celle que l’homme aurait dû apprendre de l’expé­rience, et qui est la véritable théorie, alors même que l’on n’est pas en état de la tirer de soi-même et de l’exposer systéma­tiquement, comme un professeur, dans des propositions gé­nérales, et que par conséquent on ne saurait avoir aucune prétention au titre de médecin, d’agriculteur ou de financier théoricien. Personne ne peut donc se donner pour un pra­ticien exercé dans une science et mépriser la théorie sans faire preuve d’ignorance dans sa partie; car c’est être vraiment ignorant que de croire que l’on peut dépasser la théorie en tâ­tonnant dans la voie des essais et des expériences, sans recueil­lir certains principes (qui constituent proprement ce que l’on nomme théorie) et sans faire de tout ce travail un ensemble (qui, méthodiquement traité, prend le nom de système).

Cependant on souffrira plus patiemment encore un ignorant qui, fier de sa prétendue pratique, déclare la théorie inutile et superflue, qu’un présomptueux qui la proclame bonne pour les écoles (comme une manière d’exercer l’esprit), mais qui soutient qu’il en va tout autrement dans la pratique; que, quand on quitte l’école pour le monde, on s’aperçoit qu’on n’a poursuivi jusque-là que des idées vides et des rêves philoso­phiques; en un mot que ce qui peut être bon dans la théorie n’a aucune valeur dans la pratique. (C’est ce que l’on exprime souvent aussi de cette manière: telle ou telle proposition est bonne in thesi, mais non in hypothesi.) Or on ne ferait que rire d’un mécanicien ou d’un artilleur empirique qui trancherait sur la mécanique générale ou sur la théorie mathématique de la projection des bombes, en disant que cette théorie, si ingé­nieusement conçue qu’elle soit, ne vaut rien dans la pratique, parce que, dans l’application, l’expérience donne de tout autres résultats que la théorie. (En effet, si à la première on ajoute la théorie du frottement, et à la seconde celle de la résistance de l’air, c’est-à-dire en général plus de théorie encore, elles s’ac­corderont parfaitement avec l’expérience.) Mais autre chose est une théorie qui concerne des objets d’intuition, autre chose une théorie dont les objets ne sont représentés qu’au moyen de concepts, comme les objets mathématiques et ceux de la philosophie. Peut-être ces derniers sont-ils susceptibles d'être conçus dans toute leur perfection (du côté de la raison), mais ne le sont-ils pas d'être donnés , et n'offrent-ils ainsi que des idées vides dont on ne saurait faire dans la pratique aucun usage ou qu'un usage dangereux. Par conséquent le proverbe en question pourrait bien avoir sa vérité dans les cas de ce genre. Mais dans une théorie qui est fondée sur le concept du de­voir il n'y a plus lieu de craindre l'idéalité vide de ce concept; car ce ne serait pas un devoir de se proposer un certain effet de notre volonté, si cet effet n'était pas possible dans l'expé­rience (quelque parfaite ou quelque rapprochée de la perfec­tion qu'on pût la concevoir). Or il n'est question dans le présent traité que de cette espèce de théorie.Il n'est pas rare d'en­tendre soutenir, au grand scandale de la philosophie, que ce qu'elle peut avoir d'exact ne vaut rien dans la pratique ; on dit cela sur un ton fort dédaigneux, en affichant la prétention de réformer la raison par l'expérience, même dans ce qui fait son principal titre de gloire, et en se flattant de voir plus loin et plus sûrement avec des yeux de taupe cloués sur la terre qu'avec ceux d'un être fait pour se tenir debout et regarder le ciel.

Kant, « Sur le proverbe : cela peut être bon en théorie, mais ne vaut rien pratique »

Les graissages sont évidemment de moi.
Pour la petite histoire, et pour justifier le rapport existant entre Kant et l'informatique :
À la fin du 19ème siècle, un mathématicien, logicien et philosophe allemand du nom de Frege voulut réfuter un point de la philosophie théorique de Kant selon lequel tous les jugements mathématiques sont synthétiques a priori. Il voulait montrer, en gros, que la logique formelle peut à elle seule fonder cette science. Il réforma pour cela la logique d'Aristote, et introduisit ce que l'on nomme aujourd'hui le calcul des prédicats. Malheureusement, à la fin de son siècle, le philosophe et logicien Russel trouva une contradiction dans sa théorie. S'en suivit ce que l'on appelle aujourd'hui « la crise des fondements des mathématiques ». Les paradoxes et contradictions furent assez vite résolus, mais certains cherchèrent à montrer qu'une telle situation en se reproduirait plus jamais. Tous ces travaux aboutirent, entre autre, à deux résultats fameux de Gödel : le théorème de complétude du calcul des prédicats, et les théorèmes d'incomplétude. Ce fût là, les prémisses de la théorie de la calculabilité et donc… de l'informatique théorique. Mais au final, pour un kantien, l'honneur est sauf, l'incomplétude le prouve : Kant avait raison et Frege tort !! \o/

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

Il me semble qu'Antidote se trompe pour les phrases 2 et 3.
L'expression "ce que" introduit le pronom relatif "que" avec un antécédent indéterminé, d'où le "ce" (la construction "celui qui" est identique), est joue le rôle de complément d'objet de sa subordonnée ("celui qui" joue le rôle de sujet indéfini quant à lui). Ce qu'il y a, c'est que le verbe "aimer" est le sujet du verbe "signifie" dans la subordonnée, et cela il ne le voit pas. Cela étant, faire du verbe "aimer" le sujet du verbe "être" dans le cas de la phrase 2 est discutable d'un point de vue sémantique.
En résumé :
- "aimer signifie quelque chose" est correcte
- "je sais ce que signifie aimer" l'est aussi, la proposition est devenue complément d'objet du verbe "savoir" et "ce que" joue le rôle de "quelque chose"
- "je sais ce que aimer signifie" l'est tout autant

Antidote ne tiquerai peut-être pas sur une phrase du genre : je sais ce que je veux dire (ici le sujet de la subordonnée étant "je").

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

Grosse correction : le modus ponens ce n'est pas si A alors B, or B donc A mais bien si A alors B, or A donc B (j'ai honte).

Il y a aussi des fautes de grammaire, comme quoi ce genre d'outil intégré à Firefox serai d'une grande utilité. ;)

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

Bonjour Olivier,

Il a été fait mention, dans d'autres commentaires, au parallélisme entre la correction grammaticale et la compilation de code informatique. Et ta description du fonctionnement de grammalecte n'y ai sans doute pas étrangère.
S'il est bien vrai que les compilateurs vérifient la syntaxe et la grammaire du code, ils font aussi de la traduction : c'est leur fonction première. ;)

Par contre, il t'a été proposé de regarder du côté du langage Ocaml pour écrire ton moteur d'analyse grammaticale. Je pense que ce pourrait être une bonne idée. La manipulation d'arbre de syntaxe abstraite (AST), ainsi que leur création, est un domaine dans lequel ce langage excelle. Les compilateurs manipulent essentiellement ce type de structure de données; et après la lecture de l'article wikipédia sur les syntagmes, il me semble que c'est la structure la mieux adaptée pour résoudre les questions d'analyse grammaticale (je ne suis pas programmeur, donc je me trompe peut être).

Gérard Huet (informaticien émérite français, chercheur inria) a publié un article sans rapport apparent : Fondements de l'informatique, à la croisée des mathématiques, de la logique et de la linguistique (étonnement c'est un docx !? mais pas de soucis avec LibreOffice), et pourtant…
Aux pages 22 et suivantes, lorsqu'il aborde la question de l'enseignement de l'informatique à l'école, on y trouve ce passage :
« Je vais prendre un autre exemple dans un domaine complètement différent, c’est l’analyse grammaticale dans la
classe de français. Je ne sais pas si on fait encore beaucoup ça, mais de mon temps on décortiquait les phrases : toute phrase doit avoir un verbe, tout verbe doit avoir un sujet. Là, il y a un petit bout de raisonnement aussi. Comment est-ce que l’on obtient une phrase à partir d’un verbe ? Prenons d’abord un verbe intransitif. Un verbe intransitif a besoin d’un sujet pour exprimer son action. Donc, vous pouvez voir le rôle fonctionnel de ce verbe comme utilisant le syntagme nominal représentant le sujet pour construire la phrase représentant l’action. De même, un verbe transitif peut être vu comme une fonction qui
prend son complément d’objet pour construire un syntagme
verbal, se comportant comme un verbe intransitif. Vérifier que « le chat mange la souris » est une phase correcte devient un petit raisonnement où le verbe « mange » prend la souris pour construire « mange la souris », objet fonctionnel qui peut maintenant manger le chat, si je puis dire, pour donner la phrase. Le petit arbre de raisonnement, qui exprime la composition des deux fonctions en vérifiant leurs types, hé bien, c’est ce qu’on appelle l’analyse grammaticale de la phrase. »

Suivent quelques considérations sur des différences entre les grammaires françaises et anglaises, tout en soulignant leurs points communs (et c'est le commun, l'important ;).
Et tout cela, dans l'exemple français choisi, n'est qu'une double application de la règle d'inférence logique dite du Modus Ponens (si A alors B, or B donc A).
L'exemple qui précède celui-là est le cas d'une machine à laver vue comme une fonction qui transforme des watts en euros (la facture EDF ;). En Ocaml c'est une fonction de type watt -> euro (la flèche dénote l'implication logique, si watt alors euro, d'où le modus ponens).
De plus, le même chercheur a en ligne un dictionnaire de sanskrit avec de l'analyse de lexème et de grammaire pour cette langue. Sans doute a-t-il utilisé ce type de technique, et le contacter pourra t'être utile ?

Dans le fond, au premier abord, si l'on travaille sur un AST représentant des syntagmes, vérifier la bonne formation grammaticale d'un syntagme me fait penser à de l'inférence de type, voire de la preuve automatique si l'on cherche des suggestions à soumettre à l'utilisateur.

En espérant que mon commentaire puissent t'être bénéfique,
Cordialement.

P.S : avec js_of_ocaml, tu obtiens direct du code javascript à partir de ton code OCaml.

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