Computer Aided Formal Reasoning 1996/7 Lecture notes 9 Thomas Schreiber and Judith Underwood

Unification

I’ve taken some the material in this section from Chapter 7 of First-Order Logic and Automated Theorem Proving, by Melvin Fitting. This book is mostly about classical logic, but it also discusses principles and techniques which apply more generally to other logics. In particular, Fitting is a world expert on tableau based theorem proving, and this book gives a nice introduction to this idea in the familiar setting of classical logic.

Lego often has to unify two terms t_{1} and t_{2}. This means finding substitutions for free variables which make the two terms identical. Denoting a substitution by σ, the problem of unification can be stated as, “Given t_{1} and t_{2}, find σ such that σt_{1} = σt_{2}.” This σ is called a unifier for the two terms.

We’ll look at unification in general terms. Efficient implementations of unification are of great interest, particularly for languages like Prolog. Most implementations of Prolog actually use an unsound unification algorithm because correct unification is less efficient.

Let us consider the simplest case, where terms are made up of only variables and constants. A disagreement pair for terms t_{1} and t_{2} is a pair of different terms d_{1} and d_{2}, subterms of t_{1} and t_{2} respectively, such that d_{1} and d_{2} describe the “largest” difference between t_{1} and t_{2}. This is best defined in terms of differences between the parse trees of the two terms – d_{1} and d_{2} should have the same path from the root of the parse tree but have different roots themselves.

The algorithm is as follows:

Let σ be the empty substitution. while σt_{1} ≠ σt_{2} do

begin choose a disagreement pair d_{1} and d_{2} for σt_{1}, σt_{2}. if neither d_{1} nor d_{2} is a variable, fail. Let x be whichever is a variable and t be the other

(if both are variables choose one to be x arbitrarily) if x occurs in t then fail; let σ be σ with x ↪ t added

end

This is nondeterministic, but it can be shown (see Fitting) that this algorithm is correct, i.e. if the terms are unifiable it will find a unifying substitution (in fact, a most general unifier) and if not it will fail.

Unification in Lego

In Lego, unification is made slightly more complicated by the presence of universally quantified variables and existential variables like ?. Furthermore, Lego must check that the types of the variables and the terms they are unified with agree. Lego will instantiate existential variables if possible, but there are some restrictions.

It may be easiest to see what Lego can do by looking at some examples. We use the command Immed, since it unifies the goals with the hypotheses, starting with the last goal. This makes sense because sometimes such unification will eliminate other goals.

[A:Prop];
[R:A->A->Prop];
Lego> Goal ({x:A}(R x x)) -> {y:A}Ex [z:A](R y z);

Goal
  ?0 : ({x:A}R x x)->{y:A}Ex ([z:A]R y z)
Lego> intros;
intros (2)
  H : {x:A}R x x
  y : A
  ?1 : Ex ([z:A]R y z)
Lego> Refine ExIntro y;
Refine by  ExIntro y
  ?4 : R y y
Lego> Immed;
Immediate
Discharge..  y H
*** QED ***

This proof demonstrates that Immed also does a limited amount of the work of Refine, as explained later, since the quantifier {x:A} must be eliminated for the terms to unify.

This proof will also work with an existential variable:

Lego> Goal ({x:A}(R x x)) -> {y:A}Ex [z:A](R y z);
Goal
  ?0 : ({x:A}R x x)->{y:A}Ex ([z:A]R y z)
Lego> intros;
intros (2)
  H : {x:A}R x x
  y : A
  ?1 : Ex ([z:A]R y z)
Lego> Refine ExIntro ?;
Refine by  ExIntro ?3
  ?3 : A
  ?5 : R y ?3
Lego> Immed;
Immediate
Discharge..  y H
*** QED ***

The R y ?3 unifies with R x x, so that this goal is discharged when ?3 = y. This also eliminates the goal ?3 : A.

In both cases, what actually happens is that the universally quantified variable in {x:A} R x x is provisionally instantiated with an existential variable ?6 : A, and R ?6 ?6 is unified with the appropriate goal. In both cases, ?6 : A is eventually unified with y : A, so we never see this goal. We’ll see this more when we look at what Refine does, below.

Here is a longer proof which illustrates that unification is first-order, and how Immed can go wrong:

Lego> Goal ({x:A}(R x x))->{g:A->A}{y:A}Ex [h:A->A](R (h y) (g (g y)));
Goal
  ?0 : ({x:A}R x x)->{g:A->A}{y:A}Ex ([h:A->A]R (h y) (g (g y)))
