5 kitknuth
-bendixnewcopy
.sml
7 This is a revised version
of knuth
-bendix
.sml
in which
8 (a
) val has been converted to
fun for function values
9 (b
) exceptions that carry values have been avoided
10 (c
) functions have been moved around to pass fewer
of them
12 (d
) long tail
-recursions have been broken into batches
of 1,
13 with user
-programmed copying between the batches
22 datatype term
= Var
of int | Term
of string * term list
23 datatype ordering
= Greater | Equal | NotGE
24 val rpo
: (string -> string -> ordering
) ->
25 ((term
* term
-> ordering
) -> term
* term
-> ordering
) ->
26 term
* term
-> ordering
27 val lex_ext
: (term
* term
-> ordering
) -> term
* term
-> ordering
29 (term
* term
-> bool) -> (int * (int * (term
* term
))) list
->
30 ('a
* ('b
* (term
* term
))) list
-> unit
40 |
j(k
, a
::x
) = j(k
+1,x
)
45 |
op @
(a
::r
, l
) = a
:: (r@l
)
48 |
f (a
::r
, h
) = f(r
, a
::h
)
54 |
app_rec (a
::L
) = (f a
; app_rec L
)
60 |
map_rec (a
::L
) = f a
:: map_rec L
65 (******* Quelques definitions du prelude CAML
**************)
67 exception Failure
of string
73 exception FailMatching
77 exception FailMrewrite1
81 exception FailKbComplettion
83 fun failwith s
= raise(Failure s
)
90 let fun it_rec a
[] = a
91 | it_rec
a (b
::L
) = it_rec (f a b
) L
97 let fun it_rec a
[] [] = a
98 | it_rec
a (a1
::L1
) (a2
::L2
) = it_rec (f
a (a1
,a2
)) L1 L2
99 | it_rec _ _ _
= raise FailItList2
104 let fun exists_rec
[] = false
105 |
exists_rec (a
::L
) = (p a
) orelse (exists_rec L
)
110 let fun for_all_rec
[] = true
111 |
for_all_rec (a
::L
) = (p a
) andalso (for_all_rec L
)
115 fun rev_append
[] L
= L
116 |
rev_append (x
::L1
) L2
= rev_append
L1 (x
::L2
)
119 let fun try_find_rec
[] = raise FailTryFind
120 |
try_find_rec (a
::L
) = (f a
) handle _
=> try_find_rec L
125 let fun part_rec
[] = ([],[])
127 let val (pos
,neg
) = part_rec L
in
128 if p a
then ((a
::pos
), neg
) else (pos
, (a
::neg
))
133 (* 3- Les ensembles et les listes d
'association
*)
136 let fun mem_rec
[] = false
137 |
mem_rec (b
::L
) = a
= b
orelse mem_rec L
142 let fun union_rec
[] = L2
144 if mem a L2
then union_rec L
else a
:: union_rec L
149 let fun mem_rec
[] = false
150 |
mem_rec ((b
,_
)::L
) = a
= b
orelse mem_rec L
155 let fun assoc_rec
[] = raise FailFind
156 |
assoc_rec ((b
,d
)::L
) = if a
= b
then d
else assoc_rec L
162 (* val print_string
= String.print
; *)
164 fun print_string x
= print x
166 (* val print_num
= Integer
.print
; *)
169 fun digit n
= chr(ord #
"0" + n
)
171 if n
>=0 andalso n
<=9 then digit n
:: acc
172 else digits (n
div 10, digit(n
mod 10) :: acc
)
173 fun string(n
) = implode(digits(n
,[]))
175 fun print_num n
= print_string(string n
)
178 (* fun print_newline () = String.print
"\n"; *)
180 fun print_newline () = print
"\n"
182 (* fun message s
= (String.print s
; String.print
"\n"); *)
184 fun message s
= (print s
; print
"\n")
186 (* 5- Les ensembles
*)
189 let fun union_rec
[] = L1
190 |
union_rec (a
::L
) = if mem a L1
then union_rec L
else a
:: union_rec L
194 (****************** Term manipulations
*****************)
199 | Term
of string * term list
201 (* Lars
, from now on
: seek on eq_X to see what I have modified
*)
203 fun copy_term (Var n
) = Var (n
+0)
204 |
copy_term (Term(s
, l
)) = Term(s
, map copy_term l
)
207 fun vars (Var n
) = [n
]
208 |
vars (Term(_
,L
)) = vars_of_list L
209 and vars_of_list
[] = []
210 |
vars_of_list (t
::r
) = union (vars t
) (vars_of_list r
)
212 fun substitute subst
=
213 let fun subst_rec (Term(oper
,sons
)) = Term(oper
, map subst_rec sons
)
214 |
subst_rec (t
as (Var n
)) = (assoc n subst
) handle _
=> t
219 let fun change_rec (h
::t
) n
= if n
= 1 then f h
:: t
220 else h
:: change_rec
t (n
-1)
221 | change_rec _ _
= raise FailChange
225 (* Term replacement replace M u N
=> M
[u
<-N
] *)
227 let fun reprec (_
, []) = N
228 |
reprec (Term(oper
,sons
), (n
::u
)) =
229 Term(oper
, change (fn P
=> reprec(P
,u
)) sons n
)
230 | reprec _
= raise FailReplace
234 (* matching
= - : (term
-> term
-> subst
) *)
235 fun matching term1 term2
=
236 let fun match_rec
subst (Var v
, M
) =
237 if mem_assoc v subst
then
238 if M
= assoc v subst
then subst
else raise FailMatching
241 | match_rec
subst (Term(op1
,sons1
), Term(op2
,sons2
)) =
242 if op1
= op2
then it_list2 match_rec subst sons1 sons2
243 else raise FailMatching
244 | match_rec _ _
= raise FailMatching
245 in match_rec
[] (term1
,term2
)
248 (* A naive unification algorithm
*)
250 fun compsubst subst1 subst2
=
251 (map (fn (v
,t
) => (v
, substitute subst1 t
)) subst2
) @ subst1
254 let fun occur_rec (Var m
) = m
= n
255 |
occur_rec (Term(_
,sons
)) = exists occur_rec sons
259 fun unify ((term1
as (Var n1
)), term2
) =
260 if term1
= term2
then []
261 else if occurs n1 term2
then raise FailUnify
263 |
unify (term1
, Var n2
) =
264 if occurs n2 term1
then raise FailUnify
266 |
unify (Term(op1
,sons1
), Term(op2
,sons2
)) =
268 it_list2 (fn s
=> fn (t1
,t2
) => compsubst (unify(substitute s t1
,
273 (* We need to print terms
with variables independently from input terms
274 obtained by parsing
. We give arbitrary names v1
,v2
,... to their variables
. *)
276 val INFIXES
= ["+","*"]
278 fun pretty_term (Var n
) =
279 (print_string
"v"; print_num n
)
280 |
pretty_term (Term (oper
,sons
)) =
281 if mem oper INFIXES
then
284 (pretty_close s1
; print_string oper
; pretty_close s2
)
286 raise FailPretty (* "pretty_term : infix arity <> 2"*)
291 | t
::lt
=>(print_string
"(";
293 app (fn t
=> (print_string
","; pretty_term t
)) lt
;
295 and pretty_close (M
as Term(oper
, _
)) =
296 if mem oper INFIXES
then
297 (print_string
"("; pretty_term M
; print_string
")")
299 | pretty_close M
= pretty_term M
301 (****************** Equation manipulations
*************)
303 (* standardizes an equation so its variables are
1,2,... *)
306 let val all_vars
= union (vars M
) (vars N
)
308 it_list (fn (i
,sigma
) => fn v
=> (i
+1,(v
,Var(i
))::sigma
))
310 in (k
-1, (substitute subst M
, substitute subst N
))
313 (* checks that rules are numbered
in sequence
and returns their number
*)
315 it_list (fn n
=> fn (k
,_
) =>
317 else raise Fail (*failwith
"Rule numbers not in sequence"*)
320 fun pretty_rule (k
,(n
,(M
,N
))) =
321 (print_num k
; print_string
" : ";
322 pretty_term M
; print_string
" = "; pretty_term N
;
325 fun pretty_rules l
= app pretty_rule l
327 fun copy_rules
[] = []
328 |
copy_rules ((k
,(n
,(M
,N
)))::rest
) = (k
+0,(n
+0,(copy_term M
, copy_term N
))):: copy_rules rest
330 (****************** Rewriting
**************************)
332 (* Top
-level rewriting
. Let eq
:L
=R be an equation
, M be a term such that L
<=M
.
333 With sigma
= matching L M
, we define the image
of M by eq
as sigma(R
) *)
334 (* inserted eta
; 03/07/1996-Martin
*)
336 substitute (matching L M
) t
338 (* A more efficient version
of can (rewrite1 (L
,R
)) for R arbitrary
*)
344 case M
of Term(_
,sons
) => exists redrec sons
349 (* mreduce
: rules
-> term
-> term
*)
350 fun mreduce rules M
=
351 let fun redex (_
,(_
,(L
,R
))) = reduce L M R
in try_find redex rules
end
353 (* One step
of rewriting
in leftmost
-outermost strategy
, with multiple rules
*)
354 (* fails
if no redex is found
*)
355 (* mrewrite1
: rules
-> term
-> term
*)
356 fun mrewrite1 rules
=
361 let fun tryrec
[] = raise FailMrewrite1 (*failwith
"mrewrite1"*)
362 |
tryrec (son
::rest
) =
363 (rewrec son
:: rest
) handle _
=> son
:: tryrec rest
365 Term(f
, sons
) => Term(f
, tryrec sons
)
366 | _
=> raise FailMrewrite1 (*failwith
"mrewrite1"*)
371 (* Iterating rewrite1
. Returns a normal form
. May loop forever
*)
372 (* mrewrite_all
: rules
-> term
-> term
*)
373 fun mrewrite_all rules M
=
376 rew_loop(mrewrite1 rules M
) handle _
=> M
381 pretty_term (mrewrite_all Group_rules M
where M
,_
=<<A
*(I(B
)*B
)>>);;
386 (************************ Recursive Path Ordering
****************************)
388 datatype ordering
= Greater | Equal | NotGE
390 fun ge_ord order pair
= case order pair
of NotGE
=> false | _
=> true
391 and gt_ord order pair
= case order pair
of Greater
=> true | _
=> false
392 and eq_ord order pair
= case order pair
of Equal
=> true | _
=> false
395 let fun remrec x
[] = raise FailRemEQ (*failwith
"rem_eq"*)
396 | remrec
x (y
::l
) = if equiv (x
,y
) then l
else y
:: remrec x l
400 fun diff_eq
equiv (x
,y
) =
401 let fun diffrec (p
as ([],_
)) = p
402 |
diffrec ((h
::t
), y
) =
403 diffrec (t
,rem_eq equiv h y
) handle _
=>
404 let val (x
',y
') = diffrec (t
,y
) in (h
::x
',y
') end
405 in if length x
> length y
then diffrec(y
,x
) else diffrec(x
,y
)
408 (* multiset extension
of order
*)
409 fun mult_ext
order (Term(_
,sons1
), Term(_
,sons2
)) =
410 (case diff_eq (eq_ord order
) (sons1
,sons2
) of
413 if for_all (fn N
=> exists (fn M
=> order (M
,N
) = Greater
) l1
) l2
414 then Greater
else NotGE
)
415 | mult_ext
order (_
, _
) = raise FailMultExt (*failwith
"mult_ext"*)
417 (* lexicographic extension
of order
*)
418 fun lex_ext
order ((M
as Term(_
,sons1
)), (N
as Term(_
,sons2
))) =
419 let fun lexrec ([] , []) = Equal
420 |
lexrec ([] , _
) = NotGE
421 |
lexrec ( _
, []) = Greater
422 |
lexrec (x1
::l1
, x2
::l2
) =
423 case order (x1
,x2
) of
424 Greater
=> if for_all (fn N
' => gt_ord
order (M
,N
')) l2
425 then Greater
else NotGE
426 | Equal
=> lexrec (l1
,l2
)
427 | NotGE
=> if exists (fn M
' => ge_ord
order (M
',N
)) l1
428 then Greater
else NotGE
429 in lexrec (sons1
, sons2
)
431 | lex_ext order _
= raise FailLexExt (*failwith
"lex_ext"*)
433 (* recursive path ordering
*)
434 fun Group_rules() = [
435 (1, (1, (Term("*", [Term("U",[]), Var
1]), Var
1))),
436 (2, (1, (Term("*", [Term("I",[Var
1]), Var
1]), Term("U",[])))),
437 (3, (3, (Term("*", [Term("*", [Var
1, Var
2]), Var
3]),
438 Term("*", [Var
1, Term("*", [Var
2, Var
3])]))))]
441 (1,(1,(Term ("*",[(Term ("U",[])), (Var
1)]),(Var
1)))),
442 (2,(1,(Term ("*",[(Term ("I",[(Var
1)])), (Var
1)]),(Term ("U",[]))))),
443 (3,(3,(Term ("*",[(Term ("*",[(Var
1), (Var
2)])), (Var
3)]),
444 (Term ("*",[(Var
1), (Term ("*",[(Var
2), (Var
3)]))]))))),
445 (4,(0,(Term ("*",[(Term ("A",[])), (Term ("B",[]))]),
446 (Term ("*",[(Term ("B",[])), (Term ("A",[]))]))))),
447 (5,(0,(Term ("*",[(Term ("C",[])), (Term ("C",[]))]),(Term ("U",[]))))),
452 (Term ("*",[(Term ("A",[])), (Term ("I",[(Term ("C",[]))]))]))]),
453 (Term ("I",[(Term ("A",[]))]))))),
458 (Term ("*",[(Term ("B",[])), (Term ("I",[(Term ("C",[]))]))]))]),
462 fun Group_rank
"U" = 0
468 | Group_rank _
= 100 (*added
, to avoid non
-exhaustive
patter (mads
) *)
470 fun Group_precedence op1 op2
=
471 let val r1
= Group_rank op1
472 val r2
= Group_rank op2
474 if r1
= r2
then Equal
else
475 if r1
> r2
then Greater
else NotGE
480 let fun rporec (M
,N
) =
481 if M
= N
then Equal
else
487 if occurs n M
then Greater
else NotGE
489 case (Group_precedence op1 op2
) of
491 if for_all (fn N
' => gt_ord
rporec (M
,N
')) sons2
492 then Greater
else NotGE
496 if exists (fn M
' => ge_ord
rporec (M
',N
)) sons1
497 then Greater
else NotGE
501 fun Group_order x
= rpo () x
504 case Group_order pair
of Greater
=> true | _
=> false
506 (****************** Critical pairs
*********************)
508 (* All (u
,sig) such that N
/u (&var
) unifies
with M
,
509 with principal unifier
sig *)
512 let fun suprec (N
as Term(_
,sons
)) =
513 let fun collate (pairs
,n
) son
=
514 (pairs @
map (fn (u
,sigma
) => (n
::u
,sigma
)) (suprec son
), n
+1)
515 val insides
: (int list
* (int*term
)list
)list
= (*type constraint
added (mads
)*)
516 fst (it_list
collate ([],1) sons
)
517 in ([], unify(M
,N
)) :: insides
handle _
=> insides
524 (********************
528 let (M
,_
) = <<F(A
,B
)>>
529 and (N
,_
) = <<H(F(A
,x
),F(x
,y
))>> in super M N
;;
530 ==> [[1],[2,Term ("B",[])]; x
<- B
531 [2],[2,Term ("A",[]); 1,Term ("B",[])]] x
<- A y
<- B
534 (* All (u
,sigma
), u
&[], such that N
/u unifies
with M
*)
535 (* super_strict
: term
-> term
-> (num list
& subst
) list
*)
537 fun super_strict
M (Term(_
,sons
)) =
538 let fun collate (pairs
,n
) son
=
539 (pairs @
map (fn (u
,sigma
) => (n
::u
,sigma
)) (super M son
), n
+1)
540 in fst (it_list
collate ([],1) sons
) end
541 | super_strict _ _
= []
543 (* Critical pairs
of L1
=R1
with L2
=R2
*)
544 (* critical_pairs
: term_pair
-> term_pair
-> term_pair list
*)
545 fun critical_pairs (L1
,R1
) (L2
,R2
) =
546 let fun mk_pair (u
,sigma
) =
547 (substitute
sigma (replace L2 u R1
), substitute sigma R2
) in
548 map
mk_pair (super L1 L2
)
551 (* Strict critical pairs
of L1
=R1
with L2
=R2
*)
552 (* strict_critical_pairs
: term_pair
-> term_pair
-> term_pair list
*)
553 fun strict_critical_pairs (L1
,R1
) (L2
,R2
) =
554 let fun mk_pair (u
,sigma
) =
555 (substitute
sigma (replace L2 u R1
), substitute sigma R2
) in
556 map
mk_pair (super_strict L1 L2
)
559 (* All critical pairs
of eq1
with eq2
*)
560 fun mutual_critical_pairs eq1 eq2
=
561 (strict_critical_pairs eq1 eq2
) @
(critical_pairs eq2 eq1
)
563 (* Renaming
of variables
*)
565 fun rename
n (t1
,t2
) =
566 let fun ren_rec (Var k
) = Var(k
+n
)
567 |
ren_rec (Term(oper
,sons
)) = Term(oper
, map ren_rec sons
)
568 in (ren_rec t1
, ren_rec t2
)
571 (************************ Completion
******************************)
573 fun deletion_message (k
,_
) =
574 (print_string
"Rule ";print_num k
; message
" deleted")
576 (* Generate failure message
*)
577 fun non_orientable (M
,N
) =
578 (pretty_term M
; print_string
" = "; pretty_term N
; print_newline())
580 fun copy_termpairlist
[] = []
581 |
copy_termpairlist ((M
,N
)::rest
) = (copy_term M
, copy_term N
):: copy_termpairlist rest
583 fun copy_int_pair(x
,y
) = (x
+0, y
+0)
584 fun copy_int_pair_list l
= map copy_int_pair l
585 fun copy_int (x
) = x
+0
587 fun copy_arg(n
, rules
, failures
, p
, eps
) =
588 (n
+0, copy_rules rules
, copy_termpairlist failures
, copy_int_pair p
, copy_termpairlist eps
)
590 datatype ('a
,'b
) intermediate
= FOUND
of 'a | NOTFOUND
of 'b
592 (* Improved Knuth
-Bendix completion procedure
*)
593 (* kb_completion
: num
-> rules
-> term_pair list
-> (num
& num
) -> term_pair list
-> rules
*)
594 fun kb_completion(arg
as (n
, rules
, list
, (k
,l
), eps
)) =
595 let fun kbrec count n rules
=
596 let fun normal_form x
= mrewrite_all rules x
597 fun get_rule k
= assoc k rules
598 fun process failures
=
599 let fun processf (k
,l
) =
600 let fun processkl
[] =
601 if k
<l
then next_criticals (k
+1,l
) else
602 if l
<n
then next_criticals (1,l
+1) else
604 [] => FOUND
rules (* successful completion
*)
605 | _
=> (message
"Non-orientable equations :";
606 app non_orientable failures
;
607 raise FailKbComplettion (*failwith
"kb_completion"*) ))
608 |
processkl ((M
,N
)::eqs
) =
609 let val M
' = normal_form M
610 val N
' = normal_form N
611 fun enter_rule(left
,right
) =
612 let val new_rule
= (n
+1, mk_rule left right
) in
613 (pretty_rule new_rule
;
614 let fun left_reducible (_
,(_
,(L
,_
))) = reducible left L
615 val (redl
,irredl
) = partition left_reducible rules
616 in (app deletion_message redl
;
617 let fun right_reduce (m
,(_
,(L
,R
))) =
618 (m
,mk_rule
L (mrewrite_all (new_rule
::rules
) R
));
619 val irreds
= map right_reduce irredl
620 val eqs
' = map (fn (_
,(_
,pair
)) => pair
) redl
622 then (kbrec (count
-1) ((n
+1)) ((new_rule
::irreds
)) [] ((k
,l
))
623 ((eqs @ eqs
' @ failures
))
625 else NOTFOUND(n
+1, new_rule
::irreds
, [], (k
,l
), (eqs @ eqs
' @ failures
))
629 in if M
' = N
' then processkl eqs
else
630 if greater(M
',N
') then enter_rule( M
', N
')
632 if greater(N
',M
') then enter_rule( N
', M
')
634 (process ( ((M
', N
')::failures
)) ( (k
,l
)) ( eqs
))
638 and next_criticals (k
,l
) =
639 (let val (v
,el
) = get_rule l
in
641 processf (k
,l
) (strict_critical_pairs
el (rename v el
))
643 (let val (_
,ek
) = get_rule k
in
644 processf (k
,l
) (mutual_critical_pairs
el (rename v ek
))
646 handle FailFind (*rule k deleted
*) =>
647 next_criticals (k
+1,l
))
649 handle FailFind (*rule l deleted
*) =>
650 next_criticals (1,l
+1))
656 fun kb_outer n rules
failures (k
,l
) other_failures
=
657 case kbrec
10 (copy_int n
) (copy_rules rules
) (copy_termpairlist failures
) (copy_int_pair (k
,l
))
658 (copy_termpairlist other_failures
) of
659 FOUND rules
=> copy_rules rules
660 |
NOTFOUND (n
', rules
', failures
', (k
',l
'), eqs
') =>
661 kb_outer n
' rules
' failures
' (k
',l
') eqs
'
663 fun kb_outer(arg
as (n
, rules
, failures
, (k
,l
), other_failures
)) =
664 case kbrec
1 n rules
failures (k
,l
) other_failures
of
665 FOUND result_rules
=> if false then arg
else (n
, result_rules
, failures
, (k
,l
), other_failures
)
666 |
NOTFOUND (n
', rules
', failures
', (k
',l
'), eqs
') =>
667 kb_outer(copy_arg(copy_arg((n
', rules
', failures
', (k
',l
'), eqs
'))))
672 fun kb_complete
complete_rules (* the terms
in the complete_rules are global
*) rules
=
673 let val n
= check_rules complete_rules
674 val eqs
= map (fn (_
,(_
,pair
)) => pair
) rules
675 val completed_rules
=
676 (* the copying
in the line below is to avoid that kb_completion is called
with attop modes
*)
677 kb_completion(n
+0, copy_rules complete_rules
, [], (n
+0,n
+0), copy_termpairlist eqs
)
678 in (message
"Canonical set found :";
679 pretty_rules (rev completed_rules
);
684 fun doit() = kb_complete
[] (* terms
in list global
*) (Geom_rules())
692 doit(); doit(); doit()