Re: essayer Julia ?

Le lien entre les maths et la programmation est ténu, en plus d'être souvent dangereux. L'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout.

J'imagine, comme GuieA_7, que c'est de l'humour, mais vu l'incubateur d'excellence qu'est LinuxFr, je vais quand même répondre. :)

En mathématique, on a tout de même l'habitude d'apporter des preuves de ce que l'on affirme et non de lancer des affirmations en l'air. Tentons de réfuter le propos.

Déjà il me semble bien que Gödel, Church, Turing et Von Neumann étaient avant tout des mathématiciens et logiciens. J'ai là, sous les yeux, l'article de Turing où il expose son concept de machine et celui-ci est intitulé Théorie des nombres calculables, suivie d'une application au problème de la décision. Il traite ce fameux problème à la section 8 et montre son caractère insoluble : c'est le fameux problème de l'arrêt. Le problème en question fut posé par Hilbert et renvoie au deuxième des 23 qu'il posa au deuxième congrès international des mathématiciens, tenu à Paris en août 1900.

Ceci étant dit, on s'étonnera moins du fait que le laboratoire Preuves, Programmes, Systèmes (PPS) de l'Institut de Recherche en Informatique Fondamentale, associée à l'équipe de logique de l'Institut Mathématique de Jussieu, propose un master intitulé Logique Mathématique et Fondements de l'Informatique.

On s'étonnera moins, également, d'un résultat notoirement connu chez les théoriciens sous le nom de correspondance preuve-programme ou corresponcance de Curry-Howard : un programme est la preuve d'un théorème et l'énoncé de ce dernier est le type du programme. Dans cette lignée de pensée, on trouve le système F (ou lambda-calcul polymorphe) de Jean-Yves Girard qui est la base des langages (et de leur système de type) comme Haskell ou OCaml. Le système F date tout de même de 1972 et fut mis au point, entre autre, pour résoudre la conjecture de Takeuti qui généralise un résultat obtenu par Gentzen dans les années 30 afin de résoudre le fameux deuxième problème de Hilbert.

Illustration rapide avec le calcul de la longueur d'une liste chaînée :

let rec length = function
 | [] -> 0
 | _ :: tl -> 1 + length tl
let length_tr l =
 let rec loop acc = function
 | [] -> acc
 | _ :: tl -> loop (acc + 1) tl
 in loop 0 l

Déjà, on peut faire de la récursivité sans boucle for ni boucle while. La première version a un gros défaut : on risque le débordement de pile, la deuxième utilise un espace constant sur la pile (c'est l'équivalent d'une boucle for ou while). Mais les deux miment un principe de raisonnement standard en mathématique : le raisonnement par récurrence. Si une propriété est vraie de 0 (P 0), puis qu'elle passe au successeur (si Pn alors P(n+1)) alors elle est vraie pour tout entier (pour tout n, Pn). En réalité seule la deuxième utilise ce principe, la première utilise l'hypothèse de récurrence sous la forme : si pour tout m ≤ n, Pm alors P(n+1). Autrement dit, il faut garder sur la pile toutes les preuves depuis 0 pour passer à l'étape suivante : on risque le débordement de pile sur une machine. ;-)

Je pourrais continuer comme cela pendant longtemps mais, pour des langages comme le C, on pourra se reporter à l'excellent tutoriel Introduction à la preuve de programmes C avec Frama-C et son greffon WP sur le site zeste de savoir. Frama-C développé en partenariat par le CEA list et l'Inria.

Frama-C est une plateforme d’analyse de codes sources. Elle met en œuvre des techniques d’interprétation abstraite, de vérification déductive, de slicing et d’analyse dynamique dont la caractéristique commune est de reposer sur des méthodes formelles qui assurent que leurs résultats sont rigoureusement corrects. Dans une dynamique open-source, cette plateforme permet non seulement le développement d’approches variées par une communauté d’utilisateurs divers, mais aussi de combiner ces approches pour atteindre des objectifs de validation ambitieux. Ces analyses sont particulièrement adaptées à des programmes dans lesquels la sûreté de fonctionnement, ou la sécurité face aux actions malveillantes, est essentielle.

Pour conclure rapidement, sur les mathématiciens qui ne comprennent pas le problèmes de cache (ça, c'est pour freem). Voyons voir le calcul matriciel. Un matrice carré simple comme

1 2 3
4 5 6
7 8 9

est représentée en mémoire ligne par ligne 1 2 3 4 5 6 7 8 9 pour le C, ou colonne par colonne par 1 4 7 2 5 8 3 6 9 en Fortran. Résultat dans un langage comme le C si on parcourt une matrice ligne par ligne ça va plus vite et on a moins de cache miss sur de grosses matrices. Pour faire le produit, on peut par exemple transposer d'abord la seconde matrice avant de faire la boucle for qui calcule le produit pour avoir à parcourir les deux matrices ligne par ligne.

On peut aussi découper les matrices très grandes récursivement en matrice plus petite selon le procédé de la courbe de Lebesgue

courbe lebesgue

courbe Z

comme cela on linéarise la représentation en mémoire de notre matrice en suivant la courbe et les petites matrices rentre bien sur une ligne de cache. Ensuite on fait du Map-Reduce pour opérer sur la grande matrice à partir des petites, ce qui en plus à l'avantage de bien se paralléliser.

On peut aussi utiliser, comme alternative, la courbe de Hilbert :

Pour les bases de données multi-dimensionnelles, la courbe de Hilbert a été proposée à la place de la courbe de Lebesgue parce qu'elle a un comportement préservant mieux la localité.

courbe de Moore

C'est joli et utile les fractales ! :-)

Alors toujours convaincu que : « Le lien entre les maths et la programmation est ténu, en plus d'être souvent dangereux. L'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout » ?

Ou je peux conclure comme un récent commentaire d'arnaudus :

En face de certains bistros, il y a des universités, et dans les universités, il y a des gens qui travaillent sérieusement sur de telles questions ; il existe par exemple des discipline scientifiques qui s'appellent Informatique et Mathématique et qui permettent d'aller un peu plus loin que les platitudes habituelles.

Désolé pour la conclusion, mais c'était de bonne guerre. ;-)

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