Ambiguïté et logique

17

En théorie des automates (automates finis, automates pushdown, ...) et en complexité, il existe une notion d '"ambiguïté". Un automate est ambigu s'il existe un mot avec au moins deux cycles d'acceptation distincts. Une machine est k- ambiguë si pour chaque mot w accepté par la machine il y a au plus k exécutions distinctes pour accepter w .wkwkw

Cette notion est également définie sur des grammaires hors contexte: une grammaire est ambiguë s'il existe un mot qui peut être dérivé de deux manières différentes.

Il est également connu que de nombreux langages ont une belle caractérisation logique sur des modèles finis. (Si un langage est régulier, il existe une formule monadique de second ordre ϕ sur les mots de telle sorte que chaque mot w de L est un modèle de ϕ , de la même manière NP s'il est équivalent aux formules du deuxième ordre où tous les quantificateurs du deuxième ordre sont existentiels.)LϕwLϕ

Ma question se situe donc aux confins des deux domaines: y a-t-il un résultat, voire une définition canonique, de «l'ambiguïté» des formules d'une logique donnée?

Je peux imaginer quelques définitions:

  • est non ambigu s'il existe au plus un x tel que ϕ ( x ) estvraiet que ϕ ( x ) soit non ambigu. Xϕ(X)Xϕ(X)ϕ(X)
  • serait ambigu s'il existe un modèle à la fois ϕ 0 et ϕ 1 , ou si ϕ i est ambigu. ϕ0ϕ1ϕ0ϕ1ϕje
  • Une formule SAT serait non ambiguë s'il y a au plus une affectation correcte.

Par conséquent, je me demande si c'est une notion bien connue, sinon il peut être intéressant d'essayer de faire des recherches sur ce sujet. Si la notion est connue, quelqu'un pourrait-il me donner des mots-clés que je pourrais utiliser pour rechercher des informations sur le sujet (parce que "l'ambiguïté logique" donne beaucoup de résultats sans rapport), ou un livre / pdf / références d'article?

Arthur MILCHIOR
la source

Réponses:

11

Les règles dans une grammaire et les règles d'inférence dans la logique peuvent toutes deux être considérées comme des règles de production qui nous donnent "de nouvelles choses" à partir de "choses connues". Tout comme il peut exister de nombreuses façons de produire (ou d'analyser) un mot par rapport à une grammaire, il peut également exister de nombreuses façons de produire (ou de prouver) une formule logique. Cette analogie peut être tirée plus loin. Par exemple, certains systèmes logiques admettent des formes normales de preuves. De même, certaines grammaires admettent des arbres d'analyse canoniques.

Je dirais donc que vos exemples de logique vont dans la mauvaise direction. L'analogie correcte est

"arbre d'analyse": "mot" = "preuve": "formule logique"

En fait, une grammaire suffisamment générale pourra exprimer des règles logiques d'inférence typiques, de sorte que les mots grammaticalement corrects seront précisément les formules prouvables. Dans ce cas , les arbres parse effectivement être les preuves.

Dans le sens opposé, si nous sommes prêts à penser à des règles d'inférence très générales (qui n'ont pas nécessairement une saveur logique traditionnelle), alors chaque grammaire sera exprimable comme un système d'axiomes (terminaux) et de règles d'inférence (productions). Et encore une fois, nous verrons qu'une preuve est la même chose qu'un arbre d'analyse.

Andrej Bauer
la source
Je n'ai pas vraiment pensé aux preuves. Je suis plus habitué à la théorie des modèles (finis). Nous voulons savoir quels ensembles sont des modèles de formule et quels ensembles ne le sont pas. (Surtout, pour une formule, quelle est la complexité de trouver si un ensemble est un modèle ou non, et pour une formule prouvable, d'où les tautologies, la complexité est O (1) puisque tous les ensembles sont des modèles). Mais merci beaucoup pour votre réponse.
Arthur MILCHIOR
2
Eh bien, pour ajouter l'analogie: la théorie des modèles est à la logique ce que la sémantique est aux langues. La théorie des modèles attribue un sens aux théories logiques, tandis que la sémantique attribue un sens aux langues. Parfois, il est préférable de ne pas mélanger les pommes et les oranges, même si vous y êtes habitué.
Andrej Bauer
7

