Discussion:Thèse de Church

• Discutez dans les chapitres prévus.
• Liens utiles : À recycler - À traduire - À fusionner - Orthographe à vérifier - Soupçons de copyright - Articles non neutres

Proposé par : MM (pas Utilisateur:MM)

Raisons de la demande de vérification

Traduction incorrecte, contenu à vérifier.

Discussions et commentaires

Toutes les discussions vont ci-dessous.

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)

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 personnes 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)

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)

L'hypothèse de Riemann

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

Aspects philosophiques

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)

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 eue 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)

Ackermann (Fonction) et Récursivité primitive

C'est aussi à propos de l'article Fonction_d'Ackermann (et par extension Fonction_récursive_primitive).

Constat : Il n'y a pas dans l'article Thèse_de_Church ou dans les articles cités précédemment, de liens croisés, mettant en perspective l'étendue de la thèse de Church, mais la limitation à certains systèmes tout de même assez riches, parmi lesquels il n'y a pas les fonctions récursives primitives, la preuve étant apportée par la fonction d'Ackermann.

Bémol : dans l'article sur la fonction d'Ackermann, il y a une phrase mystérieuse (fait-elle un lien ?) :

La croissance exponentielle des problèmes liés aux grands systèmes informatiques est en relation également avec la thèse de Church.

Pour l'article Thèse_de_Church, ce n'est pas essentiel, mais peut-on ajouter en fin quelque chose comme une section 'Système de calcul non équivalent', ou en remaniant la dernière section, sous le terme 'Limites de la thèse de Church' avec 2 sous-sections 'Systèmes non équivalents' et 'Fonctions non-calculables' :

Le succès de la thèse de Church ne doit pas laisser penser que tout système de calcul généraliste permet d'atteindre la notion de calculabilité de Church et Turing. Par exemple, en affaiblissant un peu la définition des fonctions récursives (en limitant à des définitions récursives reposant sur les successeurs, voir Fonction_récursive_primitive pour en savoir plus), apparaissent des fonctions qui ne sont plus calculables dans le système proposé alors qu'elles le sont avec des machines de Turing ou en Lambda-calcul. L'exemple le plus célèbre est la Fonction_d'Ackermann.

