search

fmidue / logic-tasks

0 stars 1 forks source link

Rollen von `PropFormula` und `SynTree` #221

Open jvoigtlaender opened 3 days ago

jvoigtlaender commented 3 days ago

Bisher benutzen zwei Aufgabentypen (Teilformeln, Klammern entfernen) PropFormula als Eingabetyp, andere SynTree.

Motivation für die Verwendung von PropFormula scheint zu sein, dass da die Klammerpositionen (insbesondere auch zusätzlicher Klammern) explizit festgehalten werden.

Ist es auch so, dass nur PropFormula eine Eingabe wie A /\ B /\ C überhaupt parsen kann? Also wenn ein Aufgabentyp solche Eingaben annehmen soll ("Konzertaufgabe"), kann er nicht mit SynTree arbeiten?

Wie ist es hinsichtlich der Ausgabe? Gibt es nur für PropFormula die Möglichkeit des Pretty-Printings mit minimaler Klammeranzahl?

[Mittlerweile konkret adressiert:]

Letzteres hätte zum Beispiel Relevanz bei Wahrheitstafel-Aufgaben. Zum Beispiel könnte da im Moment eine Formel wie folgende ausgewürfelt werden (als diejenige Formel, zu der eine Wahrheitstafel anzugeben/auszufüllen ist): F = (C => C) <=> (¬B ∧ (A ∧ D)). Aber zu dem Zeitpunkt in der Lehrveranstaltung, wo diese Aufgabe verwendet wird, werden assoziative Operationen eigentlich schon nicht mehr so streng geklammert (und in der Tat werden die Wahrheitstafel-Aufgaben ja alternativ auch durch KNFs/DNFs gespeist). Also eigentlich würde man da dann gern F = (C => C) <=> (¬B ∧ A ∧ D) vorgeben. Aber gibt es einen Pretty-Printer, der den erzeugten SynTree so ausgibt? Oder muss man dafür entweder statt den SynTree zu würfeln, eine PropFormula würfeln, oder eine Konvertierungsfunktion zwischen diesen Typen benutzen?

jvoigtlaender commented 2 days ago

Ist es auch so, dass nur PropFormula eine Eingabe wie A /\ B /\ C überhaupt parsen kann? Also wenn ein Aufgabentyp solche Eingaben annehmen soll ("Konzertaufgabe"), kann er nicht mit SynTree arbeiten?

Ja, bezüglich der Eingabe ist das so.

jvoigtlaender commented 2 days ago

Wie ist es hinsichtlich der Ausgabe? Gibt es nur für PropFormula die Möglichkeit des Pretty-Printings mit minimaler Klammeranzahl?

Nein, für SynTree gibt es simplestDisplay.

In der Tat ist die Entscheidung jetzt, dass für die Ausgabe bestimmte Formeln (etwa Musterlösungen) immer als SynTrees zu erzeugen sind. Maximal noch für die Eingabe sollen PropFormulas benutzt werden.

jvoigtlaender commented 2 days ago

Wenn dennoch eine PropFormula vorliegt und ausgegeben werden soll (zum Beispiel, um eine von Studierenden eingegebene Formel "vorsichtshalber" zur Gegenprüfung nochmal auszugeben), dann kann wie in https://github.com/fmidue/logic-tasks/issues/224#issuecomment-2485383606 vorgeschlagen vorgegangen werden.

jvoigtlaender commented 2 days ago

Wenn eine "nicht unbedingt vollständig, aber auch nicht zu wenig geklammerte" Formel eingelesen werden soll (etwa (A /\ B /\ C) => D ist zu akzeptieren, aber A /\ B => C nicht), wie es etwa bei der Konzertaufgabe auftritt, dann sollte m.E. ein Parser für SynTree erstellt werden, der folgendermaßen vorgeht:

jvoigtlaender commented 2 days ago

Der Parser könnte liberalParser oder so heißen.

jvoigtlaender commented 2 days ago

Ein bisschen muss die Idee wohl noch verfeinert werden. Mit dem obigen Ansatz würden ja auch "zu viele Klammern" zurückgewiesen werden, etwa bei Eingabe von ((A /\ B)) => C.