The MU Puzzle

The puzzle cannot be solved: it is impossible to change the string MI into MU by repeatedly applying the given rules. In other words, MU is not a theorem of the MIU formal system. To prove this, one must step "outside" the formal system itself. Wikipedia

using Metatheory, Test

Here are the axioms of MU:

• Composition of the string monoid is associative
• Add a uf to the end of any string ending in I
• Double the string after the M
• Replace any III with a U
• Remove any UU

function ⋅ end
miu = @theory x y z begin
  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
end

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

No matter the timeout we set here, MU is not a theorem of the MIU system

params = SaturationParams(timeout = 12, eclasslimit = 8000)
start = :(M ⋅ I ⋅ END)
g = EGraph(start)
saturate!(g, miu)
@test false == areequal(g, miu, start, :(M ⋅ U ⋅ END); params = params)

Test Passed

This page was generated using Literate.jl.