JE D'EGO, le blog personnel d'Arthur Milchior

Aller au contenu | Aller au menu | Aller à la recherche

jeudi, mai 18 2017

Conférence scientifique informatique

Je ne comprend pas les discours éducatifs live sans interactions. Vraiment, plus je vieilli, plus ça m'insupporte. Ainsi, en master, j'ai décidé d'arrêter d'aller en cours, comme beaucoup de mes camarades de classes. Et mes notes se sont considérablement amélioré. Certes, il est possible que ça soit parce qu'en master j'avais le choix de mes cours et prenait les plus intéressants. Mais je pense que le fait de lire, aller à son rythme, revenir en arrière si besoin, c'est cool. Alors qu'avec un cours, on peut pas. Certes, on a pu noter le cours, ou avoir les notes de cours, mais le prof n'arrête pas de parler pendant qu'on cherche.

Je ne dis pas qu'il faut arrêter les cours, si ça aide certains, tant mieux. Mais je suis bien incapable de comprendre qu'ils soient obligatoire. J'espère que je m'en rappellerai quand(si ?) je serai responsable d'un cours, et que je m'assurerai que tout ce qui est au programme se trouve dans un document texte accessible aux élèves qui le veulent. Malheureusement, je n'ai enseigné qu'un seul cours, et je n'étais pas responsable de ce cours là, je n'ai donc pas pu appliquer ce principe.

Je ne dis pas qu'il faut arrêter l'enseignement en face à face. Parce que parfois, c'est pratique de pouvoir poser des questions. Je n'ai pas de doute sur l'utilité des travaux dirigés et travaux pratiques quand l'enseignant-e et l'étudiant-e ont une réelle interaction. Ou quand il faut du matériel que l'étudiant-e n'a pas à sa disposition chez lui. C'est le cas pour les sciences expérimentales ou l'art de manière évidentes. Mais ça peut aussi être le cas en informatique, au moins tant que les étudiants ne savent pas utiliser ssh, pour leur permettre d'avoir un ordinateur directement utilisable pour la programmation, sans avoir besoin de faire toute l'installation eux/elles-même.


Tout ça pour dire. Je déteste les conférences. J'ai l'impression d'être revenu à l'époque où j'étais en cours. Certes, personne ne me flique. Mais si mon labo à accepter de débourser plusieurs centaines d'euros pour m'y envoyer, je me sens quand même une obligation de présence. De même que je me sens une obligation de prendre les résidences étudiantes, le train le plus tôt, pour éviter d'augmenter la facture[1]. J'en profite pour signaler ce qui me semble être une incohérence. Le train de 20 heures est en général moins cher que celui de 14 heures. Ça peut arriver à faire une centaine d'euros de différence. Donc je prend souvent le train de retour super tard. Ce qui me force à diner sur le lieu de mission. Mais comme la mission est finie, le dîner au restaurant ne m'est pas remboursé. Donc, si je voulais vraiment éviter de débourser un restaurant, il faudrait que je fasse payer 100€ de plus au labo. Pas moyen de leur faire payer juste 85 € de plus, c'est à dire «train pas cher, et un repas supplémentaire».

Retournons sur les conférences. S'il est implicitement considéré qu'il est bon que je me tienne au courant des divers sujets qui intéressent les chercheurs aujourd'hui, et de comment ils avancent, le labo pourrait aussi bien m'indiquer que j'ai le devoir d'aller à la bibliothèque, et de feuilleter régulièrement les intros des papiers de quelques journaux de recherche. Ils y gagneraient beaucoup de sous, et j'aurai probablement l'impression de plus comprendre.

Sauf qu'en réalité, personne ne me demande d'écouter, personne ne vérifie si j'écoute ou comprend. Ce qu'on me demande c'est de publier. Histoire de montrer que le laboratoire a des gens qui font effectivement de la recherche, et améliorer les résultats d'évaluation du laboratoire. Et puisqu'en informatique, les publications sont mieux vues en conférence qu'en journal, il vaut mieux publier en conférence. Et pour avoir mon article dans les annales de la conférence, il faut que je sois à la conférence. Donc que j'y parle.

En vrai, puisque le but est d'être publié, je pourrai bien ne pas venir, ne pas y parler, pour l'évaluation, ça ne changerait rien. Sauf que pour être publié, il faut s'inscrire à la conférence. Celle où je suis coûte 300 francs Suisses, environ 290€. Et encore, pour ce prix là, je n'ai même pas de copie papier des annales. Ce que je regrette beaucoup, vu que j'ai une grande affection pour le papier, et qu'avec un texte de moi dedans, je suis un peu attristé de ne pas l'avoir. (Mais je suis vraiment pas prêt à mettre cette presque centaine d'euros dans un livre, moi qui achète presque tout mes livres d'occasions).

Notons en passant, pour ceux qui ne connaitraient pas le monde de la recherche, vous avez bien lu. Pour être publié, il faut payer. Enfin, officiellement on paye la conférence, qui a certainement des frais, puisque durant trois jours on a des croissants, du café, du thé, ainsi que toute la logistique qu'il faut pour tenir des salles de conférences propres. Et puis, pour avoir une copie papier du livre où on est publié, il faut payer aussi.

Pour autant que je sache, les conférences ont deux avantages sur les journeaux. D'abord, elles sont plus rapide, alors qu'un article journal peut passer plusieurs années entre le premier envoi au journal et sa mise sous presse (et ceux, même si c'est une presse électronique, vu que certains journaux n'ont plus de versions papier, mais continue de publier le même nombre de page chaque années). Pour moi, cet argument n'a aucun sens. Rien n'empêche d'utiliser les méthodes des conférences: texte de taille limité, sans preuves, avec que les grandes idées; en faire une version journal, sans forcer les gens à bouger et payer. Après tout, si le but était vraiment d'avoir une bonne présentation, les referee devraient évaluer la présentation: l'orateur/trice filmé en train de répéter sa présentation. Mais la qualité d'un texte de 12 ou 15 pages n'indique pas si l'orateur/trice saura s'adapter au public de la conférence. Ou tout simplement si l'orateur saura s'exprimer dans un anglais à peu près compréhensible. Je ne dis pas un anglais soutenu et de grande qualité. Mais au moins assez articulé, et pas trop rapide, histoire que les mots puissent être saisis par les gens n'ayant pas l'habitude de son accent. Malheureusement, il y a beaucoup de talks où je n'arrive pas à suivre, non pas parce que c'est techniquement compliqué, mais parce que je ne comprend qu'un mot sur trois. Et encore, je le comprend car c'est un mot marqué sur les slides. (Si au moins tout était écrit sur les slides, je pourrai lire, mais il parait que ça ne se fait pas !) En fait, je ne reste dans la salle que pour une unique raison: que l'orateur/trice, ne parle pas devant une salle vide. Comme ça, par réciprocité, je ne parle pas non plus devant une salle vide.

Le deuxième avantage, c'est que ça permet aux chercheurs de se rencontrer. Il parait. Parce que, honnêtement, j'ai aucune idée de comment aborder un-e chercheur/se; je suis plutôt timide, pas sûr de bien respecter les conventions sociales - il n'y a pas de guides de bonnes manières en conférences. Et en général, quand je parle à un-e chercheur/se en conf, soit je le/la connaissais déjà (en personne, ou par son travail que j'ai lu et eu le temps de comprendre), soit parce que quelqu'un d'autre à initier la conversation; que ça soit une connaissance en commun ou parce que la personne vient me voir. À noter que, vu le nombre de gens que je vois autour de moi, poser sur leur ordinateur, pendant la pause café où je rédige ce morceau du billet, je ne suis probablement pas le seul à ne pas être là pour parler à des inconnus.

Note

[1] Et accessoirement parce que, comme les remboursements prennent parfois des mois à arriver, ça m'évite de creuser mon compte en banque de ces centaines d'euros.

dimanche, septembre 25 2016

Deux petits énervements lié à ma recherche

Un petit post pour faire part de deux énervements que j'ai dans ma recherche. Normalement, j'espère que ça sera compréhensible si vous avez au moins un niveau BAC S, pourvu que vous ne soyez pas allergique aux mathématiques[1] et que vous ayez déjà vu le fait qu'un nombre, quand on l'écrit, c'est rien d'autre qu'une suite de chiffre, où la position est importante. Et qu'un nombre peut avoir une infinité de chiffre après la virgule[2].

D'abord, j'ai du mal avec le fait qu'on parle de vecteur pour un tuple d'élément qui n'est même pas un espace vectoriel. Pour moi, un vecteur d'entier positif, ça s'appelle un uplet. Même si je dirai vecteur dans mes papiers, parce que je préfère éviter qu'on me refuse un papier car j'utilise une notation sensée et pas une notation standard.


