search

fmidue / logic-tasks

0 stars 1 forks source link

retire, or relegate to tests, the `applySteps` computation? #101

Closed jvoigtlaender closed 6 months ago

jvoigtlaender commented 6 months ago

In here: https://github.com/fmidue/logic-tasks/blob/13d9cdb36010567355e1a3f89a6ac529c6331141/src/LogicTasks/Semantics/Resolve.hs#L236-L239 there seems to be redundancy.

Is it possible at all that any isEmptyClause (fromMaybe [] applied) becomes False when fst stepsGraded is True? If not, the computation of applySteps clauses steps might as well be completely avoided here. Then, applySteps and applyStep wouldn't be needed anywhere in the task type anymore. They could still be kept around in the test suite, as a check against future regressions. That is, applyStep and applySteps would be used to test that gradeSteps works correctly and keeps making the correct decisions. But only gradeSteps (which is needed anyway for its feedback output) would be used inside the task type itself.

jvoigtlaender commented 6 months ago

Or maybe there is no full redundancy, and whatever any isEmptyClause (fromMaybe [] applied) checks on top of fst stepsGraded should be demonstrated via a unit test put in the test suite. To preserve knowledge about what it adds.

jvoigtlaender commented 6 months ago

... and maybe the coverage is the other way around, i.e., the && (printFeedbackImmediately || fst stepsGraded) is superfluous?

nimec01 commented 6 months ago

See https://github.com/fmidue/logic-tasks/pull/102#issue-2125589300

jvoigtlaender commented 6 months ago

So it seems you have to come to the conclusion there that indeed the left conjunct of

any isEmptyClause (fromMaybe [] applied) && (printFeedbackImmediately || fst stepsGraded)

was redundant, not the right one.

I had been flip-flopping above about which of the two is redundant at that point.

I just very briefly played around with an older version of the task directly in Autotool now, and am still suspicious.

Can you check what the version without using applySteps does on an input like [ ({A}, {¬A}, {}) ]? (on an arbitrary task instance)

jvoigtlaender commented 6 months ago

The old task version says this on such input: image

which appears to come from code involving applySteps, but wouldn't now be checked at all anymore?

nimec01 commented 6 months ago

You are right. It does not check that. I will add the missing check.

Betrachten Sie die folgende Formel in KNF:>>>> <B ∧ (¬A ∨ ¬B) ∧ (A ∨ ¬B)> <<<<

Führen Sie das Resolutionsverfahren an dieser Formel durch, um die leere Klausel abzuleiten.
Geben Sie die Lösung als eine Liste von Tripeln an, wobei diese folgendermaßen aufgebaut sind: (Erste Klausel, Zweite Klausel, Resolvente)
Beachten Sie dabei die folgenden möglichen Schreibweisen:
>>>>Negation: <-, ~, nicht> <<<<

>>>>Nicht-leere Klausel: <{ ... }> <<<<

>>>>Leere Klausel: <{ }> <<<<

Optional können Sie Klauseln auch durch Nummern ersetzen.
Klauseln aus der Formel sind bereits ihrer Reihenfolge nach nummeriert. (erste Klausel = 1, zweite Klausel = 2, ...).
Neu resolvierte Klauseln können mit einer Nummer versehen werden, indem Sie '= NUMMER' an diese anfügen.
>>>>Ein Lösungsversuch könnte beispielsweise so aussehen:  <[(1, 2, {A, nicht B} = 5), (4, 5, { })]> <<<<

Just ()
[({A}, {~A}, { })]
---- Input ----
[Res {trip = (Left A,Left ¬A,({ },Nothing))}]
---- Partial ----
Alle Schritte verwenden existierende Indizes?
>>>> <Ja.> <<<<

Kein Index wird mehrfach vergeben?
>>>> <Ja.> <<<<

Genutzte Literale kommen in Formel vor?
>>>> <Ja.> <<<<

Just ()
---- Complete ----
Alle Schritte sind gültig?
>>>> <Ja.> <<<<

Letzter Schritt leitet die leere Klausel ab?
>>>> <Ja.> <<<<

Lösung ist korrekt?
>>>> <Ja.> <<<<

Just ()
jvoigtlaender commented 6 months ago

