Syntactic Unification

  • Author: Gert Smolka, Saarland University
  • Based on a development of Adrien Hussung

Require Export Base.

Terms, substitutions, and unifiers

Definition var := nat.

Inductive ter : Type :=
| V : varter
| T : terterter.

Definition eqn := prod ter ter.

Implicit Types x y z : var.
Implicit Types s t u v : ter.
Implicit Types sigma tau : terter.
Implicit Types A B C : list eqn.
Implicit Type e : eqn.
Implicit Types m n k : nat.

Definition subst sigma : Prop :=
  s t, sigma (T s t) = T (sigma s) (sigma t).

Definition unif sigma A : Prop :=
 subst sigma
  s t, (s,t) el Asigma s = sigma t.

Definition unifiable A : Prop :=
   sigma, unif sigma A.

Definition principal_unifier sigma A : Prop :=
 unif sigma A
  tau, unif tau A s, tau (sigma s) = tau s.

Definition idempotent X (f : XX) : Prop :=
  x : X, f (f x) = f x.

Lemma subst_id :
 subst (fun ss).

Lemma principal_idempotent sigma A :
 principal_unifier sigma Aidempotent sigma.

Lemma unif_cons sigma s t A :
 unif sigma ((s,t)::A) sigma s = sigma t unif sigma A.

Lemma unif_app sigma A B :
  unif sigma (A ++ B) unif sigma A unif sigma B.

Contained variables

Fixpoint vart s : list var :=
 match s with
   | V x[x]
   | T s1 s2vart s1 ++ vart s2

Fixpoint varl A : list var :=
 match A with
   | nilnil
   | (s,t)::A'vart s ++ vart t ++ varl A'

Fixpoint dom A : list var :=
 match A with
   | (V x, s) :: A'x :: dom A'
   | _nil

Lemma dom_varl A :
 dom A <<= varl A.

Lemma varl_app A B :
 varl (A ++ B) = varl A ++ varl B.

Lemma vart_incl_varl s t A :
  (s,t) el Avart s <<= varl A vart t <<= varl A.

Lemma varl_incl A B :
 A <<= Bvarl A <<= varl B.

Variable replacement

Fixpoint rep s x t : ter :=
 match s with
   | V yif decision (x = y) then t else V y
   | T s1 s2T (rep s1 x t) (rep s2 x t)

Definition repe e x s : eqn :=
 let (u,v) := e in (rep u x s , rep v x s).

Definition repl A x s := map (fun erepe e x s) A.

Lemma rep_xx x t :
 rep (V x) x t = t.

Lemma rep_id x s t :
 ¬ x el vart srep s x t = s.

Lemma rep_id_subst sigma x s t :
 subst sigmasigma (V x) = sigma tsigma (rep s x t) = sigma s.

Lemma rep_var s x t :
  vart (rep s x t) <<= vart s ++ vart t.

Lemma repl_var A x t :
  varl (repl A x t) <<= vart t ++ varl A.

Lemma rep_var_not_in x s t :
  ¬ x el vart s¬ x el vart (rep t x s).

Lemma repl_var_elim A x s :
  ¬ x el vart s¬ x el varl (repl A x s).

Solved equation lists

Inductive solved : list (ter × ter) → Prop :=
| solvedN :
   solved nil
| solvedC x s A :
   ¬ x el vart s¬ x el dom Adisjoint (vart s) (dom A) →
   solved Asolved ((V x, s) :: A).

Fixpoint phi A s : ter :=
 match A with
   | (V x, t) :: A' ⇒ (rep (phi A' s) x t)
   | _s

Lemma phi_subst A :
 subst (phi A).

Lemma phi_id A s :
 disjoint (dom A) (vart s) → phi A s = s.

Lemma phi_unif A :
 solved Aunif (phi A) A.

Lemma phi_principal sigma A s :
  unif sigma Asigma (phi A s) = sigma s.

