Prouver qu'un programme se termine ne veut pas dire démontrer qu'un programme se termine.
Tu peux aussi démontrer qu'il ne se termine pas. Mais dans la plupart des cas, tu ne pourras démontrer ni l'un ni l'autre, et c'est tout le problème.
Par contre sur un programme donné, dont on connait par avance les specs et les états souhaitables il est possible (même programmatiquement) de voir
a) Si on ne rencontre effectivement que des états souhaitables
b) Si on termine le programme.
Par état souhaitable, tu veux dire état dont on sait qu'il mêne au bon résultat (et à une terminaison du programme) ? Si c'est le cas, alors la détermination des états souhaitables revient à prouver le programme, et est impossible dans le cas général par quelque chose de puissance équivalente à une machine de Turing (MT).
prouver le b) n'est qu'une question de temps.
Prouver qu'un programme termine (sur un jeu de données fixé) n'est qu'une question de temps: il suffit de l'exécuter. Prouver qu'un programme ne termine pas est une autre paire de manches.
Je pense qu'il est temps de recentrer un peu le débat, car on s'éloigne un peu. Tu disais que du moment qu'on a un langage Turing complet, on peut prouver ses programmes. Or, tout langage Turing complet permet de produire des programmes dont on ne peut pas prouver la terminaison avec quelque chose de la même puissance qu'une MT.
Je ne sais pas comment expliquer ça de manière plus claire. Tu as l'air de penser qu'à partir du moment où on choisit un programme en particulier, alors il devient prouvable. Ce n'est vrai que dans des cas particuliers. Il n'est pas possible d'écrire un programme validant la terminaison d'un autre programme quelconque. Tu peux penser qu'un humain peut le faire, mais ça suppose que la thèse de Church-Turing est fausse. En tout cas, une MT ne peut pas le faire, c'est un résultat mathématique bien établi.
[^] # Re: C'est trop compliqué !
Posté par Yusei (Mastodon) . En réponse au journal Des langages de haut niveau. Évalué à 2.
Une preuve fausse n'a pas beaucoup d'intérêt.
Tu peux aussi démontrer qu'il ne se termine pas. Mais dans la plupart des cas, tu ne pourras démontrer ni l'un ni l'autre, et c'est tout le problème.
Par état souhaitable, tu veux dire état dont on sait qu'il mêne au bon résultat (et à une terminaison du programme) ? Si c'est le cas, alors la détermination des états souhaitables revient à prouver le programme, et est impossible dans le cas général par quelque chose de puissance équivalente à une machine de Turing (MT).
Prouver qu'un programme termine (sur un jeu de données fixé) n'est qu'une question de temps: il suffit de l'exécuter. Prouver qu'un programme ne termine pas est une autre paire de manches.
Je pense qu'il est temps de recentrer un peu le débat, car on s'éloigne un peu. Tu disais que du moment qu'on a un langage Turing complet, on peut prouver ses programmes. Or, tout langage Turing complet permet de produire des programmes dont on ne peut pas prouver la terminaison avec quelque chose de la même puissance qu'une MT.
Je ne sais pas comment expliquer ça de manière plus claire. Tu as l'air de penser qu'à partir du moment où on choisit un programme en particulier, alors il devient prouvable. Ce n'est vrai que dans des cas particuliers. Il n'est pas possible d'écrire un programme validant la terminaison d'un autre programme quelconque. Tu peux penser qu'un humain peut le faire, mais ça suppose que la thèse de Church-Turing est fausse. En tout cas, une MT ne peut pas le faire, c'est un résultat mathématique bien établi.