Tools / Rewriting
Symbolic Rewrite Lab
This lab lets you explore a miniature first-order rewrite system with actual rule application, reachable-term graphs, normal forms, and toy e-class groupings. It is intentionally small, but it shows the mechanics behind confluence, termination, traversal strategy, and rewrite-driven search.
System Summary
Sample Normal Forms
Traversal Traces
Outermost Trace
Innermost Trace
Different traversal strategies can reach the same normal form by different routes, or expose different failure modes when a system is not well behaved.
Reachable Graph And Toy E-Classes
Reachable Rewrite Edges
Connected Components
The connected components are not a full equality-saturation implementation, but they give a compact way to see which terms end up living in the same local equivalence neighborhood.
How To Use This Lab
Enter a start term and one rewrite rule per line in the form left -> right. Variables begin
with ?, such as ?x. Then run the analysis to inspect traces, reachable terms, and
sample normal forms.
- Try identity-removal rules first, like
add(zero, ?x) -> ?x. - Compare outermost and innermost traces to see how strategy changes the path.
- Introduce competing rules to see how non-confluent behavior appears.
Fundamental Mathematics
A term rewriting system transforms structured expressions by applying local rules. The key global questions are whether rewriting terminates, whether different rewrite paths eventually agree, and what final forms can be reached. Confluence and termination are two of the most important properties because they determine whether “simplification” behaves predictably.
This lab is intentionally small, but it exposes the core mechanics behind normalization, symbolic search, and the rule-driven systems that appear in algebra engines, provers, and compiler-like optimizers.