Page 2 sur 3

Message Publié : 29 Juin 2012, 10:56
par shadoko
Ta question est presque tautologique. :hinhin:

Turing arrive à un moment où on se pose de sérieuses questions de logique sur la structure des mathématiques. Ce sont des questions du type: peut-on (toujours) prouver, à partir d'axiomes donnés dans un certain language (mathématique) fixé, si une question qu'on peut poser dans ce language est vraie ou fausse? Ou y a-t-il des questions qu'on ne peut pas résoudre? Y a-t-il des bons axiomes de base et des règles de base pour les mathématiques qui suffisent à ce qu'on puisse toujours répondre oui à la question plus haut? Etc. Et parmi ces questions, il y en a tout une série sur le fait d'être capable de construire des fonctions à partir d'un nombre fini d'étapes, à partir d'axiomes simples.

Et justement, la machine de Turing est une manière de définir simplement ce que veut dire "une fonction est calculable". Elle est calculable si on peut la coder sur une machine de Turing! Cela veut intuitivement dire ce que tu as écrit, mais la vraie définition de Turing, c'est ça.

Ensuite, Turing montre que cette classe de fonctions a un certain nombre de propriétés, et il travaille avec.

Il faut bien comprendre que la machine de Turing, c'était au début surtout une manière de formaliser et de répondre à des questions de logique mathématique. L'article original de Turing s'appelle:
"On computable numbers, with an application to the Entscheidungsproblem"
ce qui veut dire "Sur les nombres calculables, avec une application à l'Entscheidungsproblem"
et l'Entscheidungsproblem, qui se traduit par "problème de la décision" est une problème posé par David Hilbert, grand mathématicien allemand, qui est essentiellement la question que je décrivais plus haut.
(Il se trouve là, par exemple: http://www.thocp.net/biographies/papers/tu...mbers_1936.pdf)

Message Publié : 13 Juil 2012, 16:00
par shadoko
Un hors-série du CNRS sur Turing:
http://www2.cnrs.fr/presse/journal/4787.htm

Message Publié : 15 Juil 2012, 14:09
par Zorglub
Merci Shadoko.

Je n'avais pas pensé aux autres formes de calculateurs. En effet, on pense aux ordinateurs mais les premiers calculateurs étaient analogiques, comme le souligne l'article. Ainsi quelqu'un explique : "Même si ce n'est pas totalement démontré, nous pensons qu'un système analogique ne peut pas calculer ce qui n'est pas calculable avec un ordinateur numérique au sens de Turing".
Est-ce même démontrable ? :hinhin:

Un autre intervenant dans l'article, plus catégorique : "On ne peut pas imaginer de modèle physiquement réalisable et plus puissant que celui de Turing à cause des lois de la physique. Tous les ordinateurs doivent les respecter."
Ce qui est infini est infini que ce soit la mémoire illimitée d'une machine universelle ou même un calculateur analogique ?

Reste les hypothétiques ordinateurs quantiques qui repousseront les limites du calculable, jusqu'où ?

Sinon les programmes assistants de preuve permettent de repousser encore les limites de ce qui est démontrable. Voici un article intéressant de Jean-Paul Delahaye là-dessus. Ainsi, j'ai appris que la plupart des cent théorèmes "les plus importants" avait été démontrés grâce à l'ordinateur, comme le théorème des quatre couleurs : toute carte dessinée sur un plan peut être coloriée avec quatre couleurs de façon que deux pays voisins soient de couleurs différentes.

Dessin (de Jean-Michel Thiriet) extrait de l'article :
[center]user posted image[/center]

Message Publié : 15 Juil 2012, 19:41
par shadoko
a écrit :
Je n'avais pas pensé aux autres formes de calculateurs. En effet, on pense aux ordinateurs mais les premiers calculateurs étaient analogiques, comme le souligne l'article. Ainsi quelqu'un explique : "Même si ce n'est pas totalement démontré, nous pensons qu'un système analogique ne peut pas calculer ce qui n'est pas calculable avec un ordinateur numérique au sens de Turing".
Est-ce même démontrable ? :hinhin:

J'avoue que je ne comprends même pas bien ce qu'il veut dire, parce que tout dépend de la manière dont l'ordinateur analogique rend ses réponses. Un ordinateur tel que pensé par Turing, ça rend des zéros et des uns, en nombre fini. Un ordinateur analogique pourrait rendre totalement autre chose, selon sa conception.

a écrit :
On ne peut pas imaginer de modèle physiquement réalisable et plus puissant que celui de Turing à cause des lois de la physique. Tous les ordinateurs doivent les respecter.

Encore une fois, j'ai bien l'impression qu'il a tout de même un cadre plus précis en tête, et que c'est un peu coupé. Ou alors, ça me paraît totalement gratuit comme affirmation, et je ne vois pas du tout sur quoi il s'appuie pour dire cela.

a écrit :
Ce qui est infini est infini que ce soit la mémoire illimitée d'une machine universelle ou même un calculateur analogique ?

La mémoire est certe illimitée en théorie, mais son fonctionnement fait qu'elle rend une réponse finie, aussi grande qu'on veut, en un sens, mais finie. Pour donner un exemple précis, elle peut rendre n'importe quelle décimale du nombre pi (en un temps fini), mais pas toutes à la fois.

a écrit :
Ainsi, j'ai appris que la plupart des cent théorèmes "les plus importants" avait été démontrés grâce à l'ordinateur

Non, ce n'est pas cela. Ils ont été démontrés, bien avant, sans utiliser d'ordinateur. Mais leurs démonstrations ont été rentrées dans des logiciels de vérification de preuve.

Par ailleurs, cette liste des 100 théorèmes les plus importants se concentre, un peu exprès, sur des théorèmes dont la formalisation est relativement élémentaire, comparé à d'autres. C'est déjà un gros exploit d'arriver à les rentrer dans des logiciel de preuve, mais c'est loin d'être au niveau de tas d'autres théorèmes beaucoup plus complexes. On peut discuter de leur importance relative, mais il est clair que la formalisation de certains est beaucoup plus compliquée que d'autres, parce qu'elle demande beaucoup plus de pans entiers des mathématiques à rentrer dans la machine, pour faire court.

Quant au théorème des quatre couleurs, si la preuve originale a utilisé un ordinateur pour faire un certain nombre de réductions, elle n'était pas du tout complètement formalisée dans un logiciel de preuve. C'est seulement beaucoup plus récemment que c'est arrivé.

Personnellement, je pense que la formalisation des preuves sur ce genre de logiciels a de beaux jours devant elle, je trouve ça très intéressant.

Message Publié : 15 Juil 2012, 20:15
par Zorglub
Merci pour ces éclaircissements.
En effet les citations sont assez vagues et l'article n'en dit pas plus.

Merci aussi d'avoir rectifier mon raccourci, les assistants de preuve n'ayant évidemment pas démontré mais aidé à la démonstration ou à la confirmer a posteriori.

Message Publié : 16 Juil 2012, 15:07
par Jean-Claude
Est-ce que la preuve apportée par un "logiciel de preuve" est différente de la preuve apportée par la démonstration traditionnelle?

Message Publié : 16 Juil 2012, 15:30
par shadoko
Pas vraiment dans le fond, ou dans le contenu essentiel, si tu veux. Disons qu'elle est écrite de manière totalement formelle, ce qui permet à un ordinateur de vérifier toutes les étapes, alors que dans une preuve "traditionnelle", il y a beaucoup de raccourcis oratoires, sinon ce serait illisible. Il est entendu que les raccourcis concernent des choses bien connues par les mathématiciens, ou bien très faciles à reconstituer avec les indications données.

Dans une preuve assistée par ordinateur, il y a des axiomes, et des étapes complètement formelles en utilisant ces axiomes. Tout est alors vérifiable par un ordinateur, étape par étape. Heureusement, on peut réutiliser des morceaux d'une preuve dans une autre, c'est modulaire, en quelque sorte, pour gagner du temps de vérification.

Pour donner une sorte d'exemple concret, à chaque fois que tu utilises des nombres réels dans une preuve formelle, et que tu veux par exemple, au cours d'un calcul, utiliser que (ab)c=a(bc), tu dois invoquer une telle propriété, qui a été prouvée (de la même manière), avec ton logiciel de preuve. Si elle n'a pas été prouvée, elle ne peut pas être utilisée. Tu peux toutefois faire appel au fait que ça a déjà été vérifié par un autre, sans avoir à le refaire à la main toi-même. Bien entendu, dans un article mathématique usuel, personne ne rappellerait d'où sort une telle égalité bien connue, et elle ne serait même pas explicitement écrite, d'ailleurs, on retirerait toutes les parenthèses.

Message Publié : 16 Juil 2012, 15:43
par Jean-Claude
ok merci. Donc ça n'a rien à voir avec la question de l'énoncé vrai, mais dont la véracité est indémontrable?

Message Publié : 16 Juil 2012, 16:10
par shadoko
Non, en effet, ça n'a rien à voir directement avec ce genre de considérations.

Message Publié : 16 Juil 2012, 19:52
par Zorglub
Une petite (2 min) vidéo sur la découverte de Turing. C'est en anglais mais suffisamment explicite.