9. Unification

Question 1

What is a matching problem?

Answer 1

Given a pattern and a target, find a substitution such that: pattern[substitution] == target

Question 2

pattern: s(X) + Y target: s(0) + s(0) what is the substitution?

Answer 2

[0/X, s(0)/Y]

Question 3

What does this mean?

Answer 3

Question 4

What does this mean?

Answer 4

Question 5

What does vars(t) this mean?

Answer 5

The set of all free variables in t

Question 6

What does Vars mean?

Answer 6

the set of (all) free variables

Question 7

What is vars(f(X, Y, g(a, Z, X))?

Answer 7

{X, Y, Z}

Question 8

What is vars(f(a, b, c))?

Answer 8

{}

Question 9

What does it mean for the pattern and target to be ‘standardised apart’ for matching?

Answer 9

vars(pattern) ∩ vars(target) = {}

Change the variable names in pattern so they arn’t any with the same name as in target.

Question 10

Before/after/condition of decompose

Answer 10

Question 11

Before/after/condition of conflict

Answer 11

Question 12

Before/after/condition of eliminate

Answer 12

Question 13

Before/after/condition of delete

Answer 13

Question 14

What is the unification problem?

Answer 14

term₁[substitution] == term₂[subsitution]

Question 15

Before/after/condition of switch?

Answer 15

Question 16

Before/after/condition of occurs check?

Answer 16

Question 17

Before/after/condition of coalesce?

Answer 17

Question 18

What do the conditions of the unification algorithm ensure?

Answer 18

At most one rule applys

Question 19

What is the termination condition of the unification algorthm?

Answer 19

No further rules apply

Question 20

What is the definition of an mgu theta, given two terms s and t?

Answer 20

Question 21

Before/after/condition of mutate rule (for commutativity)?

Answer 21

Question 22

What is unitary? (mgu)

Answer 22

Single mgu (or none)

Question 23

What is finitary? (mgu)

Answer 23

Finite number of mgu’s

Question 24

What is infinitary? (mgu)

Answer 24

Possibly infinite mgu’s

Question 25

What is nullary? (mgu)

Answer 25

No mgu’s exist (unifiers may still exist)

Question 26

What type (mgu) and is it decidable: unification (no extensions)

Answer 26

unitary and decidable

Question 27

What type (mgu) and is it decidable: unification with commutivity

Answer 27

finitary and decidable

Question 28

What type (mgu) and is it decidable: unification with lambda calculus

Answer 28

infinitary and undecidable