On peut en dire un peu plus si vous voulez (définition de la fonction d'Ackermann, indécidabilité de la récursion primitive)

--Bdenis (d) 18 juin 2011 à 11:38 (CEST)

Je serais plus pour un titre de section "Systèmes non équivalents" plutôt que "Limites de la thèse de Church". En fait, ce que tu dis là - sauf erreur de ma part - ne m'apparait pas véritablement comme une limite de la thèse de Church. La thèse de Church stipule que ce qui est physiquement calculable, ou ce qui nous considérons psychologiquement comme calculable, peut s'exprimer sous la forme d'un ensemble de règles, mais pas n'importe quel ensemble de règles. S'il existe des ensembles de règles, même riches, qui n'expriment pas totalement la notion de calculabilité, cela ne remet pas du tout en cause, ni ne limite, la thèse de Church.

Mais en effet, signaler qu'il existe des ensembles de règles assez riche qui ne mène pas à la notion totale de calculabilité est intéressant. Cordialement --Jean-Christophe BENOIST (d) 18 juin 2011 à 12:09 (CEST)

Je ne suis pas sûr qu'il faille ne signaler que les fonctions primitives récursives. Il faudrait aussi citer la hiérarchie arithmétique (article qu'il faudrait d'ailleurs compléter). --Pierre de Lyon (d) 23 juin 2011 à 10:11 (CEST)

N'hésites pas ! C'est tout l'ensemble hiérarchie arithmétique, théorème de Post, degré de Turing qu'il faudrait compléter (peut-être d'abord) d'ailleurs. --Jean-Christophe BENOIST (d) 23 juin 2011 à 10:34 (CEST)

La hiérarchie arithmétique ce sont des ensembles (ou des prédicats), cas particulier en prenant les fonctions caractéristiques. En fait tout "système formel" (procédé calculatoire) qui ne permet de définir que des fonctions récursives totales est incomplet, par diagonalisation (les primitives récursives et la fonction d'Ackermann ne sont qu'un exemple). Ce serait à dire (ça doit se sourcer facilement, Cori-Lascar II ? Oddifreddi ?). Là dire que l'on affaiblit "qu'un peu" où que le système "semble aussi généraliste", ça me paraît curieux. Proz (d) 28 juin 2011 à 01:03 (CEST)

Je ne suis pas sûr d'avoir bien compris ce que tu veux dire. Tout système est effectivement incomplet, mais le pari de la thèse de Church (et c'est du réalisme mathématique) est qu'il existe un système particulier qui correspond à la "réalité" (thèse physique), ou ce que nous considérons être la réalité (thèse psychologique), en tout cas pour la notion de calculabilité. Donc, dans un sens, il existe un système qui peut être considéré comme "complet", ou "généraliste" (par rapport à la "réalité"). --Jean-Christophe BENOIST (d) 28 juin 2011 à 09:41 (CEST)

Je ne parle que des systèmes formels qui engendrent des fonctions récursives totales (comme les primitives récursives). C'est un résultat purement mathématique. Les machines de Turing y échappent car elles engendrent également des fonctions récursives partielles. Pas moyen de donner un procédé calculatoire qui n'engendre que les récursives totales (c'est lié au pb de l'arrêt mais directement compréhensible par diagonalisation, si on a un tel procédé la diagonale + 1 sur l'énumération des fonction unaires échappe au procédé). C'est "bien connu", (probablement aussi dans Kleene Introduction to metamathematics). Proz (d) 28 juin 2011 à 10:37 (CEST)

Ca y est, je crois voir ce que tu as voulu dire. Je pense qu'il y a moyen de reformuler le paragraphe en question, pour éviter les jugements qualitatifs ("un peu affaiblir", "aussi généraliste"..),et pour décrire factuellement les caractéristiques et limites des systèmes engendrant que des FR totales. Ou alors, est-ce que tu penses que ce paragraphe est finalement peu pertinent ou trop pointu ? --Jean-Christophe BENOIST (d) 28 juin 2011 à 11:35 (CEST)

C'est tout à fait pertinent au contraire, pour comprendre qu'il faut parler de fonction partielle, mais l'article n'en parle même pas. L'article ne donne pas idée de comment on montre que les fonctions calculables par machine de Turing sont mu-recursives (la méthode parait très générale, c'est un argument que donne Kleene(à vérifier) pour la thèse de Church). Quand on a vu cette démonstration on voit bien l'utilité de l'opérateur mu (essentiellement pour avoir le plus petit nombre de pas au bout duquel la machine s'arrête), qui introduit alors des fonctions partiellement calculables. Désolé de me contenter de bavarder en pdd, mais j'ai déjà trop de fers au feu. Proz (d) 28 juin 2011 à 12:29 (CEST)

liste exhaustive des modèles de calcul

Il serait bien d'énumérer la cinquantaine de modèles de calcul équivalents (machine Turing, Post, automate cellulaire, lambda calcul, langage "while" ...) et faire pour chacun un lien vers un article détaillant ce modèle, puis des liens aussi vers chaque démonstration d'équivalence.) --zorg (d) 27 février 2012 à 13:35 (CET)

ou faire un article séparé ou une infobox avec cette énumération --Camion (discuter) 17 juillet 2017 à 10:18 (CEST)

Question du caractère formel de la définition

L'article revendique que la définition n'est pas formelle. Il serait bon de préciser l'origine de ce point de vue et/ou de le justifier et de s'assurer qu'on est suffisamment sur ce que c'est qu’une définition qui aurait un caractère formel. Est-il clair que la notion d'instruction simple et précise n'est pas, par elle même suffisamment définie ? Existe-t-il une zone floue qui ferait qu'on ne sait pas trop ce que ça signifie ? Je ne dis pas que ça n'est pas le cas, mais ça devrait être montré, ou au minimum faire référence au travail d'un auteur. Le problème, ici, c'est que tout langage repose au minimum, sur des définitions exprimées dans le même langage, et pour lesquelles le jugement de la qualité d'être "suffisamment défini", repose à un moment donné sur une perception arbitraire - et c'est le cas ici aussi. Il faut donc, soit montrer en quoi ce qui est vrai pour un algorithme ne l'est pas pour la thèse de Church, soit préciser qui a dit ça ou qui revendique un consensus autour de cette question, ou préciser qu'il existe un consensus informel dont la question de la validité n'a pas vraiment été soulevée. -- Camion (discuter) 17 juillet 2017 à 10:14 (CEST)

Dans la formulation actuelle, l'article ne dit pas que "la définition n'est pas formelle". Où cela est-ce dit ? Il y a d'une part des caractéristiques intuitives de la notion de calculabilité (nulle part il y a le mot "définition"), qui sont nécessairement informelles puisque relatif à une intuition (c'est plutôt le contraire qui serait à sourcer), et exprimées en français (c'est forcément informel rien qu'à cause de cela, d'ailleurs). Et d'autre part des formalismes, formels par définition, et exprimés en langage mathématique. La thèse associe les deux et dit que c'est équivalent. Il y a en effet un "consensus informel" pour considérer que les deux sont équivalents, il y a des milliers de sources à ce sujet. --Jean-Christophe BENOIST (discuter) 17 juillet 2017 à 13:28 (CEST)

Que voulez-vous dire quand vous écrivez que « tout langage repose au minimum, sur des définitions exprimées dans le même langage » ? D'autre part, je pense que la thèse de Church n'est pas formelle dans le sens où elle ne pourra jamais être démontrée dans un assistant preuve du genre de COQ, alors que par exemple les théorèmes d'incomplétude de Gödel le sont. --Pierre de Lyon (discuter) 17 juillet 2017 à 14:52 (CEST)

Oui, une "thèse" est fondamentalement non démontrable (sinon ce serait un postulat, ou théorème quand démontré). Mais je ne crois pas que l'article dise que la thèse est formelle, ou démontrable. Elle fait simplement correspondre, informellement, quelque chose d'informel à quelque chose de formel. --Jean-Christophe BENOIST (discuter) 17 juillet 2017 à 15:13 (CEST)

JCB> Dans la formulation actuelle, l'article ne dit pas que "la définition n'est pas formelle". Où cela est-ce dit ?

Dans votre première intervention après la mienne, vous avez retiré : "Il s'agit là d'une définition intuitive assez claire, mais pas d'une définition formelle"

JCB> qui sont nécessairement informelles puisque relatif à une intuition (c'est plutôt le contraire qui serait à sourcer)

La question est surtout de savoir si la formule laisse la place à une ambiguïté. il me semble que ce qui caractérise la définition intuitive, c'est le fait qu'elle nécessite un travail de la part de celui qui la comprend, pour choisir parmi toutes les façons possibles d'interpréter une proposition, celle qui lui semble avoir du sens et correspondre à ce que l'auteur à eu l'intention d'exprimer. Si la proposition exprimée en langue naturelle n'est interprétable que d'une façon OU peut-être même (à discuter) si il existe un nombre limité de façons de l'interpréter mais que toutes sont pertinentes (au sens ou elles ne se ramènent pas à des tautologies triviales) et valides (on va éventuellement parler de sens fort ou faible, etc.), il me semble qu'il devient alors contestable d'affirmer qu'elle n'est pas formelle. car cela pourrait revenir à affirmer que non formel est équivalent à non exprimé dans NOTRE formalisme préféré, ce qui me semble être une position invalide.

Il me semble qu'au contraire, toute proposition précise et non ambiguë devrait pouvoir être considérée comme formelle même si elle est exprimée en langage naturel.

Les modifications qui ont été apportées à ce paragraphes ne me semblent pas réellement éclaircir cette question, mais me semblent plus noyer le poisson qu'autre chose. Qui plus est, elles ne sont pas plus sourcées que ce qui précédait. S'il y a des milliers de sources sur le sujet, il ne devrait pas être si difficile que ça d'en mettre dans l'article.

PdL> Que voulez-vous dire quand vous écrivez que « tout langage repose au minimum, sur des définitions exprimées dans le même langage » ?

Je n'ai pas été clair. Je voulais plutôt dire que « tout langage repose au minimum, sur des définitions exprimées dans un langage ». Il n'existe pas une référence absolue à partir de laquelle nous définissons les langages. La spécification d'un langage est elle même exprimée dans un langage, et la seule exception repose sur le fait qu'on y joint aussi des représentations issues de notre perception de la réalité, mais dans tous les cas, il reste toujours une ambiguïté possible. Le fait qu'un langage formel soit non ambigu repose essentiellement sur un consensus non remis en cause autour du fait qu'on n'a pas trouvé d'ambiguïté et non sur un absolu logique intangible.

JCB> D'autre part, je pense que la thèse de Church n'est pas formelle dans le sens où elle ne pourra jamais être démontrée dans un assistant preuve du genre de COQ, alors que par exemple les théorèmes d'incomplétude de Gödel le sont.

C'est bien probable, mais tant que ça n'est pas démontré, ça reste une conjecture.

JCB> Oui, une "thèse" est fondamentalement non démontrable (sinon ce serait un postulat, ou théorème quand démontré).

Non, une thèse n'est pas fondamentalement indémontrable. Une proposition n'est indémontrable que dans le cadre d'un ensemble d'axiomes spécifique et pour s'en assurer il faut le démontrer, ce qui n'est pas établi a priori. Dans la plupart des cas on ne sait pas si une proposition est indémontrable, et affirmer que c'est le cas de toutes les thèses par opposition aux postulats et aux conjectures, serait fortement sauvage. D'ailleurs un théorème est composé d'une hypothèse, d'une thèse et d'une démonstration et dire que le théorème est démontré revient à dire que la thèse a été démontrée dans le cadre de l’hypothèse et de l'axiomatique sous jacente.

• Une thèse est simplement une affirmation indépendamment de son caractère démontré ou non et démontrable ou non.
• une conjecture est une thèse non démontrée; et
• un postulat est une conjecture qu'on va utiliser comme prémisse dans une argumentation.

Camion (discuter) 24 juillet 2017 à 15:59 (CEST)

Je pense qu'il y a des incompréhensions et des quiproquos, des deux côtés, je ne suis pas sûr de vous comprendre. Par exemple, il y a sûrement quiproquo sur ce que vous appelez "la définition" (de quoi, au fait ?) Les deux "énoncés" (plutôt que définition) de la thèse (physique et psychologique) sont sourcées, et effectivement ne sont pas formelles bien que cela ne soit pas dit dans l'article (sinon, où ?). Donc toute une partie de la discussion concerne une chose qui n'est pas "revendiquée" dans l'article. Si cela était revendiqué, il faudrait alors le sourcer naturellement, et je pense que c'est sourçable (le contraire ne l'est pas à mon avis). Je pense qu'il y a d'autres incompréhensions et quiproquos. Pour les limiter autant que possible, vous serait-il possible de montrer une source qui présente les choses de la manière dont vous voudriez les voir présentées ? --Jean-Christophe BENOIST (discuter) 24 juillet 2017 à 16:22 (CEST)

Revenons à la thèse de Church. La thèse de Church n'a pas le même statut qu'un théorème ou qu'une conjecture, car elle exprime qu'un concept formel est identifié à un concept intuitif. Il y a un consensus des scientifiques sur ce sujet et je ne crois pas opportun à l'occasion d'un article de Wikipédia d'émettre des propositions personnelles comme celles que vous énoncez, toutes louables qu'elles soient. Ou alors comme dit -Jean-Christophe BENOIST elles sont sourcées et ne deviennent plus personnelles. --Pierre de Lyon (discuter) 24 juillet 2017 à 16:29 (CEST)

Je suis bien d'accord, mais il faut justifier ou sourcer. Le point de vue que je défend n'est pas là pour être défendu dans le cadre de l’article de wikipedia, mais seulement pour montrer que ce que dit l'article ne va pas de soi. -- Camion (discuter) 24 juillet 2017 à 17:15 (CEST)

Mais que dit l'article ? L'article ne revendique PAS que la définition n'est pas formelle. Pouvez-vous citer le passage à sourcer, ou qui vous fait croire que l'article "revendique" ? Nous sommes toujours dans le quiproquo, qui n'est pas élucidé. --Jean-Christophe BENOIST (discuter) 24 juillet 2017 à 17:22 (CEST)

• "Une thèse consiste à affirmer, sans le démontrer, qu'une notion intuitive correspond exactement à une notion formelle" :

J'ai un gros doute sur cette définition et elle n'est pas sourcée.

• "Un autre exemple de thèse consiste à affirmer que la notion intuitive de suite de nombres tirés au hasard correspond aux définitions formelles données par Gregory Chaitin ou Per Martin-Löf." :

preuve par intimidation (on fait du volume autour d'un truc non sourcé, pour noyer le poisson)

• "Les caractéristiques intuitives ne sont pas une formalisation en soi, car elle contient des termes informels comme "instruction simple et précise", ou "intelligence requise pour exécuter les instructions"" :

- Ces termes peuvent-ils être compris d'une façon ambiguë ?

- Une instruction simple peut-être être autre chose qu'une instruction qu'on peut décrire "de façon mécanisable" et

- une instruction précise peut-elle être autre chose qu'une instruction qui peut être effectuée de façon non ambiguë ?

- Si on peut trouver une autre compréhension de ces termes, est-ce qu'on peut trouver une autre compréhension de ces termes qui prend la thèse de Church en défaut ?

- L'intelligence requise pour exécuter les instructions peut elle signifier autre chose que l'existence d'une mécanique capable d'exécuter les dites instructions simples et précises de façon non ambiguë ?

• "au début du xxe siècle, les mathématiciens utilisaient des expressions informelles comme effectivement réalisable" :

En quoi, effectivement réalisable est une expression informelle ?

Tout ce que je vois là, c'est que ces formules n'utilisent pas le formalisme moderne qui est plus récent qu'elles, mais il me semble abusif de dire sans montrer ni sourcer une ambiguïté potentielle que ces notions ne sont qu'intuitives. --Camion (discuter) 24 juillet 2017 à 18:26 (CEST)

OK, tout cela est sourçable. Je vais essayer de m'en occuper. --Jean-Christophe BENOIST (discuter) 24 juillet 2017 à 21:40 (CEST)

Qu'est-ce qu'une thèse au sens mathématique et logique ?

Dans l'article thèse au paragraphe au sens mathématique et logique, je découvre la définition: « En mathématique et en logique, la thèse est la partie d'un théorème que l'on démontre dans le cadre d'une base axiomatique donnée, à partir des hypothèses et de résultats théoriques précédemment établis ». je ne sais pas d'où ça vient et c'est en contradiction avec ce que nous essayons d'expliquer ici. --Pierre de Lyon (discuter) 11 octobre 2017 à 16:16 (CEST)

Ça n'a pas de sens bien clair (partie d'un théorème que l'on démontre ?) et à supposer que l'on puisse le reformuler correctement, ça ne correspond à aucun usage que je connais, Peut-être qu'il y a à creuser autour de l'usage du signe "thèse" en logique ? Pour "thèse de CHurch" la définition donnée "en philosophie" correspond. A effacer ama. Proz (discuter) 12 octobre 2017 à 08:50 (CEST)

Tu veux parler du signe $\vdash$ qui se lit « thèse ». En effet, j'y avais pensé, mais je pense que la signification de $\vdash$ a plutôt à voir avec la définition du paragraphe Au sens philosophique et rhétorique de l'article thèse, comme d'ailleurs pour « thèse de Church » comme tu les dis.. --Pierre de Lyon (discuter) 12 octobre 2017 à 10:43 (CEST)

Je ne pense pas que ce présent article qui parle d'un sujet très précis ait besoin d'être relié à un article vague et polysémique comme thèse. Autrement dit, ce qui est connu comme thèse de Church pourrait sans dommage être connu comme pensée de Church ou idée de Church, sans qu'il soit besoin de lier ce présent article qui relève de la calculabilité avec les articles pensée ou idée. Pour finir, à mon avis, s'il y a des interrogations à se poser concernant les définitions (polysémiques) de thèse#au sens mathématique et logique, ce n'est pas dans cet article qu'il faut en discuter mais dans l'article thèse. --Epsilon0 (discuter) 15 octobre 2017 à 01:01 (CEST)

On peut déplacer ou recopier la section dans discussion:Thèse (où je ne l'aurais pas vu directement). Proz (discuter) 15 octobre 2017 à 10:29 (CEST)

Poursuite dans : Discussion:Thèse#Qu'est-ce_qu'une_thèse_au_sens_mathématique_et_logique_?

Calcul plus rapide

On ne connaît pas de modèle de calcul plus puissant que les machines de Turing, c'est-à-dire qui serait en mesure [...] de calculer plus rapidement (c'est à dire dans une complexité en temps d'ordre inférieur) les fonctions calculables. Je ne comprends pas ce qui pose problème. C'est l'inverse qu'il faudrait sourcer. On pourrait imaginer qu'il puisse exister un modèle de calcul que ne change pas le domaine de calcul des MdT, mais qui améliore seulement la complexité en temps de, par exemple, la factorisation des nombres premiers, ou d'autres algos importants. Mais même si on limite les prétentions d'un nouveau modèle de calcul, on n'en trouve pas. Il faut le dire, non ? Cela dit, il me semble que - même si c'est trivialement évident et vrai - cela peut être sourcé, si on insiste vraiment. --Jean-Christophe BENOIST (discuter) 24 novembre 2017 à 17:57 (CET)

Peut-on donner un référence, d'une étude complète comparant plusieurs modèles de calcul sous le seul aspect de leur capacité à calculer rapidement ? Toute la complexité théorique que je connais est en terme de machine de Turing. Je serais vraiment preneur d'une complexité en terme de lambda-calcul par exemple. Ce n'est que si on a deux approches de la complexité différentes sur deux modèles différents que l'on pourra les comparer. --Pierre de Lyon (discuter) 24 novembre 2017 à 18:39 (CET)

Ce n'est vrai que si l'on a une maille assez lâche (à une constante près, temps polynomial), mais les machines de Turing ont un accès en temps linéaire à la mémoire (contrairement aux machines RAM par exemple où c'est en temps constant), donc ça ne peut pas être vrai pour le temps linéaire par exemple (le temps linéaire sur machines de Turing est quelque chose de très artificiel). On ne peut pas écrire une chose pareille, je pense que c'est souvent discuté au début des livres sur la complexité (Papadimitriou par ex.), où l'auteur précise les limites de la modélisation. Proz (discuter) 24 novembre 2017 à 20:18 (CET) PS.

Conflit d’édition —Je vois ce que tu veux dire. C'est une juste remarque. Il faudrait une.. thèse qui relierait la notion intuitive de "plus rapide" à une caractéristique de chaque modèle de calcul. Cela dit, il me semble bien avoir lu quelque-chose de ce genre, sans doute dans un sens "relaxé" et formellement inexact, mais peut-être pertinent dans un certain sens. Il faut en effet une source, et en l'absence je suis d'accord pour supprimer. Cordialement --Jean-Christophe BENOIST (discuter) 24 novembre 2017 à 20:20 (CET)

Lu dans l'article machine abstraite: « La « thèse d'invariance », dans la formulation de van Emde Boas stipule que deux modèles de machine « raisonnables » peuvent être simulés l'un par l'autre dans un temps polynomialement borné et avec une proportion constante de place additionnelle. ».

• Peter van Emde Boas, « Machine Models and Simulations », dans Jan van Leeuwen (éditeur), Handbook of Theoretical Computer Science. Volume A: Algorithms and Complexity, The MIT PRESS/Elsevier, 1990, 1003 p. (ISBN 9780444880710), p. 1–66.

Personnellement, je ne connais pas le sujet. --Pierre de Lyon (discuter) 28 novembre 2017 à 10:05 (CET)

On pourrait remplacer par ça qui est une version (faible) de la thèse de Church pour le temps polynomial (et pour l'espace), faible car il faut ajouter « raisonnables », il est bien-sûr possible en le faisant exprès de faire un modèle pour lequel c'est faux. Proz (discuter) 28 novembre 2017 à 11:34 (CET)

Très intéressant. Merci Pierre pour la source et l'information. A voir en effet comment insérer cela dans l'article. --Jean-Christophe BENOIST (discuter) 28 novembre 2017 à 12:48 (CET)

A lire aussi la section 6.1 de Harry. R. Lewis et Christos H. Papadimitriou, Elements of the theory of computation, Prentice Hall, 1998. Mais les modèles qui sont comparés entre eux ne sont que les machines de Turing de différentes structures, ce qui est biaisé. --Pierre de Lyon (discuter) 30 novembre 2017 à 14:19 (CET)