Wouldn't it be enough to replace

isCorrect = printFeedbackImmediately || fst stepsGraded

by

isCorrect = isJust applied

in #102, and adding something like printWithHint (isNothing applied) (... "In mindestens einem Schritt werden ..." ...)?

jvoigtlaender commented 6 months ago

... or maybe not replacing, but adding the isJust applied check in isCorrect.

jvoigtlaender commented 6 months ago

Ah, probably scrap that. It should be isCorrect = any isEmptyClause (fromMaybe [] applied), I think.

nimec01 commented 6 months ago

Ah, probably scrap that. It should be isCorrect = any isEmptyClause (fromMaybe [] applied), I think.

This works.

Betrachten Sie die folgende Formel in KNF:>>>> <B ∧ (¬B ∨ ¬C) ∧ (¬B ∨ C)> <<<<

Führen Sie das Resolutionsverfahren an dieser Formel durch, um die leere Klausel abzuleiten.
Geben Sie die Lösung als eine Liste von Tripeln an, wobei diese folgendermaßen aufgebaut sind: (Erste Klausel, Zweite Klausel, Resolvente)
Beachten Sie dabei die folgenden möglichen Schreibweisen:
>>>>Negation: <-, ~, nicht> <<<<

>>>>Nicht-leere Klausel: <{ ... }> <<<<

>>>>Leere Klausel: <{ }> <<<<

Optional können Sie Klauseln auch durch Nummern ersetzen.
Klauseln aus der Formel sind bereits ihrer Reihenfolge nach nummeriert. (erste Klausel = 1, zweite Klausel = 2, ...).
Neu resolvierte Klauseln können mit einer Nummer versehen werden, indem Sie '= NUMMER' an diese anfügen.
>>>>Ein Lösungsversuch könnte beispielsweise so aussehen:  <[(1, 2, {A, nicht B} = 5), (4, 5, { })]> <<<<

Just ()
[({B}, {~B}, { })] 
---- Input ----
[Res {trip = (Left B,Left ¬B,({ },Nothing))}]
---- Partial ----
Alle Schritte verwenden existierende Indizes?
>>>> <Ja.> <<<<

Kein Index wird mehrfach vergeben?
>>>> <Ja.> <<<<

Genutzte Literale kommen in Formel vor?
>>>> <Ja.> <<<<

Alle Schritte sind gültig?
>>>> <Ja.> <<<<

Letzter Schritt leitet die leere Klausel ab?
>>>> <Ja.> <<<<

Just ()
---- Complete ----
Lösung ist korrekt?
>>>> <Nein.> <<<<

Nothing
jvoigtlaender commented 6 months ago

But feedback like printWithHint (isNothing applied) (... "In mindestens einem Schritt werden ..." ...) would still add something that's not currently signalled.

nimec01 commented 6 months ago

But feedback like printWithHint (isNothing applied) (... "In mindestens einem Schritt werden ..." ...) would still add something that's not currently signalled.

Should this be part of partialGrade then?

jvoigtlaender commented 6 months ago

Good point. Previously it happened in completeGrade, but actually it is something that might make sense to already reject in partialGrade, possibly even independently of whether printImmediateFeedback is set.

The message would need to be more general, then. Because using a not yet available clause is not the only reason applySteps can result in Nothing. It also results in Nothing if a resolution step itself is not correct. (Which previously would have been rejected outright via the checking that is now guarded by printImmediateFeedback. So, previously, when applySteps gave Nothing in completeGrade, one already knew that partialGrade had run through successfully and thus that other reason for Nothing was already exluded. Not so now, when the printImmediateFeedback stuff is only optionally rejecting and preventing further processing of a submission.)

jvoigtlaender commented 6 months ago

Hmm, it's really a matter of debate. Maybe it should happen inside the printImmediateFeedback stuff, and thus be either in partialGrade or in completeGrade, depending on what the lecturer sets.

nimec01 commented 6 months ago

Hmm, it's really a matter of debate. Maybe it should happen inside the printImmediateFeedback stuff, and thus be either in partialGrade or in completeGrade, depending on what the lecturer sets.

If we were to implement it in this way, wouldn't it also make sense to implement the check of "Used literals are present in formula?" in the same way? This is currently happening at partialGrade.

