Discuter:Thèse de Church

Un article de Wikipédia, l'encyclopédie libre.


Proposé par : MM (pas Utilisateur:MM)

Sommaire

[modifier] Raisons de la demande de vérification

Traduction incorrecte, contenu à vérifier.

[modifier] Discussions et commentaires

Toutes les discussions vont ci-dessous.


[modifier] Thèse de Church

L'appellation Thèse de Church-Turing ne me parait pas correcte. Je viens de lire des articles historiques par ceux qui ont participé à l'élaboration de la thèse de Church: à savoir Church, Kleene, Rosser. Il apparait clairement que la thèse de Church revient à Church et pas à Turing. En revanche tous s'accordent à dire que ce sont les machines de Turing qui ont renforcé sa crédibilité en apportant un vrai modèle « mécanique », mais l'idée d'énoncer une « thèse » est l'intuition de Church. Avant Turing, on savait seulement que les fonctions récursives générales (modèle de Hebrand-Gödel) étaient lambda-définissables. Kleene ne démontrera l'inverse que plus tard (1940). Turing montra rapidement l'équivalence entre la lambda-définissabilité et la définissabilité par machine de Turing, renforçant ainsi la thèse de Church à laquelle il adhéra tout de suite.

J'ai l'intention de renommer l'article. Question: Sait-on quand le nom « Thèse de Church-Turing est apparu?  »Pierre de Lyon 17 avril 2007 à 21:58 (CEST)

Dans la discussion de l'article anglais il y a une référence à un article de Soare de 1996 [1], qui en est peut-être bien l'origine, et qui en tout cas argumente pour "Thèse de Church-Turing", et n'a pas ton point de vue (je ne l'ai parcouru qu'en diagonale, désolé). Turing avait aussi énoncé la dite thèse dans son article de 36 (il argumente pour que la notion de réel calculable "naturellement", soit aussi celle de réel calculable par machine), où il cite cependant l'article de Church de la même année. Gödel a semble-t-il été convaincu de la justesse de la thèse par l'article de Turing. Pour l'aspect historique, il faudrait au moins connaître les arguments de Soare -- c'est aussi à cause de lui que l'on dit de plus en plus "computability theory" pour "recursion theory". Sinon, je n'ai pas vraiment d'opinion sur le renommage, on voit de plus en plus "Thèse de Church-Turing", mais comme beaucoup j'avais appris "thèse de Church". Proz 18 avril 2007 à 02:30 (CEST)

Oui, cest clair. Mais Turing a eu connaissance des travaux de Church avant la version finale de son article (cf une lettre qu'il a écrit à sa mère où il dit vouloir renoncer à publier son article. Heureusement Newman l'y a poussé. Il dit aussi dans cette lettre son intention d'aller à Princeton chez Church.). Les premiers énoncés de la thèse de Church datent des années 30-31 et affirment que la lambda-définissabilité capture la notion de fonction intuitivement calculable. Cela ne convainquait pas Gödel qui préférait la notion de fonction récursive générale. Kleene a répondu à sa critique, mais il semble bien que Gödel ait été définitivement convaincu (comme Church d'ailleurss) quand il a vu qu'un troisième modèle aussi différent de la lambda définissabilité et de la récursivité générale coïncidait. Cela ne justifie pas d'attribuer à Turing in idée due à Church. Si l'on veut alors grouper des noms il faut l'appeler thèse de Church-Gödel-Kleene-Turing. Pierre de Lyon 18 avril 2007 à 07:08 (CEST)

Tu as raison, peut-être même faudrait-il ajouter Post. Effectivement, d'après Soare, Church a bien proposé sa thèse avant 36 : il cite une lettre à Gödel de 34 où Church propose la lambda-définissabilité comme définition de calculabilité effective. Comme arguments dans l'autre sens, toujours d'après Soare, la calculabilité intuitive est mieux analysée chez Turing, plus les arguments déjà cités. La recommandation 3 de Soare, p 33, qui est de différencier thèse de Turing et thèse de Church me semble vraiment à éviter au moins pour les non spécialistes. A ce titre "thèse de Church-Turing" est un moindre mal. Je crois que l'on ne peut pas éviter de la mentionner sous ce nom dans le corps de l'article, mais après tout beaucoup de gens (dont moi) disent encore "thèse de Church", l'article peut très bien s'appeler ainsi. Proz 18 avril 2007 à 21:22 (CEST)