Je pense que je ne vous apprendrai rien si je vous dis que 7, 07 et 007 représentent le même nombre. Un entier positif naturel, égal à 7, ou a 10x0+7 ou encore à 10²x0+10x0+7. Ces trois écritures représentant ce que signifie, mathématiquement, 7, 07 et 007, qui sont trois mots différents. Je peux rajouter aussi que ce nombre est aussi égal à 6,9999... avec une infinité de 9 à droite. C'est peut-être un sujet de jeu/étonnement/débat pour les débutants en math, ou certains qui utilisent des définitions non standard des écritures des nombres, mais c'est juste une application du fait que 7, c'est la limite, quand n tend vers l'infini, de 6+(somme pour i allant de 1 à n de 9*10 puissance -i)[3]. Je sais que j'avais été très surpris quand, au collège je crois, la prof nous avait dit:
% 6,9999... = 1x 6,9999...= ((10-1)/9)x6,9999.... = ((10-1)6,9999...)/9 = (69,999999...-6,999999...)/9 = 63/9 = 7.

Dans mon travail, je m'intéresse énormément à l'écriture des nombres. Ou plus précisément, pour certains ensemble de nombre, à regarder l'ensemble des écritures des nombres de cet ensemble. C'est ce qu'on appelle un Language de Réels, LR. Un language, c'est un ensemble de mot. Ici, il se trouve que ces mots sont des nombres, représentés comme une suite de chiffre. C'est un peu confusant au début, mais on s'y fait.

Puisqu'on regarde des langages qui est un ensemble de représentation d'un ensemble de nombre, si mon language contient 7 on sait automatiquement qu'il contient aussi 07 et 007. Ou plus précisément, puisque je lis des réels, s'il contient 7,0000... on sait qu'il contient 07,000... et et 007,0000... et aussi 6,99999.... et 06,999... Bref, mon language aura de bonnes propriétés, on pourra faire de joli mathématiques dessus et obtenir une théorie relativement sympathique. Pour dire ça autrement, un Langage de Réel est un langage qui contient toutes les représentation des nombres d'un sous ensemble des réels positif.


Sauf que !

Je suis informaticien moi, pas mathématicien. Alors, cette théorie, c'est bien jolie, mais qu'est-ce que j'en fais ? comment je me débrouille avec ? Je veux écrire des algorithmes, je veux faire des choses avec ces langages de nombres. Des trucs d'apparences simples pour commencer. Par exemple, j'aimerai savoir dire si l'ensemble des nombres d'un Langage de Réel est de la forme {n x k | k un entier positif}. Et dans ce cas, trouver la valeur de n. Et mine de rien, c'est un problème compliqué, et aujourd'hui, je n'ai aucune idée de comment le résoudre efficacement. Et dire que je sais le résoudre inefficacement n'intéressera pas grand monde.

Et en fait, même si j'ai un algorithme qui est capable de répondre à cette question, comment est-ce que je sais si mon entrée est effectivement un Langage de Réel ? Car il se peut que l'algorithme utilise la jolie théorie développée pour les Langages de Réels, et que sur un autre langage, ça fasse une opération interdite, comme une division par 0 ou tenter d'accéder à quelque chose qui n'existe pas[4]. Le souci est qu'à ma connaissance, aucun des auteurs ayant considéré les Languages de Réels n'a pensé à dire comment vérifier si un langage est bien un Langage de Réel. J'ai trouvé une solution, mais elle est parfois plus compliqué[5] que l'algorithme qui m'intéresse à la base[6]. C'est quand même dommage d'avoir un algorithme où l'on doit passer plus de temps à vérifier si l'entrée satisfait les hypothèse qu'à effectivement appliquer l'algorithme.

Alors parfois, j'ai envie de dire: tant pis, n'utilisons pas cette bonne théorie, et prenons n'importe quel langage en entrée. C'est rare que ça marche, car avoir une théorie pour m'appuyer, c'est utile, mais dans quelques cas, ça passe. Et parfois Pas Du Tout. Ainsi, si je choisi l'ensemble des multiples de 7, j'aurai le droit d'avoir un langage qui contient {7, 014, 0000021, 28, 000000000000000000000000000000000000035, ...} et aussi {7, 14, 21, 28, 000000000000000000000000000000000000035, ...}. On pourrait dire que le nombre de 0 à gauche du ième nombre code une suite hyper compliqué, bien plus compliqué que le problème que je veux résoudre. Et puis, un truc tout bête: je ne serai même plus capable de regarder simplement si deux Langages de Réels sont égaux en regardant simplement si leur description est la même, puisque l'égalité de la syntaxe serait différente de l'égalité qui m'intéresse vraiment, celle des nombres. Et mine de rien, avoir le droit à utiliser le symbole =, c'est souvent utile en informatique.


Ce qui est un peu énervant, c'est que tout ce que je viens de vous dire - Enfin tout sauf le fait que je n'aime pas le mot vecteur - je dois l'écrire. Et l'écrire de manière plus formelle, en anglais et en mathématique. Parce que vu que j'ai décidé de quitter un peu la théorie habituelle, je dois justifier pourquoi je considère les Languages de Réels, mais aussi que je m'autorise des Langages qui ne sont pas «de Réels». Et c'est long[7].

Notes

[1] Je suppose qu'à force de parler d'autres choses que de science, j'ai pu avoir des lecteurs qui n'aiment pas les mathématiques. Aussi étrange que cette idée me soit, soyez les bienvenus !

[2] Et pour ceux qui s'y connaissent un peu en info théorique, niveau L2 à Paris Diderot, quand je parlerai de langage, en réalité je veux parler de l'automate minimal déterministe qui accepte ce langage.

[3] Je n'ai pas trouvé de plugin dotclear pour les maths la dernière fois que j'ai cherché, hélas

[4] nullPointerException

[5] quadratique

[6] ici, un algorithme linéaire

[7] Mais pas 200 pages non plus

vendredi, juin 10 2016

Soutenance de thèse

Comme il est de coutume, programmation de soutenance de thèse implique invitation à ladite soutenance. Ergo, cet événement, ce nouveau one-man-show, moins drôle et plus intellectuel que le dernier. Ceci aura lieu salle 0011 du bâtiment Sophie Germain, 8 Place Aurélie Nemours, 75013 Paris

Merci de me dire si vous venez, d'abord pour le pot, après 16h00 et aussi pour que je m'assure que vous puissiez rentrer dans le bâtiment. Vous pouvez le faire par commentaire sur ce billet ou sur l'événement facebook


