Rollen von PropFormula und SynTree

[jvoigtlaender]

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]

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]

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]

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 #224 (comment) vorgeschlagen vorgegangen werden.

[jvoigtlaender]

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:

• die Eingabe wird als PropFormula geparst
• auf die PropFormula wird toTree angewendet
• es wird geprüft, ob show auf der PropFormula exakt den gleichen String liefert wie simplestDisplay auf dem im vorigen Schritt erhaltenen SynTree
• falls nein, wird die Eingabe als "zu wenige Klammern verwendend" zurückgewiesen
• falls doch, wird die Eingabe akzeptiert und besagter SynTree zurückgeliefert

[jvoigtlaender]

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

[jvoigtlaender]

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.

[jvoigtlaender]

Kann sein, dass hinterher die Funktion toSynTree wieder "un-exposed" werden kann, weil sie außerhalb logic-tasks gar nicht gebraucht wird, wenn etwa entsprechend #226 (comment) vorgegangen wird.