Mes références sont

  • Step By Recursive Step: Church's Analysis Of Effective Calculability (1997) Wilfried Sieg, The Bulletin of Symbolic Logic
  • Rosser, J. B. 1982. Highlights of the history of the lambda-calculus. In Proceedings of the 1982 ACM Symposium on LISP and Functional Programming (Pittsburgh, Pennsylvania, United States, August 15 - 18, 1982). LFP '82. ACM Press, New York, NY, 216-225.
  • Origins of Recursive Function Theory in Annals of the History of Computing, Vol. 3 No. 1, Janvier 1981.

qui vont toutes dans ce sens. Pierre de Lyon 18 avril 2007 à 21:36 (CEST)

Il faut encore ajouter à ces références les articles de Feferman et de Gandy dans Collected Works of A.M Turing vol. Mathematical LogicPierre de Lyon 19 avril 2007 à 20:58 (CEST)

Ca y est j'ai renommé l'article. Pierre de Lyon 19 avril 2007 à 22:02 (CEST)

[modifier] Implications philosophiques

Ce paragraphe me parait être du charabia, pas très correct du point de vue de la théorie des machines de Turing. Comme il n'apporte rien, je propose de le supprimer. Pierre de Lyon 19 avril 2007 à 22:02 (CEST)

ça vient manifestement de la version anglaise. Sans références ce genre de choses ne peut de toute façon pas avoir grand sens. Si quelqu'un a des lumières sur le sujet, il pourra toujours écrire quelquechose de plus correct et mieux sourcé, donc d'accord pour la suppression. Proz 21 avril 2007 à 15:50 (CEST)
Je pense que l'appellation "thèse de Church-Turing" venait aussi de la version anglaise sans être plus sourcée. Pierre de Lyon 21 avril 2007 à 18:21 (CEST)
Implications philosophiques : la version anglaise a des liens internes inexistant ici et la formulation est un poil plus précautionneuse. Thèse de Church-Turing : il y quand même des sources. J'ai vu d'ailleurs ceci qui est une discussion intéressante sur la nature des algorithmes : Gurevich et Blass disent aussi thèse de Church-Turing. Je propose de laisser quand même l'autre appellation dans le corps de l'article (pas en note) et d'être un peu plus "neutre" sur la formulation. Je peux essayer quelquechose. Pourquoi ne pas mettre les sources que tu indiques ici en référence, et reconstruire un peu le paragraphe historique qui n'est pas très lisible ? Proz 21 avril 2007 à 22:56 (CEST)
Je suis d'accord que je suis peut-être aller trop fort dans l'autre sens. Ceci dit, ça n'est pas parce que trois personned ont rebaptisé un concept que tout le monde doit les suivre. Pour nous, il s'agit d'une encyclopédie. Ceci dit ça a du bon en ce qui me concerne, j'ai lu les textes historiques de Kleene, Rosser, plus un texte de Wilfrid Sieg intitulé Step by recursive step: Church' analysis of effective calculablity, je suis en train de lire Computable (comme Turing lui-même l'appelle) dans le texte, c'est une très bel article et c'est passionnant. Dans les œuvres complète de Turing, il y a avant l'article une petite note historique e Feferman qui parle de « thèse de Church ». Rien de ce que j'ai lu, n'indique qu'il faudrait parler de thèse de Church-Turing, même si Computable est vraiment une avancée dans la direction de l'acceptation de la thèse de Church. Pierre de Lyon 22 avril 2007 à 17:30 (CEST)
C'est plus de 3 personnes, et celles-là sont quand même des "autorités". Je suis sûr d'avoir lu ça ailleurs (et ailleurs que sur wikipedia), y compris dans des textes plus orientés vulgarisation. Je suis personnellement d'accord sur le fait que ce renommage était inutile, je n'avais jamais regardé de près, et tes arguments m'ont convaincu que l'on peut continuer à dire "thèse de Church", sans que ce soit injuste pour Turing. Mais comme, depuis quelques années, "thèse de Church-Turing" est utilisé également, et de plus en plus j'ai l'impression, il faut bien en prendre acte, en donnant les arguments.
Autre chose (d'un peu lié), puisque tu semble bien connaître les aspects historiques : est-il bien exact que Turing avait énoncé sa version de la thèse de Church sans connaître celle-ci (comme dit dans l'article wikipedia), alors qu'il cite Church ? Le sait-on par des versions préliminaires de l'article de Turing ?

