3 (* kitknuth
-bendixnewcopy
.sml
5 This is a revised version
of knuth
-bendix
.sml
in which
6 (a
) val has been converted to
fun for function values
7 (b
) exceptions that carry values have been avoided
8 (c
) functions have been moved around to pass fewer
of them
10 (d
) long tail
-recursions have been broken into batches
of 1,
11 with user
-programmed copying between the batches
15 (* fun eq_integer (x
: int, y
: int): bool = prim ("=", "=", (x
, y
)) *)
16 val eq_integer
: int * int -> bool = op =
17 (* fun eq_string (x
: string, y
: string): bool = prim("=", "=", (x
, y
)) *)
18 val eq_string
: string * string -> bool = op =
23 datatype term
= Var
of int | Term
of string * term list
24 datatype ordering
= Greater | Equal | NotGE
25 val rpo
: (string -> string -> ordering
) ->
26 ((term
* term
-> ordering
) -> term
* term
-> ordering
) ->
27 term
* term
-> ordering
28 val lex_ext
: (term
* term
-> ordering
) -> term
* term
-> ordering
30 (term
* term
-> bool) -> (int * (int * (term
* term
))) list
->
31 ('a
* ('b
* (term
* term
))) list
-> unit
41 |
j(k
, a
::x
) = j(k
+1,x
)
46 |
op @
(a
::r
, l
) = a
:: (r@l
)
49 |
f (a
::r
, h
) = f(r
, a
::h
)
55 |
app_rec (a
::L
) = (f a
; app_rec L
)
62 |
map_rec (a
::L
) = f a
:: map_rec L
68 (******* Quelques definitions du prelude CAML
**************)
70 exception Failure
of string
76 exception FailMatching
80 exception FailMrewrite1
84 exception FailKbComplettion
86 fun failwith s
= raise(Failure s
)
94 let fun it_rec a
[] = a
95 | it_rec
a (b
::L
) = it_rec (f a b
) L
99 fun it_list f a
[] = a
100 | it_list f
a (b
::L
) = it_list
f (f a b
) L
103 let fun it_rec a
[] [] = a
104 | it_rec
a (a1
::L1
) (a2
::L2
) = it_rec (f
a (a1
,a2
)) L1 L2
105 | it_rec _ _ _
= raise FailItList2
110 let fun exists_rec
[] = false
111 |
exists_rec (a
::L
) = (p a
) orelse (exists_rec L
)
116 let fun for_all_rec
[] = true
117 |
for_all_rec (a
::L
) = (p a
) andalso (for_all_rec L
)
121 fun rev_append
[] L
= L
122 |
rev_append (x
::L1
) L2
= rev_append
L1 (x
::L2
)
125 let fun try_find_rec
[] = raise FailTryFind
126 |
try_find_rec (a
::L
) = (f a
) handle _
=> try_find_rec L
131 let fun part_rec
[] = ([],[])
133 let val (pos
,neg
) = part_rec L
in
134 if p a
then ((a
::pos
), neg
) else (pos
, (a
::neg
))
139 (* 3- Les ensembles et les listes d
'association
*)
143 let fun mem_rec
[] = false
144 |
mem_rec (b
::L
) = (eq(a
,b
)) orelse mem_rec L
148 fun mem eq a
[]= false
149 | mem eq
a (b
::L
) = eq(a
,b
) orelse mem eq a L
152 let fun union_rec
[] = L2
154 if mem eq a L2
then union_rec L
else a
:: union_rec L
160 let fun mem_rec
[] = false
161 |
mem_rec ((b
,_
)::L
) = (eq(a
,b
)) orelse mem_rec L
166 fun mem_assoc eq a
[] = false
167 | mem_assoc eq
a ((b
,_
)::L
) = eq(a
,b
) orelse mem_assoc eq a L
170 let fun assoc_rec
[] = raise FailFind
171 |
assoc_rec ((b
,d
)::L
) = if eq(a
,b
) then d
else assoc_rec L
177 (* val print_string
= String.print
; *)
179 fun print_string x
= print x
181 (* val print_num
= Integer
.print
; *)
184 fun digit n
= chr(ord #
"0" + n
)
186 if n
>=0 andalso n
<=9 then digit n
:: acc
187 else digits (n
div 10, digit(n
mod 10) :: acc
)
188 fun string(n
) = implode(digits(n
,[]))
190 fun print_num n
= print_string(string n
)
193 (* fun print_newline () = String.print
"\n"; *)
195 fun print_newline () = print
"\n"
197 (* fun message s
= (String.print s
; String.print
"\n"); *)
199 fun message s
= (print s
; print
"\n")
201 (* 5- Les ensembles
*)
204 let fun union_rec
[] = L1
205 |
union_rec (a
::L
) = if mem eq a L1
then union_rec L
else a
:: union_rec L
209 (****************** Term manipulations
*****************)
214 | Term
of string * term list
216 (* Lars
, from now on
: seek on eq_X to see what I have modified
*)
218 fun map
' f ([]:term list
) : term list
= []
219 | map
' f (term
::terms
) = f term
:: map
' f terms
221 fun copy_term (Var n
) = Var (n
+0)
222 |
copy_term (Term(s
, l
)) = Term(s
, map
' copy_term l
)
225 (fn (Var i1
, Var i2
) =>
227 |
(Term(s1
,ts1
),Term(s2
,ts2
)) =>
228 eq_string(s1
,s2
) andalso (eq_term_list(ts1
,ts2
))
232 |
(t1
::ts1
,t2
::ts2
) => eq_term(t1
,t2
) andalso eq_term_list(ts1
,ts2
)
235 fun vars (Var n
) = [n
]
236 |
vars (Term(_
,L
)) = vars_of_list L
237 and vars_of_list
[] = []
238 |
vars_of_list (t
::r
) = union
eq_integer (vars t
) (vars_of_list r
)
241 fun substitute subst
=
242 let fun subst_rec (Term(oper
,sons
)) = Term(oper
, map subst_rec sons
)
243 |
subst_rec (t
as (Var n
)) = (assoc eq_integer n subst
) handle _
=> t
247 fun substitute
subst (t
as Term(oper
,[])) = t
248 | substitute
subst (Term(oper
,sons
)) = Term(oper
, map (substitute subst
) sons
)
249 | substitute
subst (t
as (Var n
)) = (assoc eq_integer n subst
) handle _
=> t
252 let fun change_rec (h
::t
) n
= if eq_integer(n
,1) then f h
:: t
253 else h
:: change_rec
t (n
-1)
254 | change_rec _ _
= raise FailChange
258 (* Term replacement replace M u N
=> M
[u
<-N
] *)
260 let fun reprec (_
, []) = N
261 |
reprec (Term(oper
,sons
), (n
::u
)) =
262 Term(oper
, change (fn P
=> reprec(P
,u
)) sons n
)
263 | reprec _
= raise FailReplace
267 (* matching
= - : (term
-> term
-> subst
) *)
268 fun matching term1 term2
=
269 let fun match_rec
subst (Var v
, M
) =
270 if mem_assoc eq_integer v subst
then
271 if eq_term(M
,assoc eq_integer v subst
) then subst
else raise FailMatching
274 | match_rec
subst (Term(op1
,sons1
), Term(op2
,sons2
)) =
275 if eq_string(op1
,op2
) then it_list2 match_rec subst sons1 sons2
276 else raise FailMatching
277 | match_rec _ _
= raise FailMatching
278 in match_rec
[] (term1
,term2
)
281 (* A naive unification algorithm
*)
283 fun compsubst subst1 subst2
=
284 (map (fn (v
,t
) => (v
, substitute subst1 t
)) subst2
) @ subst1
287 let fun occur_rec (Var m
) = eq_integer(m
,n
)
288 |
occur_rec (Term(_
,sons
)) = exists occur_rec sons
292 fun unify ((term1
as (Var n1
)), term2
) =
293 if eq_term(term1
,term2
) then []
294 else if occurs n1 term2
then raise FailUnify
296 |
unify (term1
, Var n2
) =
297 if occurs n2 term1
then raise FailUnify
299 |
unify (Term(op1
,sons1
), Term(op2
,sons2
)) =
300 if eq_string(op1
,op2
) then
301 it_list2 (fn s
=> fn (t1
,t2
) => compsubst (unify(substitute s t1
,
306 (* We need to print terms
with variables independently from input terms
307 obtained by parsing
. We give arbitrary names v1
,v2
,... to their variables
. *)
309 val INFIXES
= ["+","*"]
311 fun pretty_term (Var n
) =
312 (print_string
"v"; print_num n
)
313 |
pretty_term (Term (oper
,sons
)) =
314 if mem eq_string oper INFIXES
then
317 (pretty_close s1
; print_string oper
; pretty_close s2
)
319 raise FailPretty (* "pretty_term : infix arity <> 2"*)
324 | t
::lt
=>(print_string
"(";
326 app (fn t
=> (print_string
","; pretty_term t
)) lt
;
328 and pretty_close (M
as Term(oper
, _
)) =
329 if mem eq_string oper INFIXES
then
330 (print_string
"("; pretty_term M
; print_string
")")
332 | pretty_close M
= pretty_term M
334 (****************** Equation manipulations
*************)
336 (* standardizes an equation so its variables are
1,2,... *)
339 let val all_vars
= union
eq_integer (vars M
) (vars N
)
341 it_list (fn (i
,sigma
) => fn v
=> (i
+1,(v
,Var(i
))::sigma
))
343 in (k
-1, (substitute subst M
, substitute subst N
))
346 (* checks that rules are numbered
in sequence
and returns their number
*)
348 it_list (fn n
=> fn (k
,_
) =>
349 if eq_integer(k
,n
+1) then k
350 else raise Fail (*failwith
"Rule numbers not in sequence"*)
353 fun pretty_rule (k
,(n
,(M
,N
))) =
354 (print_num k
; print_string
" : ";
355 pretty_term M
; print_string
" = "; pretty_term N
;
358 fun pretty_rules l
= app pretty_rule l
360 fun copy_rules
[] = []
361 |
copy_rules ((k
,(n
,(M
,N
)))::rest
) = (k
+0,(n
+0,(copy_term M
, copy_term N
))):: copy_rules rest
363 (****************** Rewriting
**************************)
365 (* Top
-level rewriting
. Let eq
:L
=R be an equation
, M be a term such that L
<=M
.
366 With sigma
= matching L M
, we define the image
of M by eq
as sigma(R
) *)
368 substitute (matching L M
)
370 (* A more efficient version
of can (rewrite1 (L
,R
)) for R arbitrary
*)
375 case M
of Term(_
,sons
) => exists redrec sons
380 (* mreduce
: rules
-> term
-> term
*)
381 fun mreduce rules M
=
382 let fun redex (_
,(_
,(L
,R
))) = reduce L M R
in try_find redex rules
end
384 (* One step
of rewriting
in leftmost
-outermost strategy
, with multiple rules
*)
385 (* fails
if no redex is found
*)
386 (* mrewrite1
: rules
-> term
-> term
*)
387 fun mrewrite1 rules
=
389 (mreduce rules M
) handle _
=>
390 let fun tryrec
[] = raise FailMrewrite1 (*failwith
"mrewrite1"*)
391 |
tryrec (son
::rest
) =
392 (rewrec son
:: rest
) handle _
=> son
:: tryrec rest
394 Term(f
, sons
) => Term(f
, tryrec sons
)
395 | _
=> raise FailMrewrite1 (*failwith
"mrewrite1"*)
400 (* Iterating rewrite1
. Returns a normal form
. May loop forever
*)
401 (* mrewrite_all
: rules
-> term
-> term
*)
402 fun mrewrite_all rules M
=
404 rew_loop(mrewrite1 rules M
) handle _
=> M
409 pretty_term (mrewrite_all Group_rules M
where M
,_
=<<A
*(I(B
)*B
)>>);;
414 (************************ Recursive Path Ordering
****************************)
416 datatype ordering
= Greater | Equal | NotGE
419 fun eq_ordering (Greater
,Greater
) = true (*lars
*)
420 |
eq_ordering (Equal
,Equal
) = true
421 |
eq_ordering (NotGE
,NotGE
) = true
422 | eq_ordering _
= false
424 fun ge_ord order pair
= case order pair
of NotGE
=> false | _
=> true
425 and gt_ord order pair
= case order pair
of Greater
=> true | _
=> false
426 and eq_ord order pair
= case order pair
of Equal
=> true | _
=> false
429 let fun remrec x
[] = raise FailRemEQ (*failwith
"rem_eq"*)
430 | remrec
x (y
::l
) = if equiv (x
,y
) then l
else y
:: remrec x l
434 fun diff_eq
equiv (x
,y
) =
435 let fun diffrec (p
as ([],_
)) = p
436 |
diffrec ((h
::t
), y
) =
437 diffrec (t
,rem_eq equiv h y
) handle _
=>
438 let val (x
',y
') = diffrec (t
,y
) in (h
::x
',y
') end
439 in if length x
> length y
then diffrec(y
,x
) else diffrec(x
,y
)
442 (* multiset extension
of order
*)
443 fun mult_ext
order (Term(_
,sons1
), Term(_
,sons2
)) =
444 (case diff_eq (eq_ord order
) (sons1
,sons2
) of
447 if for_all (fn N
=> exists (fn M
=> eq_ordering(order (M
,N
),Greater
)) l1
) l2
448 then Greater
else NotGE
)
449 | mult_ext
order (_
, _
) = raise FailMultExt (*failwith
"mult_ext"*)
451 (* lexicographic extension
of order
*)
452 fun lex_ext
order ((M
as Term(_
,sons1
)), (N
as Term(_
,sons2
))) =
453 let fun lexrec ([] , []) = Equal
454 |
lexrec ([] , _
) = NotGE
455 |
lexrec ( _
, []) = Greater
456 |
lexrec (x1
::l1
, x2
::l2
) =
457 case order (x1
,x2
) of
458 Greater
=> if for_all (fn N
' => gt_ord
order (M
,N
')) l2
459 then Greater
else NotGE
460 | Equal
=> lexrec (l1
,l2
)
461 | NotGE
=> if exists (fn M
' => ge_ord
order (M
',N
)) l1
462 then Greater
else NotGE
463 in lexrec (sons1
, sons2
)
465 | lex_ext order _
= raise FailLexExt (*failwith
"lex_ext"*)
467 (* recursive path ordering
*)
468 fun Group_rules() = [
469 (1, (1, (Term("*", [Term("U",[]), Var
1]), Var
1))),
470 (2, (1, (Term("*", [Term("I",[Var
1]), Var
1]), Term("U",[])))),
471 (3, (3, (Term("*", [Term("*", [Var
1, Var
2]), Var
3]),
472 Term("*", [Var
1, Term("*", [Var
2, Var
3])]))))]
475 (1,(1,(Term ("*",[(Term ("U",[])), (Var
1)]),(Var
1)))),
476 (2,(1,(Term ("*",[(Term ("I",[(Var
1)])), (Var
1)]),(Term ("U",[]))))),
477 (3,(3,(Term ("*",[(Term ("*",[(Var
1), (Var
2)])), (Var
3)]),
478 (Term ("*",[(Var
1), (Term ("*",[(Var
2), (Var
3)]))]))))),
479 (4,(0,(Term ("*",[(Term ("A",[])), (Term ("B",[]))]),
480 (Term ("*",[(Term ("B",[])), (Term ("A",[]))]))))),
481 (5,(0,(Term ("*",[(Term ("C",[])), (Term ("C",[]))]),(Term ("U",[]))))),
486 (Term ("*",[(Term ("A",[])), (Term ("I",[(Term ("C",[]))]))]))]),
487 (Term ("I",[(Term ("A",[]))]))))),
492 (Term ("*",[(Term ("B",[])), (Term ("I",[(Term ("C",[]))]))]))]),
496 fun Group_rank
"U" = 0
502 | Group_rank _
= 100 (*added
, to avoid non
-exhaustive
patter (mads
) *)
504 fun Group_precedence op1 op2
=
505 let val r1
= Group_rank op1
506 val r2
= Group_rank op2
508 if eq_integer(r1
,r2
) then Equal
else
509 if r1
> r2
then Greater
else NotGE
514 let fun rporec (M
,N
) =
515 if eq_term(M
,N
) then Equal
else
521 if occurs n M
then Greater
else NotGE
523 case (Group_precedence op1 op2
) of
525 if for_all (fn N
' => gt_ord
rporec (M
,N
')) sons2
526 then Greater
else NotGE
530 if exists (fn M
' => ge_ord
rporec (M
',N
)) sons1
531 then Greater
else NotGE
535 fun Group_order x
= rpo () x
538 case Group_order pair
of Greater
=> true | _
=> false
540 (****************** Critical pairs
*********************)
542 (* All (u
,sig) such that N
/u (&var
) unifies
with M
,
543 with principal unifier
sig *)
546 let fun suprec (N
as Term(_
,sons
)) =
547 let fun collate (pairs
,n
) son
=
548 (pairs @
map (fn (u
,sigma
) => (n
::u
,sigma
)) (suprec son
), n
+1)
549 val insides
: (int list
* (int*term
)list
)list
= (*type constraint
added (mads
)*)
550 fst (it_list
collate ([],1) sons
)
551 in ([], unify(M
,N
)) :: insides
handle _
=> insides
558 (********************
562 let (M
,_
) = <<F(A
,B
)>>
563 and (N
,_
) = <<H(F(A
,x
),F(x
,y
))>> in super M N
;;
564 ==> [[1],[2,Term ("B",[])]; x
<- B
565 [2],[2,Term ("A",[]); 1,Term ("B",[])]] x
<- A y
<- B
568 (* All (u
,sigma
), u
&[], such that N
/u unifies
with M
*)
569 (* super_strict
: term
-> term
-> (num list
& subst
) list
*)
571 fun super_strict
M (Term(_
,sons
)) =
572 let fun collate (pairs
,n
) son
=
573 (pairs @
map (fn (u
,sigma
) => (n
::u
,sigma
)) (super M son
), n
+1)
574 in fst (it_list
collate ([],1) sons
) end
575 | super_strict _ _
= []
577 (* Critical pairs
of L1
=R1
with L2
=R2
*)
578 (* critical_pairs
: term_pair
-> term_pair
-> term_pair list
*)
579 fun critical_pairs (L1
,R1
) (L2
,R2
) =
580 let fun mk_pair (u
,sigma
) =
581 (substitute
sigma (replace L2 u R1
), substitute sigma R2
) in
582 map
mk_pair (super L1 L2
)
585 (* Strict critical pairs
of L1
=R1
with L2
=R2
*)
586 (* strict_critical_pairs
: term_pair
-> term_pair
-> term_pair list
*)
587 fun strict_critical_pairs (* r1908
*) (L1
,R1
) (L2
,R2
) =
588 let fun mk_pair (u
,sigma
) =
589 (substitute
sigma (replace L2 u R1
), substitute sigma R2
) in (* these applications
of substitute put terms attop
*)
590 map
mk_pair (super_strict L1 L2
)
593 (* All critical pairs
of eq1
with eq2
*)
594 fun mutual_critical_pairs eq1 eq2
=
595 (strict_critical_pairs eq1 eq2
) @
(critical_pairs eq2 eq1
)
597 (* Renaming
of variables
*)
599 fun rename
n (t1
,t2
) =
600 let fun ren_rec (Var k
) = Var(k
+n
)
601 |
ren_rec (Term(oper
,sons
)) = Term(oper
, map ren_rec sons
)
602 in (ren_rec t1
, ren_rec t2
)
605 (************************ Completion
******************************)
607 fun deletion_message (k
,_
) =
608 (print_string
"Rule ";print_num k
; message
" deleted")
610 (* Generate failure message
*)
611 fun non_orientable (M
,N
) =
612 (pretty_term M
; print_string
" = "; pretty_term N
; print_newline())
614 fun copy_termpairlist
[] = []
615 |
copy_termpairlist ((M
,N
)::rest
) = (copy_term M
, copy_term N
):: copy_termpairlist rest
617 fun copy_int_pair(x
,y
) = (x
+0, y
+0)
618 fun copy_int_pair_list l
= map copy_int_pair l
619 fun copy_int (x
) = x
+0
623 fun copy_arg(interm
:bool, n
, rules
, failures
, p
, eps
) =
624 (interm
, n
, copy_rules rules
, copy_termpairlist failures
, copy_int_pair p
, copy_termpairlist eps
)
626 (* Improved Knuth
-Bendix completion procedure
*)
627 (* kb_completion
: num
-> rules
-> term_pair list
-> (num
& num
) -> term_pair list
-> rules
*)
628 fun kb_completion (* [r2225
] *)(arg
as (done
,n
, rules
, list
, (k
,l
), eps
)) =
629 let fun kbrec (* [r2272
] *) count n rules
=
630 let fun normal_form x
= mrewrite_all rules x
631 fun get_rule k
= assoc eq_integer k rules
632 fun process failures
=
633 let fun processf (k
,l
) =
634 let fun processkl
[] =
635 if k
<l
then next_criticals (k
+1,l
) else
636 if l
<n
then next_criticals (1,l
+1) else
638 [] => (true, n
, rules
, [], (k
,l
), failures
) (* successful completion
*)
639 | _
=> (message
"Non-orientable equations :";
640 app non_orientable failures
;
641 raise FailKbComplettion (*failwith
"kb_completion"*) ))
642 |
processkl ((M
,N
)::eqs
) =
643 let val M
' = normal_form M
644 val N
' = normal_form N
645 fun enter_rule(left
,right
) =
646 let val new_rule
= (n
+1, mk_rule left right
) in
647 (pretty_rule new_rule
;
648 let fun left_reducible (_
,(_
,(L
,_
))) = reducible left L
649 val (redl
,irredl
) = partition left_reducible rules
650 in (app deletion_message redl
;
651 let fun right_reduce (m
,(_
,(L
,R
))) =
652 (m
,mk_rule
L (mrewrite_all (new_rule
::rules
) R
));
653 val irreds
= map right_reduce irredl
654 val eqs
' = map (fn (_
,(_
,pair
)) => pair
) redl
656 then (kbrec (count
-1) ((n
+1)) ((new_rule
::irreds
)) [] ((k
,l
))
657 ((eqs @ eqs
' @ failures
))
659 else (false,n
+1, new_rule
::irreds
, [], (k
,l
), (eqs @ eqs
' @ failures
))
663 in if eq_term(M
',N
') then processkl eqs
else
664 if greater(M
',N
') then enter_rule( M
', N
')
666 if greater(N
',M
') then enter_rule( N
', M
')
668 (process ( ((M
', N
')::failures
)) ( (k
,l
)) ( eqs
))
672 and next_criticals (k
,l
) =
673 (let val (v
,el
) = get_rule l
in
674 if eq_integer(k
,l
) then
675 processf (k
,l
) (strict_critical_pairs
el (rename v el
))
677 (let val (_
,ek
) = get_rule k
in
678 processf (k
,l
) (mutual_critical_pairs
el (rename v ek
))
680 handle FailFind (*rule k deleted
*) =>
681 next_criticals (k
+1,l
))
683 handle FailFind (*rule l deleted
*) =>
684 next_criticals (1,l
+1))
690 fun kb_outer (* [r2517
] *)(arg
as (_
, n
, rules
, failures
, (k
,l
), other_failures
)) =
691 case kbrec
1 n rules
failures (k
,l
) other_failures
of
692 result
as (true,_
, result_rules
,_
,_
,_
) => if false then arg
else result
693 | arg0
as (false, n
', rules
', failures
', (k
',l
'), eqs
') =>
694 kb_outer(let val arg1
= copy_arg arg0
695 in (*resetRegions arg0
; *)
701 in (fn (_
,_
,x
,_
,_
,_
) => x
)(kb_outer(arg
))
704 fun kb_complete
complete_rules (* the terms
in the complete_rules are global
*) rules
=
705 let val n
= check_rules complete_rules
706 val eqs
= map (fn (_
,(_
,pair
)) => pair
) rules
707 (* letregion r2656
*)
708 val completed_rules
=
709 (* the copying
in the line below is to avoid that kb_completion is called
with attop modes
*)
710 kb_completion(false,n
+0, copy_rules complete_rules
, [], (n
+0,n
+0), copy_termpairlist eqs
)
711 in (message
"Canonical set found :";
712 pretty_rules (rev completed_rules
);
718 fun doit() = kb_complete
[] (* terms
in list global
*) (Geom_rules())
725 val _
= (doit(); doit(); doit());