|
1 (* Title: Subst/Unify |
|
2 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
3 Copyright 1997 University of Cambridge |
|
4 |
|
5 Unification algorithm |
|
6 *) |
|
7 |
|
8 Unify = Unifier + WF_Rel + |
|
9 |
|
10 datatype 'a subst = Fail | Subst ('a list) |
|
11 |
|
12 consts |
|
13 |
|
14 uterm_less :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" |
|
15 unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" |
|
16 unify :: "'a uterm * 'a uterm => ('a * 'a uterm) subst" |
|
17 |
|
18 defs |
|
19 |
|
20 uterm_less_def "uterm_less == rprod (measure uterm_size) |
|
21 (measure uterm_size)" |
|
22 |
|
23 (* Termination relation for the Unify function *) |
|
24 unifyRel_def "unifyRel == inv_image (finite_psubset ** uterm_less) |
|
25 (%(x,y). (vars_of x Un vars_of y, (x,y)))" |
|
26 |
|
27 recdef unify "unifyRel" |
|
28 "unify(Const m, Const n) = (if (m=n) then Subst[] else Fail)" |
|
29 "unify(Const m, Comb M N) = Fail" |
|
30 "unify(Const m, Var v) = Subst[(v,Const m)]" |
|
31 "unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])" |
|
32 "unify(Comb M N, Const x) = Fail" |
|
33 "unify(Comb M N, Var v) = (if (Var v <: Comb M N) then Fail |
|
34 else Subst[(v,Comb M N)])" |
|
35 "unify(Comb M1 N1, Comb M2 N2) = |
|
36 (case unify(M1,M2) |
|
37 of Fail => Fail |
|
38 | Subst theta => (case unify(N1 <| theta, N2 <| theta) |
|
39 of Fail => Fail |
|
40 | Subst sigma => Subst (theta <> sigma)))" |
|
41 end |