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
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 discerne 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 devenir 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'expé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ématiquement, 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 praticien 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 recueillir 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 philosophiques; 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’accorderont 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 devoir 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 perfection 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'entendre 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.
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.
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.
[^] # Re: Bon en théorie, mais inutile en pratique
Posté par kantien . En réponse au journal François Hollande visite 42, non mais allô quoi.... Évalué à 0.
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.
[^] # Re: Bon en théorie, mais inutile en pratique
Posté par kantien . En réponse au journal François Hollande visite 42, non mais allô quoi.... Évalué à 1.
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
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 :
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.
# Bon en théorie, mais inutile en pratique
Posté par kantien . En réponse au journal François Hollande visite 42, non mais allô quoi.... Évalué à 8.
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.
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.
[^] # Re: Exemples de limites en vrai
Posté par kantien . En réponse à la dépêche Grammalecte, correcteur grammatical. Évalué à 3.
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.
[^] # Re: Inférence de type, ou preuve automatique ?
Posté par kantien . En réponse à la dépêche Grammalecte, correcteur grammatical. Évalué à 3.
Grosse correction : le modus ponens ce n'est pas
si A alors B, or B donc Amais 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.
# Inférence de type, ou preuve automatique ?
Posté par kantien . En réponse à la dépêche Grammalecte, correcteur grammatical. Évalué à 3.
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.