status SRS-Relative/Zantema_06_relative/

Das sind 13 hand-crafted Beispiele von Hans Zantema. Für jedes (?) sieht ein Mensch durch Draufgucken "sofort", daß es terminiert, weil jeweils ein Buchstabe eine besondere Rolle spielt (z.B. in #399 der Buchstabe p)

In der letzten Competition blieben offen: rel03, rel07, rel11, rel12. Siehe https://termcomp.github.io/Y2021/job_47874_47873.html (im Textfeld unter "benchmark" kann man eintragen "/rel", um die Anzeige zu beschränken).

Inzwischen sind gelöst:

• rel12 (RULES b p b -> a b a p b a, p ->= a p a, a p a ->= p) (#399): skeleton: (1/2,3)\Matrix{\Natural}{10}(0/2,2)[]
• rel07 ( https://termcomp.github.io/tpdb.html?ver=11.2&path=SRS_Relative%2FZantema_06_relative%2Frel07.xml hat das einen Sinn? Da fährt irgendwas hin und her?) Beweis:

skeleton: (6/2,4)\TileAllAll{3}(1536/512,64)\Weight(310/512,61)\Unlabel
(5/2,4)\TileAllAll{3}(1280/512,64)\Weight(310/512,61)\Matrix{\Natural}{2}
(164/512,61)\Weight(16/512,54)\Unlabel(1/2,3)\Matrix{\Natural}{3}(0/2,3)[]

Ich kann mir ein nettes kleines Workshop-Paper vorstellen, in dem diese Lösungen diskutiert werden sowie die beiden noch offenen

(RULES a c -> c c a,          -- rel03
       c ->= b a a b,
       b a a b ->= c)

(RULES b p b -> b a p b,       -- rel11
       p ->= a p a,
       a p a a ->= p)

rel11 sollte doch wie rel12 gehen. Warum findet es mein Solver nicht?

Zu rel03: der Beweis für den Menschen ist: es handelt sich hier eigentlich (genau das ist zu zeigen) um a b a a b \to b a a b b a a b a, ist Instanz von a(b a^i b)\to (b a^i b)^j a, ist RFC-MB by i, steht in Jörgs Diplomarbeit, und

cat tpdb/tpdb-4.0/SRS/HofWald/4.srs
( RULES a b a a a a b -> b a a a a b b a a a a b a )

( COMMENT this is a test case for RFC/Matchbound implementations
          as we think that  a w  -> w w a  for  w = b a^n  b
          is RFC-matchbounded by n )

Tja, das Problem gibts noch, aber es heißt jetzt Mixed_SRS/4.xml https://termcomp.github.io/tpdb.html?ver=11.2&path=SRS_Standard%2FMixed_SRS%2F4.xml und der Kommentar ist weg.