# 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
end.

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

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

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)
end.

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
end.

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
end.

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.

# Refinement

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
end.

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

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
end.

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
end.
trivially unifiable *)
nonunifiable *)
eliminable variable *)

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

# 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 }.