unify_pattern

logicaffeine_proof::unify

Function unify_pattern 

Source 
pub fn unify_pattern(
    lhs: &ProofExpr,
    rhs: &ProofExpr,
) -> ProofResult<ExprSubstitution>
Expand description

Attempt higher-order pattern unification (Miller patterns).

Given lhs and rhs, if lhs is of the form Hole(h)(args...) where args are distinct BoundVarRefs, solves: h = λargs. rhs.

§Miller Patterns

A Miller pattern is a meta-variable applied to distinct bound variables:

  • ?P(x) is a valid pattern
  • ?F(x, y) is a valid pattern (x ≠ y)
  • ?G(x, x) is NOT valid (duplicate variable)
  • ?H(f(x)) is NOT valid (non-variable argument)

§Why This Matters

Higher-order pattern unification is decidable and has unique most general solutions, unlike full higher-order unification. This restriction enables automatic motive inference for structural induction.

§Returns

  • Ok(subst) - An ExprSubstitution mapping hole names to lambdas
  • Err(PatternNotDistinct) - If pattern has duplicate variables
  • Err(NotAPattern) - If arguments aren’t bound variable references
  • Err(ScopeViolation) - If RHS uses variables not in pattern scope

§Example

unify_pattern(?P(x), Even(x))
→ { "P" ↦ λx. Even(x) }

§See Also