MU-puzzle tutorial example has a flawed rule and test

[tgorordo]

Hi! This is maybe a bit of a silly little thing to bring up just before the 3.0 release where I assume the docs will get/need some rewrites, but the MU-puzzle tutorial example has a couple of issues which were unfortunate to run into as a first-time-user.

The first hint that something is off is that Metatheory saturates - it shouldn't be able to and should timeout/hit a param limit for the MIU theory, but more concretely it can't prove some theorems that are true when they need the associativity axiom: e.g. substituting 'MUIIU' for 'MU' still finds it unreachable (the tutorial test succeeds). This is wrong: 'MUIIU' has a derivation - from GEB: MI, MII, MIIII, MIIIIU, MUIU, MUIUUIU, MUIIU.

I'm new to playing with Metatheory, but I think the string concatenation associativity rule:
x ⋅ (y ⋅ z) --> (x ⋅ y) ⋅ z should be an EqualityRule i.e. x ⋅ (y ⋅ z) == (x ⋅ y) ⋅ z (for it to correctly find 'MUIIU' it's actually enough just to reverse the order of the rule to (x ⋅ y) ⋅ z --> x ⋅ (y ⋅ z), but in general I suspect it would need to be able to go both ways; I haven't gone hunting for an example).

And for the unreachable 'MU', the test should check for a missing result, since Metatheory will fail to meet it's goal and can't saturate, in which case areequal returns missing - not false as the test in the tutorial is written to expect (which would be correct except the system should not saturate).

[gkronber]

I was able to reproduce this with branch ale/3.0.

The rule set given in the example is:

5-element Vector{RewriteRule}:
 ~x ⋅ (~y ⋅ ~z) --> (~x ⋅ ~y) ⋅ ~z
 (~x ⋅ I) ⋅ END --> ((~x ⋅ I) ⋅ U) ⋅ END
 (M ⋅ ~x) ⋅ END --> ((M ⋅ ~x) ⋅ ~x) ⋅ END
 (I ⋅ I) ⋅ I --> U
 ((~x ⋅ U) ⋅ U) ⋅ ~y --> ~x ⋅ ~y

The analysis is correct, we need x ⋅ (y ⋅ z) == (x ⋅ y) ⋅ z to be able to produce the form (I ⋅ I) ⋅ I within a sequence. Since the rules only use the left-associative form of ⋅ , we would otherwise not be able to produce .... (I ⋅ I) ⋅ I .

Additionally, I'm not sure the last rule ((~x ⋅ U) ⋅ U) ⋅ ~y --> ~x ⋅ ~y is correct as it requires non-empty x and y. Will check the original source.

[0x0f0f0f]

fixed