Le papier
- Lauri Hella et José María Turull-Torres, Requêtes informatiques avec des logiques d'ordre supérieur , TCS 355 197–214, 2006. doi: 10.1016 / j.tcs.2006.01.009
propose une logique VO, une logique d'ordre variable. Cela permet de quantifier les commandes sur les variables. VO est assez puissant et peut exprimer certaines requêtes non calculables. (Comme le souligne Arthur Milchior ci-dessous, il capture en fait l'ensemble de la hiérarchie analytique .) Les auteurs montrent que le fragment de VO obtenu en autorisant uniquement une quantification universelle limitée sur les variables d'ordre exprime exactement toutes les requêtes ce. La VO permet aux variables d'ordre de s'étendre sur les nombres naturels, donc délimiter les variables d'ordre est clairement une condition naturelle à imposer.
Existe-t-il un (joli) fragment de VO qui capture P ou NP?
Par analogie, dans la logique classique du premier ordre permettant la quantification sur des ensembles d'objets donne une logique plus puissante appelée logique du deuxième ordre ou SO. SO capture l'ensemble de la hiérarchie polynomiale ; ceci est généralement écrit comme PH = SO. Il existe des formes restreintes de SO capturant des classes de complexité importantes: NP = SO, P = SO-Horn et NL = SO-Krom. Ceux-ci sont obtenus en imposant des restrictions sur la syntaxe des formules autorisées.
Il existe donc des moyens simples de restreindre SO pour obtenir des classes intéressantes. Je voudrais savoir s'il existe des restrictions simples et similaires de VO qui sont à peu près le bon niveau d'expressivité pour P ou NP. Si de telles restrictions ne sont pas connues, je serais intéressé par des suggestions de candidats potentiels, ou par certains arguments pourquoi il est peu probable que de telles restrictions existent.
J'ai vérifié les (quelques) articles qui citent celui-ci et vérifié les phrases évidentes sur Google et Scholar, mais je n'ai rien trouvé de bien évident. La plupart des articles traitant de logiques plus puissantes que le premier ordre ne semblent pas traiter des restrictions pour faire baisser le pouvoir dans le domaine des calculs "raisonnables", mais semblent se contenter d'habiter dans l'univers de la CE des classes arithmétiques et analytiques. Je serais heureux avec un pointeur ou une phrase non évidente à rechercher; cela peut être bien connu de quelqu'un qui travaille dans des logiques d'ordre supérieur.
la source
Réponses:
Remarque: cela ne répond pas vraiment à la question, ce ne sont que quelques commentaires postés comme réponse. :)
Le problème est que vous voulez probablement que le langage soit sans symboles supplémentaires comme l'égalité, l'addition, la multiplication (non?), Si nous les avions alors par le théorème MRDP, les formules diophantiennes (quantificateurs existentiels de premier ordre devant une égalité de deux polynômes) capturerait les ensembles de ce. Si nous n'autorisons pas ces symboles dans le langage, le problème est plus compliqué, on peut utiliser des quantificateurs d'ordre supérieur pour les définir, mais cela augmenterait la complexité des quantificateurs. Donc, si je veux répondre brièvement à votre question sur un seul quantificateur, je ne sais pas.
Quelques commentaires supplémentaires:
la source
Pour information, VO est en fait vraiment plus puissant que ce que vous dites; il contient toute la hiérarchie analytique (donc aussi toute la hiérarchie arithmétique). Le résultat n'est pas publié, ni soumis à aucun endroit, mais vous pouvez le trouver sur ma page, www.milchior.fr/ho.pdf section 7 page 47.
Sinon, vous pouvez certainement restreindre VO en restreignant l'ordre maximal accepté; mais ensuite vous obtenez une langue "d'ordre supérieur" (HO), et ce n'est probablement pas ce que vous voulez.
la source
Pour répondre à votre commentaire, je suppose que je devrais faire une autre réponse, en ne parlant que sur Krom et Horn (Peut-être devrais-je poser une question à ce sujet à CSTheory)
Je vous suggère de lire la section 5.3 page 34 de mon article sur le problème que j'ai rencontré sur Horn et Krom dans une logique d'ordre élevé. Vous rencontrerez le même problème dans l'ordre variable (qui est clairement un surensemble de l'ordre élevé).
Je ne sais pas si vous y avez prêté attention, mais SO (krom) est égal à P lorsque le premier ordre est universel; en effet, vous pouvez exprimer un problème NP-complet si vous ajoutez une variable de premier ordre existante. (Je ne me souviens pas de l'exemple que j'avais avant, je peux essayer de le rechercher si vous le souhaitez)
Je ne sais pas ce que deviendrait cette restriction syntaxique pour la logique d'ordre élevé ou d'ordre variable ... mon point est juste que vous devriez également penser à un bon moyen de restreindre les quantificateurs, car restreindre la partie sans quantificateur seule n'est pas utile ( au moins pour les formules Krom)
la source