9. Unification Flashcards
What is a matching problem?
Given a pattern and a target, find a substitution such that: pattern[substitution] == target
pattern: s(X) + Y target: s(0) + s(0) what is the substitution?
[0/X, s(0)/Y]
What does this mean?
What does this mean?
What does vars(t) this mean?
The set of all free variables in t
What does Vars mean?
the set of (all) free variables
What is vars(f(X, Y, g(a, Z, X))?
{X, Y, Z}
What is vars(f(a, b, c))?
{}
What does it mean for the pattern and target to be ‘standardised apart’ for matching?
vars(pattern) ∩ vars(target) = {}
Change the variable names in pattern so they arn’t any with the same name as in target.
Before/after/condition of decompose
Before/after/condition of conflict
Before/after/condition of eliminate
Before/after/condition of delete
What is the unification problem?
term1[substitution] == term2[subsitution]
Before/after/condition of switch?
Before/after/condition of occurs check?
Before/after/condition of coalesce?
What do the conditions of the unification algorithm ensure?
At most one rule applys
What is the termination condition of the unification algorthm?
No further rules apply
What is the definition of an mgu theta, given two terms s and t?
Before/after/condition of mutate rule (for commutativity)?
What is unitary? (mgu)
Single mgu (or none)
What is finitary? (mgu)
Finite number of mgu’s
What is infinitary? (mgu)
Possibly infinite mgu’s
What is nullary? (mgu)
No mgu’s exist (unifiers may still exist)
What type (mgu) and is it decidable: unification (no extensions)
unitary and decidable
What type (mgu) and is it decidable: unification with commutivity
finitary and decidable
What type (mgu) and is it decidable: unification with lambda calculus
infinitary and undecidable
