Analogie entre Curry-Howard et méthode scientifique.

[invite6eb1b431]

Bonjour,

Il y a une analogie qui me semble intéressante à mettre en évidence,
et je me demandais si cet aspect avait déjà été exploré :



Cordialement,

Korzibsk
-----

[karatekator]

Bonjour,

Il y a une analogie qui me semble intéressante à mettre en évidence,
et je me demandais si cet aspect avait déjà été exploré :
...
Cordialement,

Korzibsk

Ben pour être honnête, je ne suis pas sur que la correspondance Curry-Howard soit bien comprise sur ce tableau.
Curry-Howard dit: «À chaque calcul je peux associer une démonstration et réciproquement»
Ainsi le rapprochement axiome <-> Sytème d'exploitation me semble abusive (cela n'a rien à voir). Programme d'échappement <-> raisonnement par l'absurde ? Le raisonnement par l'absurde c'est je démontre A=>B par (A et non B) => non A. Par besoin d'échappement ou je ne sais quoi... Tu aurais le lien où tu as trouvé ce schéma (avec les explications) stp?

Mais bon n'étant pas spécialiste de Curry-Howard, peut-être que je me trompe.


Après pour en revenir au débat initial. L'informatique et les mathématiques sont des sciences formels. On résonne et on calcul sur des objets abstraits et exacts. L'analogie du Curry-Howard dit que l'outil de démonstration mathématique est comparable au calcul de l'informaticien. Mais la comparaison est sensée, car on compare deux modes de «raisonnement» formel.

Concernant la comparaison avec la physique, je la trouve abusive car on parle de deux domaines distincts: les sciences formels et les vrais sciences (ie expérimental). Donc dans le meilleur des cas ce sera une analogie intéressante mais elle ne pourra jamais être prouvée ou être utilisée (dans le but de démontrer) comme on peut le faire avec Curry-Howard.

De plus les analogies me semble abusive et inexacte:
Récurrence <-> série de mesure: une récurrence est un raisonnement infini, une série de mesure est par contre fini. Donc cela n'a rien à voir.
Comparaison <-> Raisonnement par l'absurde. Euh où est le rapport ?


En fait si on veut vraiment un Curry-Howard généralisé à la physique, la question à se poser est: Une machine peut elle dire si une démonstration physique (expérience, mesure, hypothèse...) est valide.
Si oui alors on aura une équivalence et on pourra prouver des résultats physiques automatiquement par les machines (en théorie en tous cas).
Mais cela supposerai que les machines refont les expériences... Donc on s'éloignerait pas mal du domaine de l'informatique = science du calcul.

Donc pour conclure:

• Le tableau est à mon avis approximatif pour ne point dire faux.
• Un Curry-Howard généralisé à la physique n'as pas vraiment de sens car la physique (expérimentale) n'est pas une science formel.
• Mais si on veut vraiment généralisé, il faudrait que la machine puisse faire des expériences et là après tous pourquoi pas... Mais permet moi d'en douter.