Un article de vulgarisation

Bin c'est de la vulgarisation :-D , donc pour ce qui est des discussions sur le forum, complètement inutile (même s"il y est redit après 200 lignes que logique classique s'obtient en ajoutant [non(non A)] => A. à la logique intuitionniste et que la logique intuitionniste ne prouve pas que [non(non A)] => A.

Par ailleurs, il est assez hallucinant de voir l'auteur mettre la logique classique dans le camp des matheux et la logique intuitionniste dans celui des informaticiens. Je ne sais pas ce qui lui a pris. La découverte de la CCH ne s'est pas faite "d'un coup sec". Il y a eu plusieurs progrès espacés, mais cela fait quand-même maintenant longtemps qu'on sait que cette nomenclature n'est pas pertinente et que la logique classique s'exécute et est aussi constructive que l'intuiionniste (du moins que l'intuitionniste ne l'as pas vraiment plus que la classique).

Si on devait mettre en place une "logique informatique", il y a longtemps que logique classique comme logique intuitionniste seraient hors course, mais je ne suis pas sûr qu'il soit pertinent de le faire. Toujours est-il que ce qui est couteux en informatique c'est de copier une ressource et non pas d'échanger deux bits.

Bref, je ne comprends pas trop cette façon de vulgariser. Et surtout, je ne comprends pas trop le besoin de le faire. Les sous-ensembles d'axiomes de l'ensemble de ceux qui définissent la logique classiques portent des noms, c'est tout. Il y en a un qui s'appelle "logique intuitionniste". Les gens qui connaissent ça n'ont pas à être classés comme s'ils adhéraient à l'un ou à l'autre. Or c'est un peu le préjugé faux que renvoie l'article.

C'est-à-dire qu'en informatique, on s'aperçoit qu'il y a un gouffre entre, par exemple, pour deux objets $x,y $ d'un type donné $T$:
(1) affirmer que $x=y$ ou $x\neq y$
(2) être en possession d'un test (une fonction $f$ définie sur $T^2$ et à valeurs dans les booléens) tel que $f(x,y)=true$ si $x=y$ et $false$ si $x \neq y$.

Quand $T$ est un bête truc fini, ou une construction ad-hoc (des entiers entrées dans un annuaire avec nom et adresse ou quelque chose comme ça) ça va, on construit facilement une telle fonction booléenne (temps d'exécution?)
Quand $T$ est le type des flottants ça commence à sentir le souffre
Quand $T$ est le type des fonctions de $A$ dans $B$, là ça devient carrément impossible si par exemple $A=\N$ (cas particulier du théorème de Rice, l'égalité étant comprise au sens suivant: $f=g$ ssi $f(x)=g(x)$ pour tous $x\in A$).


La logique intuitionniste s'impose en info en raison de ces considérations pratiques puisqu'elle prouve $A\vee B$ si et seulement si elle prouve $A$ ou elle prouve $B$ (*) (i.e. on sait décider dans le cas d'une alternative, laquelle des possibilités est la bonne).

[small](*) avec des conditions sur les axiomes, cf formules de Harrop[/small]

Je prouve mon affirmation en conjecturant que cc ne sait pas faire du roller avec des roues alignées.

S

Ton lien ne m'embête pas, dom, mais je ne situe pas vraiment quel rôle il peut vouloir jouer. Pourquoi vulgariser la logique intuitionniste alors que de toute façon, les lecteurs potentiels, ne connaissant pas bien tout ça, n'ont même aucune idée de ce que veut dire logique (même classique). Et le texte n'explique pas vraiment ce que c'est.

CCH ?

"CCH" veut dire "correspondance de Curry Howard".

christophe c a écrit:

Non, attention, ça c'est complètement faux, tu confonds "ne pas être la logique classique" avec "être la logique intuitionniste". grinning smiley

Je ne parlais pas de Curry Howard, mais simplement d'un problème (bien plus simple) de manque d'accès à une certaine information (pour prendre un exemple extrême: deux fonctions sont extentionnellement égales ou non). J'ai des informaticiens qui m'ont parlé de ce genre de problèmes et CCH ils ne savent pas ce que c'est.

En plus pour les versions où ((A->B)->A-)>A est un type habité, il faut de nouvelles règles de typage. Ce n'est plus la même chose.