-Si vous vous intéresser aux résultats présenté dans cette thèse (énoncé ci-dessous), sachez que je serai prêt aussi prêt à vous présenter ces résultats n'importe quand (par exemple au séminaire automate du 17 juin, où j'ai un quart d'heure de plus et où je peux me concentrer sur un résultat)
-Où alors, et ça concernera probablement plus de monde, vous pensez que vous ne comprendrez rien à ce dont la thèse peut parler. Si ça vous amuse de voir à quoi ressemble une soutenance de thèse, que vous pensez que c'est important de venir, etc... n'hésitez pas à venir. Mais si comme moi, quand on vous parle de recherche (et que ce n'est pas votre domaine), vous avez surtout l'impression d'entendre des gens parler une langue étrangère, que seul quelques inconnus au premier rang sont capable de distinguer d'un discours de médecin de molière, alors n'hésitez surtout pas à ne pas venir. Ou alors venez au pot, qui devrait être approximativement vers 16 heures. (Ami-e-s vegan, il y aura des gâteaux pour vous, et je m’assurerai de les marquer comme tels)


Ce manuscrit traite de la logique du premier ordre avec la relation d'ordre et les prédicats modulaires, notée FO<,mod. La classe des ensembles réguliers, c'est à dire des ensembles FO<,mod-définissables, est la classe des ensembles acceptés par un automate en base 1. C'est aussi la plus grande classe C d'ensembles telle que FOC ne définisse que des langages réguliers. Il est donc naturel de s'intéresser à cette logique et nous donnons dans ce manuscrit de nouvelles caractérisations des ensembles réguliers. Nous montrons que les ensembles réguliers ont une caractérisation en terme d'ensembles de dimension inférieure et en terme de périodicité. Nous montrons que si un ensemble R est définissable dans l'arithmétique de Presburger, alors il est régulier si et seulement si toutes les fonctions unaires FO<,R-définissable sont réguliers. Cette caractérisation nous sert à montrer que le fragment maximal C de l'arithmétique de Presburger tel que la satisfiabilité de FO<,C soit décidable est la classe des ensembles réguliers. Similairement, la satisfiabilité de la logique du premier ordre sur les mots avec la fonction successeur et une fonction unaire f croissante est indécidable dès que n-f(n) est non borné. Si f est non interprété, la logique du premier ordre avec la fonction successeur et f est indécidable sur les entiers. Enfin, on donne un algorithme en temps linéaire prenant en entrée un automate A en base b supérieur à 1 et acceptant si et seulement si A accepte un ensemble régulier. Un deuxième algorithme, en temps quasi-cubique, retourne alors une FO<,mod-formule qui définit l'ensemble d'entiers accepté par l'automate.

P.S: pour rappel, il y a deux ans j'écrivais ça sur la soutenance de thèse.

mercredi, avril 6 2016

Comment faire un article de 200 pages de long ?

"Comment faire un article de 200 pages de long ?" Voilà une question que tu ne t'étais jamais posé, et à laquelle j'ai la possibilité d'apporter des éléments de réponses. Parce que oui, j'ai un papier qui fait maintenant 198 pages de long, mais on va arrondir, ce n'est pas comme si j'étais certain que deux pages supplémentaires ne pousseront pas.

Entendons nous bien d'abord sur l'énoncé du problème. Il ne s'agit pas de faire un livre, un recueil, un manuscrit, un cours. Il s'agit juste de faire un article, c'est à dire un texte qui présente entre un et quatre résultats principaux, disons, tous relié entre eux de manière forte.

D'abord, pour faire un article aussi long, il faut prévoir plusieurs années. Tu ne peux pas espérer faire un article de 200 pages en 3 mois. Même en un an, c'est compliqué. Il faut laisser le temps à l'article de pousser.

Je vais commencer par les astuces les plus classique : la mise en page. Évitez le pacquage fullpage, qui met autant de texte que possible par page. Ici, ça réduit l'article à 172 pages. On peut même garder le format par défaut de LaTeX, le format letter (dans ce cas, je pars sur du 213 pages, mais je trouve ça exagéré).

En fait, toutes les autres astuces de mise en pages que je pourrai vous donner son ridicules, parce qu'elles ne font gagner que quelques pages à chaque fois. Par exemple, utiliser des chapitres au lieu d'utiliser des parties, ce qui vous offre un saut de page, ça fait gagner environ une demi-page par chapitre. Ici j'ai 7 chapitres, ce n'est pas trois pages et demi qui me permettront d'atteindre les 200 pages. En plus, ça veut dire que vous aurez beau rajouter quelques lignes par-ci par-là paragraphe, si ce n'est pas absorbé par la mise en page de LaTeX qui évite que les paragraphes s'étendent sur plusieurs pages, alors ça poussera la fin du chapitre de quelques lignes vers le bas, mais ne poussera pas le chapitre suivant une page plus loin.

Quelques autres petites pages à gagner: avoir une table des matières, avec chapitre, section, sous-sections et sous-sous-section. Là je gagne 3 pages. Plus une page pour la table des matières des figures. Avoir un index, c'est bien aussi. Mais il faut du courage, car pour faire 3 pages d'index, il faut penser, régulièrement, à taper \index quand on introduit des nouvelles notations. En ayant un index à deux colonne, pour faire 3 pages, je parle ici de 238 éléments indexés !


Passons aux choses sérieuse, ce qui fait le gros des 200 pages.

Déjà, ne présentez pas qu'un seul résultat, mais présentez plusieurs variantes. Ainsi, un résultat qui s'applique à 10 cas différent, c'est bien. Si en plus il y a des subtiles différences selon chaque cas, c'est mieux. Ainsi, on peut souvent dire dans les lemmes "dans les 5 premiers cas, la preuve est ceci... sinon il suffit de rajouter l'hypothèse que truc, et se rapporter aux premiers cas". Mais en général, il faudra dire plutôt "dans les cas 1, 4 et 5, ceci, sinon cela", ça permet de faire une petite énumération. Surtout si au lieu d'être numéroté, les cas ont des noms, ça prend plus de place (mais il faut avouer, que c'est aussi plus compréhensible si les noms sont parlants.) Le mieux étant quand même quand au lieu de faire une disjonction de cas dans un lemme, on peut faire une section pour un cas, et une autre pour l'autre cas. Attention cependant, il faut que ces sections soient petite par rapport à la taille du papier, sinon ça devient deux papiers distincts ! Ici, 15 pages en plus pour traiter trois cas particulier, c'est à peu près raisonnable au vu de la taille du papier. Il ne faut cependant pas oublier que, 15 pages, en vrai, c'est la taille d'un grand papier de conférence.

La règle précédente peut se reformuler en: généraliser vos résultats autant que possible. Ainsi, pourquoi travailler sur les entiers naturels si on peut travailler sur les relatifs ? Réduire le cas des entiers relatifs vers les naturels me prend dix pages, et hop, déjà 5% de mon papier. Pour justifier de ne pas regarder que les naturels, c'est pratique si la réduction des relatifs vers les naturels te pousse à considérer un problème plus général que le problème que tu aurais intuitivement voulu résoudre sur les naturels.

Tu peux aussi prouver un résultat. Puis partir de ce résultat pour en prouver un autre. Et ainsi de suite. Tout ces résultats n'ont pas forcément grand chose à voir entre eux, il faut simplement que tout les résultats intermédiaires servent à prouver le résultat final et prétendre que ce qui t'intéresse est le résultat final.

Une autre règle pratique est d'utiliser pleins d'outils mathématiques différents. Comme il faut introduire tous les objets mathématiques que tu utilises, tu peux gagner 7 autres pages en disant tout ce qu'il faut savoir sur les automates, les monoide, l'écriture d'un nombre dans une base, les graphes, la logique, et le temps de calcul. Ceci dit, il faut admettre que cette règle n'avait pas vraiment besoin d'être énoncé, quand un papier fait 200 pages, il arrive assez rapidement que plein de domaines soit utilisés.

Toutes ces règles poussent à en considérer une autre : ne pas être avare sur les exemples. Si on a suivi les règles précédentes, il y a plein de cas différents considéré. À chaque fois qu'un exemple arrive naturellement, on peut à la place mettre plusieurs exemples pour illustrer les petites nuances selon le cas considérés. Bien sûr, l'exemple doit surtout montrer la ressemblance entre ces différents cas, sans ces ressemblance, on ne pourrait pas justifier de traiter tous les cas à la fois.


Fini de jouer, il reste encore plus d'une centaine de page à créer, et là, on a fini le tour des trucs simples.

Le VRAI truc, c'est d'utiliser des objets compliqués. Pas compliqué théoriquement, ni au sens informatique. Ainsi, l'objet principal dont mes preuves se servent est un quadruplet, composé d'un entier, un uplet d'entier, un vecteur et une matrice. Informatiquement, c'est très simple de représenter tout ça, un quadruplet c'est juste un type produit. Un uplet d'entier, c'est juste un tableau. Un mathématicien n'aura, en général, pas de mal à comprendre ce qu'est un quadruplet. C'est juste compliqué parce que, à chaque fois que tu dois prouver que deux éléments sont égaux, il faut prouver 4 égalités. En pratique, beaucoup de ces égalités sont triviales à prouver, donc tu ne gagnes pas beaucoup de pages comme ça, mais a fait toujours quelques lignes en plus par-ci par-là. Mais si en plus tu veux faire un ordre lexicographique sur le quadruplet, là tu gagnes beaucoup de pages, à considérer les cas selon quel est la première des 4 positions qui est plus petite dans un quadruplet que dans l'autre.

Le dernier point, je suis forcé d'imaginer, en vrai, j'ai des ordres plus compliqués que l'ordre lexicographique. Et surtout, j'ai des relations d'ordre, des relations d'ordres sur ces relations d'ordre, et même un lemme qui ordonne les relations d'ordre sur les relations d'ordre. Donc dans tous les textes où je parle d'ordre, je suis forcé de préciser l'ordre considéré. Dire "le plus grand élément selon <" ou "une L-section commençante[1]", c'est toujours quelques symboles de gagner. Ça ne rajoute pas beaucoup de pages, mais c'est pour le sport !

Mais le plus compliqué de cet objet, est qu'il ne s'agit pas de n'importe quel quadruplet. Il s'agit exactement d'un quadruplet qui vérifie 21 axiomes. Et là, crois moi, tu en gagnes, des dizaines de pages de preuves, quand tu veux prouver que certains objets que tu définis explicitement respecte ces 21 axiomes !


J'ai une dernière recommandation: avoir des formules très longues. Évitez les formules avec indices/exposants sur les indices/exposants, c'est assez illisible. En plus, les indices/exposants ne prennent pas beaucoup de place. Quand prouver que deux termes sont égaux se fait par une dizaine d'étape, et que les formules font trois lignes de longs, tu arrives facilement à prendre une page par égalité.

Attention cependant, quand tu utilises des formules de trois lignes de long, il faut que TOUT dans les trois lignes sert. Peut-être pas à chaque étape, mais au moins une fois durant l'égalité, sinon tu vas vouloir simplifier le tout et retirer la partie de la formule qui ne change jamais.

Cette dernière astuce est assez dure à utiliser en pratique, il est très rare que tu tombes naturellement sur des formules de trois ligne de long que tu aies envie de démontrer. En général, tu veux prouver des égalités qui ont un sens précis, explicable en français/anglais. Et si c'est humainement explicable, la formule est en général plus long.