Proz 25 avril 2007 à 11:36 (CEST)

Je réponds à tes deux points. Je veux préciser que j'admire le travail de Turing dans Computable que je viens de lire, ce que je n'avais jamais fait, parce que la rédaction de cet article m'a poussé à le faire.

  • J'ai lu l'article de Soare (qui n'est pas un historien). Je le trouve partial, il énonce d'emblée un point de vue qu'il ne justifie pas et qui n'est pas fondé historiquement. On voit qu'il ignore ce qu'est le lambda-calcul et qu'il n'a jamais entendu parlé de la correspondance de Curry-Howard, qui place le lambda-calcul comme l'un des (si ce n'est le) modèles de calcul de référence et non pas, comme il s'évertue à la faire, comme un modèle de seconde zone (ou même comme un formalisme qui n'est pas un modèle de calcul si on le suit bien). Je remarque aussi qu'il filtre les références qui ne vont pas dans le sens de son a priori: par exemple Turing lui-même (pourquoi Turing a-t-il prouvé l'équivalence de la λ-définissabilité avec son modèle si le modèle du λ-calcul est sans intérêt?), l'article historique de Rosser, la plupart du contenu de l'article historique de Kleene. Je note que Sieg a écrit un article postérieur à celui de Soare qui rétablit des vérités sur la thèse de Church.
  • Dans une lettre à sa mère (qui était autrefois en ligne et qui ne l'est plus), Turing disait qu'il avait fini la rédaction de Computable et qu'il avait appris qu'un certain Church avait démontré le même résultat (le Entscheidungproblem). Il disait aussi que Newman lui avait demandé de maintenir sa publication, car les résultats étaient suffisamment différents. Il termine en se disant décidé à aller à Princeton travailler avec Church. De là j'infère, comme d'autres (dont Sieg) avec d'autres preuves, que Turing a rédigé Computable sans connaitre les résultats de Church. C'est mieux ainsi car il aurait été influencé et n'aurait pas produit son modèle si radicalement différent, qui a convaincu Gödel.

Pierre de Lyon 25 avril 2007 à 15:38 (CEST)

Merci pour le second point. Pour le premier, sans avoir autant de connaissances historiques que toi à ce sujet, l'article de Soare m'a aussi paru discutable. Je pense juste que, même si c'est à tort, comme l'appellation thèse de Church-Turing existe (en anglais au moins "Church-Turing thesis" est abondemment utilisé, cf. google), il faut en rendre compte de façon visible. Comme tu le sais les attributions de théorèmes en mathématiques ne rendent pas forcément justice à la bonne personne. Le plus important est que la partie historique de l'article soit claire sur le sujet. Si tu trouves que je n'ai pas rendu assez justice à Church dans le paragraphe d'introduction que j'ai ajouté, n'hésite pas à modifier, pour moi c'est une proposition. Je n'ai d'ailleurs pas effacé la note que tu avais ajoutée, mais l'ai juste commentée. Proz 25 avril 2007 à 23:03 (CEST)
Je pense que l'introduction est bonne. Quant à Blass et Gurévich, ils parlent plus d'algorithme que de fonctions calculables, c'est le but de leur article, et quant à l'appellation « Church-Turing », j'ai compris qu'il faut plutôt en chercher l'explication du côté de la sociologie de la discipline (dichotomie volume A -- volume B, comme on l'appelle familièrement). Il faudrait un historien-sociologue des sciences pour démêler ça. Toute autre personne, impliqué dans le domaine scientifique, ne peut que prendre parti. Une autre explication de la terminologie est l'engouement pour la personnalité de Turing, suscité entre autres par le livre de Hodge. Pierre de Lyon 26 avril 2007 à 08:23 (CEST)

