Se calcul et calculabilité
Contexte
Théorème de base sur la relation entre le calcul (→c) et la calculabilité.
Énoncé
Variables
x, y
Conditions
- x et y sont des formules
- x →c y ou y →c x
Conclusion
La calculabilité de x et y sont identiques.
Preuve
Supposons x calculable et x →c y : alors il existe z qui est un calcul terminé et tel que x c→ z. Comme x →c y et que le calcul est linéaire (il n'y a pas le choix de la manière de calculer), on déduit que l'on a soit y = z soit y →c z. Dans les deux cas on déduit que y est calculable.
Supposons x calculable et y →c x : y est alors clairement calculable.
Par symétrie des propriétés utilisées dans l'énoncé, si y est calculable alors x est calculable.