Une technique qui marche bien pour obtenir des longues formules: Avoir dans ses formules plusieurs sommes de séquences, parfois imbriqués. Quand les preuves sont par induction, comme il est désagréable de faire des inductions imbriqué, chaque imbrication de sommes pourra justifier un lemme à part. De même, deux sommes côte à côte pourront aussi justifier deux lemmes, un pour chaque somme, et un corollaire pour montrer comment mélanger les deux lemmes.

Souvent, le but est de montrer qu'une somme de termes x_n est égal à une somme de terme y_n. On peut donc dans l'induction faire une somme partielle sur les x_n et une somme partielle sur les y_n, ce qui prend plus de place. Et si en plus x_n s'exprime en fonction de y_n et de y_{n+1}, (et donc que y_n s'exprime en fonction de x_{n-1} et x_n), il vaut mieux passer par un troisième terme intermédiaire, avec un terme dépendant d'une part de x_n et de y_n, et une partie avec un terme dépendant de x_n et de y_{n+1}.


Au cas où ça ne soit pas clair, tout ce qui précède consiste bien sûr en une liste de chose que je déconseille. Je n'encourage personne à écrire un papier de plus de 50 pages. Théoriquement, une seule faute fait tout s'effondrer, c'est mentalement un exercice périlleux. Même si, comme je l'ai déjà expliqué, je ne pense pas que ça puisse arriver, car quand on en arrive à faire tant de page, on a nécessairement une idée très clair de ce qui se passe, de comment tout s'agence, et dans ce cas, une petite faute fera juste prendre une déviation, mais ne bloquera pas tout accès au but final.

Et surtout, je suis bien conscient que la lecture d'un tel papier demande plus d'un mois de boulot, et que presque personne ne va le faire à moins que le résultat soit vraiment fondamental. Mais si vous avez démontré que P est (égal/différent) de NP, je ne pense pas que tu aies besoin de mes conseils (en fait, je ne pense pas que tu aies besoin de mes conseils).

Le seul vrai truc que je peux donner, et qui est déjà bien connu, c'est de faire des fichiers séparés. Mon article fait 20471 lignes de LaTeX (avec un fill-column à 70), et avant que je découpe en plusieurs morceau, ça finissait à prendre plus d'une seconde à Emacs de faire une sauvegarde (ce qui est ennuyeux car je fais le raccourci clavier pour sauvegarder à peu près à chaque fois que mes doigts arrêtent de taper.) De même, quand on édite une partie, compiler juste la partie qu'on édite, en commentant l'input des autres parties, peut faire gagner du temps (mais ça signifie que toutes les \newcommand doivent être fait dans le préambule). D'ailleurs, faites PLEIN de \newcommand (ici, j'en compte 391), après tout, le but c'était de faire un pdf long, pas un fichier latex long. Et factoriser ce qui revient souvent en commande, c'est bien !

Note

[1] je ne connaissais pas la traduction française de Upper-set avant aujourd'hui

vendredi, janvier 15 2016

Les booléens

Dans Général ou particulier je parlais d'une difficulté que j'avais pour avoir des résultats généraux. Je vais donner un exemple de plus, qui a fait bien rire un de mes directeurs de thèse. La question est: comment traiter les valeurs booléennes en logique du premier ordre ?

En effet, parfois, je créé des formules logiques explicitement et j'ai besoin dans ma formule de rajouter «Vrai» ou «Faux». La solution la plus simple théoriquement, c'est de dire qu'en plus de «Non F», «F ou F», «il existe x tel que F» et «R(t,...,t)»[1] je rajoute comme construction de base de ma logique «Vrai». Comme ça, pas de question à se poser, j'ai effectivement le droit de dire «Vrai» et «Faux» (enfin, «Non Vrai»). Le seul souci c'est que mes dizaines de preuves par induction sur les formules logiques devraient alors considérer la formule «Vrai». Ce qui est d'autant moins intéressant que dans la quasi-totalité des cas, ce traitement serait trivial.

L'autre solution est de dire que la formule atomique «Vrai» est implicitement supprimée dès qu'elle apparait. Ainsi «(Vrai et F)=(F et Vrai)=F», «(Vrai ou F)=(F ou Vrai)=Vrai», «(Non Non Vrai)=Vrai», «(Non Vrai et F)=(F et Non Vrai)=(Non Vrai)», «(Non Vrai ou F)=(F ou Non Vrai)=F». Ce qui fait que je n'ai plus besoin de regarder Vrai dans mes inductions... Sauf dans le cas de la formule atomique «Vrai», qui ne peut pas se simplifier. Ce qui amène à l'absurdité que chaque preuve serait une disjonction de la forme «Si F est Vrai, ou Non Vrai alors c'est trivial, sinon par induction sur F».