[modifier] Historique

Je précise ce qui me semble à revoir : suivre l'ordre chronologique, en présentant d'abord les modèles de calcul, séparer les sources du texte, particulièrement dans ce qui est actuellement le début du paragraphe (j'ai commencé une section "sources", à compléter). Proz 22 avril 2007 à 11:17 (CEST)

J'ai fait une simple traduction de la version anglaise pour le début, puis j'ai ajouté quelques citations de mes lectures. Je suis d'accord que ça n'est pas très lisible. Pierre de Lyon 22 avril 2007 à 17:17 (CEST)

[modifier] L'hypothèse de Riemann

L'hypothèse de Riemmann est une conjecture. Pierre de Lyon 24 mai 2007 à 23:10 (CEST)

[modifier] Aspects philosophiques

[modifier] Discussion sur l'ajout

(réponse à epsilon0 - J'ose tenter d'initier un nouveau dvpt en philo. Mais si c'est pas bon tout virer ...) Et si en plus tu tends la perche ! ;) Sans entrer dans le détail, globabalement je suis au minimum dubitatif, mais tu dois bien savoir toi même si c'est sérieux. Proz 25 mai 2007 à 01:27 (CEST)

(Je me suis auto-reverté et je colle ci-bas le texte mis hier, pour discussion)

(réponse à Proz et Pierre ici) Bonjour, je pense que ce que j'ai mis est sérieux, (sauf ..la partie 1. exemples) qui est spéculative (aspect p.e. mauvais). L'aspect de ce que j'ai appelé par défaut "semi-décidable" de la thèse me semble a minima une chose à dvper (p.e. autrement). Sinon, le dvpt sur Penrose (avec lequel par ailleurs je ne suis pas d'accord : il pense que seul un humain peut démontrer les thms d'incomplétude) m'est inspiré par la vulgate relativement commune (donc critères de notoriété certain) qu'il existe en philosophie (je crois que l'origine remonte à Lucas) concernant ce sujet (voir la partie philosophique qui a antèrieurement été supprimée (+- avec raison pour moi)).

Sinon je ne crois pas que l'on pourra longtemps sur la wikipédia francophone faire l'économie de la "double culture" (cf Snow) philosophique et mathématique concernant la logique (p.e. je développerait cet aspect un jour (étant passé par les 2 disciplines)) : à mon avis elle sont très peu conciliables.

Bon je colle le texte antérieur, pour avoir des avis, objections, dubitations précises. Et je tenterais d'en dire un peu plus la semaine prochaine. Cordialement --Epsilon0 25 mai 2007 à 21:29 (CEST)

[modifier] Le texte retiré de l'article

Cadre formel Contrairement à d'autres thèses ou hypothèses (comme l'hypothèse de Riemann) suggérant une solution attendue à un problème non résolu relevant du domaine strict des mathématiques, la thèse de Church ne relève pas de la simple mathématique. Ceci car elle postule une équivalence, non entre deux concepts formellement identifiés, mais entre le concept formellement bien défini de "récursif" et celui, quasi par définition d'informalisable, de calculable au sens intuitif d'effectif. Ceci appelle plusieurs remarques :

  • 1. Si cette thèse est fausse, il suffit pour le prouver d'exhiber un programme effectuant un calcul qui serait prouvé non Turing-calculable.
    • Exemples : La découverte fortuite que le raisonnement par l'absurde passe la correspondance de Curry-Howard peut être jugé comme une réfutation partielle de cette thèse [Grosse demande sur ce sujet d'avis d'experts]. La découverte que l'Axiome du choix passe cette correspondance en serait une réfutation forte [Idem]. La découverte (+ démonstration de ce fait) qu'un ordinateur quantique peut calculer les premières décimales du nombre oméga de Chaitin en serait une réfutation avérée.
  • 2. Si cette thèse est vraie, elle semble totalement improuvable. A moins que l'on ait une axiomatisation totale du monde physique (mais affirmer que l'on possède une telle axiomatisation pourrait être une réaffirmation de cette thèse au niveau physique) qui prouverait que rien de calculable effectivement au sens physique n'est incalculable par une machine de Turing.
  • Ainsi cette thèse est semi décidable (au sens ou la cohérence du calcul des prédicats du 1er ordre est semi décidable; voir théorème de Church) : si c'est faux on peut prouver, sinon pas.
  • Il semble[ref nécessaires] que ce soit une des(la?) seule(s) thèse(s), semi-décidable de la logique dont la partie non décidable de la solution relève d'un domaine qui excède son cadre de pertinence.