Juste deux remarques. J'espère qu'ils vous aideront.

Les définitions standard de la sémantique d'une logique et de la vérité suivent la présentation de Tarski, procédant par induction sur la structure des formules. Une autre possibilité est de donner une sémantique basée sur le jeu comme suggéré par Hintikka. La vérité et la satisfiabilité sont toutes définies en termes de stratégies dans un jeu. Pour les formules de premier ordre, on peut prouver qu'une formule est vraie selon la notion de Tarski si et seulement s'il existe une stratégie gagnante dans le jeu Hintikka.

Pour formaliser votre question, on peut se demander si le jeu admet plusieurs stratégies. Il y a aussi la question intéressante de savoir si les stratégies doivent être déterministes. Hintikka les obligeait à être déterministes. La preuve que l'original de Hintikka et la sémantique de Tarski sont équivalents nécessite l'Axiom of Choice. On peut aussi formaliser la vérité en termes de jeux avec des stratégies non déterministes avec moins de complications.

Votre exemple de théorie du langage a évoqué le déterminisme, les relations de simulation et l'acceptation du langage. Une relation de simulation entre automates implique l'inclusion d'une langue entre leurs langues bien que l'inverse ne soit pas vrai. Pour les automates déterministes, les deux notions coïncident. On peut se demander s'il est possible d'étendre les relations de simulation d'une manière «fluide» pour capturer l'équivalence du langage pour les automates non déterministes. Kousha Etessami a un très bon article montrant comment faire cela en utilisant des k-simulations ( Une hiérarchie de simulations calculables en temps polynomial pour les automates). Intuitivement, le «k» reflète le degré de non-déterminisme que la relation de simulation peut capturer. Lorsque «k» est égal au niveau de non-déterminisme dans l'automate, la simulation et l'équivalence du langage coïncident. Cet article donne également une caractérisation logique des k-simulations en termes de logique modale polyadique et un fragment variable borné de logique de premier ordre. Vous obtenez l'inclusion de la langue, le déterminisme, les jeux, la logique modale et la logique du premier ordre, le tout dans un package pare-chocs.

Vijay D
la source
4

Cela a commencé comme un commentaire sous la réponse d'Andrej Bauer, mais c'est devenu trop gros.

Je pense qu'une définition évidente de l'ambiguïté du point de vue de la théorie des modèles finis serait: unembjeguous(ϕ)M1,M2|M1ϕM2ϕM1ψM2ψ

En d'autres termes, il existe des modèles distincts de votre grammaire codés comme une formule qui peuvent être distingués par une formule ψ , peut-être une sous-formule de ϕ .ϕψϕ

Vous pouvez connecter cela à la réponse d'Andrej sur les preuves via la complexité descriptive. La combinaison de l'existence d'un codage d'un modèle particulier et de son acceptation par une MT appropriée comme modèle d'une formule donnée EST une preuve que les axiomes et les inférences (et donc une grammaire équivalente) codés dans cette formule sont cohérents.

Pour rendre cela entièrement compatible avec la réponse d'Andrej, vous devez dire que le modèle est "généré" par la formule agissant comme un filtre sur l'espace de tous les modèles finis possibles (ou quelque chose comme ça), avec l'encodage et l'action du filtrage sur le modèle d'entrée comme "preuve". Les preuves distinctes témoignent alors de l'ambiguïté.

Ce n'est peut-être pas un sentiment populaire, mais j'ai tendance à penser que la théorie des modèles finis et la théorie des preuves sont la même chose vue sous des angles différents. ;-)

Marc Hamann
la source
ϕ
Oui, cela aurait dû être "une formule". Je l'ai corrigé. Quant à distinguer les modèles finis, l'autre situation est qu'il n'y a qu'un seul modèle fini accepté pour votre langue (peut-être jusqu'à une certaine notion d'isomorphisme). C'est l'opposé de l'ambiguïté.
Marc Hamann
J'imagine que ce serait en effet une "ambiguïté". Je n'y ai tout simplement pas pensé comme ça. Surtout parce qu'en ce qui concerne la langue, cela ne serait pas vraiment intéressant. Mais d'un point de vue logique si
ça
Je ne suis pas sûr que la partie linguistique doive être ennuyeuse. J'ai plus d'idées à ce sujet, mais je pense que cela nous amènerait au-delà de la portée de ce forum. ;-)
Marc Hamann
0