Pour éviter ça, une solution classique est de dire que «Vrai» est du sucre syntaxique pour «0=0», ou pour «x=x», ou pour «\forall x. x=x», selon qu'on ait accès aux constantes, à une variable libre x, ou aux quantifications respectivement. Seulement, il se trouve qu'il m'arrive de me restreindre à des logiques sans symbole de constantes(Parce que sur les réels, cela change l'expressivité), sans quantificateurs (quand je m'intéresse à la satisfiabilité de formules), ou sans quantificateurs (car ça simplifie énormément les preuves, et que j'ai la chance de considérer des logiques qui acceptent l'élimination des quantificateurs). Donc aucune de ces solutions ne fonctionnent pour moi.

Mais, le pire, de mon point de vue, c'est que aucune ne fonctionne uniquement à cause de la volonté d'avoir un formalisme unifié. En effet, je ne considère aucune logique sans quanticateurs, ni constantes, ni variables libres, pour la bonne raison que cette logique ne permettrait de ne rien exprimer.

Je fais de la théorie des modèles (finis), je tiens à vous dire que je n'envie pas ceux qui font de la théorie de la preuve, je crois qu'à côté d'eux, mais problèmes font figure de petit joueurs.

Note

[1] où F sont des formules, R un prédicat et t des termes.

dimanche, décembre 27 2015

Exemple d'exemple

Un défaut que j'ai (avais?) en rédaction mathématique, c'est que les exemples ne sont pas une notion naturelle pour moi. Il a fallu que mes directeurs insistent beaucoup avant que je prenne spontanément le réflexe de rajouter des exemples.

Eh bien, c'est peut être drôlement pratique pour le lecteur. Mais pour moi... Je vais vous donner quelques exemples d'exemples.

Même si je ne fais pas de géométrie à proprement parler, j'ai des résultats qui considèrent des relations sur des entiers ou sur des réels. Autrement dit, des sous-ensemble de vecteur de nombres entiers ou naturel. Or, quand on a des vecteurs, il est naturel de faire un dessin pour montrer l'ensemble de points/vecteurs/tuples(c'est la même chose pour moi). Sauf qu'avec des résultats qui ne deviennent intéressant qu'à partir de la 3ème dimension, j'en suis venu à rêver que je mettais un plan d'origami dans mon papier pour le lecteur. D'ailleurs, le résultat est encore assez simple, mais pour montrer par l'exemple que c'est vrai en dimension plus grande, là, ça devient marrant. Personnellement, mon intuition disparaît en dimension 4.

Un autre problème que j'ai, c'est trouver un petit exemple. Parce que, parfois, les exemples que je trouve sont: soit triviaux, soit gigantesque. Ou dans le meilleur des cas, ça se découpe en plusieurs exemples, un pour chaque cas, et ça donne une impression de succession d'exemple qui retardent simplement la preuve.

Et encore, là, c'est quand je trouve comment découper. Parce que, je réalise que j'ai un cas encore plus marrant. J'ai un papier où j'ai un algorithme, et cet algorithme commence par tester une condition. Si x=y alors ceci, sinon cela. Il faut donc que je trouve un cas où x=y pour illustrer ceci, et un cas où x est différent de y pour illustrer cela. Et j'ai beau me creuser la tête, je ne trouve pas de cas où x est différent de y. Et pas moyen de prouver que c'est impossible. Or, soit j'ai pas d'exemple, et c'est pas bien. Soit c'est impossible, et dans ce cas, même si mon algorithme est mathématiquement correcte, il est moche, puisqu'il fait un test inutile et possède une partie de code jamais exécuté. Sauf que, ce qui est encore plus marrant, c'est que si ça se trouve, x est toujours égal à y, mais c'est dur à prouver. Donc pour éviter l'algorithme moche, je me retrouverai paradoxalement à allonger la preuve mathématique.

Dans l'absolu, si c'était une propriété très intéressante, que x=y, ça pourrait valoir le coup. Mais vu que c'est un résultat technique. Y a conflit.


D'un autre côté, je n'ai cherché d'exemple pour x différent de y qu'en dimension 2. J'ai fait des petits dessins (mentaux), mais je n'ai rien trouvé. Peut-être que c'est parce que je n'ai pas cherché en dimension 3. Et dans ce cas, je me retrouve avec tout ces problèmes combinés. Ça serait marrant.

vendredi, décembre 11 2015

Induction étrange

Je suis tombé récemment sur deux systèmes de preuves que je n'avais jamais vu, il me semble. Je ne sais pas s'il est possible de les simplifier ou pas. Je m'en vais donc les donner, histoire de partager ces curiosités.

Soit E un ensemble fini. Soit P une propriété que je veux prouver. Soit Q(S) une propriété que je veux prouver où S est un sous-ensemble de E. Je suis capable de prouver:

  • Q(ensemble vide)
  • Pour tout ensemble S dans E tel que Q(S), alors:
    • Soit il existe un surensemble S' stricte de S dans E tel que Q(S')
    • soit P

On peut donc montrer P par induction sur un entier i en disant que soit il existe un ensemble Ei de cardinal au moins i tel que Q(E), soit P est vrai. Ce que je trouve perturbant car, d'une part, P ne dépend pas de i, et d'autre part, il existe un entier i (le cardinal de E) tel que je sais que qu'il n'existe pas d'ensemble Ei.

Pour dire ça autrement, j'ai deux propriétés presque indépendantes, tel que je fais une induction sur l'une, que je sais être fausse au bout d'un moment, pour prouver un truc qui ne dépend pas de l'induction.


Mon autre résultat est probablement moins bizarre, à part que je ne l'avais jamais vu en vrai, jamais vu utiliser ailleurs que dans des preuves coq, preuves qui nécessitent de s'intéresser à la base, aux axiomes.

Je veux créer un grand entier. J'ai deux algorithmes A(E) et B(x), où E est un ensemble fini d'entiers et x un truc. L'algorithme A génère un ensemble un élément n(E), et B(n(E)) génère un entier n'appartenant pas à E. Ensuite, je fais A(E U {x}), et je recommence. Il me reste alors qu'à appliquer alternativement A et B jusqu'à obtenir un élément assez grand.

Bon, dis comme ça, c'est clair que je pourrais dire que AoB(E) génère simplement un entier n'appartenant pas à E. Mais intuitivement, c'est vraiment deux algorithme très différents, qui n'ont rien à faire ensemble. D'ailleurs, ce n'est même pas des algorithmes, officiellement c'est des preuves qui sont accessoirement constructive.


En passant, je me suis fait refuser le papier d'où je sors ça. Parait qu'il y a de la place pour améliorer la rédaction. Alors même que le résultat est jugé intéressant (mais pas révolutionnaire non plus), non trivial, dans l'optique du journal, et sans faute mathématiques pour autant que les referee puissent dire. Je pense en écrivant ce billet que je vois un peu mieux pour quoi.

mardi, juin 30 2015

Rédaction mathématiques

Je suis actuellement doctorant, en 3ème année. Autant dire que je rédige, que j'écris. Beaucoup. Plus précisément que je réécris. Sans arrêt. La thèse un peu, mais indirectement. En vrai, je réécris des articles de recherche, jusqu'à ce qu'ils soient lisible. Comme ça, ça fera de la matières pour le tapuscrit de thèse, et les retours des referee permettront d'anticiper les retours des rapporteurs de la thèse.

Sauf que c'est très dur d'avoir un article lisible. C'est très long de relire. J'ai un article en cours de rédaction qui fait 79 pages. Pour un seul résultat. Bon, 79 pages, ce n'est pas que l'algorithme et sa preuve, c'est aussi introduction, définitions, conclusion, bibliographie, table des matières (avec 61 sections/sous-sections/sous-sous-section, je me suis permis) et index (124 entrées). Je vous déconseille très fortement l'article de 79 pages. Vraiment. C'est pas ce genre de pratique qui va me permettre d'avoir une bibliographie bien fournie.

Quand j'ai fini la 1ère version de ce papier, à l'été 2013, il faisait 30 pages. Et depuis, j'ai l'impression de n'avoir fondamentalement rien rajouté. À part 49 pages d'explications, d'exemples, d'illustrations. Et cette inflation n'est pas finie.


Ok, j'exagère quand je dis qu'il y a un seul résultat, en vrai j'ai deux algorithmes. Parce que, un truc marrant, c'est que j'utilise uniquement des preuve constructive. Or une preuve constructive, c'est un algorithme. Donc j'ai deux algorithmes, dont un en temps exponentiel, qui est la preuve de mon algorithme en temps O(n log(n)). Ce qui nécessite donc en plus que je rajoute des explications du style «Ne vous en faites pas, ce lemme introduit un algorithme A en temps exponentiel alors que ce papier promet que le problème est décidé en temps O(n log(n)). Mais il n'y a pas de contradiction puisque l'algorithme A n'est pas utilisé dans la décision du problème. Mais non, ça ne veut pas dire que l'algorithme A ne sert à rien.»


Voici quelques illustrations des problèmes que j'ai: «Tu dis que la preuve de ton lemme est claire par une simple étude de cas. Mais c'est pas si claire.»
Puis une semaine plus tard, après avoir rédigé les 5 cas:
«C'est pas la peine de faire une preuve si longue, c'est totalement trivial.»

Ou encore «Met une introduction à ta section. Et ce paragraphe ne sert à rien.»

Pour tout dire, je dois être tellement illisible que mon directeur de thèse m'a récemment demandé en LaTeX si j'utilisais les labels.

De manière moins anecdotique, j'ai 119 calculs qui font plusieurs lignes. Par exemple, dans celui mis dans l'imageespace.png, j'ai une liste d'équivalences. Eh bien, ce n'est pas simple de savoir comment le présenter. Tel que c'est fait, j'ai choisi d'avoir plein d'espace, qui ne rendent pas forcément les lignes très lisible. Mais dans l'image suivantediagonale.png, ce n'est pas simple de voir exactement ce qui change d'une ligne à l'autre.

dimanche, avril 5 2015

Général ou Particuliers

Pour une raison que j'ignore, j'ai un problème qui se pose dans la moitié de mes résultats de recherche. J'ai des résultats très généraux. Voir trop.

Quand je fais des maths, y a deux trucs dont j'ai envie: des preuves compréhensible, et des théorèmes aussi général que possible. Le premier point et le deuxième s'opposent souvent. Par exemple, en analyse, beaucoup de théorème sont enseigné sur les nombres réels, et les complexes, mais sont vrai en fait sur n'importe quel espace métrique, voir n'importe quel espace topologique. Sauf que c'est beaucoup plus simple de dire qu'on a une fonction continue de R dans R que de dire qu'on a une fonction continue, puisque ça nécessite de définir ce qu’est une mesure, un ensemble mesurable et une fonction mesurable. Et qu'en pratique, si tu dis «R», ça a toute les bonnes propriété, et qu'on a plus d'intuition si on dit que «|x-y|<e» plutôt que si on reformule en terme de suite d'ensemble ouvert.

Bien sûr, la notion topologique est extrêmement intéressante, elle permet d'aller loin, de traiter des cas différents. Mais elle est plus difficile à comprendre. Et souvent[1], tu peux faire la définition sur R puis dire que modulo le changement de formalisme, la même définition marche pour toute topologie.


Il est hors de question de jeter la topologie, ça concerne bien trop de notion. Mais quand tu vas dans des domaines moins joli, tu peux aussi te retrouver avec deux objets très semblable, deux preuves très semblables. Et là, ça devient problématique, est-ce que tu fais deux papiers, ou est-ce que tu en fais qu'un ? Si tu en fais deux, ça double ton nombre de publication, ce qui est bien pour ta carrière. Et puis ça peut être dans deux journaux différents, s'adressant à deux types de personnes différentes, si t'as un peu de chance. Le souci, c'est que c'est un peu «triché», ça augmente inutilement le nombre de papier, si quelqu'un s'intéresse aux deux résultats, tu lui fait prendre plus de temps à te lire deux fois. Et surtout, tu ne mets pas en avant la proximité de ces deux résultats, et souvent, voir que deux choses sont proches peut être scientifiquement très intéressant, car donner des idées pour utiliser un résultat d'un domaine dans l'autre domaine.

Le souci, si tu fais un seul papier, c'est que tu dois expliciter ce qui rapproche les notions, parfois créer ta notation, et donc tes lecteurs ne pourront pas se reposer sur l'intuition qu'ils se sont formés, et auront plus de mal à lire. Surtout si un morceau de preuve est distinct, il faudra retrouver à quoi s'applique un morceau, si on s'intéresse a un des deux cas et qu'on lit le bout de preuve fonctionnant sur l'autre, on peut être perdu. Et en faisant deux papiers, tu évites ça.


Ce problème je l'ai sans arrêt depuis le Master 1. Sauf que c'est jamais que deux cas. Ça serait trop simple.

Mon premier résultat, je cite des gens, ils ont fait trois papiers. Ces trois papiers ont chacun un résultat, et chacun de ses trois résultats utilise la même idée globale. Mon résultat traite en pratique huit cas différents, en généralisant entre autre leur idée. Chacun de ces huit cas demande juste des variations sur des détails de la preuve, mais l'idée globale est la même.

Je dis entre autre, parce que c'est de la logique d'ordre supérieure. Si vous savez pas ce que c'est, c'est pas bien grave. Disons qu'une logique à un ordre. Traditionnellement, on étudie la logique d'ordre 1, parfois celle d'ordre 2, rarement plus. Au delà, on parle de logique d'ordre supérieure. Et bien, il se trouve que des tas de résultat de complexité descriptive on été prouvé pour la logique d'ordre 1, ça a donné lieu a des dizaines de papiers. Puis des gens on montré qu'il y avait des résultats similaires pour la logique d'ordre 2, ce qui a donné lieu à quelques autres papiers. Et devinez quoi: les mêmes résultats sont vrai en logique de n'importe quel ordre. Pourquoi ça n'a pas été montré en même temps, je ne sais pas, peut-être comme je disais, car c'est plus simple en étant moins général. Et puis la logique d'ordre 3 n'intéresse pour ainsi dire personne, par rapport à celle d'ordre un et deux. Encore une fois, le même souci se pose.

Il y a en gros 9 résultats de base dans ce domaine, 3 ont été montré pour l'ordre supérieur, j'ai prouvé que les 9 sont vrais, dont en particulier les trois déjà prouvé. Alors, est-ce que je tente de faire 6 papiers ? Ou un seul ? J'ai tenté un seul. Après, comme j'ai soumis trois fois et est été refusé trois fois [2], la question est purement théorique.


Mais ce n'est pas fini. Depuis 2013, je travaille sur un résultat reliant logique et automate. Et ce résultat vaut pour 16 formalisme logiques différents. 16 n'est pas un nombre magique, ou quoi que ce soit, il a pas de propriété mathématiques spécifique dans ce cas là. J'ai juste compté tout ce que j'ai réussi à faire rentrer dans mes critères, et je suis tombé sur 16. Qui sont tous assez proche les uns des autres.

Ainsi, je travaille sur des formules logiques considérant les ensembles d'entiers, parfois positifs parfois aussi négatifs. En fait, pour traiter le cas général, je dois d'abord le cas des ensembles de nombres positifs, passer d'un cas à l’autre est presque simple[3], donc on pourrait se dire que pour simplifier le papier, qui fait tout de même 63 pages, je pourrais me restreindre au positif, et gagner une dizaine de page. D'un autre côté, il sera impossible de publier le cas avec les nombres négatifs tout seul, il n'est pas assez intéressant pour valoir une publication à lui tout seul.

Alors, dit comme ça, ça a l'air de rien, si vraiment je réduit Z à N[4], alors on peut lire que la partie sur N si ça nous intéresse. Et ça ira. Ça serait beau si c'était le cas. Sauf qu'en fait, quand on considère les sous ensemble de Z, on doit tenir compte de quelques petits détails supplémentaire. Qui ne changent pas fondamentalement la preuve, à part sur un point ou deux. Mais qu'on doit quand même se trimballer dans les notations dans la cinquantaine d'autres pages !

Bon, c'est une petite notation, un indice, c'est pas bien grave.

Mais j'étudie 9 logiques différentes sur N. Plus précisément, c'est toujours de la logique du premier ordre, ce qui change, c'est le vocabulaire, l'ensemble des fonctions et prédicats que je m'autorise. Et aussi l'ensemble des quantificateurs. Ma première étape est de toute façon d'éliminer les quantificateurs, donc je peux me restreindre à voir des logiques sans quantificateurs. Sauf que FO(<,mod), c'est quand même plus joli que \Sigma_0(\N,<,+\N,mod)[5]. C'est plus court, et puis on voit mieux ce que c'est à priori, c'est les formules avec la relation d'ordre et les relations modulaires. Le souci, c'est que j'ai aussi FO(+1,mod) et FO(=N)[6]. Et c'est tout ce que j'ai sans quantificateur. \Sigma_0(<,+N,mod) par exemple, une logique ou on a l'ajout de constante, l'ordre et les prédicats modulaires, mais pas de quantificateurs, n'a pas d'équivalent avec quantificateurs, puisque l'addition de constante permet toujours de définir les constantes quand il y a des quantificateurs, et qu'ici les constantes ne sont pas considérées.

Alors, la question se pose, est-ce que ça vaut le coup de considérer cette logique ? D'un côté elle est pas très intéressante, n'est jamais étudiée pour elle même, n'a pas de propriété aussi intéressante que FO(<,mod), la classe des ensemble régulier. D'un autre côté, le résultat fonctionne, avec (quasi)-exactement la même preuve, alors autant le mettre, si un jour quelqu'un en a besoin, ça sera là, il aura pas à chercher comment adapter mon théorème. Le diable est dans les détails, c'est «quasi», il y a un petit point qui se rajoute un peu partout, qui rajoute une ou deux ligne pour traiter ce cas dans une dizaine de lemme, c'est pas grand chose sur 63 pages, mais quand même...

Mais si je le prend pas, je garde quoi ? Après tout, traiter une seule logique serait bien plus simple, et le lecteur se souviendra plus facilement de ce que signifie FO(<,mod) que de ce que signifie FOV, où V est un vocabulaire qui peut prendre 16 valeurs.

Et si je les gardes tous, comment est-ce que je décris cet ensemble de 16 valeurs ? Je fais la liste exhaustive ? Alors on ne voit pas la logique derrière, et aucun lecteur, même moi, peut se souvenir de la liste par cœur en lisant les 63 pages. Mais si je donne les conditions qui caractérisent ces logiques, alors ça devient compliqué de voir quel est l'ensemble des logiques qui respectent cette caractérisation. Mais ce n'est pas comme si je devais faire le choix une seule fois, sinon, ça serait pas bien grave, je pourrai juste donner la liste une fois, avec sa caractérisation. Mais régulièrement, je dois dire que tel lemme est vrai, car si on suppose que ceci est dans V, alors on sait que cela est dans V, ou alors dire que dans ce cas précis, le lemme se fait comme ceci, sinon comme cela.


Comme conclusion, je dirai juste que j'aimerai bien que c'est vraiment pas un des problèmes les plus compliqués dans la recherche. Mais quand même, ça obsède.

Notes

[1] dans les exercice des premières année d'université

[2] Pas assez clair, pas assez intéressant pour la prestigieuse conférence où c'est soumis

[3] relativement au reste du papier

[4] oui, j'en ai assez, j'utilise les notations mathématique, mais bon, c'était niveau lycée

[5] Désolé, j'ai la flemme de chercher un mod pour les maths

[6] Ici =N correspond à l'ensemble des constantes

jeudi, janvier 1 2015

Quelques remarques sur un article

Je me suis encore fait refuser un papier en conférence, mais je suis content. Pour la première fois, les commentaires étaient précis et me donnaient l'impression d'avoir été lu. D'ailleurs on m'a même conseillé des papiers que je ne connaissais pas et qui étaient pertinent pour mon sujet. En gros, mon résultat méritait publication. Mais une fois totalement réécrit, car c'était (c'est?) illisible.

