Unification is an algorithmic process of solving equations between symbolic expressions.
I have solved a few execercises in FOL: f(x,b()) = f(a(),y) has one unifier: [a()/x,b()/y],
Is it possible to use Unification for Lambda Calculus terms?
For example (= means beta reduces to):
Equation: (λx.T) b = a b. Solve for T
Solution: [(a x)/T].
Verification: ((λx.T) b) [(a x)/T] = (λx.a x) b = a b
I have also found that Gérard Huet created unification algorithm for simply typed lambda calculus. I have just started learning and would appreciate any hint.