Hétérotopos

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

Le lambda-calcul pour les nuls

arton31.jpgL’obs­cur fonc­tion­naire du dépar­te­ment Jeu­nesse & Sports de la mai­rie d’Alfort­ville qui, en ce magni­fi­que mois d’août 1982, avait décidé de met­tre une ving­taine de Thom­son TO7-70 en libre accès, afin de per­met­tre aux jeu­nes désœu­vrés que nous étions de venir goû­ter aux joies de l’infor­ma­ti­que per­son­nelle nais­sante, se dou­tait-il de l’avan­tage déci­sif qu’allait nous pro­cu­rer cette ini­tia­tive ?

Car aussi incroya­ble que cela puisse vous paraî­tre, à vous qui n’étiez peut-être pas encore nés et qui lisez aujourd’hui ces lignes sur l’écran d’un iBook G4 con­necté en Wifi à l’ADSL, un ordi­na­teur indi­vi­duel, en 1982, ça ne ser­vait … à rien ! Et si les publi­ci­tai­res ten­taient déses­pé­ré­ment de per­sua­der Mon­sieur que pour moins de 3000 FF[1], les 16Ko de mémoire vive de la bête l’aide­raient à orga­ni­ser sa col­lec­tion de films sur cas­set­tes Beta­max tan­dis que Madame aurait enfin les moyens de tenir une comp­ta­bi­lité fami­liale stricte, ces machi­nes venues du futur se trans­for­maient rapi­de­ment en con­so­les de jeu, avant de finir au pla­card, vous savez comme sont les enfants, cette année il veut jouer de la gui­tare.

Pour nous autres cepen­dant, jeu­nes pré­pu­bè­res bou­ton­neux aux dents ruti­lan­tes, guère encore per­tur­bés par la com­plexité de la nature fémi­nine, l’ordi­na­teur appa­rais­sait comme le pro­lon­ge­ment natu­rel de nos jeux de cons­truc­tion grâce à une fonc­tion­na­lité, qui ne sem­blait guère inté­res­ser que nous : la pro­gram­ma­tion.

Pro­gram­mez, pro­gram­mez, il en res­tera bien quel­que chose…

Le con­cept de pro­gram­ma­tion est plu­tôt sim­ple à sai­sir : il s’agit essen­tiel­le­ment d’orga­ni­ser une séquence d’ins­truc­tions qui, implan­tées dans la mémoire d’un ordi­na­teur, le mène­ront à trai­ter des don­nées et à four­nir un résul­tat. Et pour tout dire, la pra­ti­que n’en est guère plus com­plexe : une fois com­blé, par l’appren­tis­sage d’un lan­gage[2], le fossé séman­ti­que et syn­taxi­que qui sépare l’homme de la machine, le codage des ins­truc­tions devient une tâche assez répé­ti­tive et ingrate sou­vent délais­sée, dans les labo­ra­toi­res, aux « peti­tes mains » de l’infor­ma­ti­que.

eniac-f22a8.jpgIl est donc impor­tant de remar­quer que la par­tie à la fois la plus inté­res­sante et la plus ardue de la pro­gram­ma­tion se situe en amont de la machine et n’a même aucun rap­port avec le lan­gage employé. Toute la dif­fi­culté réside dans la capa­cité de l’esprit à appré­hen­der, pour un pro­gramme donné, l’ensem­ble des situa­tions sus­cep­ti­bles de se pré­sen­ter à l’entrée de façon à ne jamais lais­ser le pro­gramme démuni. C’est le pro­pos de l’algo­rith­mi­que[3], une forme de pro­gram­ma­tion théo­ri­que « papier-crayon » qui s’opère soit dans un pseudo-lan­gage, soit sous forme de dia­gramme synop­ti­que et qui per­met, lorsqu’elle est menée avec atten­tion et rigueur, de s’assu­rer qu’aucune éven­tua­lité n’est res­tée incon­si­dé­rée.

