Mutate misconceptions in a richer operator space (W/M/R/xor), and decide a simplification policy for distractors

[sidprasad]

Follow-up to #173, which added exact in-grammar rewrite identities for W/M/R/xor in spotutils (_rewrite_to_tutor_grammar). Those identities make a more interesting generalization possible: apply misconception mutations in the richer operator space, then rewrite back into the tutor grammar. Filing so the design discussion doesn't get lost; this should not land while the three-arm framing experiment is collecting data (English-to-LTL distractors are the instrument).

The generalization

applyWeakU in codebook.py is already the weak-until identity hand-coded at a single AST shape: a U b → (a U b) | G a, i.e. a W b expressed in-grammar. Generalizing:

1. Expand: canonicalize the answer formula with SPOT's simplifier, which naturally introduces W/M/R/xor.
2. Mutate: apply misconception rules where they are single operator swaps — strong↔weak (U ↔ W, M ↔ R), inclusive↔exclusive (<-> ↔ xor), etc.
3. Rewrite back into the tutor grammar via the Simplify randltl exercise formulas within the tutor grammar #173 identities, so students never see out-of-grammar operators.

Why bother: attribution, not just reach

The distractor→misconception mapping drives the adaptive weights and the feedback explainers, and mutating surface forms can get the label wrong:

• For a pool formula like G a | (a U b) (canonically a W b), the strong-reading error is a U b. Today the only syntactic path there is dropping a disjunct via applyUnderconstraint, which tags the distractor OtherImplicit instead of WeakU — so the evidence model and the explainer both learn the wrong thing. In W-space it is a one-step W → U swap with the correct label.
• An exclusive reading of | (a | b → !(a <-> b)) is a documented propositional misconception that changeBinaryOperator's class-swap machinery cannot reach at all today.

Should distractors themselves be simplified?

Related question with real trade-offs (scope note: trace-sat questions are unaffected — the mutant formula is never displayed, and simplification preserves the traces).

For: (a) form symmetry — after #173 correct answers are idiomatic while mutants can carry machine-generated redundancy (e.g. changeUnaryOperator turning X(F a) into F(F a)), so option bloat becomes a cue correlated with wrongness; (b) a genuine misconception-holder should endorse the proposition, not a spelling.

Against: (a) diagnosis runs through structural recognition — novices recognize their own reading by structural correspondence with the English, not by closing over equivalence, so a structurally remote equivalent spelling produces false negatives in the evidence model; (b) simplification destroys minimal-pair contrast at the decision point; (c) explainers (#172) point at structure that must remain visible in the option; (d) the codebook is grounded in observed student errors in their observed surface forms; (e) much of the gain is illusory — applyWeakU's output round-trips to itself ((a U b) | G a → a W b → (a U b) | G a).

Suggested resolution — tiered: full simplification stays inside the equivalence/dedup/trace machinery where form is invisible; display gets hygiene-only normalization (idempotence collapse F F a → F a, G G a → G a, double negation), which removes the machine-generated tells while preserving the mutation's structural skeleton, minimal pairs, and explainer anchoring.

Cautions

• New mutation rules mean new MisconceptionCode entries plus explainer text in the syntax-aware renderer — a research-taxonomy decision, not just engineering, since the codebook is empirically grounded.
• Whatever policy is chosen, keep simplification out of the displayed option unless it is the hygiene tier above.
• Timing: after the current experiment concludes, or behind a flag.