jvoigtlaender commented 6 months ago

I've made a refashioned implementation over at #102.

Can you check it altogether gives reasonable feedback (modulo issue #107) now?

I opted to not move the "Used literals are present in formula?" check into the "optional feedback at submission time" part. That check is really purely syntactic, in contrast to the others. So, I think it makes sense to always run it. If the submission contains made-up literals, that is really a different kind of issue than not being able to perform resolution steps or writing them down with correct referencing etc.

nimec01 commented 6 months ago

The feedback is probably what you expected.

Invalid steps:

Betrachten Sie die folgende Formel in KNF:>>>> <D ∧ (¬A ∨ ¬D) ∧ (A ∨ ¬D)> <<<<

Führen Sie das Resolutionsverfahren an dieser Formel durch, um die leere Klausel abzuleiten.
Geben Sie die Lösung als eine Liste von Tripeln an, wobei diese folgendermaßen aufgebaut sind: (Erste Klausel, Zweite Klausel, Resolvente)
Beachten Sie dabei die folgenden möglichen Schreibweisen:
>>>>Negation: <-, ~, nicht> <<<<

>>>>Nicht-leere Klausel: <{ ... }> <<<<

>>>>Leere Klausel: <{ }> <<<<

Optional können Sie Klauseln auch durch Nummern ersetzen.
Klauseln aus der Formel sind bereits ihrer Reihenfolge nach nummeriert. (erste Klausel = 1, zweite Klausel = 2, ...).
Neu resolvierte Klauseln können mit einer Nummer versehen werden, indem Sie '= NUMMER' an diese anfügen.
>>>>Ein Lösungsversuch könnte beispielsweise so aussehen:  <[(1, 2, {A, nicht B} = 5), (4, 5, { })]> <<<<

Just ()
[({A},{~A},{ })]
---- Input ----
[Res {trip = (Left A,Left ¬A,({ },Nothing))}]
---- Partial ----
Alle Schritte verwenden existierende Indizes?
>>>> <Ja.> <<<<

Kein Index wird mehrfach vergeben?
>>>> <Ja.> <<<<

Genutzte Literale kommen in Formel vor?
>>>> <Ja.> <<<<

Alle Schritte sind gültig?
>>>> <Ja.> <<<<

Letzter Schritt leitet die leere Klausel ab?
>>>> <Ja.> <<<<

Alle Schritte nutzen vorhandene oder zuvor abgeleitete Klauseln?
>>>> <Nein.> <<<<

>>>>Mindestens ein Schritt beinhaltet Klauseln, die weder in der Formel vorhanden sind, noch zuvor abgeleitet wurden.
<<<<
Nothing
---- Complete ----
Lösung ist korrekt?
>>>> <Nein.> <<<<

Nothing

Valid steps:

Betrachten Sie die folgende Formel in KNF:>>>> <¬A ∧ (A ∨ ¬D) ∧ (A ∨ D)> <<<<

Führen Sie das Resolutionsverfahren an dieser Formel durch, um die leere Klausel abzuleiten.   
Geben Sie die Lösung als eine Liste von Tripeln an, wobei diese folgendermaßen aufgebaut sind: (Erste Klausel, Zweite Klausel, Resolvente)
Beachten Sie dabei die folgenden möglichen Schreibweisen:
>>>>Negation: <-, ~, nicht> <<<<

>>>>Nicht-leere Klausel: <{ ... }> <<<<

>>>>Leere Klausel: <{ }> <<<<

Optional können Sie Klauseln auch durch Nummern ersetzen.
Klauseln aus der Formel sind bereits ihrer Reihenfolge nach nummeriert. (erste Klausel = 1, zweite Klausel = 2, ...).
Neu resolvierte Klauseln können mit einer Nummer versehen werden, indem Sie '= NUMMER' an diese anfügen.
>>>>Ein Lösungsversuch könnte beispielsweise so aussehen:  <[(1, 2, {A, nicht B} = 5), (4, 5, { })]> <<<<

Just ()
[(1,2,{~D}),(1,3,{D}),({D},{~D},{ })]
---- Input ----
[Res {trip = (Right 1,Right 2,(¬D,Nothing))},Res {trip = (Right 1,Right 3,(D,Nothing))},Res {trip = (Left D,Left ¬D,({ },Nothing))}]
---- Partial ----
Alle Schritte verwenden existierende Indizes?
>>>> <Ja.> <<<<

Kein Index wird mehrfach vergeben?
>>>> <Ja.> <<<<

Alle Schritte verwenden existierende Indizes?
>>>> <Ja.> <<<<

Kein Index wird mehrfach vergeben?
>>>> <Ja.> <<<<

Alle Schritte verwenden existierende Indizes?
>>>> <Ja.> <<<<

Kein Index wird mehrfach vergeben?
>>>> <Ja.> <<<<

Genutzte Literale kommen in Formel vor?
>>>> <Ja.> <<<<

Alle Schritte sind gültig?
>>>> <Ja.> <<<<

Letzter Schritt leitet die leere Klausel ab?
>>>> <Ja.> <<<<

Alle Schritte nutzen vorhandene oder zuvor abgeleitete Klauseln?
>>>> <Ja.> <<<<

Just ()
---- Complete ----
Lösung ist korrekt?
>>>> <Ja.> <<<<

Just ()
jvoigtlaender commented 6 months ago

Um zu prüfen, ob recoverFrom den gewünschten Effekt hat (wie er laut Kommentar vielleicht auch in #89 gebraucht werden wird), könnte mal noch mit printFeedbackImmediately = False getestet werden und:

Denn dann wird stepsGraded ja erst in completeGrade durchgeführt und dort soll selbst wenn stepsGraded "Nicht-Okay" sagt, dennoch nicht abgebrochen sondern bis zur Lösungsanzeige weitergegangen werden. (Und in beiden Fällen sollen die Ausgaben von stepsGraded angezeigt werden.)

nimec01 commented 6 months ago

Auch mit printFeedbackImmediately = False sieht das Feedback in beiden Fällen wie erwartet aus (und läuft bis zur Lösungsanzeige durch). Hier der Output von dem Negativfall:

Betrachten Sie die folgende Formel in KNF:>>>> <¬D ∧ (¬B ∨ D) ∧ (B ∨ D)> <<<<

Führen Sie das Resolutionsverfahren an dieser Formel durch, um die leere Klausel abzuleiten.
Geben Sie die Lösung als eine Liste von Tripeln an, wobei diese folgendermaßen aufgebaut sind: (Erste Klausel, Zweite Klausel, Resolvente)
Beachten Sie dabei die folgenden möglichen Schreibweisen:
>>>>Negation: <-, ~, nicht> <<<<

>>>>Nicht-leere Klausel: <{ ... }> <<<<

>>>>Leere Klausel: <{ }> <<<<

Optional können Sie Klauseln auch durch Nummern ersetzen.
Klauseln aus der Formel sind bereits ihrer Reihenfolge nach nummeriert. (erste Klausel = 1, zweite Klausel = 2, ...).
Neu resolvierte Klauseln können mit einer Nummer versehen werden, indem Sie '= NUMMER' an diese anfügen. 
>>>>Ein Lösungsversuch könnte beispielsweise so aussehen:  <[(1, 2, {A, nicht B} = 5), (4, 5, { })]> <<<<

Just ()
[({B}, {~B}, { })]
---- Input ----
[Res {trip = (Left B,Left ¬B,({ },Nothing))}] 
---- Partial ----
1. Schritt verwendet nur existierende Indizes?
>>>> <Ja.> <<<<

1. Schritt vergibt keinen Index wiederholt?   
>>>> <Ja.> <<<<

Genutzte Literale kommen in Formel vor?
>>>> <Ja.> <<<<

Just ()
---- Complete ----
Alle Schritte sind gültig?
>>>> <Ja.> <<<<

Letzter Schritt leitet die leere Klausel ab?
>>>> <Ja.> <<<<

Alle Schritte nutzen vorhandene oder zuvor abgeleitete Klauseln?
>>>> <Nein.> <<<<

>>>>Mindestens ein Schritt beinhaltet eine Klausel, die weder in der Formel vorhanden ist, noch zuvor abgeleitet wurde.
<<<<
Lösung ist korrekt?
>>>> <Nein.> <<<<

Nothing