Question sur le programe MPI: la logique

Messages : 711

Inscription : 01 sept. 2008 16:49

Profil de l'utilisateur : Professionnel

Question sur le programe MPI: la logique

Message par Wilfried.kro » 15 mars 2023 20:36

Bonjour

J'ai des questions sur le programme de MPI et en particulier sur la partie logique. Ces questions sont probablement naives et refletent certainement mon ignorance de l'enseignement de l'informatique en prepas en generale et en MPI en particuliers. Mais je les ai posé comme elle me sont venu à la lecture, j'espere que ce n'est pas trop irritant.

Ma motivation premiere est de mieux comprendre la maniere dont l'info est enseigner en MPI en partant d'un cas precis (pour eviter autant se peut generalité et jugement de valeurs). Par ailleurs, je suis aussi curieux d'un point de vue didactique.

en tout cas merci à ceux qui auraient la patience de me repondre.

W.


6.1 Syntaxe des formules logique
L’expression « logique classique du premier ordre » ne figure pas dans le programme. Est-ce que la notion de terme est au programme ? (le programme parle de formule propositionnel mais pas de formule de la logique du premier ordre)

Le programme ne mentionne pas les diagrammes de Wenn. OK, ca peut sembler un outil pour amuser les gosses (ou pour les maths modernes en primaire) mais c’est LA métaphore plebiscité par la UX et les utilisateurs qui doivent être expos" à ce genre de notion (l’informatique c’est aussi faire des programmes pour des utilisateurs, qui sont, comme chacun sait un peu con ou du moins qui n’ont pas fait d’etudes de maths ou c’était il y a longtemps, cette notion d’utilisateurs semblent complètement absente du programme). Par ailleurs je trouve personnellement que c’est la meilleur manière de se persuader que not(A xor B) c’est (A <=> B) – cette équivalence n’est pas mentionné dans le programme, est-ce que parce que ca va sans le dire ?