Cepen­dant, la taille d’un algo­rithme étant inti­me­ment liée à la com­plexité de la situa­tion qu’il est chargé de décom­po­ser, rien ne per­met d’affir­mer avec cer­ti­tude qu’un algo­rithme com­plexe ne con­tient pas d’erreurs d’inat­ten­tion, de « bou­cles sans fin » ou autres chausse-trap­pes. Qui plus est, serait-il par­fai­te­ment écrit qu’il en exis­te­rait peut-être un autre plus « élé­gant », ou tout sim­ple­ment plus éco­nome en res­sour­ces, un para­mè­tre impor­tant puisqu’il se tra­duit, en bout de chaîne, par une con­som­ma­tion inu­tile d’élec­tri­cité. Y a-t-il donc un moyen de s’assu­rer qu’un pro­gramme fonc­tionne inté­gra­le­ment, sans erreurs et sans « plan­tage » ? Comme sou­vent, seu­les les mathé­ma­ti­ques peu­vent pré­ten­dre répon­dre à ce genre de ques­tion.

Can­toooo­réééé, woooo­hoooo….

Au début du XXème siè­cle, les mathé­ma­ti­ques tra­ver­sent une période de crise : les tra­vaux de l’alle­mand Georg Can­tor sur la Théo­rie dite « naïve » des Ensem­bles cons­ti­tuent cer­tes une avan­cée majeure, mais sou­lè­vent éga­le­ment un cer­tain nom­bre de para­doxes logi­ques[4] , créant une situa­tion insup­por­ta­ble pour une dis­ci­pline qui se veut aussi rigou­reuse. Il appa­raît alors indis­pen­sa­ble de refon­der entiè­re­ment les mathé­ma­ti­ques sur des bases inat­ta­qua­bles.

hilbert-b92dc.jpgLa pre­mière étape de ce tra­vail – ou tout du moins l’énoncé de la néces­sité de ce tra­vail – incombe his­to­ri­que­ment à l’illus­tre mathé­ma­ti­cien alle­mand David Hil­bert. Le 8 août 1900, lors du Con­grès Inter­na­tio­nal de Mathé­ma­ti­ques de Paris, il sou­met à la com­mu­nauté des mathé­ma­ti­ciens une série de 23 pro­blè­mes ouverts[5] dont le deuxième s’énonce ainsi : « Démon­trer la con­sis­tance des axio­mes de l’arith­mé­ti­que ». Le pro­blème est tout sauf sim­ple : l’objec­tif est de mon­trer que la con­sis­tance[6] de l’arith­mé­ti­que est démon­tra­ble à par­tir des seuls axio­mes[7] de l’arith­mé­ti­que. Dans le pro­lon­ge­ment de cette inter­ro­ga­tion, Hil­bert va rapi­de­ment éta­blir en 1920 un pro­gramme de recher­che, qui porte son nom, et dans lequel il s’agira de mon­trer qu’un sys­tème for­mel qui fonde l’arith­mé­ti­que est non seu­le­ment con­sis­tant, mais qui plus est com­plet[8]. En clair, il s’agit de mon­trer que dans un tel sys­tème, toute pro­po­si­tion vraie est démon­tra­ble en un nom­bre fini d’opé­ra­tions, et donc qu’il existe, pour toute pro­po­si­tion logi­que don­née, une pro­cé­dure effec­tive per­met­tant de savoir si elle est vraie ou fausse : c’est ce qu’Hil­bert appelle le « Ent­schei­dung­spro­blem », ou pro­blème de la déci­sion.

La voie ouverte par Hil­bert va diri­ger toute la recher­che mathé­ma­ti­ques du pre­mier quart du XXème siè­cle, et four­nir un ensem­ble de résul­tats fon­da­men­taux déci­sifs. Mais c’est sur­tout ce der­nier cri­tère de « déci­da­bi­lité » qui sera le plus déter­mi­nant pour l’infor­ma­ti­que nais­sante, après le véri­ta­ble coup de ton­nerre que cons­ti­tuera, en 1931, la démons­tra­tion par Kurt Gödel de son Théo­rème d’Incom­plé­tude.

Le point aveu­gle ? Kurt l’a vu !

kurt-48139.jpgCar con­trai­re­ment à ce qu’espé­raient démon­trer les for­ma­lis­tes[9], un sys­tème for­mel suf­fi­sam­ment éla­boré pour expri­mer l’arith­mé­ti­que pré­sente un point aveu­gle : sa pro­pre con­sis­tance ! C’est ce que mon­tre Gödel, dans une démons­tra­tion célè­bre[10] qui n’uti­lise que l’arith­mé­ti­que fon­da­men­tale, et dont la con­clu­sion peut être expri­mée en ces ter­mes :



