PropFormula-Parser benutzt falsche Priorität für Implikation und Bi-Implikation

[patritzenfeld]

Die Parser-Instanz von PropFormula Char gibt diesen Operatoren zu hohe Priorität: Sie binden stärker als das Und. Das ist bisher nicht relevant, aber da ich PropFormulas mit ToSat auf Äquivalenz testen möchte (und das möglicherweise auch hier hinzufüge), kommen leider falsche Ergebnisse zustande.

fromRight (Atomic 'X') $ parse parser "" "A /\\ B => C"

Erwartung: Assoc Impl (Assoc And (Atomic 'A') (Atomic 'B')) (Atomic 'C')

Tatsächliches Resultat: Assoc And (Atomic 'A') (Assoc Impl (Atomic 'B') (Atomic 'C')) (enspricht A /\\ (B => C))

[jvoigtlaender]

Ich überblicke die Auswirkungen nicht sofort, aber ist vielleicht die Verwendung von ToSat für PropFormula einfach der falsche Weg für den konkreten Zweck? Sollte besser ToSat für SynTree verwendet werden?

[patritzenfeld]

Ich wollte explizit PropFormula verwenden, weil diese erlaubt weniger Klammern zu nutzen. Bei SynTree kann man keine redundante Klammerung weglassen und das wäre bei der Eingabe eher nervig.

[owestphal]

Das Problem besteht grundsätzlich für alle Parser, die auf FromGrammar basieren. Der UniversalParser hat die falschen Präzedenzen. Ich schaue gerade mal wie schnell sich das beheben lässt.

[jvoigtlaender]

Okay, da kommt es natürlich auf den Kontext an. Also in einer beliebigen Logik-Vorlesung (etwa bei Frau König) und fast jedem beliebigen Logik-Textbuch sind sehr viel mehr Klammern redundant als in der aktuellen Fassung von "Komedia-Logik". Wenn man also Übungsaufgaben für "Komedia-Logik" stellt, dann ist A /\\ B => C keine syntaktisch korrekte Eingabe. (Das schränkt natürlich die Verwendbarkeit von Aufgaben in anderen Lehrveranstaltungen ein, und das ist zugegebenermaßen ein gewisses Problem, aber irgendwie ein nicht-im-Moment-Problem.)

Für "Komedia-Logik" kann man in (A /\\ (B /\\ D)) => C die inneren Klammern weglassen, aber die äußeren nicht. Man kann, genauer, exakt die Klammern weglassen, die in Aufgabentyp LogicTasks.Syntax.SimplestFormula als redundant angesehen werden. (Ob genau dafür ein passgenauer und einfach drop-in verwendbarer Parser existiert, weiß ich gerade nicht.)

[jvoigtlaender]

Das Problem besteht grundsätzlich für alle Parser, die auf FromGrammar basieren. Der UniversalParser hat die falschen Präzedenzen. Ich schaue gerade mal wie schnell sich das beheben lässt.

Dieses Beheben ist prinzipiell wohl sinnvoll, und macht das Ganze zumindest nicht weniger gut nutzbar als zuvor. Für den Einsatz in "Komedia-Logik" stellt sich auch dann allerdings noch die Frage, ob man (als Aufgabensteller) explizit verbieten können sollte, dass etwas wie A /\\ B => C eingegeben wird. Denn aus Sicht der Lehrveranstaltung ist überhaupt nicht klar, ob die Lesart davon als (A /\\ B) => C überhaupt korrekter ist denn die als A /\\ (B => C). Zumindest die Studierenden haben (außer durch Lesen eines Textbuches) keinen wirklichen Grund, mit A /\\ B => C gerade (A /\\ B) => C zu "meinen". Es könnte also sogar in gewissem Sinne falsches Feedback gegeben werden, wenn jemand A /\\ B => C eingibt. (Es bestünde natürlich die Möglichkeit, es dann nochmal als (A /\\ B) => C auszugeben, als Teil der Syntax-Vorabprüfung, und Studierende könnten dann merken, dass sie Klammern nutzen müssten, wenn sie mit A /\\ B => C eigentlich A /\\ (B => C) meinten.)

[owestphal]

Das Problem besteht grundsätzlich für alle Parser, die auf FromGrammar basieren. Der UniversalParser hat die falschen Präzedenzen.

Das stimmt so natürlich auch nicht ganz, da die meisten dieser Parser gar keine Implikationen erlauben. Nur PropFormula Char hat die Kombination strictParens= False und allowImplicaton/allowBiImplication = True.

[jvoigtlaender]

Vielleicht sollte für den Moment die Erwartung eher sein:

fromRight (Atomic 'X') $ parse parser "" "A /\\ B => C"

führt zu Error?

[patritzenfeld]

Mir war nicht bewusst, dass in Komedia-Logik die Präzedenz nicht besprochen wird. Dann ist das wohl auch erstmal nicht besonders schlimm.

[patritzenfeld]

Vielleicht sollte für den Moment die Erwartung eher sein:

fromRight (Atomic 'X') $ parse parser "" "A /\\ B => C"

führt zu Error?

Das hier wäre dann genau das Verhalten das ich brauche.