Theorem solved_principal A :
 solved Aprincipal_unifier (phi A) A.

Fixpoint size s : nat :=
  match s with
    | V _ ⇒ 1
    | T s1 s2 ⇒ 1 + size s1 + size s2

Lemma subst_size x s sigma :
  subst sigmax el vart ssize (sigma (V x)) size (sigma s).

Lemma bad_eqn x s sigma :
  subst sigmax el vart sV x ssigma (V x) sigma s.


Definition ueq A B : Prop :=
   sigma, unif sigma A unif sigma B.

Definition red A B : Prop :=
 varl B <<= varl A ueq A B.

Lemma ueq_sym A B :
  ueq A Bueq B A.

Lemma ueq_principal_unifier A B sigma :
 ueq A Bprincipal_unifier sigma Aprincipal_unifier sigma B.

Instance red_preorder :
  PreOrder red.

Instance equi_red :
 subrelation (@equi eqn) red.

Instance cons_red_proper e :
  Proper (red ==> red) (cons e).

Instance app_red_proper :
 Proper (red ==> red ==> red) (@app eqn).

Instance unif_red_proper sigma :
 Proper (red ==> iff) (unif sigma).

Unification rules

Lemma red_delete s :
 red [(s,s)] nil.

Lemma red_swap s t:
 red [(s,t)] [(t,s)].

Lemma red_decompose s1 s2 t1 t2 :
 red [(T s1 s2, T t1 t2)] [(s1, t1); (s2, t2)].

(* The next 2 lemmas have smart proof scripts avoiding combinatorial explosion *)

Lemma repl_unif sigma x t A :
  sigma (V x) = sigma t → (unif sigma A unif sigma (repl A x t)).

Lemma repl_ueq x t A :
  ueq ((V x, t) :: A) ((V x, t) :: repl A x t).

Lemma red_repl x t A :
 red ((V x,t)::A) ((V x,t)::repl A x t).

Presolved equation lists

Inductive presolved : list eqnProp :=
| presolvedN : presolved nil
| presolvedC x s A : V x spresolved ((V x, s) :: A).

Instance ter_eq_dec :
 eq_dec ter.

Fixpoint pre' s t : list eqn :=
 if decision (s=t) then nil
 else match s, t with
        | V _, _[(s,t)]
        |_, V _[(t,s)]
        | T s1 s2, T t1 t2pre' s1 t1 ++ pre' s2 t2

Fixpoint pre A : list eqn :=
 match A with
   | nilnil
   | (s,t) :: A'pre' s t ++ pre A'

Lemma pre'_red s t :
 red [(s,t)] (pre' s t).

Lemma pre_red A :
 red A (pre A).

Lemma presolved_app A B :
 presolved Apresolved Bpresolved (A ++ B).

Lemma pre'_presolved s t :
 presolved (pre' s t).

Lemma pre_presolved A :
 presolved (pre A).

Unification algorithm

Fixpoint solveN n A B : option (list eqn) :=
  match n, pre B with
    | O, _None
    | S n', (V x, t) :: Cif decision (x el vart t) then None
                             else solveN n' ((V x, t)::A) (repl C x t)
    | _, _Some A

Definition solve C : option (list eqn) :=
 solveN (S (card (varl C))) nil C.

Lemma solveN_correct A B C n :
 red C (A ++ B) →
 solved A
 disjoint (dom A) (varl B) →
 card (varl B) < n
 match solveN n A B with
   | Some A'red C A' solved A'
   | None¬ unifiable C
 trivially unifiable *)
 nonunifiable *)
 eliminable variable *)

Theorem solve_correct C :
  match solve C with
    | Some Ared C A solved A
    | None¬ unifiable C

Main theorems

Theorem solved_form_exists A :
 { B | red A B solved B } + { ¬ unifiable A }.

Theorem principal_unifier_exists A :
  { sigma | principal_unifier sigma A } + { ¬ unifiable A }.