Module unify 

First-order unification for proof search.

Implements Robinson’s Unification Algorithm with occurs check. This is the core pattern-matching engine that enables logical reasoning.

What Unification Does

Unification finds a substitution that makes two terms identical:

Pattern	Target	Substitution
Mortal(x)	Mortal(Socrates)	{x ↦ Socrates}
Add(Succ(n), 0)	Add(Succ(Zero), 0)	{n ↦ Zero}
f(x, x)	f(a, b)	Fails (x can’t be both a and b)

Occurs Check

The occurs check prevents infinite terms. x = f(x) has no finite solution since it would require x = f(f(f(...))). We reject such unifications.

Alpha-Equivalence

Bound variable names are arbitrary: ∃e P(e) ≡ ∃x P(x). We handle this by substituting fresh constants for bound variables when unifying quantified expressions.

See Also

• beta_reduce - Normalizes lambda applications before unification
• ProofTerm - The term representation being unified
• ProofExpr - The expression representation for higher-order unification

Functions

apply_subst_to_expr

Apply a substitution to an expression.

apply_subst_to_term

Apply a substitution to a term.

beta_reduce

Beta-reduce an expression to Weak Head Normal Form (WHNF).

compose_substitutions

Compose two substitutions: apply s2 after s1.

unify_exprs

Unify two expressions, returning the Most General Unifier.

unify_pattern

Attempt higher-order pattern unification (Miller patterns).

unify_terms

Unify two terms, returning the Most General Unifier (MGU).

Type Aliases

ExprSubstitution

Substitution for expression-level meta-variables (holes).

Substitution

A substitution mapping variable names to terms.