J'ai 2 directeurs de thèse, et ait principalement travaillé avec l'un. Mon autre directeur de thèse a fini par me faire comprendre un point sur la rédaction qui m'échappaient, alors qu'il semble tout bête en principe: expliquer ce que je fais. En gros, mes résultats étaient mathématiquement corrects (encore que), mais à la manière d'une preuve formelle, à la manière de coq. Mais sans le coté formellement formel. Par exemple, ça ne m'a jamais gêné d'écrire «on suppose sans perte de généralité que b est supérieur ou égal à 4». J’expliquai pourquoi il n'y a pas de «perte de généralité», puisque j'en parle. Mais je ne disais pas pourquoi c'est utile. Ça a été mon déclic, quand mon directeur a lu l'introduction du papier devant moi et m'a demandé pourquoi b est supérieur ou égal[1] à 4, je lui ai expliqué, et il m'a demandé «ce que tu viens de m'expliquer, pourquoi tu ne l'as pas écrit ?».

En fait, il m'a signalé que c'était important, car il pouvait y avoir plusieurs raisons très différentes. -Le résultat serait faux si b valait 2 ou 3, -la démonstration plus complexe, - la démonstration serait totalement fausse. Et quel étape serait fausse pour 3 et vrai pour 4 ? Tout ça, c'est des questions naturelles qu'un lecteur peut se poser: «à quoi ça sert ?», et auxquels je ne répond pas, ou pas directement. Car en fait la réponse était donné, 6 pages plus loin.

Je précise, ici «À quoi ça sert», ce n'est pas «à quoi ça sert dans l'absolu: est-ce que ça va sauver des vies que b soit au moins 4 ?». Non, on fait des maths, on admets que les résultats sont intéressant en soit, avec ou sans application plus tard, on ne sait pas, pour l'instant ce n'est pas la question. Dans le titre, le résumé, l'introduction, j'ai indiqué que j'allais démontrer un théorème, alors on se demande: «à quoi ça sert que b ne soit pas plus petit ou égal à 3 pour démontrer ce théorème». Alors, finalement, j'explique qu'on veut pouvoir avoir 3 entiers distinct entre 0 et b-1, tels qu'il y en ait deux d'entre eux dont la différence soit au moins 2.

