fmidue / logic-tasks

0 stars 1 forks source link

Backwards implication operator #129

Closed nimec01 closed 3 months ago

nimec01 commented 4 months ago

Partial implementation of #29. The UniversalParser still needs some updates. For that, we need to decide whether => or <= has a higher precedence.

(A => B <= C) <=> (A => B) <= C

or

(A => B <= C) <=> A => (B <= C)

or completely disallow the use of <= without parentheses.

jvoigtlaender commented 4 months ago

or completely disallow the use of <= without parentheses.

This.

Also A /\ B \/ C is not allowed, must instead be explicitly written as (A /\ B) \/ C or A /\ (B \/ C). That's different from most text books or also from the BAI-Logik lecture (which has the convention that /\ binds stronger than \/). For the Komedia-Logik lecture I made the didactic decision that all parantheses must be written (except in specific cases/tasks on CNFs and DNFs, where associative uses of \/ and /\ are allowed), and hope the parsers faithfully implement that.

@owestphal will take a look at what needs to happen here concerning the implication symbols and parsing.

owestphal commented 4 months ago

This should be the straightforward way to implement backward implications. [untested] A few things to note:

Side note on precedence: With strictParens=False the parser uses the usual precedence of (allowed) operators. For implications, this means that A => B => C is parsed as A => (B => C). A <= B <= C should then be parsed as (A <= B) <= C.

jvoigtlaender commented 4 months ago

Hmm, this seems quite restrictive, and will make it impossible to input certain solutions. For example, after merging of the pull request, the syntax tree task will be able to generate and display a syntax tree for formula (A => B) /\ (C <= D), and will want the student to enter this formula as solution. But the parser will prevent this? Then the whole task generator would have to be reworked in order to not produce that syntax tree in the first place.

owestphal commented 4 months ago

I was under the impression that the idea was to have either => or <= in a formula but not both. If that is intended the commit is indeed insufficient. I'll revise that.

jvoigtlaender commented 4 months ago

@nimec01, the genIllegalOperator line mentioned in https://github.com/fmidue/logic-tasks/issues/29#issuecomment-2039005910 was not yet touched here in the pul request. Oversight or some specific reason for that?

owestphal commented 4 months ago

With both implications allowed simultaneously, strictParens=False now parses them with the same precedence and associativity. I.e. A => B <= C => D means A => (B <= (C => D)). We could change that but if the intent is to only use these with strictParens=True I think that should be fine for now.

jvoigtlaender commented 4 months ago

but if the intent is to only use these with strictParens=True

That's not the case, I think.

And maybe there is already a problem right now independently of whether backwards implementation is allowed?

In the "superfluous brackets task", it could happen (after introduction of <=, but the issue would also appear with just =>?) that the students are shown the formula A => (B <= (C => D)) and asked to remove superfluous brackets. Their input will then be parsed with strictParens = False (because the instance could also have been (A /\ B) /\ C and then they should be allowed to input A /\ B /\ C), but arrow operators are also present.

jvoigtlaender commented 4 months ago

The CI also seems unhappy about something.