Tout sys­tème for­mel con­sis­tant, et sus­cep­ti­ble de for­ma­li­ser l’arith­mé­ti­que, est incom­plet. Aucun sys­tème for­mel con­sis­tant, et capa­ble de défi­nir l’arith­mé­ti­que des entiers, ne peut prou­ver sa pro­pre con­sis­tance.

L’impact de ce théo­rème est immense, aussi bien d’un point de vue mathé­ma­ti­que que phi­lo­so­phi­que. Tout d’abord, il impli­que qu’il existe en arith­mé­ti­que des énon­cés dont on ne saura peut-être jamais démon­trer s’ils sont vrais ou faux. Il induit donc qu’à l’inté­rieur d’un sys­tème, l’ensem­ble des véri­tés est plus impor­tant que l’ensem­ble de ce qui est démon­tra­ble, que le péri­mè­tre de la réa­lité y est supé­rieur à celui de la con­nais­sance. Le cons­tat n’est cepen­dant pas aussi som­bre qu’il en a l’air : de la même manière qu’il est pos­si­ble de démon­trer la con­sis­tance de l’arith­mé­ti­que à par­tir d’un sys­tème plus grand[11], il signi­fie sim­ple­ment que la rai­son ne peut pas se per­met­tre de n’être que pro­cé­du­rière, mais doit éga­le­ment être créa­tive et ori­gi­nale, de façon à trou­ver les axio­mes nou­veaux qui per­met­tront de répon­dre aux indé­mon­tra­bles d’un sys­tème donné.

Après avoir été sérieu­se­ment mal­mené par le Théo­rème d’Incom­plé­tude de Gödel, le pro­gramme de Hil­bert rece­vra le coup de grâce en 1936 lors­que deux logi­ciens[12], l’amé­ri­cain Alonzo Church et le bri­tan­ni­que Alan Turing, démon­tre­ront l’un après l’autre et en uti­li­sant deux métho­des effec­ti­ves dif­fé­ren­tes, l’exis­tence d’un pro­blème indé­ci­da­ble en arith­mé­ti­que, met­tant ainsi un terme au pro­blème de la déci­sion de Hil­bert. Mais pour ce faire, ils met­tront au point deux nou­veaux con­cepts fon­da­men­taux en infor­ma­ti­que théo­ri­que : le lambda cal­cul pour Church et la Machine de Turing pour… Turing !

Rage against Turing

machine-e68e8.jpgLe pro­pos n’est pas ici d’entrer dans une des­crip­tion pré­cise du con­cept de Machine de Turing[13]. Il nous suf­fit de com­pren­dre qu’il s’agit d’une machine « vir­tuelle » rudi­men­taire, essen­tiel­le­ment com­po­sée d’une tête de lec­ture/écri­ture, d’un ruban de papier infini divisé en cases qui con­tien­nent les don­nées à trai­ter et con­tien­dront les résul­tats obte­nus, et qu’elle est capa­ble d’exé­cu­ter méca­ni­que­ment un jeu d’ins­truc­tions très sim­ples (avan­cer d’une case, lire la case, si la case con­tient 0, écrire 1 et recu­ler d’une case, etc. ). La véri­ta­ble beauté de ce con­cept réside dans le fait qu’il sub­sti­tue à l’idée ancienne d’algo­rithme[14] un objet mathé­ma­ti­que rigou­reu­se­ment défini, sub­sti­tuant au con­cept intui­tif de cal­cu­la­bi­lité effec­tive le con­cept mathé­ma­ti­que­ment for­mel de cal­cu­la­bi­lité. Cepen­dant, une Machine de Turing ne pou­vant réa­li­ser qu’un seul algo­rithme, Turing détaille immé­dia­te­ment le con­cept de Machine de Turing Uni­ver­selle pour laquelle le fameux jeu d’ins­truc­tions peut être lui-même codé au début de la bande de papier, ren­dant ainsi une même machine capa­ble d’effec­tuer n’importe quel algo­rithme. Quel est son objec­tif ?

