Crate mrs_unify 

First-order unification and matching algorithms.

This crate provides algorithms for finding substitutions that make terms equal:

• unify - Most general unifier (MGU) of two terms
• match_term - One-way matching: find a substitution making a pattern equal to a target

Multiple algorithm implementations are available for educational comparison:

• robinson - Classic recursive algorithm (simple, easy to understand)

Examples

use mrs_core::{Term, SymbolTable};
use mrs_unify::unify;

let mut syms = SymbolTable::new();
let f = syms.intern("f");
let a = syms.intern("a");

// Unify f(X, a) with f(b, Y)
let b = syms.intern("b");
let t1 = Term::app(f, vec![Term::var(0), Term::constant(a)]);
let t2 = Term::app(f, vec![Term::constant(b), Term::var(1)]);

let mgu = unify(&t1, &t2).unwrap();
// X -> b, Y -> a
assert_eq!(mgu.apply_term(&Term::var(0)), Term::constant(b));
assert_eq!(mgu.apply_term(&Term::var(1)), Term::constant(a));

Modules

matching

One-way matching: find a substitution making a pattern equal to a target.

robinson

Robinson’s unification algorithm.

Enums

UnifyError

Error type for unification failures.

Functions

match_term

Matches a pattern against a target term (one-way unification).

unify

Unifies two terms, returning their most general unifier (MGU).

unify_comm

Unifies two terms with commutativity support for a set of binary symbols.

Type Aliases

UnifyResult

Result type for unification.