28:
741:
if and only if all critical pairs are convergent. Thus, to find out if a term rewriting system is weakly confluent, it suffices to test all critical pairs and see if they are convergent. This makes it possible to find out algorithmically if a term rewriting system is weakly confluent or not, given
156:
The actual definition of a critical pair is slightly more involved as it excludes pairs that can be obtained from critical pairs by substitution and orients the pair based on the overlap. Specifically, for a pair of overlapping rules
261:
208:
483:
419:
303:
100:(lower row, left and right), respectively. The latter two terms form the critical pair. They can be eventually rewritten to a common term, if the rewrite rule set is
380:
353:
333:
134:
for which two different applications of a rewrite rule (either the same rule applied differently, or two different rules) yield the terms
815:
52:
21:
751:
755:
738:
727:
101:
858:
306:
213:
160:
424:
838:
730:, the critical pair may not converge, so critical pairs are potential sources where confluence will fail.
385:
113:
17:
48:
726:
have a common reduct and thus the critical pair is convergent. If the term rewriting system is not
811:
774:
488:
When both sides of the critical pair can reduce to the same term, the critical pair is called
492:. Where one side of the critical pair is identical to the other, the critical pair is called
266:
358:
338:
311:
852:
833:
829:
94:
79:
62:
56:
777:
116:
when two rewrite rules overlap to yield two different terms. In more detail, (
782:
759:
710:
Confluence clearly implies convergent critical pairs: if any critical pair ⟨
624:
As another example, consider the term rewriting system with the single rule
27:
843:
31:
Triangle diagram of a critical pair obtained from two rewrite rules
742:
that one can algorithmically check if two terms converge.
810:. Cambridge, UK: Cambridge University Press. p. 53.
658:
By applying this rule in two different ways to the term
16:
This article is about terms resulting from overlaps in
601:)⟩. Both of these terms can be derived from the term
504:
For example, in the term rewriting system with rules
427:
388:
361:
341:
314:
269:
216:
163:
754:, an algorithm based on critical pairs to compute a
477:
413:
374:
347:
327:
297:
255:
202:
85:(lower row, middle) can be rewritten to the term
762:term rewriting system equivalent to a given one
8:
421:that are most general, the critical pair is
321:
463:
444:
426:
402:
387:
366:
360:
340:
313:
274:
268:
247:
234:
221:
215:
194:
181:
168:
162:
256:{\displaystyle \rho _{1}:l_{1}\to r_{1}}
203:{\displaystyle \rho _{0}:l_{0}\to r_{0}}
130:) is a critical pair if there is a term
26:
798:
737:states that a term rewriting system is
478:{\displaystyle (D\sigma ,r_{0}\sigma )}
621:) by applying a single rewrite rule.
7:
842:, Cambridge University Press, 1998
414:{\displaystyle s\sigma =l_{1}\tau }
14:
739:weakly (a.k.a. locally) confluent
702:)) is a (trivial) critical pair.
355:(that is not a variable) matches
472:
453:
437:
428:
322:
318:
292:
286:
263:, with the overlap being that
240:
187:
1:
74:. The resulting overlay term
839:Term Rewriting and All That
577:the only critical pair is ⟨
875:
15:
382:under some substitutions
752:Knuth–Bendix completion
298:{\displaystyle l_{0}=D}
808:Term rewriting systems
479:
415:
376:
349:
329:
299:
257:
204:
105:
39:(upper row, left) and
20:. For other uses, see
18:term rewriting systems
480:
416:
377:
375:{\displaystyle l_{1}}
350:
330:
300:
258:
205:
114:term rewriting system
30:
425:
386:
359:
339:
312:
267:
214:
161:
735:critical pair lemma
706:Critical pair lemma
305:for some non-empty
775:Weisstein, Eric W.
475:
411:
372:
345:
325:
295:
253:
200:
106:
859:Rewriting systems
654:
653:
573:
572:
348:{\displaystyle s}
328:{\displaystyle D}
866:
822:
821:
803:
788:
787:
678:), we see that (
629:
628:
509:
508:
484:
482:
481:
476:
468:
467:
449:
448:
420:
418:
417:
412:
407:
406:
381:
379:
378:
373:
371:
370:
354:
352:
351:
346:
334:
332:
331:
326:
304:
302:
301:
296:
279:
278:
262:
260:
259:
254:
252:
251:
239:
238:
226:
225:
209:
207:
206:
201:
199:
198:
186:
185:
173:
172:
874:
873:
869:
868:
867:
865:
864:
863:
849:
848:
826:
825:
818:
806:Terese (2003).
805:
804:
800:
795:
778:"Critical Pair"
773:
772:
769:
748:
718:⟩ arises, then
708:
502:
459:
440:
423:
422:
398:
384:
383:
362:
357:
356:
337:
336:
335:, and the term
310:
309:
270:
265:
264:
243:
230:
217:
212:
211:
190:
177:
164:
159:
158:
154:
147:
140:
129:
122:
99:
84:
69:
25:
12:
11:
5:
872:
870:
862:
861:
851:
850:
847:
846:
844:(book weblink)
824:
823:
816:
797:
796:
794:
791:
790:
789:
768:
767:External links
765:
764:
763:
747:
744:
707:
704:
656:
655:
652:
651:
644:
575:
574:
571:
570:
563:
548:
547:
532:
501:
498:
474:
471:
466:
462:
458:
455:
452:
447:
443:
439:
436:
433:
430:
410:
405:
401:
397:
394:
391:
369:
365:
344:
324:
320:
317:
294:
291:
288:
285:
282:
277:
273:
250:
246:
242:
237:
233:
229:
224:
220:
197:
193:
189:
184:
180:
176:
171:
167:
153:
150:
145:
138:
127:
120:
95:
80:
65:
13:
10:
9:
6:
4:
3:
2:
871:
860:
857:
856:
854:
845:
841:
840:
835:
834:Tobias Nipkow
831:
828:
827:
819:
817:0-521-39115-6
813:
809:
802:
799:
792:
785:
784:
779:
776:
771:
770:
766:
761:
757:
753:
750:
749:
745:
743:
740:
736:
731:
729:
725:
721:
717:
713:
705:
703:
701:
697:
693:
689:
685:
681:
677:
673:
669:
665:
661:
649:
645:
642:
638:
634:
631:
630:
627:
626:
625:
622:
620:
616:
612:
608:
604:
600:
596:
592:
588:
584:
580:
568:
564:
561:
557:
553:
550:
549:
545:
541:
537:
533:
530:
526:
522:
518:
514:
511:
510:
507:
506:
505:
499:
497:
495:
491:
486:
469:
464:
460:
456:
450:
445:
441:
434:
431:
408:
403:
399:
395:
392:
389:
367:
363:
342:
315:
308:
289:
283:
280:
275:
271:
248:
244:
235:
231:
227:
222:
218:
195:
191:
182:
178:
174:
169:
165:
151:
149:
144:
137:
133:
126:
119:
115:
111:
110:critical pair
103:
98:
92:
88:
83:
77:
73:
68:
64:
61:
58:
54:
50:
47:(right). The
46:
42:
38:
35: →
34:
29:
23:
22:Critical pair
19:
837:
830:Franz Baader
807:
801:
781:
734:
732:
723:
719:
715:
711:
709:
699:
695:
691:
687:
683:
679:
675:
671:
667:
663:
659:
657:
647:
640:
636:
632:
623:
618:
614:
610:
606:
602:
598:
594:
590:
586:
582:
578:
576:
566:
559:
555:
551:
543:
539:
535:
528:
524:
520:
516:
512:
503:
493:
489:
487:
155:
142:
135:
131:
124:
117:
112:arises in a
109:
107:
96:
90:
86:
81:
75:
71:
66:
59:
49:substitution
44:
40:
36:
32:
760:terminating
152:Definitions
793:References
490:convergent
783:MathWorld
756:confluent
728:confluent
470:σ
451:τ
435:σ
409:τ
393:σ
241:→
219:ρ
188:→
166:ρ
102:confluent
853:Category
746:See also
500:Examples
494:trivial
307:context
57:subterm
53:unifies
814:
63:|
70:with
832:and
812:ISBN
758:and
733:The
722:and
210:and
141:and
89:and
55:the
690:),
589:),
855::
836:,
780:.
714:,
674:),
650:.
646:→
617:),
569:,
565:→
546:)
534:→
527:),
496:.
485:.
148:.
123:,
108:A
87:tσ
51:σ
820:.
786:.
724:b
720:a
716:b
712:a
700:x
698:,
696:x
694:(
692:f
688:x
686:,
684:x
682:(
680:f
676:x
672:x
670:,
668:x
666:(
664:f
662:(
660:f
648:x
643:)
641:y
639:,
637:x
635:(
633:f
619:z
615:y
613:,
611:x
609:(
607:g
605:(
603:f
599:z
597:,
595:x
593:(
591:f
587:z
585:,
583:x
581:(
579:g
567:x
562:)
560:y
558:,
556:x
554:(
552:g
544:z
542:,
540:x
538:(
536:g
531:)
529:z
525:y
523:,
521:x
519:(
517:g
515:(
513:f
473:)
465:0
461:r
457:,
454:]
446:1
442:r
438:[
432:D
429:(
404:1
400:l
396:=
390:s
368:1
364:l
343:s
323:]
319:[
316:D
293:]
290:s
287:[
284:D
281:=
276:0
272:l
249:1
245:r
236:1
232:l
228::
223:1
196:0
192:r
183:0
179:l
175::
170:0
146:2
143:t
139:1
136:t
132:t
128:2
125:t
121:1
118:t
104:.
97:p
93:σ
91:s
82:p
78:σ
76:s
72:l
67:p
60:s
45:r
43:→
41:l
37:t
33:s
24:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
