3192
|
1 |
(* Title: Subst/Unify
|
3267
|
2 |
ID: $Id$
|
3192
|
3 |
Author: Konrad Slind, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1997 University of Cambridge
|
|
5 |
|
|
6 |
Unification algorithm
|
|
7 |
*)
|
|
8 |
|
12406
|
9 |
Unify = Unifier +
|
3192
|
10 |
|
|
11 |
consts
|
|
12 |
|
3267
|
13 |
unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
|
3298
|
14 |
unify :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
|
3192
|
15 |
|
|
16 |
defs
|
|
17 |
|
3267
|
18 |
(*Termination relation for the Unify function:
|
|
19 |
--either the set of variables decreases
|
|
20 |
--or the first argument does (in fact, both do)
|
|
21 |
*)
|
8703
|
22 |
unifyRel_def "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
|
3267
|
23 |
(%(M,N). (vars_of M Un vars_of N, M))"
|
3192
|
24 |
|
|
25 |
recdef unify "unifyRel"
|
3298
|
26 |
"unify(Const m, Const n) = (if (m=n) then Some[] else None)"
|
|
27 |
"unify(Const m, Comb M N) = None"
|
|
28 |
"unify(Const m, Var v) = Some[(v,Const m)]"
|
|
29 |
"unify(Var v, M) = (if (Var v <: M) then None else Some[(v,M)])"
|
|
30 |
"unify(Comb M N, Const x) = None"
|
|
31 |
"unify(Comb M N, Var v) = (if (Var v <: Comb M N) then None
|
|
32 |
else Some[(v,Comb M N)])"
|
3192
|
33 |
"unify(Comb M1 N1, Comb M2 N2) =
|
|
34 |
(case unify(M1,M2)
|
3298
|
35 |
of None => None
|
|
36 |
| Some theta => (case unify(N1 <| theta, N2 <| theta)
|
|
37 |
of None => None
|
|
38 |
| Some sigma => Some (theta <> sigma)))"
|
3192
|
39 |
end
|