search

fmidue / logic-tasks

0 stars 1 forks source link

Potenzielles Refactoring von `correctMapping` #107

Closed nimec01 closed 6 months ago

nimec01 commented 6 months ago

Die correctMapping Funktion bei dem Resolve task überprüft, ob der Nutzende

und gibt ein entsprechendes Feedback aus.

Dieses Feedback wird aber pro Resolutionsschritt ausgegeben und könnte verwirrend sein, falls erst im zweiten Resolutionsschritt ein ungültiger Index verwendet wird. Hier ein Beispiel:

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

Führen Sie das Resolutionsverfahren an dieser Formel durch, um die leere Klausel abzuleiten.
[...]
>>>>Ein Lösungsversuch könnte beispielsweise so aussehen:  <[(1, 2, {A, nicht B} = 5), (4, 5, { })]> <<<<

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

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

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

Nothing
---- Complete ----
[...]

Die beiden Aussagen 

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

sind hier widersprüchlich.

Mir fallen zwei Möglichkeiten ein, dies zu verbessern:

  1. Das Feedback gibt spezifisch an, welcher Resolutionsschritt gerade überprüft wird
  2. correctMapping wird so umgeschrieben, dass sie zwei Bools und kein Feedback ausgibt. Das Feedback wird dann einmalig mit den Ergebnissen des Aufrufs ausgegeben.
jvoigtlaender commented 6 months ago

Die 1. Möglichkeit ist sicher die attraktivere.

Die Implementierung könnte so laufen, dass

    checkMapping = correctMapping sol $ baseMapping clauses

durch

    checkMapping = correctMapping (zip [1..] sol) $ baseMapping clauses

ersetzt wird und dann

correctMapping :: OutputMonad m => [ResStep] -> [(Int,Clause)] -> LangM m
correctMapping [] _ = pure()
correctMapping (Res (c1,c2,(c3,i)): rest) mapping = do

durch

correctMapping :: OutputMonad m => [(Int,ResStep)] -> [(Int,Clause)] -> LangM m
correctMapping [] _ = pure ()
correctMapping ((j, Res (c1,c2,(c3,i))) : rest) mapping = do

und in "Alle Schritte verwenden existierende Indizes?" wird etwas wie "{j}. Schritt verwendet nut existierende Indizes?" und in "Kein Index wird mehrfach vergeben?" etwas wie "{j}. Schritt vergibt keinen Index wiederholt?" geschrieben.