Pas sûr de la question appliquée à CS, mais essayez de rechercher le terme d'imprécision et de logique. En philosophie de la logique, l'ambiguïté est généralement distinguée du flou (voir ici par exemple), et je pense que ce que vous recherchez est le flou (car le flou est défini comme des termes où il y a des cas limites). Le livre majeur dans ce domaine est Vagueness de Timothy Williamson (mais aussi voir la bibliographie sur le site de Stanford ci-dessus).

DanielC
la source
1
Merci pour votre réponse. Mais comme vous le dites, je ne vois pas vraiment de relation avec l'informatique. Surtout qu'un univers est ou n'est pas un modèle de formule, il n'y a pas vraiment de flou ici. Au lieu de cela, sur les automates, l'ambiguïté est quelque chose de bien défini, et il existe un algorithme connu pour décider si un automate est abigu, k-ambigu ou non ambigu. (uniquement sur une sorte d'automate)
Arthur MILCHIOR
Vous avez tout à fait raison, je n'aurais probablement pas dû me lancer sur cette question et m'en tenir à ce qui se cache. Je ne suis qu'un noob chez CS (sur le point de terminer mon premier cycle en logique / philosophie des sciences et mathématiques pures). Merci pour l'information.
DanielC
0

Je suis (également) d'accord avec Anrej.

Je pense que la complexité descriptive est une caractérisation sans calcul (ce qui la rend intéressante à sa manière) et donc les exemples d'ambiguïté computationnelle de la théorie des langages formels (automates / grammaires / ...) que vous avez donnés semblent être dans un domaine assez différent . Dans la complexité descriptive, les langages correspondent à des classes de complexité et les requêtes (dans un langage) correspondent à des problèmes de calcul (pas d'algorithmes). Il n'y a aucun moyen prévu de vérifier / calculer une requête AFAIK, donc si vous ne recherchez pas une ambiguïté de calcul à mon humble avis, ces exemples sont trompeurs.

Kaveh
la source
Kaveh, je ne suis pas sûr d'être d'accord pour dire que la caractérisation sans calcul de la complexité descriptive est 100% correcte. Les détails de calcul sont très importants pour comprendre comment une logique particulière capture une classe de complexité. L'avantage est qu'une fois que vous avez fait vos preuves et compris comment cela fonctionne, vous pouvez mettre de côté le calcul et vous concentrer sur les détails logiques à l'aide de méthodes logiques standard.
Marc Hamann
Même remarque à Mark. La complexité descriptive est également connue sous le nom de théorie de base de données, un vocabulaire étant la structure d'une base de données et les modèles de la théorie étant le contenu de la base de données. C'est pourquoi nous sommes heureux de pouvoir calculer et déterminer si une base de données respecte une formule.
Arthur MILCHIOR
UNEC0FO
1
@Kaveh, je fais un point légèrement subtil, mais qui je pense est important, car il semble être souvent mal compris (par exemple par des tentatives P = NP? Échouées). Il existe un algorithme sous-jacent, assez brutal, qui sous-tend la correspondance d'un langage logique et d'une classe de complexité. Travailler avec la logique vous permet de ne pas avoir à penser aux détails de cet algorithme à chaque seconde, mais la beauté et le génie des preuves de Fagin, Immerman, Vardi et d'autres résident exactement dans la description de ces algorithmes. Les personnes qui les perdent complètement de vue se retrouvent généralement en difficulté.
Marc Hamann
1
@Kaveh, je pense que nous nous comprenons et partageons notre respect pour le terrain. "Brute-force" n'a pas été conçu comme une légère influence sur les algorithmes sous-jacents, juste pour clarifier que nous parlons de quelque chose d'un peu plus abstrait que ce que quelqu'un qui fait, par exemple, un travail d'optimisation algorithmique pourrait penser comme un algorithme.
Marc Hamann