A simple online string rewriting tool

Basics of string rewriting

• A "string" is a sequence of "symbols".
• A "symbol" is a sequence of symbols that appear on your keyboard (avoid using some reserved ones).
• A "reduction rule" or "rewriting rule" is two strings l and r (or written as "l>r"). It says the left string can be reduced to the right one.
• This tool applies reduction rules to a string until no rules can be applied, the string we got is called a "normal form".

Features of this tool

• Simple syntax. Only 6 reserved symbols i.e. "(){}>,".
  • "()" used for specify which part you want to simplify first.
  • "{}" used for comment.
  • ">" used for writing reduction rule, e.g. "H>" reads "H" reduces to empty term.
  • "," used for separating symbols, rules, terms.
• Limited way to specify your reduction strategy.
  • Use "(x)" to tell the program to reduce "x" first.
  • Nested use is supported.
• Support multiple-term rewriting at a single run. Just separate terms using commas.

WARNING: Save your inputs on your device. This page stores no data.

Input 1. Symbols

Input 2. Rewriting rules

Input 3. Strings to be reduced

Load examples

Mod3 Arithmetic S4 Permutation group 4x4 Dyadic Matrix group

See Also

We know the rules seen as relations for 4x4 dyadic matrix group are complete. But that doesn't mean these rewriting rules are confluent and termninating. Actually, we don't know yet. But I have run 10000 tests all of which reached the normal form. Compared to the size 1152 of this group, the tests might suggest the two properties are true. Also, maybe we should be able to directly prove it by inspecting the rules.

Opened on: 08/07/2019. Last edited on: 08/23/2019