1 (*kitknuth_bendix36c
.sml
*)
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
18 fun eq_integer (x
: int, y
: int): bool = x
= y
19 fun eq_string (x
: string, y
: string): bool = x
= y
24 datatype term
= Var
of int | Term
of string * term list
25 datatype ordering
= Greater | Equal | NotGE
26 val rpo
: (string -> string -> ordering
) ->
27 ((term
* term
-> ordering
) -> term
* term
-> ordering
) ->
28 term
* term
-> ordering
29 val lex_ext
: (term
* term
-> ordering
) -> term
* term
-> ordering
31 (term
* term
-> bool) -> (int * (int * (term
* term
))) list
->
32 ('a
* ('b
* (term
* term
))) list
-> unit
42 |
j(k
, a
::x
) = j(k
+1,x
)
47 |
op @
(a
::r
, l
) = a
:: (r@l
)
50 |
f (a
::r
, h
) = f(r
, a
::h
)
56 |
app_rec (a
::L
) = (f a
; app_rec L
)
63 |
map_rec (a
::L
) = f a
:: map_rec L
69 (******* Quelques definitions du prelude CAML
**************)
71 exception Failure
of string
77 exception FailMatching
81 exception FailMrewrite1
85 exception FailKbComplettion
87 fun failwith s
= raise(Failure s
)
95 let fun it_rec a
[] = a
96 | it_rec
a (b
::L
) = it_rec (f a b
) L
100 fun it_list f a
[] = a
101 | it_list f
a (b
::L
) = it_list
f (f a b
) L
104 let fun it_rec a
[] [] = a
105 | it_rec
a (a1
::L1
) (a2
::L2
) = it_rec (f
a (a1
,a2
)) L1 L2
106 | it_rec _ _ _
= raise FailItList2
111 let fun exists_rec
[] = false
112 |
exists_rec (a
::L
) = (p a
) orelse (exists_rec L
)
117 let fun for_all_rec
[] = true
118 |
for_all_rec (a
::L
) = (p a
) andalso (for_all_rec L
)
122 fun rev_append
[] L
= L
123 |
rev_append (x
::L1
) L2
= rev_append
L1 (x
::L2
)
126 let fun try_find_rec
[] = raise FailTryFind
127 |
try_find_rec (a
::L
) = (f a
) handle _
=> try_find_rec L
132 let fun part_rec
[] = ([],[])
134 let val (pos
,neg
) = part_rec L
in
135 if p a
then ((a
::pos
), neg
) else (pos
, (a
::neg
))
140 (* 3- Les ensembles et les listes d
'association
*)
144 let fun mem_rec
[] = false
145 |
mem_rec (b
::L
) = (eq(a
,b
)) orelse mem_rec L
149 fun mem eq a
[]= false
150 | mem eq
a (b
::L
) = eq(a
,b
) orelse mem eq a L
153 let fun union_rec
[] = L2
155 if mem eq a L2
then union_rec L
else a
:: union_rec L
161 let fun mem_rec
[] = false
162 |
mem_rec ((b
,_
)::L
) = (eq(a
,b
)) orelse mem_rec L
167 fun mem_assoc eq a
[] = false
168 | mem_assoc eq
a ((b
,_
)::L
) = eq(a
,b
) orelse mem_assoc eq a L
171 let fun assoc_rec
[] = raise FailFind
172 |
assoc_rec ((b
,d
)::L
) = if eq(a
,b
) then d
else assoc_rec L
178 (* val print_string
= String.print
; *)
180 fun print_string x
= print x
182 (* val print_num
= Integer
.print
; *)
185 fun digit n
= chr(ord #
"0" + n
)
187 if n
>=0 andalso n
<=9 then digit n
:: acc
188 else digits (n
div 10, digit(n
mod 10) :: acc
)
189 fun string(n
) = implode(digits(n
,[]))
191 fun print_num n
= print_string(string n
)
194 (* fun print_newline () = String.print
"\n"; *)
196 fun print_newline () = print
"\n"
198 (* fun message s
= (String.print s
; String.print
"\n"); *)
200 fun message s
= (print s
; print
"\n")
202 (* 5- Les ensembles
*)
205 let fun union_rec
[] = L1
206 |
union_rec (a
::L
) = if mem eq a L1
then union_rec L
else a
:: union_rec L
210 (****************** Term manipulations
*****************)
215 | Term
of string * term list
217 (* Lars
, from now on
: seek on eq_X to see what I have modified
*)
219 fun map
' f ([]:term list
) : term list
= []
220 | map
' f (term
::terms
) = f term
:: map
' f terms
222 fun copy_term (Var n
) = Var (n
+0)
223 |
copy_term (Term(s
, l
)) = Term(s
, map
' copy_term l
)
226 (fn (Var i1
, Var i2
) =>
228 |
(Term(s1
,ts1
),Term(s2
,ts2
)) =>
229 eq_string(s1
,s2
) andalso (eq_term_list(ts1
,ts2
))
233 |
(t1
::ts1
,t2
::ts2
) => eq_term(t1
,t2
) andalso eq_term_list(ts1
,ts2
)
236 fun vars (Var n
) = [n
]
237 |
vars (Term(_
,L
)) = vars_of_list L
238 and vars_of_list
[] = []
239 |
vars_of_list (t
::r
) = union
eq_integer (vars t
) (vars_of_list r
)
242 fun substitute subst
=
243 let fun subst_rec (Term(oper
,sons
)) = Term(oper
, map subst_rec sons
)
244 |
subst_rec (t
as (Var n
)) = (assoc eq_integer n subst
) handle _
=> t
248 fun substitute
subst (t
as Term(oper
,[])) = t
249 | substitute
subst (Term(oper
,sons
)) = Term(oper
, map (substitute subst
) sons
)
250 | substitute
subst (t
as (Var n
)) = (assoc eq_integer n subst
) handle _
=> t
253 let fun change_rec (h
::t
) n
= if eq_integer(n
,1) then f h
:: t
254 else h
:: change_rec
t (n
-1)
255 | change_rec _ _
= raise FailChange
259 (* Term replacement replace M u N
=> M
[u
<-N
] *)
261 let fun reprec (_
, []) = N
262 |
reprec (Term(oper
,sons
), (n
::u
)) =
263 Term(oper
, change (fn P
=> reprec(P
,u
)) sons n
)
264 | reprec _
= raise FailReplace
268 (* matching
= - : (term
-> term
-> subst
) *)
269 fun matching term1 term2
=
270 let fun match_rec
subst (Var v
, M
) =
271 if mem_assoc eq_integer v subst
then
272 if eq_term(M
,assoc eq_integer v subst
) then subst
else raise FailMatching
275 | match_rec
subst (Term(op1
,sons1
), Term(op2
,sons2
)) =
276 if eq_string(op1
,op2
) then it_list2 match_rec subst sons1 sons2
277 else raise FailMatching
278 | match_rec _ _
= raise FailMatching
279 in match_rec
[] (term1
,term2
)
282 (* A naive unification algorithm
*)
284 fun compsubst subst1 subst2
=
285 (map (fn (v
,t
) => (v
, substitute subst1 t
)) subst2
) @ subst1
288 let fun occur_rec (Var m
) = eq_integer(m
,n
)
289 |
occur_rec (Term(_
,sons
)) = exists occur_rec sons
293 fun unify ((term1
as (Var n1
)), term2
) =
294 if eq_term(term1
,term2
) then []
295 else if occurs n1 term2
then raise FailUnify
297 |
unify (term1
, Var n2
) =
298 if occurs n2 term1
then raise FailUnify
300 |
unify (Term(op1
,sons1
), Term(op2
,sons2
)) =
301 if eq_string(op1
,op2
) then
302 it_list2 (fn s
=> fn (t1
,t2
) => compsubst (unify(substitute s t1
,
307 (* We need to print terms
with variables independently from input terms
308 obtained by parsing
. We give arbitrary names v1
,v2
,... to their variables
. *)
310 val INFIXES
= ["+","*"]
312 fun pretty_term (Var n
) =
313 (print_string
"v"; print_num n
)
314 |
pretty_term (Term (oper
,sons
)) =
315 if mem eq_string oper INFIXES
then
318 (pretty_close s1
; print_string oper
; pretty_close s2
)
320 raise FailPretty (* "pretty_term : infix arity <> 2"*)
325 | t
::lt
=>(print_string
"(";
327 app (fn t
=> (print_string
","; pretty_term t
)) lt
;
329 and pretty_close (M
as Term(oper
, _
)) =
330 if mem eq_string oper INFIXES
then
331 (print_string
"("; pretty_term M
; print_string
")")
333 | pretty_close M
= pretty_term M
335 (****************** Equation manipulations
*************)
337 (* standardizes an equation so its variables are
1,2,... *)
340 let val all_vars
= union
eq_integer (vars M
) (vars N
)
342 it_list (fn (i
,sigma
) => fn v
=> (i
+1,(v
,Var(i
))::sigma
))
344 in (k
-1, (substitute subst M
, substitute subst N
))
347 (* checks that rules are numbered
in sequence
and returns their number
*)
349 it_list (fn n
=> fn (k
,_
) =>
350 if eq_integer(k
,n
+1) then k
351 else raise Fail (*failwith
"Rule numbers not in sequence"*)
354 fun pretty_rule (k
,(n
,(M
,N
))) =
355 (print_num k
; print_string
" : ";
356 pretty_term M
; print_string
" = "; pretty_term N
;
359 fun pretty_rules l
= app pretty_rule l
361 fun copy_rules
[] = []
362 |
copy_rules ((k
,(n
,(M
,N
)))::rest
) = (k
+0,(n
+0,(copy_term M
, copy_term N
))):: copy_rules rest
364 (****************** Rewriting
**************************)
366 (* Top
-level rewriting
. Let eq
:L
=R be an equation
, M be a term such that L
<=M
.
367 With sigma
= matching L M
, we define the image
of M by eq
as sigma(R
) *)
369 substitute (matching L M
)
371 (* A more efficient version
of can (rewrite1 (L
,R
)) for R arbitrary
*)
376 case M
of Term(_
,sons
) => exists redrec sons
381 (* mreduce
: rules
-> term
-> term
*)
382 fun mreduce rules M
=
383 let fun redex (_
,(_
,(L
,R
))) = reduce L M R
in try_find redex rules
end
385 (* One step
of rewriting
in leftmost
-outermost strategy
, with multiple rules
*)
386 (* fails
if no redex is found
*)
387 (* mrewrite1
: rules
-> term
-> term
*)
388 fun mrewrite1 rules
=
390 (mreduce rules M
) handle _
=>
391 let fun tryrec
[] = raise FailMrewrite1 (*failwith
"mrewrite1"*)
392 |
tryrec (son
::rest
) =
393 (rewrec son
:: rest
) handle _
=> son
:: tryrec rest
395 Term(f
, sons
) => Term(f
, tryrec sons
)
396 | _
=> raise FailMrewrite1 (*failwith
"mrewrite1"*)
401 (* Iterating rewrite1
. Returns a normal form
. May loop forever
*)
402 (* mrewrite_all
: rules
-> term
-> term
*)
403 fun mrewrite_all rules M
=
405 rew_loop(mrewrite1 rules M
) handle _
=> M
410 pretty_term (mrewrite_all Group_rules M
where M
,_
=<<A
*(I(B
)*B
)>>);;
415 (************************ Recursive Path Ordering
****************************)
417 datatype ordering
= Greater | Equal | NotGE
420 fun eq_ordering (Greater
,Greater
) = true (*lars
*)
421 |
eq_ordering (Equal
,Equal
) = true
422 |
eq_ordering (NotGE
,NotGE
) = true
423 | eq_ordering _
= false
425 fun ge_ord order pair
= case order pair
of NotGE
=> false | _
=> true
426 and gt_ord order pair
= case order pair
of Greater
=> true | _
=> false
427 and eq_ord order pair
= case order pair
of Equal
=> true | _
=> false
430 let fun remrec x
[] = raise FailRemEQ (*failwith
"rem_eq"*)
431 | remrec
x (y
::l
) = if equiv (x
,y
) then l
else y
:: remrec x l
435 fun diff_eq
equiv (x
,y
) =
436 let fun diffrec (p
as ([],_
)) = p
437 |
diffrec ((h
::t
), y
) =
438 diffrec (t
,rem_eq equiv h y
) handle _
=>
439 let val (x
',y
') = diffrec (t
,y
) in (h
::x
',y
') end
440 in if length x
> length y
then diffrec(y
,x
) else diffrec(x
,y
)
443 (* multiset extension
of order
*)
444 fun mult_ext
order (Term(_
,sons1
), Term(_
,sons2
)) =
445 (case diff_eq (eq_ord order
) (sons1
,sons2
) of
448 if for_all (fn N
=> exists (fn M
=> eq_ordering(order (M
,N
),Greater
)) l1
) l2
449 then Greater
else NotGE
)
450 | mult_ext
order (_
, _
) = raise FailMultExt (*failwith
"mult_ext"*)
452 (* lexicographic extension
of order
*)
453 fun lex_ext
order ((M
as Term(_
,sons1
)), (N
as Term(_
,sons2
))) =
454 let fun lexrec ([] , []) = Equal
455 |
lexrec ([] , _
) = NotGE
456 |
lexrec ( _
, []) = Greater
457 |
lexrec (x1
::l1
, x2
::l2
) =
458 case order (x1
,x2
) of
459 Greater
=> if for_all (fn N
' => gt_ord
order (M
,N
')) l2
460 then Greater
else NotGE
461 | Equal
=> lexrec (l1
,l2
)
462 | NotGE
=> if exists (fn M
' => ge_ord
order (M
',N
)) l1
463 then Greater
else NotGE
464 in lexrec (sons1
, sons2
)
466 | lex_ext order _
= raise FailLexExt (*failwith
"lex_ext"*)
468 (* recursive path ordering
*)
469 fun Group_rules() = [
470 (1, (1, (Term("*", [Term("U",[]), Var
1]), Var
1))),
471 (2, (1, (Term("*", [Term("I",[Var
1]), Var
1]), Term("U",[])))),
472 (3, (3, (Term("*", [Term("*", [Var
1, Var
2]), Var
3]),
473 Term("*", [Var
1, Term("*", [Var
2, Var
3])]))))]
476 (1,(1,(Term ("*",[(Term ("U",[])), (Var
1)]),(Var
1)))),
477 (2,(1,(Term ("*",[(Term ("I",[(Var
1)])), (Var
1)]),(Term ("U",[]))))),
478 (3,(3,(Term ("*",[(Term ("*",[(Var
1), (Var
2)])), (Var
3)]),
479 (Term ("*",[(Var
1), (Term ("*",[(Var
2), (Var
3)]))]))))),
480 (4,(0,(Term ("*",[(Term ("A",[])), (Term ("B",[]))]),
481 (Term ("*",[(Term ("B",[])), (Term ("A",[]))]))))),
482 (5,(0,(Term ("*",[(Term ("C",[])), (Term ("C",[]))]),(Term ("U",[]))))),
487 (Term ("*",[(Term ("A",[])), (Term ("I",[(Term ("C",[]))]))]))]),
488 (Term ("I",[(Term ("A",[]))]))))),
493 (Term ("*",[(Term ("B",[])), (Term ("I",[(Term ("C",[]))]))]))]),
497 fun Group_rank
"U" = 0
503 | Group_rank _
= 100 (*added
, to avoid non
-exhaustive
patter (mads
) *)
505 fun Group_precedence op1 op2
=
506 let val r1
= Group_rank op1
507 val r2
= Group_rank op2
509 if eq_integer(r1
,r2
) then Equal
else
510 if r1
> r2
then Greater
else NotGE
515 let fun rporec (M
,N
) =
516 if eq_term(M
,N
) then Equal
else
522 if occurs n M
then Greater
else NotGE
524 case (Group_precedence op1 op2
) of
526 if for_all (fn N
' => gt_ord
rporec (M
,N
')) sons2
527 then Greater
else NotGE
531 if exists (fn M
' => ge_ord
rporec (M
',N
)) sons1
532 then Greater
else NotGE
536 fun Group_order x
= rpo () x
539 case Group_order pair
of Greater
=> true | _
=> false
541 (****************** Critical pairs
*********************)
543 (* All (u
,sig) such that N
/u (&var
) unifies
with M
,
544 with principal unifier
sig *)
547 let fun suprec (N
as Term(_
,sons
)) =
548 let fun collate (pairs
,n
) son
=
549 (pairs @
map (fn (u
,sigma
) => (n
::u
,sigma
)) (suprec son
), n
+1)
550 val insides
: (int list
* (int*term
)list
)list
= (*type constraint
added (mads
)*)
551 fst (it_list
collate ([],1) sons
)
552 in ([], unify(M
,N
)) :: insides
handle _
=> insides
559 (********************
563 let (M
,_
) = <<F(A
,B
)>>
564 and (N
,_
) = <<H(F(A
,x
),F(x
,y
))>> in super M N
;;
565 ==> [[1],[2,Term ("B",[])]; x
<- B
566 [2],[2,Term ("A",[]); 1,Term ("B",[])]] x
<- A y
<- B
569 (* All (u
,sigma
), u
&[], such that N
/u unifies
with M
*)
570 (* super_strict
: term
-> term
-> (num list
& subst
) list
*)
572 fun super_strict
M (Term(_
,sons
)) =
573 let fun collate (pairs
,n
) son
=
574 (pairs @
map (fn (u
,sigma
) => (n
::u
,sigma
)) (super M son
), n
+1)
575 in fst (it_list
collate ([],1) sons
) end
576 | super_strict _ _
= []
578 (* Critical pairs
of L1
=R1
with L2
=R2
*)
579 (* critical_pairs
: term_pair
-> term_pair
-> term_pair list
*)
580 fun critical_pairs (L1
,R1
) (L2
,R2
) =
581 let fun mk_pair (u
,sigma
) =
582 (substitute
sigma (replace L2 u R1
), substitute sigma R2
) in
583 map
mk_pair (super L1 L2
)
586 (* Strict critical pairs
of L1
=R1
with L2
=R2
*)
587 (* strict_critical_pairs
: term_pair
-> term_pair
-> term_pair list
*)
588 fun strict_critical_pairs (* r1908
*) (L1
,R1
) (L2
,R2
) =
589 let fun mk_pair (u
,sigma
) =
590 (substitute
sigma (replace L2 u R1
), substitute sigma R2
) in (* these applications
of substitute put terms attop
*)
591 map
mk_pair (super_strict L1 L2
)
594 (* All critical pairs
of eq1
with eq2
*)
595 fun mutual_critical_pairs eq1 eq2
=
596 (strict_critical_pairs eq1 eq2
) @
(critical_pairs eq2 eq1
)
598 (* Renaming
of variables
*)
600 fun rename
n (t1
,t2
) =
601 let fun ren_rec (Var k
) = Var(k
+n
)
602 |
ren_rec (Term(oper
,sons
)) = Term(oper
, map ren_rec sons
)
603 in (ren_rec t1
, ren_rec t2
)
606 (************************ Completion
******************************)
608 fun deletion_message (k
,_
) =
609 (print_string
"Rule ";print_num k
; message
" deleted")
611 (* Generate failure message
*)
612 fun non_orientable (M
,N
) =
613 (pretty_term M
; print_string
" = "; pretty_term N
; print_newline())
615 fun copy_termpairlist
[] = []
616 |
copy_termpairlist ((M
,N
)::rest
) = (copy_term M
, copy_term N
):: copy_termpairlist rest
618 fun copy_int_pair(x
,y
) = (x
+0, y
+0)
619 fun copy_int_pair_list l
= map copy_int_pair l
620 fun copy_int (x
) = x
+0
624 fun copy_arg(interm
:bool, n
, rules
, failures
, p
, eps
) =
625 (interm
, n
, copy_rules rules
, copy_termpairlist failures
, copy_int_pair p
, copy_termpairlist eps
)
627 (* Improved Knuth
-Bendix completion procedure
*)
628 (* kb_completion
: num
-> rules
-> term_pair list
-> (num
& num
) -> term_pair list
-> rules
*)
629 fun kb_completion (* [r2225
] *)(arg
as (done
,n
, rules
, list
, (k
,l
), eps
)) =
630 let fun kbrec (* [r2272
] *) count n rules
=
631 let fun normal_form x
= mrewrite_all rules x
632 fun get_rule k
= assoc eq_integer k rules
633 fun process failures
=
634 let fun processf (k
,l
) =
635 let fun processkl
[] =
636 if k
<l
then next_criticals (k
+1,l
) else
637 if l
<n
then next_criticals (1,l
+1) else
639 [] => (true, n
, rules
, [], (k
,l
), failures
) (* successful completion
*)
640 | _
=> (message
"Non-orientable equations :";
641 app non_orientable failures
;
642 raise FailKbComplettion (*failwith
"kb_completion"*) ))
643 |
processkl ((M
,N
)::eqs
) =
644 let val M
' = normal_form M
645 val N
' = normal_form N
646 fun enter_rule(left
,right
) =
647 let val new_rule
= (n
+1, mk_rule left right
) in
648 (pretty_rule new_rule
;
649 let fun left_reducible (_
,(_
,(L
,_
))) = reducible left L
650 val (redl
,irredl
) = partition left_reducible rules
651 in (app deletion_message redl
;
652 let fun right_reduce (m
,(_
,(L
,R
))) =
653 (m
,mk_rule
L (mrewrite_all (new_rule
::rules
) R
));
654 val irreds
= map right_reduce irredl
655 val eqs
' = map (fn (_
,(_
,pair
)) => pair
) redl
657 then (kbrec (count
-1) ((n
+1)) ((new_rule
::irreds
)) [] ((k
,l
))
658 ((eqs @ eqs
' @ failures
))
660 else (false,n
+1, new_rule
::irreds
, [], (k
,l
), (eqs @ eqs
' @ failures
))
664 in if eq_term(M
',N
') then processkl eqs
else
665 if greater(M
',N
') then enter_rule( M
', N
')
667 if greater(N
',M
') then enter_rule( N
', M
')
669 (process ( ((M
', N
')::failures
)) ( (k
,l
)) ( eqs
))
673 and next_criticals (k
,l
) =
674 (let val (v
,el
) = get_rule l
in
675 if eq_integer(k
,l
) then
676 processf (k
,l
) (strict_critical_pairs
el (rename v el
))
678 (let val (_
,ek
) = get_rule k
in
679 processf (k
,l
) (mutual_critical_pairs
el (rename v ek
))
681 handle FailFind (*rule k deleted
*) =>
682 next_criticals (k
+1,l
))
684 handle FailFind (*rule l deleted
*) =>
685 next_criticals (1,l
+1))
691 fun kb_outer (* [r2517
] *)(arg
as (_
, n
, rules
, failures
, (k
,l
), other_failures
)) =
692 case kbrec
1 n rules
failures (k
,l
) other_failures
of
693 result
as (true,_
, result_rules
,_
,_
,_
) => if false then arg
else result
694 | arg0
as (false, n
', rules
', failures
', (k
',l
'), eqs
') =>
695 kb_outer(let val arg1
= copy_arg arg0
696 in (*resetRegions arg0
;*)
702 in (fn (_
,_
,x
,_
,_
,_
) => x
)(kb_outer(arg
))
705 fun kb_complete
complete_rules (* the terms
in the complete_rules are global
*) rules
=
706 let val n
= check_rules complete_rules
707 val eqs
= map (fn (_
,(_
,pair
)) => pair
) rules
708 (* letregion r2656
*)
709 val completed_rules
=
710 (* the copying
in the line below is to avoid that kb_completion is called
with attop modes
*)
711 kb_completion(false,n
+0, copy_rules complete_rules
, [], (n
+0,n
+0), copy_termpairlist eqs
)
712 in (message
"Canonical set found :";
713 pretty_rules (rev completed_rules
);
719 fun doit() = kb_complete
[] (* terms
in list global
*) (Geom_rules())
724 val _
= (doit(); doit(); doit())