1 (* From the SML
/NJ benchmark suite
. *)
5 val testit
: TextIO.outstream
-> unit
12 datatype term
= Var
of int | Term
of string * term list
;
13 datatype ordering
= Greater | Equal | NotGE
;
14 val rpo
: (string -> string -> ordering
) ->
15 ((term
* term
-> ordering
) -> term
* term
-> ordering
) ->
16 term
* term
-> ordering
;
17 val lex_ext
: (term
* term
-> ordering
) -> term
* term
-> ordering
;
19 (term
* term
-> bool) -> (int * (int * (term
* term
))) list
->
20 ('a
* ('b
* (term
* term
))) list
-> unit
;
27 val name
= "Knuth-Bendix"
31 |
j(k
, a
::x
) = j(k
+1,x
)
36 |
op @
(a
::r
, l
) = a
:: (r@l
)
39 |
f (a
::r
, h
) = f(r
, a
::h
)
45 |
app_rec (a
::L
) = (f a
; app_rec L
)
51 |
map_rec (a
::L
) = f a
:: map_rec L
56 (******* Quelques definitions du prelude CAML
**************)
58 exception Failure
of string;
60 fun failwith s
= raise(Failure s
)
67 let fun it_rec a
[] = a
68 | it_rec
a (b
::L
) = it_rec (f a b
) L
73 let fun it_rec a
[] [] = a
74 | it_rec
a (a1
::L1
) (a2
::L2
) = it_rec (f
a (a1
,a2
)) L1 L2
75 | it_rec _ _ _
= failwith
"it_list2"
80 let fun exists_rec
[] = false
81 |
exists_rec (a
::L
) = (p a
) orelse (exists_rec L
)
86 let fun for_all_rec
[] = true
87 |
for_all_rec (a
::L
) = (p a
) andalso (for_all_rec L
)
91 fun rev_append
[] L
= L
92 |
rev_append (x
::L1
) L2
= rev_append
L1 (x
::L2
)
95 let fun try_find_rec
[] = failwith
"try_find"
96 |
try_find_rec (a
::L
) = (f a
) handle Failure _
=> try_find_rec L
101 let fun part_rec
[] = ([],[])
103 let val (pos
,neg
) = part_rec L
in
104 if p a
then ((a
::pos
), neg
) else (pos
, (a
::neg
))
109 (* 3- Les ensembles et les listes d
'association
*)
112 let fun mem_rec
[] = false
113 |
mem_rec (b
::L
) = (a
=b
) orelse mem_rec L
118 let fun union_rec
[] = L2
120 if mem a L2
then union_rec L
else a
:: union_rec L
125 let fun mem_rec
[] = false
126 |
mem_rec ((b
,_
)::L
) = (a
=b
) orelse mem_rec L
131 let fun assoc_rec
[] = failwith
"find"
132 |
assoc_rec ((b
,d
)::L
) = if a
=b
then d
else assoc_rec L
138 fun print s
= TextIO.output(TextIO.stdOut
, s
)
140 val print_string
= print
141 val print_num
= print
o Int.toString
142 fun print_newline () = print
"\n";
143 fun message s
= (print s
; print
"\n");
145 (* 5- Les ensembles
*)
148 let fun union_rec
[] = L1
149 |
union_rec (a
::L
) = if mem a L1
then union_rec L
else a
:: union_rec L
153 (****************** Term manipulations
*****************)
157 | Term
of string * term list
159 fun vars (Var n
) = [n
]
160 |
vars (Term(_
,L
)) = vars_of_list L
161 and vars_of_list
[] = []
162 |
vars_of_list (t
::r
) = union (vars t
) (vars_of_list r
)
164 fun substitute subst
=
165 let fun subst_rec (Term(oper
,sons
)) = Term(oper
, map subst_rec sons
)
166 |
subst_rec (t
as (Var n
)) = (assoc n subst
) handle Failure _
=> t
171 let fun change_rec (h
::t
) n
= if n
=1 then f h
:: t
172 else h
:: change_rec
t (n
-1)
173 | change_rec _ _
= failwith
"change"
177 (* Term replacement replace M u N
=> M
[u
<-N
] *)
179 let fun reprec (_
, []) = N
180 |
reprec (Term(oper
,sons
), (n
::u
)) =
181 Term(oper
, change (fn P
=> reprec(P
,u
)) sons n
)
182 | reprec _
= failwith
"replace"
186 (* matching
= - : (term
-> term
-> subst
) *)
187 fun matching term1 term2
=
188 let fun match_rec
subst (Var v
, M
) =
189 if mem_assoc v subst
then
190 if M
= assoc v subst
then subst
else failwith
"matching"
193 | match_rec
subst (Term(op1
,sons1
), Term(op2
,sons2
)) =
194 if op1
= op2
then it_list2 match_rec subst sons1 sons2
195 else failwith
"matching"
196 | match_rec _ _
= failwith
"matching"
197 in match_rec
[] (term1
,term2
)
200 (* A naive unification algorithm
*)
202 fun compsubst subst1 subst2
=
203 (map (fn (v
,t
) => (v
, substitute subst1 t
)) subst2
) @ subst1
206 let fun occur_rec (Var m
) = (m
=n
)
207 |
occur_rec (Term(_
,sons
)) = exists occur_rec sons
211 fun unify ((term1
as (Var n1
)), term2
) =
212 if term1
= term2
then []
213 else if occurs n1 term2
then failwith
"unify"
215 |
unify (term1
, Var n2
) =
216 if occurs n2 term1
then failwith
"unify"
218 |
unify (Term(op1
,sons1
), Term(op2
,sons2
)) =
220 it_list2 (fn s
=> fn (t1
,t2
) => compsubst (unify(substitute s t1
,
223 else failwith
"unify"
225 (* We need to print terms
with variables independently from input terms
226 obtained by parsing
. We give arbitrary names v1
,v2
,... to their variables
. *)
228 val INFIXES
= ["+","*"];
230 fun pretty_term (Var n
) =
231 (print_string
"v"; print_num n
)
232 |
pretty_term (Term (oper
,sons
)) =
233 if mem oper INFIXES
then
236 (pretty_close s1
; print_string oper
; pretty_close s2
)
238 failwith
"pretty_term : infix arity <> 2"
243 | t
::lt
=>(print_string
"(";
245 app (fn t
=> (print_string
","; pretty_term t
)) lt
;
247 and pretty_close (M
as Term(oper
, _
)) =
248 if mem oper INFIXES
then
249 (print_string
"("; pretty_term M
; print_string
")")
251 | pretty_close M
= pretty_term M
253 (****************** Equation manipulations
*************)
255 (* standardizes an equation so its variables are
1,2,... *)
258 let val all_vars
= union (vars M
) (vars N
);
260 it_list (fn (i
,sigma
) => fn v
=> (i
+1,(v
,Var(i
))::sigma
))
262 in (k
-1, (substitute subst M
, substitute subst N
))
265 (* checks that rules are numbered
in sequence
and returns their number
*)
266 fun check_rules l
= it_list (fn n
=> fn (k
,_
) =>
267 if k
=n
+1 then k
else failwith
"Rule numbers not in sequence")
270 fun pretty_rule (k
,(n
,(M
,N
))) =
271 (print_num k
; print_string
" : ";
272 pretty_term M
; print_string
" = "; pretty_term N
;
275 fun pretty_rules l
= app pretty_rule l
278 (****************** Rewriting
**************************)
280 (* Top
-level rewriting
. Let eq
:L
=R be an equation
, M be a term such that L
<=M
.
281 With sigma
= matching L M
, we define the image
of M by eq
as sigma(R
) *)
283 substitute (matching L M
)
285 (* A more efficient version
of can (rewrite1 (L
,R
)) for R arbitrary
*)
290 case M
of Term(_
,sons
) => exists redrec sons
295 (* mreduce
: rules
-> term
-> term
*)
296 fun mreduce rules M
=
297 let fun redex (_
,(_
,(L
,R
))) = reduce L M R
in try_find redex rules
end
299 (* One step
of rewriting
in leftmost
-outermost strategy
, with multiple rules
*)
300 (* fails
if no redex is found
*)
301 (* mrewrite1
: rules
-> term
-> term
*)
302 fun mrewrite1 rules
=
304 (mreduce rules M
) handle Failure _
=>
305 let fun tryrec
[] = failwith
"mrewrite1"
306 |
tryrec (son
::rest
) =
307 (rewrec son
:: rest
) handle Failure _
=> son
:: tryrec rest
309 Term(f
, sons
) => Term(f
, tryrec sons
)
310 | _
=> failwith
"mrewrite1"
315 (* Iterating rewrite1
. Returns a normal form
. May loop forever
*)
316 (* mrewrite_all
: rules
-> term
-> term
*)
317 fun mrewrite_all rules M
=
319 rew_loop(mrewrite1 rules M
) handle Failure _
=> M
324 pretty_term (mrewrite_all Group_rules M
where M
,_
=<<A
*(I(B
)*B
)>>);;
329 (************************ Recursive Path Ordering
****************************)
331 datatype ordering
= Greater | Equal | NotGE
;
333 fun ge_ord order pair
= case order pair
of NotGE
=> false | _
=> true
334 and gt_ord order pair
= case order pair
of Greater
=> true | _
=> false
335 and eq_ord order pair
= case order pair
of Equal
=> true | _
=> false
338 let fun remrec x
[] = failwith
"rem_eq"
339 | remrec
x (y
::l
) = if equiv (x
,y
) then l
else y
:: remrec x l
343 fun diff_eq
equiv (x
,y
) =
344 let fun diffrec (p
as ([],_
)) = p
345 |
diffrec ((h
::t
), y
) =
346 diffrec (t
,rem_eq equiv h y
) handle Failure _
=>
347 let val (x
',y
') = diffrec (t
,y
) in (h
::x
',y
') end
348 in if length x
> length y
then diffrec(y
,x
) else diffrec(x
,y
)
351 (* multiset extension
of order
*)
352 fun mult_ext
order (Term(_
,sons1
), Term(_
,sons2
)) =
353 (case diff_eq (eq_ord order
) (sons1
,sons2
) of
356 if for_all (fn N
=> exists (fn M
=> order (M
,N
) = Greater
) l1
) l2
357 then Greater
else NotGE
)
358 | mult_ext
order (_
, _
) = failwith
"mult_ext"
360 (* lexicographic extension
of order
*)
361 fun lex_ext
order ((M
as Term(_
,sons1
)), (N
as Term(_
,sons2
))) =
362 let fun lexrec ([] , []) = Equal
363 |
lexrec ([] , _
) = NotGE
364 |
lexrec ( _
, []) = Greater
365 |
lexrec (x1
::l1
, x2
::l2
) =
366 case order (x1
,x2
) of
367 Greater
=> if for_all (fn N
' => gt_ord
order (M
,N
')) l2
368 then Greater
else NotGE
369 | Equal
=> lexrec (l1
,l2
)
370 | NotGE
=> if exists (fn M
' => ge_ord
order (M
',N
)) l1
371 then Greater
else NotGE
372 in lexrec (sons1
, sons2
)
374 | lex_ext order _
= failwith
"lex_ext"
376 (* recursive path ordering
*)
378 fun rpo op_order ext
=
379 let fun rporec (M
,N
) =
380 if M
=N
then Equal
else
386 if occurs n M
then Greater
else NotGE
388 case (op_order op1 op2
) of
390 if for_all (fn N
' => gt_ord
rporec (M
,N
')) sons2
391 then Greater
else NotGE
395 if exists (fn M
' => ge_ord
rporec (M
',N
)) sons1
396 then Greater
else NotGE
400 (****************** Critical pairs
*********************)
402 (* All (u
,sig) such that N
/u (&var
) unifies
with M
,
403 with principal unifier
sig *)
406 let fun suprec (N
as Term(_
,sons
)) =
407 let fun collate (pairs
,n
) son
=
408 (pairs @
map (fn (u
,sigma
) => (n
::u
,sigma
)) (suprec son
), n
+1);
410 fst (it_list
collate ([],1) sons
)
411 in ([], unify(M
,N
)) :: insides
handle Failure _
=> insides
417 let (M
,_
) = <<F(A
,B
)>>
418 and (N
,_
) = <<H(F(A
,x
),F(x
,y
))>> in super M N
;;
419 ==> [[1],[2,Term ("B",[])]; x
<- B
420 [2],[2,Term ("A",[]); 1,Term ("B",[])]] x
<- A y
<- B
423 (* All (u
,sigma
), u
&[], such that N
/u unifies
with M
*)
424 (* super_strict
: term
-> term
-> (num list
& subst
) list
*)
426 fun super_strict
M (Term(_
,sons
)) =
427 let fun collate (pairs
,n
) son
=
428 (pairs @
map (fn (u
,sigma
) => (n
::u
,sigma
)) (super M son
), n
+1)
429 in fst (it_list
collate ([],1) sons
) end
430 | super_strict _ _
= []
432 (* Critical pairs
of L1
=R1
with L2
=R2
*)
433 (* critical_pairs
: term_pair
-> term_pair
-> term_pair list
*)
434 fun critical_pairs (L1
,R1
) (L2
,R2
) =
435 let fun mk_pair (u
,sigma
) =
436 (substitute
sigma (replace L2 u R1
), substitute sigma R2
) in
437 map
mk_pair (super L1 L2
)
440 (* Strict critical pairs
of L1
=R1
with L2
=R2
*)
441 (* strict_critical_pairs
: term_pair
-> term_pair
-> term_pair list
*)
442 fun strict_critical_pairs (L1
,R1
) (L2
,R2
) =
443 let fun mk_pair (u
,sigma
) =
444 (substitute
sigma (replace L2 u R1
), substitute sigma R2
) in
445 map
mk_pair (super_strict L1 L2
)
448 (* All critical pairs
of eq1
with eq2
*)
449 fun mutual_critical_pairs eq1 eq2
=
450 (strict_critical_pairs eq1 eq2
) @
(critical_pairs eq2 eq1
)
452 (* Renaming
of variables
*)
454 fun rename
n (t1
,t2
) =
455 let fun ren_rec (Var k
) = Var(k
+n
)
456 |
ren_rec (Term(oper
,sons
)) = Term(oper
, map ren_rec sons
)
457 in (ren_rec t1
, ren_rec t2
)
460 (************************ Completion
******************************)
462 fun deletion_message (k
,_
) =
463 (print_string
"Rule ";print_num k
; message
" deleted")
465 (* Generate failure message
*)
466 fun non_orientable (M
,N
) =
467 (pretty_term M
; print_string
" = "; pretty_term N
; print_newline())
469 (* Improved Knuth
-Bendix completion procedure
*)
470 (* kb_completion
: (term_pair
-> bool) -> num
-> rules
-> term_pair list
-> (num
& num
) -> term_pair list
-> rules
*)
471 fun kb_completion greater
=
472 let fun kbrec n rules
=
473 let val normal_form
= mrewrite_all rules
;
474 fun get_rule k
= assoc k rules
;
475 fun process failures
=
476 let fun processf (k
,l
) =
477 let fun processkl
[] =
478 if k
<l
then next_criticals (k
+1,l
) else
479 if l
<n
then next_criticals (1,l
+1) else
481 [] => rules (* successful completion
*)
482 | _
=> (message
"Non-orientable equations :";
483 app non_orientable failures
;
484 failwith
"kb_completion"))
485 |
processkl ((M
,N
)::eqs
) =
486 let val M
' = normal_form M
;
487 val N
' = normal_form N
;
488 fun enter_rule(left
,right
) =
489 let val new_rule
= (n
+1, mk_rule left right
) in
490 (pretty_rule new_rule
;
491 let fun left_reducible (_
,(_
,(L
,_
))) = reducible left L
;
492 val (redl
,irredl
) = partition left_reducible rules
493 in (app deletion_message redl
;
494 let fun right_reduce (m
,(_
,(L
,R
))) =
495 (m
,mk_rule
L (mrewrite_all (new_rule
::rules
) R
));
496 val irreds
= map right_reduce irredl
;
497 val eqs
' = map (fn (_
,(_
,pair
)) => pair
) redl
498 in kbrec (n
+1) (new_rule
::irreds
) [] (k
,l
)
499 (eqs @ eqs
' @ failures
)
503 in if M
'=N
' then processkl eqs
else
504 if greater(M
',N
') then enter_rule(M
',N
') else
505 if greater(N
',M
') then enter_rule(N
',M
') else
506 process ((M
',N
')::failures
) (k
,l
) eqs
510 and next_criticals (k
,l
) =
511 (let val (v
,el
) = get_rule l
in
513 processf (k
,l
) (strict_critical_pairs
el (rename v el
))
515 (let val (_
,ek
) = get_rule k
in
516 processf (k
,l
) (mutual_critical_pairs
el (rename v ek
))
518 handle Failure
"find" (*rule k deleted
*) =>
519 next_criticals (k
+1,l
))
521 handle Failure
"find" (*rule l deleted
*) =>
522 next_criticals (1,l
+1))
530 fun kb_complete greater complete_rules rules
=
531 let val n
= check_rules complete_rules
;
532 val eqs
= map (fn (_
,(_
,pair
)) => pair
) rules
;
533 val completed_rules
=
534 kb_completion greater n complete_rules
[] (n
,n
) eqs
535 in (message
"Canonical set found :";
536 pretty_rules (rev completed_rules
);
541 (1, (1, (Term("*", [Term("U",[]), Var
1]), Var
1))),
542 (2, (1, (Term("*", [Term("I",[Var
1]), Var
1]), Term("U",[])))),
543 (3, (3, (Term("*", [Term("*", [Var
1, Var
2]), Var
3]),
544 Term("*", [Var
1, Term("*", [Var
2, Var
3])]))))];
547 (1,(1,(Term ("*",[(Term ("U",[])), (Var
1)]),(Var
1)))),
548 (2,(1,(Term ("*",[(Term ("I",[(Var
1)])), (Var
1)]),(Term ("U",[]))))),
549 (3,(3,(Term ("*",[(Term ("*",[(Var
1), (Var
2)])), (Var
3)]),
550 (Term ("*",[(Var
1), (Term ("*",[(Var
2), (Var
3)]))]))))),
551 (4,(0,(Term ("*",[(Term ("A",[])), (Term ("B",[]))]),
552 (Term ("*",[(Term ("B",[])), (Term ("A",[]))]))))),
553 (5,(0,(Term ("*",[(Term ("C",[])), (Term ("C",[]))]),(Term ("U",[]))))),
558 (Term ("*",[(Term ("A",[])), (Term ("I",[(Term ("C",[]))]))]))]),
559 (Term ("I",[(Term ("A",[]))]))))),
564 (Term ("*",[(Term ("B",[])), (Term ("I",[(Term ("C",[]))]))]))]),
568 fun Group_rank
"U" = 0
575 fun Group_precedence op1 op2
=
576 let val r1
= Group_rank op1
;
577 val r2
= Group_rank op2
579 if r1
= r2
then Equal
else
580 if r1
> r2
then Greater
else NotGE
583 val Group_order
= rpo Group_precedence lex_ext
585 fun greater pair
= (case Group_order pair
of Greater
=> true | _
=> false)
587 fun doit() = kb_complete greater
[] Geom_rules