Classe d'ensembles dont les complémentaires sont récursivement énumérables ; équivalemment, problèmes pour lesquels la non-appartenance peut être semi-décidée par une procédure effective qui s'arrête sur les instances négatives.

Principe

Un ensemble est co-récursivement énumérable (co-r.e.) s'il existe une machine de Turing qui s'arrête et accepte exactement les entrées qui ne sont pas dans l'ensemble ; co-r.e. capture la semi-décidabilité de la fausseté plutôt que de la vérité.

Démonstration

Si l'ensemble de l'arrêt K est récursivement énumérable, alors son complément, constitué des codages de couples programme/entrée qui ne s'arrêtent pas, est co-récursivement énumérable ; l'appartenance au complément peut être confirmée si un reconnaisseur de non-arrêt existe (souvent via l'énumération de preuves de non-arrêt dans des contextes restreints).

Mauvaise application

Supposer que co-r.e. implique décidabilité, ou traiter une procédure qui parfois infirme l'appartenance comme une méthode de réfutation uniforme pour toutes les entrées sans vérifier la couverture de tous les cas.

Conséquence

Pour un ensemble co-r.e., on peut certifier algorithmiquement la non-appartenance en exécutant le co-reconnaisseur jusqu'à l'acceptation ; comme les ensembles r.e., les ensembles co-r.e. peuvent ne pas admettre de réfutation universelle efficace de l'appartenance sans structure supplémentaire.

Inversion

Récursivement énumérable : ensembles semi-décidables pour l'appartenance ; décidables : ensembles à la fois r.e. et co-r.e. ; Non-co-r.e. : complémentaires d'ensembles dépourvus d'énumérateurs pour les non-membres.

Limite

Défini par rapport à des modèles standards ; la classe n'est pas fermée par complément en général (le complément d'un ensemble co-r.e. est r.e., mais beaucoup d'ensembles ne sont ni r.e. ni co-r.e.) ; exclut les classes d'oracle ou de complexité supérieure sauf indication contraire.

Tension sémantique

La tension est avec r.e. : l'asymétrie entre reconnaissance de preuves positives et de preuves négatives engendre des comportements algorithmiques et des propriétés de clôture différentes.

Synthèse

Co-récursivement énumérable formalise la reconnaissabilité algorithmique de la non-appartenance : alors que l'appartenance peut rester inatteignable, la non-appartenance peut être certifiée par une procédure effective halting lorsque l'ensemble appartient à cette classe.