Discussion:Correspondance de Curry-Howard

J'ai noté le sujet comme d'importance Maximum, vu que la catégorie Élevée est remplie de chose comme IPod ou Wiki. Cela ma parait raisonnable pour un concept aussi important de l'informatique (théorique).Outs (d) 18 février 2009 à 15:25 (CET)

J'ai mis Élevée finalement Outs (d) 25 février 2009 à 09:37 (CET)

Ca me parait plus réaliste. Pierre de Lyon (d) 2 mars 2009 à 21:40 (CET) grand défenseur de la correspondance de Curry-Howard

Krivine sibyllin

À propos du résumé des travaux de Krivine, J'ai un sérieux doute sur le fait que le λ-terme associé à l'absurde soit λx.x, c'est à dire l'identité. D'une part la notion de λ-terme associé à une formule plutôt qu'à une preuve ne correspond pas à l'énoncé de l'isomorphisme, d'autre part, les trois exemples donnés manquent singulièrement de contexte. Est-ce que quelqu'un sait ce dont il est question, et peut corriger/étendre, ou doit-on supprimer la section? — Le message qui précède, non signé, a été déposé par 130.149.247.173 (discuter)

J'ai rajouté une ref en ce qui concerne le thm de complétude. Sinon il y a les autres papiers présents sur sa page je vais tenter de retrouver ce que j'avais vu, mais pour l'absurde je ne sais pas. --Epsilon0 ε₀ 11 mai 2009 à 18:13 (CEST)

Effectivement l'identité ne correspond pas du tout à l'absurde, elle correspond à (A → A) (Si A alors A) qui est "vrai" (prouvable) dans toute les logiques raisonnables. L'absurde n'a pas de lambda-terme canonique associé quoique tout lambda-terme non typable peut-être dit correspondant à l'absurde. Certains langages introduisent des constructions qui ont le type absurde Forall A . A (Tout est vrai), qui correspondent effectivement aux exceptions, ou à des programmes qui ne finissent jamais (et dont le type n'a donc pas de sens). --Jedai

L’intérêt de la correspondance de curry howard dans par exemple les assistant de preuve comme par exemple Coq?

Bonjour, je m’intéresse aux mathématiques et en particulier aux démonstrateur automatique de théorème, et j'ai déjà lu et posé pas mal de question sur wikipedia:

Ma question serait la suivante:

Pourquoi apparemment certains assistant de preuve tel que Coq sont basé sur un langage utilisent la correspondance de curry howard? car pour moi le seul intérêt que j'ai compris à utiliser une telle correspondance est de facilement simplifier un preuve en un preuve plus courte! il n'y a t'il pas d'autres intérêts? car si je ne me trompe pas, le but d'un assistant de preuve est de permettre de trouver facilement la preuve qu'un énoncé est vrai ou faux, et je ne vois pas l’intérêt de la correspondance de curry howard là dedans?

Merci.

--Nicobzz (d) 23 décembre 2010 à 21:24 (CET)

Il y a plusieurs intérêts à établir une correspondance entre démontrer et calculer.

1. La démonstration est un objet mathématique de première classe, c'est-à-dire que c'est un objet mathématique (un lambda-terme) que l'on peut fabriquer (c'est essentiellement ce que fait l'assistant de preuve), écrire, échanger, vérifier, conserver comme un autre objet mathématique tel qu'un nombre ou une fonction.
2. On peut extraire un programme à partir d'une démonstration d'une propriété existentielle.
3. On peut intercaler des calculs efficaces et corrects par construction à l'intérieur d'une démonstration, pour obtenir une démonstration efficace.

--Pierre de Lyon (d) 23 décembre 2010 à 22:30 (CET)

Ah merci bien, je comprend une partie, mais j'ai du mal pour le reste, je comprend que je dois encore faire des efforts pour comprendre comment fonctionne les démonstrateur automatique de théorème et les assistants de preuve. En tout cas merci de m'éclairer et de contribuer à wikipedia. Bon noël--Nicobzz (d) 24 décembre 2010 à 17:48 (CET)