Lego> intros;
intros (3)
  H : {x:A}R x x
  g : A->A
  y : A
  ?1 : Ex ([h:A->A]R (h y) (g (g y)))
Lego> Refine ExIntro ?;

Refine by  ExIntro ?3
  ?3 : A->A
  ?5 : R (?3 y) (g (g y))
Lego> Immed;
Immediate
  ?5 : R (g y) (g (g y))

Lego couldn’t do anything with ?5, so it went on to ?3 and unified this with g:A->A. If Lego had a more sophisticated unification algorithm, it would have been able to produce the function [z:A](g (g z)) to fill in for ?3. This is called higher-order unification.

We can give Lego the hint, though, by introducing a name for this function:

Lego> Undo 1;
Undo
  H : {x:A}R x x
  g : A->A
  y : A
  ?3 : A->A
  ?5 : R (?3 y) (g (g y))
Lego> [h2 = [z:A] g (g z)];
defn  h2 = [z:A]g (g z)
      h2 : A->A
Lego> Prf;
  H : {x:A}R x x
  g : A->A
  y : A
  h2 = ... : A->A
  ?3 : A->A
  ?5 : R (?3 y) (g (g y))
Lego> Immed;
Immediate
  ?5 : R (h2 y) (g (g y))

Now ?3 : A->A has unified with h2: A->A, leaving another goal which can also be solved by unification:

Lego> Immed;
Immediate
Discharge..  h2 y g H
*** QED ***

Refinement

In many cases, Lego’s refinement command can be used without understanding its precise effect. However, to master more complex proofs, it is important to employ refinement with more proficiency. In particular, one has to be able to construct appropriate refinement terms. In this section, we explain (a model of) Lego’s implementation of refinement.

Let ?n:G be the current goal and r be a term, possibly containing existential variables. Refining by r might lead to one of the following:

1. Refinement has been successful and a proof term for the goal G has been constructed.

2. The error message doesn't solve goal indicates that refinement has failed.

3. Refinement has been successful and the goal G will be replaced by one or more (hopefully easier) goals.

Refinement is a recursive algorithm consisting of three steps:

1. Does the type of the current refinement term r unify^{1} with the current goal G?

If so, refinement has been successful and, after possible unifications, the term r is a proof inhabiting the goal G.

2. If the above attempt has failed, bring the type of the current refinement term into headnormal form. Is this type of the form {x:A}B x? If not, refinement is impossible.

3. We know that r:{x:A}B x, but {x:A}B x does not unify with the current goal. However, the refinement term r can be considered as a collection of proofs indexed by A. Maybe, a special instance of r will lead to refinement. What instance of A would work? This decision is delayed by introducing a new goal ?n+1:A and specialising the refinement term to r ?n+1 : B ?n+1, reinvoking the refinement procedure. Of course, all intermediate goals will be discarded, should refinement eventually fail, but otherwise, all such intermediate goals, which have not been unified (in the first step), will be the refined goals replacing the original goal G.

Example

1. P : Prop
  p : P
  ?1 : P

Refine p; will succeed, because the type of the refinement term p unifies with the goal.

2. ?0 : bool->nat

Refine bool rec; yields the proof state

  ?2 : nat
  ?3 : nat

Why?

(a) i. The type of the refinement term is {T|Type}T->T->bool->T, which does not unify

        with bool->nat.

ii. The type {T|Type}T->T->bool->T is already in head-normal form.

iii. An existential variable ?1:Type is introduced and the refinement term bool rec is

        specialised to bool_rec|?1: ?1->?1->bool->?1.
 (b) i. ?1->?1->bool->?1 does not unify with bool->nat.

1first-order unification only

ii. The type of the refinement term bool_rec|?1: ?1->?1->bool->?1 is again in

head-normal form. iii. An existential variable ?2 : ?1 is introduced and the refinement term bool_rec|?1

is specialised to bool_rec|?1 ?2. The type of the new refinement term is ?1->bool->?1.

(c) i. ?1->bool->?1 does not unify with bool->nat.

ii. The type of the refinement term bool_rec|?1 ?2: ?1->bool->?1 is again in head-

normal form. iii. An existential variable ?3 : ?1 is introduced and the refinement term bool_rec|?1 ?2 is specialised to bool_rec|?1 ?2 ?3. The type of the new refinement term is

             bool->?1.
     (d) Now bool->?1 unifies with bool->nat with ?1 = nat, and bool_elim|nat ?2 ?3

is a proof term inhabiting the goal bool->nat. Refinement has succeeded and the goal ?0 : bool->nat will be replaced by ?2 : nat and ?3 : nat. The intermediate goal ?1 : Type does not show up because it has been discarded after unification, after substitution of nat for ?1 wherever the latter occurred.

