Arrêter le problème sans référence personnelle: pourquoi cet argument ne suffit-il pas (ou le fait-il)?

J'essaie de trouver un moyen d'expliquer l'idée de la preuve du problème de l'arrêt de la manière la plus accessible possible (aux étudiants CS de premier cycle). L'argument le plus simple que j'ai trouvé est celui-ci ; c'est précisément le style de traitement que je vise. Cependant, l'auto-référence (en particulier, vérifier si un programme s'arrête sur lui-même) n'est pas la plus didactique.

Ce que je me demande, en tant que croquis de preuve, c'est pourquoi nous ne pourrions pas simplifier encore plus et dire: si nous supposons un programme H(P,I)pour le problème de l'arrêt qui s'arrête avec vrai si P(I)s'arrête et s'arrête avec faux sinon, alors nous pourrions créer un programme de la forme:

def Q(J):
  if H(Q,J) then loop forever
  else halt

... qui est un programme valide si et seulement si le problème d'arrêt est un programme valide. Nous pouvons alors nous demander: à quoi devrait H(Q,J)revenir une valeur arbitraire J? Nous voyons une contradiction dans les deux possibilités, et nous concluons que puisque l'existence de Hnous permet de construire le programme contradictoire Q, donc un programme de la forme Hne peut pas exister.

Il y a encore une certaine auto-référence ici dans la mesure où le programme Qvérifie s'il s'arrête ou non sur l'entrée actuelle (et fait le contraire), mais pour moi, cela semble beaucoup plus intuitif que de mettre en place une situation où nous avons besoin d'un appel de la forme P(P)ou H(P,P), etc. Cependant, je n'ai pas vu cet argument plus simple utilisé, et je pense qu'il l'aurait été s'il était valable. Mes questions sont donc les suivantes:

• L'argument ci-dessus est-il suffisant comme preuve (esquisse) du problème de l'arrêt?
  • Si oui, pourquoi tant d'arguments vont-ils avec une étape déroutante du formulaire P(P)ou H(P,P)? (Est-ce juste pour supprimer "l'entrée" sans importance de l'équation?)
  • Sinon, qu'est-ce qui manque?

Il existe une variété de questions connexes sur ce sujet, telles que:

• Arrêter le problème sans autoréférence
• Existe-t-il une preuve plus intuitive de l'indécidabilité du problème d'arrêt que la diagonalisation?

J'ai également trouvé la mention de la preuve basée sur le paradoxe de Berry, qui est assez attrayante. Pourtant, je n'ai pas encore réussi à me convaincre si l'argument spécifique ci-dessus fonctionne ou non (même si ce n'est que pour ma propre compréhension; je sens que je manque peut-être quelque chose de stupide et je voudrais savoir ce que c'est).

Je ne pense pas que ce soit une bonne façon de présenter le problème de l'arrêt, car il balaie un problème critique sous les couvertures de manière sournoise. Je suggère de m'en tenir à une présentation plus standard, comme celle que vous avez liée. Si vous voulez trouver un moyen de l'expliquer de manière à minimiser le contenu technique, la présentation de cette vidéo est étonnamment accessible et reste fidèle à la logique de la preuve standard.

Passons aux difficultés de votre proposition. Dans votre proposition, il n'est pas trivial d'écrire le code d'un tel Q. Pensez à ce que signifie avoir la ligne

  if H(Q,J) then loop forever 

Rappelez-vous que le premier argument de Hest une chaîne de bits qui contient le code / algorithme / machine de Turing - ce n'est pas un pointeur vers la fonction, mais une chaîne. Naïvement, cela semble signifier que nous incluons une chaîne codée en dur qui contient le code source de Q, à l'intérieur du code de Q. Mais ce n'est pas possible. Supposons que le code de Qprenne 100 caractères. Ensuite, nous devons coder en dur une constante de chaîne de 100 caractères dans la définition de Q, et nous avons également besoin de plus de caractères pour le reste de la logique - et cela représente plus de 100 caractères. Si vous y réfléchissez, il est évident que nous ne pouvons pas avoir une constante de chaîne à l'intérieur du code Qqui est le code de Q, car ce serait trop long.

Vous pensez peut-être que ce n'est pas ce que vous aviez en tête. Peut-être que vous pensiez que le langage de programmation aura une API intégrée pour obtenir le code de la fonction actuelle, donc en fait, le code auquel vous pensiez est quelque chose comme:

def Q(J):
  if H(get_source_code_of_current_function(),J) then loop forever
  else halt

OK bien. Cela prouve que le problème d'arrêt ne peut pas être résolu pour le code écrit dans n'importe quel langage de programmation doté d'une get_source_code_of_current_function()API. Cependant, mon langage de programmation préféré n'a pas une telle API. Donc, cette preuve ne prouve rien sur mon langage de programmation préféré - peut-être que le problème d'arrêt est résolu pour mon langage, qui sait? De même, les machines Turing n'ont pas une telle API, donc cela ne prouve pas que le problème d'arrêt des machines Turing est indécidable.

Et c'est une faille majeure dans votre preuve. Et c'est une faille qui est subtile et pas du tout évidente. Je ne pense pas que ce soit pédagogiquement une bonne idée de présenter une preuve qui "semble valide" en surface mais qui est en fait, une fois que vous y creusez plus profondément, défectueuse.

Maintenant, il est possible de récupérer votre preuve proposée. Il est en fait possible de construire une fonction Qqui fonctionne comme vous l'avez dit; vous en avez essentiellement besoin pour être une quine . Je suppose qu'en principe, vous pourriez expliquer l'idée des quines, puis présenter votre preuve et expliquer comment implémenter une fonction en Q utilisant ces idées. Mais cela me semble une mauvaise idée, d'un point de vue pédagogique. Les quines sont hallucinantes et mystérieuses et flippantes à comprendre. Un étudiant qui ne comprend pas les quines ne comprendra pas votre preuve. Et cela rend la preuve de l'indécidabilité du problème d'arrêt beaucoup plus mystérieuse qu'elle ne devrait l'être. Cela ne me semble donc pas être un moyen plus accessible de comprendre le problème de l'arrêt.

Je ne vois pas comment l'auto-référence est difficile sur le plan pédagogique. Le Barber Paradox est assez facile à comprendre. Et votre argument a une auto-référence implicite, et je trouve cela plus difficile à comprendre qu'une simple auto-référence. En plus de cela, c'est incohérent. Pour définir H (Q, J), vous devez d'abord savoir ce qu'est Q, et pour définir Q, vous devez d'abord savoir ce qu'est H (Q, J). Ça ne marche pas. Au mieux, vous pouvez affirmer que Q est un point fixe de cette définition autoréférentielle, mais si vous essayez de tirer quelque chose de la nature contradictoire de Q, vous montrez simplement que H n'existe pas OU qu'aucun tel point fixe n'existe ; vous devez maintenant prouver que si H existait, le point fixe devrait exister.