Le langage de coq est basé sur le calcul des constructions qui est une variante de la théorie des types. Il est vrai que coq utilise la correspondance de CH en représentant les preuves comme des lambda-termes, ce qui permet comme l'explique ci-dessus Pierre, de voir les preuves effectuées en coq comme des programmes. Mais cette interprétation est extérieure à coq et n'a pas d'incidence sur la manière dont celui-ci fonctionne en tant qu'assistant de preuves.

D'autre part la normalisation des preuves, utilisée par coq pour décider certaines égalités, pré-existait à la découverte de la correspondance de CH, on peut même dire que c'est elle qui a conduit à la découverte de la correspondance. Pour ces deux raisons on ne peut donc pas vraiment dire que le langage de coq est « basé sur la correspondance de CH », un énoncé plus correct serait plutôt que la correspondance de CH « s'applique à coq »..

Un dernier élément de réponse à propos de « trouver si un énoncé est vrai ou faux » : un assistant de preuve sert à... réaliser des preuves formelles, c'est à dire vérifiables par un ordinateur. En général la vérité de l'énoncé est connue avant de commencer la preuve (parcequ'on dispose d'une preuve informelle) et donc l'assistant n'est d'aucune aide sur ce point. Pourquoi faire des preuves formelles ? On peut imaginer (au moins) deux raisons :

- prouver la correction d'un programme, dans ce cas l'assistant va aider à formaliser la spécification du programme et à vérifier que le programme réalise cette spécification, éventuellement après correction des bugs que l'on aura trouvés ; l'assistant est alors utilisé comme outil de débogage.

- réaliser de bibliothèques formelles de mathématiques ; dans ce cas on connait déjà le statut des énoncés que l'on prouve puisque qu'ils sont dans des bouquins, l'intérêt est plutôt de permettre des traitements formels, typiquement pour faire du data-mining, de la recherche par pattern-matching, etc.

Laurent de Marseille (d) 25 septembre 2011 à 17:18 (CEST)

Merci beaucoup Laurent :) --Nicobzz (d) 26 septembre 2011 à 00:31 (CEST)

Laurent: Il serait intéressant de rajouter une partie de ce commentaire dans la page des assistants de preuves et des démonstrateurs automatiques de preuves? --Nicobzz (d) 26 septembre 2011 à 21:49 (CEST)

déduction modulo

Bonjour,
Cette déduction modulo est citée à différentes reprises et annoncée comme article à venir (ou nécessaire).
En attendant l'existence d'un tel article une brève définition serait la bienvenue. Autrement il faut annoncer d'office aux novices le niveau d'étude minimal obligatoire pour avoir une chance minimale de comprendre l'article. Ce qui ne serait pas une attitude encyclopédique.
Merci d'avance--Overkilled ^[discuter] 25 octobre 2020 à 19:45 (CET)

Programme de réparation de fichiers

Bonsoir,

Dans la section "Logique et informatique", il est fait mention d'une correspondance entre le premier théorème d'incomplétude et un programme de réparation de fichiers, suggérée par Jean-Louis Krivine. Je n'arrive pas à trouver de source convenable dans ses différents articles (https://www.pps.jussieu.fr/~krivine/articles/).

La modification a été faite, il y a très longtemps, par @Tom~frwiki.

Serait-il possible d'indiquer un article où Krivine aurait abordé ce point?

Merci. Thmgd (discuter) 12 février 2023 à 23:10 (CET)

Bonsoir,

En effet ça fait longtemps. Certainement avant que l'on ne commence à ajouter des sources dans Wikipedia. Je ne me souviens plus, c'était peut-être une interview ou un article de vulgarisation. Mais franchement je ne m'en souviens plus. Si ça me revient je referai un tour ici. Tom (discuter) 5 février 2024 à 20:59 (CET)