Notons tout d’abord qu’il est aisé d’ima­gi­ner une Machine de Turing qui ne s’arrête jamais (un algo­rithme qui bou­cle / un ordi­na­teur qui plante), avec par exem­ple le jeu d’ins­truc­tions sui­vant : lire la case / écrire 0 / avan­cer d’une case. Or la Thèse de Church-Turing con­siste en sub­stance à affir­mer que tout – bon - algo­rithme est des­crip­ti­ble par une Machine de Turing qui s’arrête tou­jours. Turing sou­haite donc régler le Pro­blème de l’Arrêt , en cher­chant une Machine A qui accep­te­rait, comme don­nées, le jeu d’ins­truc­tions d’une Machine B : la Machine A est-elle capa­ble de dire si la Machine B va s’arrê­ter ? Dans une élé­gante démons­tra­tion qui n’uti­lise que la logi­que for­melle, Turing en arrive à la con­clu­sion qu’un tel pro­blème est indé­ci­da­ble : il n’existe pas d’algo­rithme capa­ble d’affir­mer qu’un autre algo­rithme va s’arrê­ter. Par la cor­res­pon­dance qu’il a crée avec les mathé­ma­ti­ques, il résout ainsi l’Ent­schei­dung­spro­blem de Hil­bert, et ouvre la voie à une nou­velle dis­ci­pline, l’infor­ma­ti­que théo­ri­que, qui cher­che à opti­mi­ser les pro­cé­du­res infor­ma­ti­ques déci­da­bles grâce à la Théo­rie de la com­plexité .

Dans le même temps, de l’autre coté de l’Atlan­ti­que, Alonzo Church déve­lop­pait l’équi­va­lent for­mel des Machi­nes de Turing, le lambda-cal­cul, qui n’est qu’une forme cal­cu­la­toire des algo­rith­mes. La théo­rie com­plète de ce for­ma­lisme est bien évi­dem­ment com­plexe, mais sa pra­ti­que est rela­ti­ve­ment sim­ple, et mon pro­pos est ici de vous prou­ver cette sim­pli­cité à l’aide d’un petit jeu, le Jeu des Ser­pents.

Le Jeu des Ser­pents

Les piè­ces du jeu

Voici les ser­pents. Les ser­pents ont tou­jours faim, ils man­gent tout ce qu’ils trou­vent devant eux. Mais les ser­pents sont aussi res­pon­sa­bles, ils savent sur­veiller atten­ti­ve­ment les ser­pents et les œufs. serp1.jpg Voici de vieux ser­pents. Ils sont ras­sa­siés, donc ils ne man­gent plus. Cepen­dant, ils sur­veillent tou­jours avec autant d’atten­tion. serp2.jpg Voici des œufs. Les œufs éclo­sent pour don­ner de nou­veaux nids de ser­pents. serp3.jpg

Les nids

Voici un petit nid : un ser­pent vert garde un œuf vert. serp4.jpg Voici un nid plus impor­tant : un ser­pent vert garde un ser­pent rouge, un œuf vert et un œuf rouge. serp5.jpg Voici un grand nid : des ser­pents vert, jaune, rouge gar­dent un œuf rouge, un vieux ser­pent, et un œuf vert. Le vieux ser­pent garde quant à lui un œuf jaune et un œuf vert. serp6.jpg Il est impor­tant de noter qu’il ne peut y avoir, dans un nid, un œuf d’une famille (cou­leur) non repré­sen­tée parmi les gar­diens : si il y a un œuf bleu dans un nid, alors il doit y avoir un ser­pent bleu parmi les gar­diens.

La règle de l’éli­mi­na­tion

Voici deux nids l’un à coté de l’autre. Le gar­dien du nid de gau­che sent la faim mon­ter en lui : il va man­ger les occu­pants du nid de droite. serp7.jpg Ce fai­sant, le ser­pent affamé va faire une indi­ges­tion et dis­pa­raî­tre. Et l’œuf de sa famille va éclore… serp8.jpg Et par la magie de la nature, cet œuf va don­ner nais­sance à l’ensem­ble des occu­pants du nid qui a été avalé ! serp9.jpg

La règle des famil­les