Expectations au delà Certains, comme Roger Penrose dans les Ombres de l'esprit tentent de réfuter la thèse de Church en exhibant du calculable effectif qui ne serait pas Turing-calculable. Les voies d'attaque de ce problème sont en gros de deux sortes :

  • Déterminer un calcul connu effectué par l'esprit humain qui serait inaccessible à un ordinateur (même doué d'une mémoire finie mais illimité comme il en est des machines de Turing).
  • Exhiber dans le domaine physique, notamment en physique quantique, un calcul non Turing-calculable. L'idée devenue courante d'un univers comme ordinateur ultime dont l'évolution relèverait d'un calcul dont les axiomes et règles d'inférences seraient les conditions initiales est le cadre intellectuel usuel [ref nécessaires] de ce genre d'attaque de la thèse de Church.
Quleques précisions. Curry-Howard pour le raisonnement par l'absurde ou l'axiome du choix : rien à voir avec le sujet, c'est la façon dont on calcule, ce à quoi correspond le "calcul" éventuellement, pas ce qui est calculable. L'improuvabilité "totale" de la thèse : on peut quand même définir un cadre général (voir Turing, article original, me semble-t-il), Kleene. Avis de Penrose, je n'y connais rien, mais il faudrait être plus précis. Ordinateur quantique : idem. Univers = ordinateur, qualifier ça d'idée courante, quand même ! Je n'ai pas grande culture philosophique, mais il me semble qu'il faut aussi y être précis et citer ses sources, etc. Certains philosophes qui se sont intéressés à ce sujet sont aussi considérés en mathématiques comme des logiciens comme par exemple Quine, Putnam, Davis, donc je ne vois pas en quoi les deux cultures seraient irréconciliables. Proz 25 mai 2007 à 22:07 (CEST)
"Expectations au delà" est entièrement à revoir (en effet très mal dit), je tenterais une autre version. Pour les exemples que j'ai donné, ils sont mauvais d'ac c'est pourquoi j'ai mis mes "warning derrière". Sinon, oui ya Quine et Putnam (connais pas Davis), mais je ne sais si on peut aller plus loin. Et la philo de Putnam me semble disjointe (bcp de politique, mais ne connais pas tout) de son travail de logicien (sa "philo de la logique" est bcp plus historique et moins originale que celle de "Quine" )--Epsilon0 25 mai 2007 à 22:18 (CEST)

J'ajoute ci-dessu une discussion qu'Epsilon0 avons ue sur nos pages de discussion.Pierre de Lyon 26 mai 2007 à 08:22 (CEST)


Désolé de te le dire, mais je n'aime pas ta discussion philosophique de la thèse de Church. Je pense qu'il n'y pas lieu de « vérifier » la thèse de Church, car elle a un aspect arbitraire. On peut ou non l'accepter, comme on accepte ou non l'axiome du choix, l'axiome de l'infini. Peu de gens rejettent l'axiome de l'infini, comme peu de gens rejettent la thèse de Church.

D'autre part, je travaille sur le contenu calculatoire de la logique classique et je peux dire que ce que tu dis à son propos n'est pas vrai. En gros, on donne un contenu calculatoire à la logique classique en incorporant des opérateurs de contrôle, pas en étendant le concept de calculabilité. Pierre de Lyon 24 mai 2007 à 23:23 (CEST)