Je ne sais pas si c'est clair pour tout le monde, ce que ça veut dire quand j'écris: «b est supérieur ou égal à 4». Une chose qu'on entend souvent quand on fait des math et qu'on parle à des gens dont ce n'est pas le métier, c'est: «Comment une lettre peut être égale à un chiffre ?» La notion de variable pose problème. Et bien, un point que je trouve marrant dans mon domaine, c'est qu'en théorie des langages les chiffres sont des lettres. Par exemple 2015[2] est un mot sur l'alphabet {0,1,2,3,4,5,6,7,8,9} et donc pour nous 2 est une lettre.


Cela fait donc plus d'un mois que je réécris mes documents pour expliquer ce que je fais. Et j'ai donc 3 ans de documents à réécrire. C'est long, plus d'une centaine de page (avant réécriture). Pour vous donner une idée, déjà, je sais écrire «straightforwardly» du 1er coup sans me tromper maintenant ! Et ça, je trouve ça impressionnant. Pour vous donner une autre idée, l'article dont je parle depuis tout à l'heure, il démontre 3 théorèmes. Pour cela j'utilise 39 définitions, des classiques et d'autres que j'introduit pour le papier spécifiquement. J'utilise 49 lemmes, c'est à dire 49 résultats intermédiaires, car contrairement en cours de maths, un théorème se prouve rarement directement. J'utilise 74 équations, et encore je ne compte que celles assez importantes pour mériter une ligne à elle seule, et pas les petites formules dans les phrases. J'ai un découpage en 45 sections, sous-sections et sous-sous-sections. J'ai aussi 154 entrées d'index, car mon directeur m'a fait remarquer, à juste titre je le crains, que je ne pouvais pas lui demander de retenir tant de dizaines de notations par cœur. J'utilise aussi 13 citations, 13 papiers dont les travaux m'ont inspirés, s'ils n'ont pas fondés le domaine. Le tout en 52 pages.

Et c'est là que je me redis que j'aurai du comprendre cette leçon plus tôt. 52 pages pour avoir l'explication entière du résultats, c'est énorme. En conférence, j'avais le droit à 12 pages. Je déteste ça, car supprimer 40 pages, c'est retirer beaucoup d'explications. C'est rendre le papier incompréhensible il me semble. Sauf que non, au contraire, j'aurai du comprendre, que c'est garder l'essence du papier. Certes, je donne un algorithme, que personne ne pourra implémenter sans les détails. Mais les détails, ce n'est pas pour une conférence. Après tout, c'est 5500 lignes de codes et 600 lignes de commentaires en oCaml. C'est énorme.

Dans mes 13 citations, à force de faire de la logique, ça devait arriver. Je met en bibliographie un papier en allemand. Alors que la seule chose que je sache dire en Allemand, je le dois à l'humoriste Yacine, c'est «Das ist die toilette»(sic). Et Yacine en est fier en plus ! Plus précisément, je cite Presburger. C'est à dire que j'indique le nom du papier dans lequel a été défini ce qui s'appelle aujourd'hui la Logique de Presburger, même si je n'ai jamais lu ce papier moi même, et même si son résultat a depuis pu être amélioré par d'autres. Autant dire que je connais le nom de Presburger, mais rien de lui. Ça fait 3 ans que je travaille sur le domaine qu'il a initié sans avoir eu de curiosité sur sa personne. Je dis ça car ça m'a fait bizarre, au détour d'un clic par accident sur wikipédia, j'ai découvert qu'il est mort en camp de concentration. Je ne sais même pas pourquoi ça m'a donné un coup, après tout, je supposais qu'il était mort depuis un bon moment, vu que je ne connais personne qui ne l'est connu. Alors qu'en général, les grands mathématiciens vivant ou récemment décédé, j'ai toujours un prof qui a une anecdote à nous raconter à leurs sujets. En plus, ce n'est pas comme Galois, un génie à l'histoire romantique et romançable, et dont finalement je ne connais pas vraiment le travail mathématique. Presburger, même si je n'ai lu qu'une traduction de sa démonstration dans un bouquin, j'ai pu comprendre sa trouvaille et l'adapter à mon travail, ça fait une proximité mentale. En fait, je perçois les mathématiciens que je cite comme des collègues, j'utilise leur travail quand j'en ai besoin. C'est donc un collègue mort en camp.

Ça m'amuse[3] d'écrire ce dernier paragraphe, car je sais que mon professeur d'initiation à l'informatique théorique nous avait mis dans son cours quelques biographies. À l'époque je ne comprenais pas trop. Ceci dit, j'étais touché qu'il parle de Turing et de sa mort. Que ça ne soit pas passé sous silence. J'arrivais à l'université, une époque où je ne disais pas aussi facilement que j'étais homo, et ça rassurait. Et bien aujourd'hui que je fais de la recherche, je comprend mieux l'envie de mettre une mini bio d'autres chercheurs. Surtout dans un domaine aussi récent.

Notes

[1] C'est bizarre d'écrire en toute lettres «supérieur ou égal», alors que ça se dit bien. Je devrais peut-être dire: est au moins 4

[2] En passant, bonne année

[3] en me relisant, je me rend compte de l'horreur de cette expression. Pour moi et pour d'autres matheux que je connaisse, «ça m'amuse» ne signifie pas que ça me fasse rire. Loin de là. Juste que je trouve ça particulièrement intéressant, loin d'être anodin. Ça attire mon attention de manière intellectuellement plaisante.

vendredi, octobre 24 2014

Rédaction de la thèse et choix des notations

Tiens, exceptionnellement, je vais parler de math, de mon boulot, ça fait longtemps.

Je suis en phase où je réalise 2 trucs. D'abord, que même si c'est bien d'avoir des résultats - et j'en ai - ça ne fait pas une thèse. Donc qu'il va falloir que je la rédige. Et surtout que je rende le tout cohérent.

J'ai uniquement des résultats en rapport avec la logique sur des nombres. Sauf qu'une logique ça a plein de paramètres:

  • Parfois c'est de la logique d'ordre 1, monadique existentielle, parfois de la logique d'ordre supérieur, voire de la logique d'ordre variable ! Et puis parfois je rajoute mêmes des opérateurs. de point fixe, de clôture transitive, déterministe ou non, et même alternant.
  • En plus, mes modèles sont soit finis, en particulier sur les mots, soit sur les entiers, donc infinis, soit carrément sur les réels.
  • Quant aux prédicats que je m'autorise, c'est simple, je ne prend jamais quelque chose de plus compliqué que l'addition. Je peux prendre les modulos, la relation d'ordre, le successeur d'un nombre... Enfin, quand je dis jamais, j'ai un résultat où j'ai aussi la multiplication, mais c'est une exception. Et puis la fonction «Partie entière» mais c'est pratiquement la même chose que l'ordre. Et puis les flèches de Knuth, mais ça c'est un accident, j'ai démontré qu'on pouvait l'avoir à partir de +1 et d'une fonction non interprétée.
  • Oui, parce que j'ai certes des prédicats connus. Mais j'ai aussi des prédicats dont l'interprétation n'est pas fixée. Et puis aussi des prédicats non interprétés. J'y reviendrai plus tard.

Et puis j'ai plusieurs types de résultats:

  • De la complexité descriptive, c'est à dire que je relie une logique et une difficulté de calcul. Dans mon cas les calcul qu'on peut faire avec un temps limité par une tour d'exponentielle.
  • Des maths presque pures, c'est à dire que je décris de manière exhaustive certains types d'objets, des relations sur les entiers où les réels. Ou alors quand je ne peux pas les décrire, au moins je dis «Regardez, à partir de ça, qui est tout simple, je peux créer des trucs très complexes. Alors peut-être que ce premier objet n'était pas si simple qu'il en a l'air.
  • Certains sont de la logique qui parle de la logique, ce qu'on appelle la «Définissabilité de la définissabilité», c'est à dire qu'on crée une formule dans une logique L qui dit «tel objet est définissable dans une logique L'». Même qu'en général, L est égal à L'.
  • Enfin j'ai des résultats informatiques, quand même ! En particulier, quelques résultats d'indécidabilité - cas où j'ai prouvé qu'un ordinateur ne peut pas répondre à une question. En général, je dis «on ne peut pas savoir si une formule de la logique L est vraie ou non». Ou au contraire des résultats de décidabilité. C'est à dire que je donne un algorithme, parfois même je le code, qui résout un problème donné. En l'occurence j'ai principalement des «Est-ce que tel objet est définissable dans une logique».

