SO (complexité) - SO (complexity)

La logique du second ordre est une extension du premier ordre avec des quantificateurs de second ordre , par conséquent, le lecteur doit d'abord lire FO (complexité) pour être en mesure de comprendre cet article. Dans la complexité descriptive, nous pouvons voir que les langages reconnus par les formules SO sont exactement égaux aux langages décidés par les machines de Turing dans la hiérarchie polynomiale . Les extensions de SO avec certains opérateurs nous donnent également la même expressivité que celle donnée par une classe de complexité bien connue , c'est donc un moyen de faire des preuves sur la complexité de certains problèmes sans avoir à passer au niveau algorithmique .

Définition et exemples

Nous définissons une variable de second ordre, une variable SO a une arité et représente toute proposition d'arité , c'est-à-dire un sous-ensemble des -tuples de l'univers. Ils sont généralement écrits en majuscules. La logique du second ordre est l'ensemble des formules FO où nous ajoutons la quantification sur les variables du second ordre, par conséquent nous utiliserons les termes définis dans l' article FO sans les redéfinir .

Propriété

Forme normale

Chaque formule équivaut à une formule sous forme normale prenex, où nous écrivons d'abord la quantification sur la variable au second ordre, puis une formule FO sous la forme normale prenex.

Relation avec les classes de complexité

SO est égal à la hiérarchie polynomiale , plus précisément nous avons cette formule sous forme normale prenex où existentielle et universelle de second ordre alternées k fois sont le k ème niveau de la hiérarchie polynomiale.

Cela signifie que SO avec seulement une quantification existentielle du second ordre est égal à qui est NP , et avec seulement une quantification universelle est égal à qui est Co-NP .

Ajout de restrictions

Les formules de corne sont égales à P

SO (corne) est l'ensemble des requêtes booléennes définissables avec des formules SO sous forme normale disjonctive de sorte que les quantificateurs du premier ordre soient tous universels et que la partie sans quantificateur de la formule soit sous forme de corne , ce qui signifie qu'il s'agit d'un grand ET de OU, et dans chaque "OU", toutes les variables sauf peut-être une sont annulées.

Cette classe est égale à P .

Ces formules peuvent être faites sous forme de prenex où le second ordre est existentiel et le premier ordre universel sans perte de généralités.

Les formules Krom sont égales à NL

SO (Krom) est l'ensemble des requêtes booléennes définissables avec des formules du second ordre sous forme normale conjonctive de telle sorte que les quantificateurs du premier ordre sont universels et que la partie sans quantificateur de la formule est sous forme Krom , ce qui signifie que la formule du premier ordre est un grand ET de OU, et dans chaque "OU" il y a au plus deux variables.

Cette classe est égale à NL .

Ces formules peuvent être faites sous forme de prenex où le second ordre est existentiel et le premier ordre universel sans perte de généralités.

La fermeture transitive est PSPACE

SO (TC) est à SO ce que FO (TC) est à FO . L'opérateur TC peut désormais également prendre une variable de second ordre comme argument. SO (TC) est égal à PSPACE .

Le point le moins fixe est EXPTIME

SO (LFP) est à SO ce que FO (LFP) est à FO . L'opérateur LFP peut désormais également prendre une variable de second ordre comme argument. SO (LFP) est incroyablement similaire à EXPTIME .

Itérer

SO ( t ( n )) est à SO ce que FO [ t ( n )] est à FO . Mais nous avons maintenant également un quantificateur de second ordre dans le bloc de quantificateur. Il est connu que:

  • est égal à PSPACE c'est aussi une autre façon d'écrire SO (TC).
  • est égal à EXPTIME c'est aussi une autre façon d'écrire SO (LFP)

Voir également

Les références

Liens externes