1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
|
(***********************************************************************)
(* *)
(* OCaml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the Q Public License version 1.0. *)
(* *)
(***********************************************************************)
(* $Id$ *)
open Terms
open Equations
(****************** Critical pairs *********************)
(* All (u,subst) such that N/u (&var) unifies with M,
with principal unifier subst *)
let rec super m = function
Term(_,sons) as n ->
let rec collate n = function
[] -> []
| son::rest ->
List.map (fun (u, subst) -> (n::u, subst)) (super m son)
@ collate (n+1) rest in
let insides = collate 1 sons in
begin try
([], unify m n) :: insides
with Failure _ ->
insides
end
| _ -> []
(* Ex :
let (m,_) = <<F(A,B)>>
and (n,_) = <<H(F(A,x),F(x,y))>> in super m n
==> [[1],[2,Term ("B",[])]; x <- B
[2],[2,Term ("A",[]); 1,Term ("B",[])]] x <- A y <- B
*)
(* All (u,subst), u&[], such that n/u unifies with m *)
let super_strict m = function
Term(_,sons) ->
let rec collate n = function
[] -> []
| son::rest ->
List.map (fun (u, subst) -> (n::u, subst)) (super m son)
@ collate (n+1) rest in
collate 1 sons
| _ -> []
(* Critical pairs of l1=r1 with l2=r2 *)
(* critical_pairs : term_pair -> term_pair -> term_pair list *)
let critical_pairs (l1,r1) (l2,r2) =
let mk_pair (u,subst) =
substitute subst (replace l2 u r1), substitute subst r2 in
List.map mk_pair (super l1 l2)
(* Strict critical pairs of l1=r1 with l2=r2 *)
(* strict_critical_pairs : term_pair -> term_pair -> term_pair list *)
let strict_critical_pairs (l1,r1) (l2,r2) =
let mk_pair (u,subst) =
substitute subst (replace l2 u r1), substitute subst r2 in
List.map mk_pair (super_strict l1 l2)
(* All critical pairs of eq1 with eq2 *)
let mutual_critical_pairs eq1 eq2 =
(strict_critical_pairs eq1 eq2) @ (critical_pairs eq2 eq1)
(* Renaming of variables *)
let rename n (t1,t2) =
let rec ren_rec = function
Var k -> Var(k+n)
| Term(op,sons) -> Term(op, List.map ren_rec sons) in
(ren_rec t1, ren_rec t2)
(************************ Completion ******************************)
let deletion_message rule =
print_string "Rule ";print_int rule.number; print_string " deleted";
print_newline()
(* Generate failure message *)
let non_orientable (m,n) =
pretty_term m; print_string " = "; pretty_term n; print_newline()
let rec partition p = function
[] -> ([], [])
| x::l -> let (l1, l2) = partition p l in
if p x then (x::l1, l2) else (l1, x::l2)
let rec get_rule n = function
[] -> raise Not_found
| r::l -> if n = r.number then r else get_rule n l
(* Improved Knuth-Bendix completion procedure *)
let kb_completion greater =
let rec kbrec j rules =
let rec process failures (k,l) eqs =
(****
print_string "***kb_completion "; print_int j; print_newline();
pretty_rules rules;
List.iter non_orientable failures;
print_int k; print_string " "; print_int l; print_newline();
List.iter non_orientable eqs;
***)
match eqs with
[] ->
if k<l then next_criticals failures (k+1,l) else
if l<j then next_criticals failures (1,l+1) else
begin match failures with
[] -> rules (* successful completion *)
| _ -> print_string "Non-orientable equations :"; print_newline();
List.iter non_orientable failures;
failwith "kb_completion"
end
| (m,n)::eqs ->
let m' = mrewrite_all rules m
and n' = mrewrite_all rules n
and enter_rule(left,right) =
let new_rule = mk_rule (j+1) left right in
pretty_rule new_rule;
let left_reducible rule = reducible left rule.lhs in
let (redl,irredl) = partition left_reducible rules in
List.iter deletion_message redl;
let right_reduce rule =
mk_rule rule.number rule.lhs
(mrewrite_all (new_rule::rules) rule.rhs) in
let irreds = List.map right_reduce irredl in
let eqs' = List.map (fun rule -> (rule.lhs, rule.rhs)) redl in
kbrec (j+1) (new_rule::irreds) [] (k,l) (eqs @ eqs' @ failures) in
(***
print_string "--- Considering "; non_orientable (m', n');
***)
if m' = n' then process failures (k,l) eqs else
if greater(m',n') then enter_rule(m',n') else
if greater(n',m') then enter_rule(n',m') else
process ((m',n')::failures) (k,l) eqs
and next_criticals failures (k,l) =
(****
print_string "***next_criticals ";
print_int k; print_string " "; print_int l ; print_newline();
****)
try
let rl = get_rule l rules in
let el = (rl.lhs, rl.rhs) in
if k=l then
process failures (k,l)
(strict_critical_pairs el (rename rl.numvars el))
else
try
let rk = get_rule k rules in
let ek = (rk.lhs, rk.rhs) in
process failures (k,l)
(mutual_critical_pairs el (rename rl.numvars ek))
with Not_found -> next_criticals failures (k+1,l)
with Not_found -> next_criticals failures (1,l+1)
in process
in kbrec
(* complete_rules is assumed locally confluent, and checked Noetherian with
ordering greater, rules is any list of rules *)
let kb_complete greater complete_rules rules =
let n = check_rules complete_rules
and eqs = List.map (fun rule -> (rule.lhs, rule.rhs)) rules in
let completed_rules =
kb_completion greater n complete_rules [] (n,n) eqs in
print_string "Canonical set found :"; print_newline();
pretty_rules (List.rev completed_rules)
|
