Tools / Matching
Unification And Matching Lab
Test whether two simple first-order terms unify, and whether a pattern matches a concrete target. This lab is designed to make substitution and binding behavior visible instead of leaving it as a hidden part of a symbolic rule engine.
Binding Summary
Substitutions
Educational Notes
Matching is directional: the pattern can bind variables to fit the target. Unification is symmetric: both terms are allowed to constrain the final substitution as long as they can be made identical.
- Try changing only the inner argument to see when a match fails.
- Use repeated variables like
f(?x, ?x)to test consistency constraints. - Use different function symbols to see structural mismatch immediately.
Why This Matters
Unification and matching sit underneath rewrite engines, theorem provers, logic programming, and many symbolic assistants. Even when a tool feels algebraic on the surface, this kind of structural binding is often what determines whether a rule can fire.
How To Use This Lab
Enter two terms in simple prefix form such as f(?x, g(?y)) and f(a, g(b)). Terms
with leading ? names are treated as variables that may bind to subterms.
- Use repeated variables like
pair(?x, ?x)to test consistency constraints. - Change function symbols to see structural mismatch immediately.
- Compare the unification result with the one-way pattern-match result.
Fundamental Mathematics
Unification asks whether two symbolic terms can be made identical by substituting values for variables. Matching is the directional version where only the pattern side is allowed to bind. These operations are central to rule application, logic programming, theorem proving, and symbolic pattern systems.
The important point is that this is structural mathematics, not string replacement. The tree shape of the expression determines whether a substitution is valid.