Donc, non seulement, il faut que je dise quel est le rapport entre tous ça. Et le fait que «c'est les idées qui me sont passées par la tête, parfois soufflées pas mon directeur de thèse, et que j'ai réussi à démontrer» ça ne fait pas une vraie raison. Mais surtout, il faut que je trouve une notation cohérente pour TOUT ça. Et ça, c'est le 2ème point que je suis en train de réaliser.


J'ai pratiquement utilisé une notation différente par papier. Ce qui semble très bizarre à la relecture. D'abord car quand je reprend un papier des mois après je peux croire qu'une notation signifie ce qu'elle voulait dire dans un autre papier. Encore que la confusion soit rare. Mais surtout, j'ai l'envie d'unifier les notations. Or c'est une mauvaise idée, en effet j'ai un papier qui parle d'opérateurs, donc ma notation indique systématiquement quels sont les opérateurs que je m'autorise - en particulier, ça peut être «aucun opérateur». Mais dans tous les autres papiers où je n'ai jamais d'opérateurs, je ne vais pas mettre sans arrêt la notation «aucun opérateur», ça serait lourd inutilement.

Bon, là, c'est simple. Voyons un autre exemple. Mettons que je travaille en logique du premier ordre (abrégé en «FO») avec l'addition et un symbole R. Dans un cas je dis, «si R vérifie tel propriétés, alors on une formule f dans FO+,R qui vérifie tel propriété». Là, R se comporte comme un paramètre, en fait, c'est comme si on avait une infinité de théorèmes pour chaque valeur possible de R. Mais dans un autre cas, je dis «On a une formule f de FO+,R tel que R vérifie tel propriété si et seulement si f vérifie tel propriété». R est une variable comme une autre du théorème. La première différence, c'est que tout d'un coup, f est fixé, elle ne peut plus dépendre de R. Ça c'est habituel, c'est une inversion de l'ordre des quantificateurs. Mais on réalise qu'en fait, ce n'est pas «f» qui vérifie la propriété, «f» c'est une formule, et elle n'a pas de sens tant que R n'a pas de sens. Donc il faudrait dire: «On a une formule f de FO+,R telle que R vérifie tel propriété si et seulement si l'interprétation de f vérifie tel propriété», mais alors il faudrait aussi parler de l'interprétation de R par souci de cohérence. Et je me retrouve à dire «On a une formule f de FO+,R tel que l'interprétation de R vérifie tel propriété si et seulement si l'interprétation de f vérifie tel propriété». Et je le fais, car c'est le seul moyen d'être vraiment correct. Sauf que, voilà, si je veux être cohérent dans mes notations sur tous les papiers, mon premier résultat devrait être «si l'interprétation de R vérifie telle propriété, alors on une formule f dans FO+,R dont l'interprétation vérifie telle propriété». Et pour le coup, j'ai inutilement complexifié le premier résultat, car j'ai rajouté la distinction artificielle entre R et son interprétation. Artificielle, car je n'ai jamais tenté de distinguer + de son interprétation, qui est toujours l'addition.

En fait, le problème est que je dois faire comprendre que la signification de R peut varier énormément. R peut être considéré comme une variable, comme l'entrée d'un algorithme. Donc «si tu me donnes R, et qu'il vérifie tel propriété, alors je peux calculer ce truc» (ou au contraire, il est impossible de le calculer). Ça peut aussi être une valeur qu'on cherche à caractériser, comme dans «R est un nombre pair si et seulement si il existe un entier n tel que 2n=R».Et puis ça peut être une variable au sens mathématique, on cherche à caractériser les valeurs de R pour lesquelles une propriété est vraie. Voire simplement savoir s'il existe une telle valeur, auquel cas c'est comme si R était existentiellement quantifié. Mais ça serait lourd d'introduire explicitement R en tant que variable, et de le quantifier, car dans la plupart des papiers, cette notion n'est définie que pour les objets de premier ordre, et que ces objets n'ont pas le même statut que R.

Pour faire une comparaison, quand je dis «Cette logique est indécidable» je montre que pour toute machine de Turing, il existe une formule qui la simule. Mais je ne vais pas écrire «∃ f: formule» alors que f contiendra elle même des quantificateurs existentiels ∃, ça ne rendrait le tout que plus confus.


Je ne sais pas quoi conclure.

dimanche, juin 23 2013

Le doctorat

- 3 ans, ce n'est pas assez pour faire une thèse.
- T'as besoin de plus de temps pour la finir, tu prend le tardis et l'apporte au jour de ta soutenance.
- Et c'est bien la preuve qu'à ce moment là, tu es docteur.

Sinon, un autre copain "complimente" ma coiffure. "Arthur, je crois que tes cheveux sont Turing-complet".

mercredi, mars 9 2011

Logic in Computer Science and in Europe

C'est avec un grand regret que j'ai le malheur de vous annoncer la mort de mes notes sur la logique d'ordre supérieure et d'ordre variable en théorie des modèles finis, version LICS[1] suite au refus des conférenciers de me faire payer un voyage à Toronto.

Il a donc laissé la place à la version pour CSL[2] qui a simplement changé de mise en page.

Leurs parent, l'article entier, est toujours présent.

Notes

[1] Logic In Computer Science

[2] Computer Science Logic

lundi, août 2 2010

Base de donnée temporelles

Je ne dénoncerai pas les gens concernés, mais je suis très impressionné ! 3 auteurs ont publié des articles ensembles. On trouve 4 article au même titre sur le même sujet, avec un nombre variable de pages (12 en 92 et 93, 29 en février 96 et 30 en aout 96), et la version de 93 porte le nom fichier92.pdf et cite un article de 95 écrit par deux des trois auteurs.

Si je revois ce monsieur, je lui demanderai où se trouve sa machine à voyager dans le temps.

samedi, juillet 24 2010

Langage reconnaissable

Personne aurait une machine à voyager dans le temps ? Ça me permettrait de décider la hiérarchie arithmétique.

Au premier niveau de la hiérarchie, je lance un calcul, il affichera des tas de réponses puis s'arrêtera, la dernière réponse sera la bonne, mais je dois attendre la fin des temps pour être sur que c'est bien la dernière réponse. Je pourrais alors revenir aujourd'hui, donner la réponse à mon ordinateur et passer au deuxième niveau... Si je fais ça suffisamment de fois je dois pouvoir monter tout en haut de la hiérarchie arithmétique !

Arthur Rainbow, qui commence par de la recherche raisonnable au lieu de s'attaquer tout de suite à la hiérarchie analytique !

lundi, juillet 19 2010

P, NP, et au dessus

Je pense que ma nouvelle citation fétiche va être :

Prouver la réponse à P vs NP, c'est très simple ! Je l'ai déjà fait 7 fois !

Sinon, j'ai une propriété avec des conditions sur les classes de fonctions non closes par composition, quelqu'un pourrait aller lui dire qu'elle n'était pas sensé s'attaquer à la classes des polynômes(qui sont clos par compositions) ?

En plus, j'ai une propriété que je pensais triviale, elle est tout le temps vraie, sauf sur dans certains précis, où elle devient fausse (sauf dans certains cas spéciaux bien défini où étrangement elle redevient vraie)... J'aimerai dire à mes théorème qu'en générales je leur demande de ce comporter plus gentiment.

Dernière question: si je deviens fou, c'est qui le responsable de l'accident de travail ?

mercredi, avril 1 2009

Une question triviardu.

Ce billet fait suite à C'est joli un graphe hamiltonien, non?. Si vous voulez voir l'avancement, la dernière version est ici, appuyez sur le graphe, puis sur la touches page down/Pg.Suiv de votre clavier. Mais ce n'est pas le sujet.

Je ne comprend pas mon professeur, il a un don. Il est capable de mélanger des questions d'une facilité déconcertante et des questions qui peuvent à priori prendre des années de calculs. Voici un exemple qui n'amusera que les matheux.

Soit G un graphe avec 64 noeuds[1], combien y a t-il de circuit hamiltonien, et ont-ils tous le même nombre d'arête?

Si vous avez éclaté de rire, bravo, j'attends au moins la moitié de la réponse en commentaire (si vous avez les deux moitié, merci de m'expliquer comment faire).

Si la question vous laisse de marbre, voici une petite explication de texte. Si on connait le nombre de circuit, on sait si il y en a au moins un. Or en général sur un graphe, savoir si il existe au moins un circuit hamiltonien est NP-complet[2]. Donc en général, connaitre le nombre de circuit Hamiltonien appartient à #P. Mais par définition un circuit hamiltonien passe une fois et une seule par chaque nœud et boucle. Il y a donc autant d'arête que de nœuds, soit 64.

Donc, combien il y en a: j'en sais rien, je peux pas tous vous les donner, ni les compter dans un temps humain (IE, pas des millions d'année), mais je peux vous assurer qu'ils ont tous le même nombre d'arête.

PS: je vous rassure, ceci n'a rien à voir avec mon spectacle. N'ayez pas peur.

Notes

[1] pour la description exacte, voir le billet précédant, C'est joli un graphe hamiltonien, non?

[2] IE très très dur à trouver