Exercise:

1. Starting with the goal {T|Type}(list T)->(list T)->list T, analyse the effect of refining

     by list_rec

As a consequence of type theory’s intrinsic dependencies and the desire to delay unification of existential variables, unification may lead to incorrect proof terms. Lego will detect such incorrect unification attempts later when the resulting proof term is either malformed or does not type-check against the original goal.

Example

Consider the context

  ?2 : nat
  ?4 : nat->Eq ?2 ?2

We now try to solve the last goal. This is usually a good idea, because the first goal might be unified.

Lego> intros -0 n;
intros (1) n
  n : nat
  ?5 : Eq ?2 ?2

However, the following proof attempt leads to incorrect unification of the first goal. We may use the natural number n in the proof of the current goal, but it would illegal to use it in the unification of ?2. We can fool Lego by invoking Refine Eq_refl n. Lego detects the mistake while building the proof term

Refine by  Eq_refl n
Discharge..  n
Error: search: undefined or out of context: n

Exercises

1. Construct a goal and a proof script leading to the above proof state

       ?2 : nat
       ?4 : nat->Eq ?2 ?2

2. Prove that the relation [Le [m,n:nat] = Ex [k:nat]Eq (plus m k) n is transitive

3. Modify the previous proof such that it leads to incorrect unification.

Implicit syntax

As we have observed above, Lego can deal with incomplete terms containing existential variables. This feature can be exploited by the user, too.

Example

   • cons1 is of type {T:Type}T->(list T)->list T. Instead of cons1 nat three, Lego can

unify the first argument and we may specify cons1 ? three instead.

• For composing two functions, we can define the operator

     [compose [A,B,C:Type][f:B->C][g:A->B] = [x:A]f (g x)]
     where compose ??? suc (length|nat) would be a valid (implicit) term of type (list nat)->nat

Outside of refinement, all existential variables must be unified if Lego is supposed to accept the term i.e., every implicit term is a valid refinement term, but not vice versa.

With terms such as cons1:{T:Type}T->(list T)->list T, if we supply at least two arguments, Lego will always be able to unify the first one. It is therefore convenient to indicate positions where Lego should automatically insert existential variables. This can be achieved by using {x|A}B rather than {x:A}B and [x|A]B rather than [x:A]B

Example

   • cons is of type {T|Type}T->(list T)->list T and cons three is a valid Lego term.

• For composing two functions, we can define the operator

     [compose [A,B,C|Type][f:B->C][g:A->B] = [x:A]f (g x)]

where compose suc (length|nat) would be a valid (implicit) term of type (list nat)->nat

Notice that cons nat three will be rejected, because it is equivalent to cons ? nat three. A new form of application, M|N rather than M N is introduced to overwrite implicit argument synthesis e.g., cons|nat three is a valid term.

Lego is liberal in handling applications containing implicit terms. A term M N is considered legal if, for the corresponding explicit forms M' and N', either M' N' is legal, or M' X N' for any explicit term X is legal.

Example

[I :{A|Type}A->A]
[A:Type][a:A]
[F [f:{A:Type}A->A] = f A a]

Then, Lego accepts F I.

Although convenient, the implementation of implicit syntax is in some sense too liberal e.g, in the above example, expanding the definition of F will cause the malformed term I A a. In practice, such problems can be avoided by manually coercing implicit syntax into explicit syntax.

Exercises Write coercion functions mediating between implicit and explicit syntax in the context

of [A|Type][B|A->Type]
   • Goal exp2imp: ({x:A}(B x))->{x|A}(B x)
   • Goal imp2exp: ({x|A}(B x))->{x:A}(B x)

Notice that for formulating lemmata dealing with equality, it is usually better to use explicit arguments for the arguments of an equality, because Qrepl will not synthesise these e.g., associativity of plus is best specified as

{k,m,n:nat}Eq (plus (plus k m) n) (plus k (plus m n))

even though k, m and n could be synthesised.

References

Huet, G. and Plotkin, G. D., editors (1990). Electronic Proceedings of the First Annual BRA Workshop on Logical Frameworks (Antibes, France). Available on the Web

    http://www.dcs.ed.ac.uk/lfcsinfo/research/types bra/proc90.dvi.gz.

Pollack, R. (1992). Implicit syntax. Available by anonymous FTP at ftp.dcs.ed.ac.uk in pub/lego/ImplicitSyntax.ps.Z, An earlier version of this paper appeared in (Huet and Plotkin, 1990).