Dans cette situa­tion, le ser­pent vert en haut à gau­che est affamé. Seu­le­ment, le nid qu’il con­voite con­tient des élé­ments de sa famille (un ser­pent vers et un œuf vert) ainsi que des élé­ments d’une famille qu’il est censé sur­veiller (un ser­pent rouge et un œuf rouge). serp10.jpg La règle des famil­les dit que dans ce genre de situa­tion, il faut chan­ger la cou­leur des élé­ments qui vont être englou­tis en con­ser­vant les liens fami­liaux, pour per­met­tre au glou­ton de com­men­cer son repas. serp11.jpg Le fes­tin peut com­men­cer : le ser­pent vert englou­tit le nid à sa droite, et l’œuf vert éclot… serp12.jpg C’est au tour du ser­pent rouge d’englou­tir le nid jaune, et l’œuf rouge d’éclore… serp13.jpg Et au tour du ser­pent beige d’englou­tir le nid jaune… serp14.jpg Et enfin au ser­pent jaune d’englou­tir le nid bleu : la séquence s’achève ! serp15.jpg

La règle des vieux ser­pents

Le vieux ser­pent n’a plus faim : il garde son nid, tant que ce nid est com­posé de plu­sieurs bran­ches, ici la bran­che verte et la bran­che rouge serp16.jpg Le ser­pent vert cepen­dant est affamé : il englou­tit le nid rouge, et l’œuf vert éclot… serp17.jpg Le vieux ser­pent, qui ne garde plus qu’une bran­che, n’a plus de rai­son d’être, et dis­pa­raît à son tour… serp18.jpg et la séquence s’achève avec le der­nier repas. serp19.jpg

Ce jeu n’est évi­dem­ment qu’une méta­phore. Mais avant d’en arri­ver à la nota­tion mathé­ma­ti­que du lambda-cal­cul, nous allons pas­ser par une nota­tion inter­mé­diaire qui va éclai­rer notre pro­pos. tableau.jpg

Comme vous l’avez cer­tai­ne­ment remar­qué, les ser­pents sont une méta­phore pour une lambda-abs­trac­tion, la famille d’un ser­pent est la varia­ble affec­tée, les vieux ser­pents sont les paren­thè­ses. Dans la théo­rie du lambda-cal­cul, la règle des famil­les est appe­lée alpha-con­ver­sion et le règle de la dis­pa­ri­tion une bêta-réduc­tion.

A titre d’exem­ple, voici la réduc­tion déjà effec­tuée plus haut, lors de l’expli­ca­tion de la règle des famil­les : tab2-dbec4.jpg Bien évi­dem­ment, pour com­men­cer à faire des lambda-cal­culs, il faut des opé­ra­teurs. Voici les plus sim­ples d’entre eux : tab3-3e92f.jpg Et à titre d’exem­ple, voici une réduc­tion Not True -> False : tab4-ffa75.jpg

Vous voilà prêts à faire vos pre­miers lambda-cal­culs ! Comme vous pou­vez cer­tai­ne­ment l’ima­gi­ner, la théo­rie mathé­ma­ti­que qui jus­ti­fie le lambda-cal­cul est autre­ment plus com­plexe que ma petite con­tri­bu­tion. A ce titre, et si vous avez quel­ques bases en logi­que, vous pour­rez con­sul­ter à loi­sir les cours joints, issus de l’Uni­ver­sité de Jus­sieu et de l’ENS.

Bon cou­rage !

P.-S. : l’idée de cet arti­cle m’est venue en par­cou­rant le magni­fi­que site de Bret Vic­tor.

Notes

[1] Soit près de 800 € d’aujourd’hui, d’après la table de con­ver­sion de l’INSEE.

[2] Il existe des dizai­nes de lan­ga­ges dif­fé­rents, qui se dis­tin­guent sur­tout par l’homo­lo­gie qu’ils éta­blis­sent avec la struc­ture men­tale de leurs uti­li­sa­teurs et le champ d’appli­ca­tion auquel ils sont des­ti­nés.

[3] Pour une intro­duc­tion rapide et effi­cace à cette science, je vous con­seille vive­ment le cours d’intro­duc­tion de Chris­to­phe Dar­man­geat, de l’Uni­ver­sité Paris 7.

[4] Parmi les­quels le célè­bre Para­doxe de Rus­sel  : l’ensem­ble des ensem­bles n’appar­te­nant pas à eux-mêmes appar­tient-il à lui-même ?, soit dans un lan­gage plus imagé : le cata­lo­gue de tous les cata­lo­gues qui ne se recen­sent pas se recense-t-il lui-même ?.

