Décidabilité d'un problème
Bonjour,
j'étudie actuellement le théorème de Rice et le problème de l'arrêt. Je suis tombé sur un questionnaire sans les solutions en rapport avec ce sujet et j'aurai aimé avoir quelques avis.
Voilà le problème :
Citation:
Question 2 :
Les propriétés suivantes sont-elles extensionnelles ? Les formaliser d’abord logiquement puis
dire si elles sont extensionnelles.
1. Le programme p calcule une fonction.
2. Le programme p calcule une fonction bornée par une constante c.
Question 3
Est-ce qu’une de ces propriétés est décidable ?
Voilà ce que j'en pense :
1 ) La propriété d'un programme de calculer une fonction est extensionnelle. En effet, pour un programme p et q, si SEM(p)=SEM(q) et que p calcul une fonction, q calculera aussi une fonction.
Je pense par contre que ce problème n'est pas décidable. Je m'explique :
soit calcFonct un programme dont la sémantique est la suivante
SEM(calcFonct)(p) = vrai si p calcul une fonction
On peut donc réduire ce problème à celui de l'arrêt existentiel et donc de l'arrêt tout court.
2 ) Pareil, propriété extensionnelle. Si un programme C a pour sémantique la réalisation d'une fonction qui rend des couples dont les images sont inférieurs à "c", un programme q de me sémantique aura les mêmes résultats.
Pour la décidabilité, c'est donc une propriété extensionnelle, et non triviale (on peut facilement trouver un programme qui réalise cette propriété et un programme qui ne la réalise pas), donc Rice nous dit que c'est indécidable.
Voilà en gros, est-ce le bon raisonnement ?
Merci d'avance.
Edit : je ne suis pas certain que ce soit le bon endroit pour cette question, mais je ne savais vraiment pas ou la poser.