Ce sur quoi je voulais insister, c'est que si cette thèse en effet n'est pas prouvable en logique (comme les axiomes, je suis d'accord), néanmoins elle est réfutable (contrairement aux axiomes), ce qui en fait tout de même une sorte d'ovni logique que l'on peut exposer comme tel (j'ai tenté en en parlant comme thèse "semi-décidable"). Maintenant, hors du monde des logiciens mathématiciens comme tu l'es, il existe une littérature philosophique connue tendant à penser que cette thèse est fausse (à mon avis avec de mauvais arguments) : ceci peut être abordé dans l'article.
Sur les exemples que j'ai donné, j'ai mis de gros warning, en pensant notamment à toi comme "expert". Peux tu poindre précisément quelles phrases que j'ai énoncées sont fausses, ce pourrait amener à une version améliorée de ce qu'on va appeler mon brouillon?
Sinon, je me suis auto-reverté et ai collé le tout sur la page de discussion (ou on peut continuer à parler là-bas). Je ne pourrais pas répondre avant la semaine prochaine. --Epsilon0 25 mai 2007 à 21:46 (CEST)
Pour moi la thèse de Church n'est pas réfutable, car elle dit « Si vous voulez savoir quelles sont les fonctions calculables eh bien je vous dis: ce sont celles-ci.» La réfuter pourrait consister à donner une classe avec plus de fonctions calculables, mais pour moi ça n'est plus la thèse de Church, c'est une autre thèse. Elle a donc pour moi exactement le même statut qu'un axiome, on l'admet ou la rejette.
Je crains en effet que les gens qui n'ont pas pratiqué la thèse de Church dans leur vie de tous les jours disent des sornettes.
La seule « réfutation » sérieuse de la thèse de Church que je connaisse est celle de Peter Wegner, mais il sait de quoi il parle et propose un modèle très différent à base de calcul distribué interactif avec communication dans les deux sens, il donne l'exemple de google. Quand je fais une requête à google, je reçois de l'information, mais je donne aussi de l'information à google. Par ce moyen, il y a un calcul qui va au delà de celui des machines de Turing, mais on est dans un autre paradigme. Ca ressemble à la description que tu donnes de Wikipédia sur ta page perso. Pierre de Lyon 25 mai 2007 à 22:43 (CEST)

Il me semble que l'on retrouve dans cette discussion l'opposition entre « platonisme » et « réalisme » en mathématique. Est-ce que je me trompe?Pierre de Lyon 26 mai 2007 à 08:32 (CEST)

Il me semble que ce que l'on appelle réalisme en mathématique, c'est de croire à la réalité des objets mathématiques, que découvriraient les mathématiciens, et non qu'ils créeraient, c'est donc très platonicien ; la dénomination doit remonter à Poincaré, voir http://www.ac-nancy-metz.fr/enseign/philo/textesph/Dernierespensees.pdf ch 5, je l'ai toujours lue utilisée dans ce sens (à propos des math.).
D'après ce que tu écris, et de ce que je vérifie rapidement ici http://www.cs.brown.edu/people/pw/papers/bcj1.pdf, Wegner réfute l'idée que les machines de Turing soient un modèle général du calcul informatique, pas la thèse de Church qui ne parle que des fonctions calculables.
La thèse de Church ne s'exprime pas dans un langage formel, ce qui lui donne quand même un statut très différent d'un axiome. La comparaison que fait Soare (voir article cité) avec la définition de la continuité de Cauchy et Weierstrass, qui capture bien l'idée intuitive de continuité, (on peut imaginer d'autres exemples) me semble assez juste (ça n'a donc rien d'un "ovni" en math.). On aurait pu la réfuter à ses débuts, se tromper, mais on sait maintenant que la définition de la calculabilité est suffisamment solide mathématiquement pour avoir un sens, on n'est plus en 1936. Au final la conclusion est la même que celle de Pierre. Ca n'empêche pas de chercher à comprendre son sens, à mieux dessiner les contours de son champs d'application, ce que veulent faire j'ai l'impression les gens qui la discutent. Pour écrire à ce sujet dans l'article, il faut aller les lire. Proz 26 mai 2007 à 11:49 (CEST)
Tu mets bien en évidence deux questions:
  1. Y a-t-il un modèle de calcul au delà des fonctions calculables (machine de Turing, récursivté générale, lambda calcul, etc.)?
  2. Que signifie, du point de vue philosophique, « fonction calculable » et quelle est son champ d'application?Pierre de Lyon 29 mai 2007 à 07:07 (CEST)