[5] A titre indi­ca­tif, en voici la liste. Ces pro­blè­mes sont révé­la­teurs de l’état d’esprit de Hil­bert, pour qui les mathé­ma­ti­ques étaient le champ du savoir absolu, sans zone d’ombre. Dans une inter­ven­tion datant de 1930, il achè­vera son allo­cu­tion par ces mots res­tés célè­bres : “Wir müs­sen wis­sen, Wir wer­den wis­sen”./Nous devons savoir, Nous sau­rons.

[6] En mathé­ma­ti­ques, un sys­tème for­mel est dit con­sis­tant si il est impos­si­ble d’y démon­trer à la fois une for­mule et son con­traire.

[7] En mathé­ma­ti­ques, une axio­ma­ti­que est un ensem­ble de pro­po­si­tions élé­men­tai­res défi­nies comme « vraies », dont la seule con­trainte est d’être non con­tra­dic­toi­res.

[8] En mathé­ma­ti­ques, un sys­tème for­mel est dit com­plet si, pour toute pro­po­si­tion de ce sys­tème, il existe un pro­ces­sus de trans­for­ma­tion – une série de règles d’infé­rence – qui per­met de prou­ver qu’elle est vraie ou fausse. Il est impor­tant de noter que dans l’esprit d’Hil­bert, ce pro­ces­sus doit être fini, réa­li­sa­ble en un nom­bre fini d’impli­ca­tions.

[9] Il y a der­rière ce cou­rant, qui cher­che à mon­trer que les mathé­ma­ti­ques exis­tent en dehors de toute inten­tion et de toute pen­sée, une vision phi­lo­so­phi­que de la con­nais­sance qui méri­te­rait un arti­cle à elle toute seule. Je vous invite, pour plus d’infor­ma­tions, à con­sul­ter l’excel­lent « Hil­bert et la notion d’exis­tence en mathé­ma­ti­ques » de Jac­que­line Boni­face.

[10] Pour une écri­ture com­pré­hen­si­ble de cette démons­tra­tion, vous pou­vez lire cet arti­cle.

[11] Par exem­ple, il est pos­si­ble de démon­trer l’Arith­mé­ti­que de Pres­bur­ger, qui ne con­tient pas la mul­ti­pli­ca­tion, à par­tir de l’Arith­mé­ti­que de Peano qui la con­tient.

[12] Après trois décen­nies de tra­vaux, les mathé­ma­ti­ciens impli­qués dans les recher­ches sur la logi­que méri­taient bien la créa­tion d’un terme spé­ci­fi­que !

[13] Pour une telle des­crip­tion, voir ce cours d’infor­ma­ti­que théo­ri­que de l’Uni­ver­sité de Jus­sieu.

[14] Le pre­mier algo­rithme célè­bre, qui per­met de trou­ver le Plus Grand Com­mun Divi­seur de deux entiers, appa­raît dans le Livre VII des Elé­ments d’Euclide pro­ba­ble­ment écrit vers 300 av J.C.

Evrim Evci

Auteur: Evrim Evci

Restez au courant de l'actualité et abonnez-vous au Flux RSS de cette catégorie

Commentaires (0)

Les commentaires sont fermés



À voir également

arton49.jpg

L’algorithme de Dijkstra pour les nuls

Dans quel­ques jours débu­tera en France ce qu’il est désor­mais com­mun d’appe­ler la « lon­gue trêve esti­vale », période pro­pice à une trans­hu­mance auto­mo­bile sans équi­va­lent dans l’uni­vers connu, et qui voit se déver­ser sur nos rou­tes des mil­lions d’euro­péens en quête de ces riva­ges enso­leillés où ils pour­ront plei­ne­ment pro­fi­ter de leurs con­gés si dure­ment acquis. Nul doute qu’en cette période de grave crise éner­gé­ti­que, tous ces con­duc­teurs esti­vaux auront pris soin d’étu­dier leurs par­cours au plus près, cer­tains d’entre eux n’hési­tant pas à acqué­rir le der­nier modèle de GPS embar­qué. Que les autres, moins for­tu­nés, ne s’inquiè­tent pas pour autant : Le Poulpe a décidé de leur venir en aide en leur pro­po­sant d’opti­mi­ser leur par­cours à la main, à l’ancienne, grâce à la puis­sance de la science algo­rith­mi­que !

Lire la suite