Substitution d’une variable: Est ce une restriction ou faut il être capable de gérer le cas générale, par exemple A(f(x, g(y), c)[x:=h(a, y), y := b]. Est-ce que l’implémentation de la substitution est traiter en TP (IMHO on saisi vraiment après l’avoir implémenter) ? Ou au contraire ne s’agit t’il que du renommage d’une variable lié ?

Le programme mentione le liens avec entre les notions de variables libres, liées et de portées avec la programmation. Très bien mais est ce qu’on explique comment les variables sont gérées par diffèrent languages ? (on est bien d’accord, il n’y pas de trace de lambda calcul dans le programme ?)

6.2 SAT
L’algortithme de Quine, est ce ceci : https://en.wikipedia.org/wiki/Quine%E2% ... _algorithm

Ou juste l’algo brute forte sur les CNF (eg le fait de pouvoir virer un literal d’une clause quand il s’evalue à True et virer une clause quand elle s’evalue à True) ?
Le programme ne mentionne pas la complexité. Cependant il parait etrange de ne pas parler de P ?= NP sur un cours sur SAT.

J’ai vue que certains enseignants en parlent :
https://mp2i-info.github.io/9_logic/3_sat/sat/
en évitant de mentioner la machine de Turing (deterministe ou pas) et à priori en admettat que SAT est NP complet. Ceci dit le programme ne mentionne pas non plus la décidabilité.
Parler de compexité permetrait d’évoquer le fait que 2-SAT et les clauses de Horn sont soluble en temps polynomiale
Bref est ce que cela doit être traiter ou pas ?

Je trouve l’exemple d’incarnation de SAT via la coloration des sommets d’un graphe très mathématiques. N’y aurait il pas un sens à prendre des exemples concrets/modelisations (« méthodes formelleux ») ?

Est-ce que de savoir implémenter un algorithme de sat solving (en renvoyant l’assignement quand il y a lieu) en Camel, en C fait partie de ce qui est exigible ? Ca implique plus ou moins introduire le format DIMACS et être capable de le lire à partir d’un fichier (et donc avoir un outil pour generer les jeux de tests, eg https://logictools.org/prop.html)

D’un point de vue terminologie et défense de la langue française, faut il vraiment parler de FNC (et non de CNF) ? Tout de même on note bien le noyau Ker et on parle de Caml pas de Lmac…

Sur les CNF, le programme mentionne de souligner que le passage en CNF peut induire une explosion combinatoire sur la taille de la formule. La conclusion logique est que l’approche est condamnée (même si par extraordinaire P=NP). Ca parait étrange de continuer sans se poser de question (on ne peut pas faire de l’informatique sans tenir compte des problèmes d’intractabilité ou alors IMHO on se trompe de discipline). Sauf erreur ENS MPI 2016 aborde ce point. Mais faut-il systématiquement aborder la transformé de Tseitin et la notion d’equi satisfiabilité (qui est un concept interressant et qu'on retrouve d'ailleurs avec la transformé de skolem pour le premier ordre)?

Sur les CNF toujours, quelle est la bonne façon d’expliquer qu’une clause vide s’évalue à False et une CNF vide à True ?

6.3 Deduction naturelle
Faut il aborder le fait qu’il existe d’autre logique, par exemple la logique intuitionniste et illustrer ce que cela veut dire en terme par exemple de déduction naturelle ?

Est-ce que la preuve de l’élimination des coupures dans le cas propositionnel est au programme ?

Si on ne parle pas de decidabilité, comment convient il de faire passer l’idee que la logique du premier ordre est semi decidable ? Faut il seulement admettre que la recherche d'une preuve peut ne jamais se terminer ?

A propos de la mise en œuvre, le fait d’explicitement écarter une implementation pour privilégier l’ecriture de de petites preuves à la main n’est il pas un partie pris trop logicien et pas assez informaticien ? Par exemple ne serait il pas intéressant d’implémenter au moins la résolution propositionnel ?

Il est mentionné que l’utilisation du calcul de la deduction naturel est plus efficace que les tables de vérités. Ca demande un peu d’explication (parceque dans le pire des cas….) et c’est un peu étonnant car cette question de l’efficacité n’est pas mentionner pour le sat solving qui est ce qui est utiliser dans la pratique, enfin pour le bounded model checking en tout cas (évidement sans transformer de Tseitin, ca ne veut pas dire grand-chose…)

Le programme est, je trouve, peu disert sur les justifcations de l’introduction de ce formalisme (pourquoi tant de haine apres tout ?).
S’agit il simplement de mentionner le programme de Hilbert et de recommander la lecture de Logicomix (bonne chose en soit de mon point de vue) ? Faut il mentionner l’isomorphisme de Curry Howard ? (vu que le programme semble avoir été rédiger au moins partiellement par des COQins, ca semblerait naturel, mais bon sans logique intuitioniste c'est un peu hazardeux)

Sinon d’un point de vue pratique, pour avoir une meilleur idée de l’incarnation de ce programme en MPI, combien d’heures de cours et de TP sont consacrés à 6.1, 6.2 et 6.3 ?

Messages : 78

Inscription : 24 juil. 2015 09:44

Profil de l'utilisateur : Enseignant (CPGE)

Re: Question sur le programe MPI: la logique

Message par JB Bianquis » 15 mars 2023 20:57

Beaucoup de questions extrêmement pertinentes, que les profs de MPI ont été amenés à se poser cette année ! Dans certains cas il y a une réponse claire et non ambiguë, dans d'autres moins. Je vais commencer par celles auxquelles il est facile de répondre.

Pour les questions de complexité, il y a un chapitre sur les classes de complexité, et un sur la décidabilité (c'est la partie 9 du programme officiel). On n'introduit pas les machines de Turing donc c'est légèrement avec les mains, mais ce n'est pas très gênant (on admet la NP-complétude de SAT, le reste peut se faire assez proprement).
La résolution de 2SAT en temps linéaire par recherche des composantes fortement connexes est également au programme, mais elle est dans la partie sur les graphes (algorithme de Kosaraju). Les clauses de Horn on va dire que c'est un exercice classique, mais pas au programme (et je ne l'ai pas fait cette année, par exemple).
Pour les réductions à SAT, j'ai fait le coloriage de graphe et le Sudoku (bon, c'est un peu la même chose) en première année, et évidemment on en fait plein quand on parle de problèmes NP-complets (mais on ne les code pas forcément).
Écrire un SAT solver et lire un DIMACS, je pense que beaucoup de gens l'ont fait (c'est mon cas, en première année), mais ce n'est pas exigible.
La transformée de Tseitin et l'équisatisfiabilité c'est un peu pareil : on est plus ou moins obligé de le faire quand on montre que 3SAT est NP-complet (seule la NP-complétude de SAT est au programme), mais le programme ne la mentionne pas explicitement. Typiquement, les élèves n'ont pas à connaître le nom.
Pour le sujet XENS 2016 c'est assez clair : en MPI c'est entièrement du cours de mon point de vue (ce qui ne veut pas dire que tous les élèves de MPI seraient capables de traiter l'intégralité du sujet en 4h !).

Pour la bonne façon d'expliquer à nos élèves qu'une disjonction vide est fausse et une conjonction vide est vraie, c'est de regarder l'élément neutre pour « et » et pour « ou ». Mais c'est parce qu'ils font beaucoup de maths à côté, je ne dis pas que c'est la meilleure manière dans l'absolu.

J'essaierai de répondre au reste quand j'aurai le temps.
Professeur d'informatique - Lycée du Parc

Messages : 711

Inscription : 01 sept. 2008 16:49

Profil de l'utilisateur : Professionnel

Re: Question sur le programe MPI: la logique

Message par Wilfried.kro » 20 mars 2023 10:44

Merci beaucoup pour ces premieres reponses.
Pour la bonne façon d'expliquer à nos élèves qu'une disjonction vide est fausse et une conjonction vide est vraie, c'est de regarder l'élément neutre pour « et » et pour « ou ».
C'est ce que je fais aussi mais à la reflexion ca merite quand meme explication (enfin à mon avis).

Voici ce qui dit wikipedia à l'entré" empty sum
Allowing a "sum" with only 1 or 0 terms reduces the number of cases to be considered in many mathematical formulas. Such "sums" are natural starting points in induction proofs, as well as in algorithms. For these reasons, the "empty sum is zero" extension is standard practice in mathematics and computer programming (assuming the domain has a zero element).
En y pensant je pense qu'il faut insiter sur le coté "standard pratice" et faire remarquer que ca marche tout autant sans (eg si une clause n'a qu'un literal et que ce literal s'avalue à False, la clause est fausse, pas la peine "d'enlever le literal" pour le savoir) mais que l'algo est plus lourd.

Bien sur si on definie generalise les connecteurs binaires ayant un element neutre en des operateurs d'arité n entiere par recurence ca va marcher, mais dans ce cas la il faudrait definir ainsi la syntaxe de la logique propositionelle. Par ailleurs je pense que personne ne veut voir des choses ressemblant de pres ou de loins à une equivalence entre un connecteur et une constante.

A la reflexion, factorielle est un exemple d'utilisation de produit nul (!0) que tout le monde connait.

Je coupe peut etre les cheveux en quatre ceci dit.
W.

Répondre