314:
985:
577:
1575:
980:{\displaystyle {\begin{aligned}(\mathbf {\lambda } x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \cdots \,\end{aligned}}}
235:(abbreviated CR) implies NF implies UN implies UN. The reverse implications do not generally hold. {a→b,a→c,c→c,d→c,d→e} is UN but not UN as b=e and b,e are normal forms. {a→b,a→c,b→b} is UN but not NF as b=c, c is a normal form, and b does not reduce to c. {a→b,a→c,b→b,c→c} is NF as there are no normal forms, but not CR as a reduces to b and c, and b,c have no common reduct.
246:
One example is that simplifying arithmetic expressions produces a number - in arithmetic, all numbers are normal forms. A remarkable fact is that all arithmetic expressions have a unique value, so the rewriting system is strongly normalizing and confluent:
38:
if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms.
1098:, otherwise one could solve the halting problem by seeing if the program type checks. This means that there are computable functions that cannot be defined in the simply typed lambda calculus, and similarly for the
531:
582:
1053:
569:
446:
1503:
258:
Examples of non-normalizing systems (not weakly or strongly) include counting to infinity (1 ⇒ 2 ⇒ 3 ⇒ ...) and loops such as the transformation function of the
1285:
470:
1139:
262:(1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ..., it is an open problem if there are any other loops of the Collatz transformation). Another example is the single-rule system {
1462:
1321:
1233:
1670:
1090:
A lambda calculus system with the normalization property can be viewed as a programming language with the property that every program
313:
1435:
1410:
1371:
1346:
1196:
478:
1629:
1094:. Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be
1489:
1650:
1496:
1134:
1068:
1286:"logic - What is the difference between strong normalization and weak normalization in the context of rewrite systems?"
1149:
232:
993:
413:
does not satisfy the strong normalization property, and not even the weak normalization property. Consider the term
1660:
1188:
1655:
1099:
1084:
1055:
is not strongly normalizing. And this is the only reduction sequence, hence it is not weakly normalizing either.
52:
1665:
1539:
1534:
1107:
1521:
1396:
1182:
1559:
1544:
1124:
1064:
1554:
1548:
1529:
1091:
1401:
539:
416:
1624:
1601:
1591:
259:
31:
1583:
1458:
1431:
1406:
1367:
1342:
1317:
1229:
1192:
1144:
1452:
1311:
1213:
306:(2,4) → ..., which is infinitely long. This leads to the idea of rewriting "modulo
1619:
1611:
1265:
1221:
1072:
449:
1596:
1574:
1388:
1095:
1080:
410:
353:} (pictured) is an example of a weakly normalizing but not strongly normalizing system.
1426:
N. Dershowitz and J.-P. Jouannaud (1990). "Rewrite
Systems". In Jan van Leeuwen (ed.).
1119:
455:
1644:
1270:
1253:
1178:
307:
17:
1174:
1564:
1430:. Handbook of Theoretical Computer Science. Vol. B. Elsevier. p. 268.
1214:"Church-Rosser theorems for abstract reduction modulo an equivalence relation"
1387:
Dershowitz, Nachum; Jouannaud, Jean-Pierre (1990). "6. Rewrite
Systems". In
1129:
238:
WN and UN imply confluence. Hence CR, NF, UN, and UN coincide if WN holds.
98:
if there exists at least one particular sequence of rewrites starting from
122:
eventually terminates with a normal form. An abstract rewriting system is
1103:
1076:
1481:
1225:
310:" where a term is in normal form if no rules but commutativity apply.
229:
This section presents some well known results. First, SN implies WN.
286:) }, which has no normalizing properties since from any term, e.g.
254:(3 + 5) * (1 + 2) ⇒ (3 + 5) * 3 ⇒ 3*3 + 5*3 ⇒ 9 + 5*3 ⇒ 9 + 15 ⇒ 24
312:
1254:"Unique normal forms for lambda calculus with surjective pairing"
1220:. Lecture Notes in Computer Science. Vol. 1379. p. 18.
102:
that eventually yields a normal form. A rewriting system has the
1451:
Riolo, Rick; Worzel, William P.; Kotanchek, Mark (4 June 2015).
1485:
526:{\displaystyle (\mathbf {\lambda } x.xxx)t\rightarrow ttt}
1316:. Springer Science & Business Media. pp. 13–14.
1366:. Cambridge, UK: Cambridge University Press. p. 2.
1341:. Cambridge, UK: Cambridge University Press. p. 1.
138:(SN), if each of its objects is strongly normalizing.
110:(WN) if every object is weakly normalizing. An object
996:
580:
542:
481:
458:
419:
203:
unique normal form property with respect to reduction
193:
by a series of rewrites and inverse rewrites only if
161:
by a series of rewrites and inverse rewrites only if
1610:
1582:
1520:
452:). It has the following rewrite rule: For any term
1047:
979:
563:
525:
464:
440:
317:Weakly but not strongly normalizing rewrite system
1108:self-interpreter in a total programming language
205:(UN) if for every term reducing to normal forms
1140:Barendregt–Geuvers–Klop conjecture
1048:{\displaystyle (\lambda x.xxx)(\lambda x.xxx)}
1497:
1252:Klop, J.W.; de Vrijer, R.C. (February 1989).
290:(4,2) a single rewrite sequence starts, viz.
8:
251:(3 + 5) * (1 + 2) ⇒ 8 * (1 + 2) ⇒ 8 * 3 ⇒ 24
118:if every sequence of rewrites starting from
1454:Genetic Programming Theory and Practice XII
27:Expression that cannot be rewritten further
1504:
1490:
1482:
1400:
1269:
995:
972:
837:
729:
645:
588:
581:
579:
541:
485:
480:
457:
418:
1395:. Vol. B. Elsevier. pp. 9–10.
1393:Handbook of Theoretical Computer Science
536:But consider what happens when we apply
1166:
1218:Rewriting Techniques and Applications
7:
1247:
1245:
25:
1313:Advanced Topics in Term Rewriting
1310:Ohlebusch, Enno (17 April 2013).
1106:. A typical example is that of a
1573:
1630:Normal form (natural deduction)
1290:Computer Science Stack Exchange
136:(strong) normalization property
1042:
1021:
1018:
997:
963:
953:
932:
929:
908:
905:
884:
881:
860:
857:
834:
831:
821:
800:
797:
776:
773:
752:
749:
726:
723:
713:
692:
689:
668:
665:
642:
639:
632:
611:
608:
585:
511:
505:
482:
1:
564:{\displaystyle \lambda x.xxx}
441:{\displaystyle \lambda x.xxx}
377:, but the infinite reduction
201:. A rewriting system has the
173:(UN) if for all normal forms
169:. A rewriting system has the
1271:10.1016/0890-5401(89)90014-X
1135:Total functional programming
1069:simply typed lambda calculus
1428:Formal Models and Semantics
1258:Information and Computation
1184:Term Rewriting and All That
1150:Normalization by evaluation
171:unique normal form property
141:A rewriting system has the
104:weak normalization property
1687:
1189:Cambridge University Press
1087:are strongly normalizing.
1671:Logic in computer science
1571:
1100:calculus of constructions
1085:calculus of constructions
401:is strongly normalizing.
393:→ ... means that neither
53:abstract rewriting system
1457:. Springer. p. 59.
1212:Ohlebusch, Enno (1998).
145:(NF) if for all objects
87:is an irreducible term.
1540:Disjunctive normal form
1535:Conjunctive normal form
405:Untyped lambda calculus
1364:Term rewriting systems
1339:Term rewriting systems
1049:
981:
565:
527:
466:
442:
361:are normal forms, and
318:
1560:Canonical normal form
1545:Algebraic normal form
1125:Typed lambda calculus
1065:typed lambda calculus
1059:Typed lambda calculus
1050:
982:
566:
528:
467:
443:
316:
47:Stated formally, if (
1651:Computability theory
1555:Blake canonical form
1549:Zhegalkin polynomial
1530:Negation normal form
994:
990:Therefore, the term
578:
540:
479:
456:
417:
189:can be reached from
157:can be reached from
143:normal form property
124:strongly normalizing
116:strongly normalizing
108:(weakly) normalizing
18:Strong normalization
1522:Propositional logic
1063:Various systems of
1625:Modal clausal form
1602:Prenex normal form
1592:Skolem normal form
1226:10.1007/BFb0052358
1045:
977:
975:
561:
523:
462:
438:
369:can be reduced to
319:
302:(4,2) →
298:(2,4) →
294:(4,2) →
260:Collatz conjecture
96:weakly normalizing
34:, an object is in
32:abstract rewriting
1661:Rewriting systems
1638:
1637:
1464:978-3-319-16030-6
1323:978-1-4757-3661-8
1235:978-3-540-64301-2
968:
465:{\displaystyle t}
409:The pure untyped
149:and normal forms
75:exists such that
16:(Redirected from
1678:
1656:Formal languages
1620:Beta normal form
1577:
1506:
1499:
1492:
1483:
1476:
1475:
1473:
1471:
1448:
1442:
1441:
1423:
1417:
1416:
1404:
1384:
1378:
1377:
1359:
1353:
1352:
1334:
1328:
1327:
1307:
1301:
1300:
1298:
1296:
1282:
1276:
1275:
1273:
1249:
1240:
1239:
1209:
1203:
1202:
1171:
1073:Jean-Yves Girard
1054:
1052:
1051:
1046:
986:
984:
983:
978:
976:
966:
959:
841:
827:
733:
719:
649:
592:
570:
568:
567:
562:
532:
530:
529:
524:
489:
471:
469:
468:
463:
450:left associative
448:(application is
447:
445:
444:
439:
21:
1686:
1685:
1681:
1680:
1679:
1677:
1676:
1675:
1666:Lambda calculus
1641:
1640:
1639:
1634:
1606:
1597:Herbrandization
1584:Predicate logic
1578:
1569:
1516:
1510:
1480:
1479:
1469:
1467:
1465:
1450:
1449:
1445:
1438:
1425:
1424:
1420:
1413:
1389:Jan van Leeuwen
1386:
1385:
1381:
1374:
1362:Terese (2003).
1361:
1360:
1356:
1349:
1337:Terese (2003).
1336:
1335:
1331:
1324:
1309:
1308:
1304:
1294:
1292:
1284:
1283:
1279:
1251:
1250:
1243:
1236:
1211:
1210:
1206:
1199:
1173:
1172:
1168:
1163:
1158:
1116:
1096:Turing complete
1081:Thierry Coquand
1061:
992:
991:
974:
973:
957:
956:
825:
824:
717:
716:
635:
576:
575:
538:
537:
477:
476:
454:
453:
415:
414:
411:lambda calculus
407:
244:
227:
45:
28:
23:
22:
15:
12:
11:
5:
1684:
1682:
1674:
1673:
1668:
1663:
1658:
1653:
1643:
1642:
1636:
1635:
1633:
1632:
1627:
1622:
1616:
1614:
1608:
1607:
1605:
1604:
1599:
1594:
1588:
1586:
1580:
1579:
1572:
1570:
1568:
1567:
1562:
1557:
1552:
1542:
1537:
1532:
1526:
1524:
1518:
1517:
1511:
1509:
1508:
1501:
1494:
1486:
1478:
1477:
1463:
1443:
1436:
1418:
1411:
1402:10.1.1.64.3114
1379:
1372:
1354:
1347:
1329:
1322:
1302:
1277:
1241:
1234:
1204:
1197:
1165:
1164:
1162:
1159:
1157:
1154:
1153:
1152:
1147:
1145:Newman's lemma
1142:
1137:
1132:
1127:
1122:
1120:Canonical form
1115:
1112:
1067:including the
1060:
1057:
1044:
1041:
1038:
1035:
1032:
1029:
1026:
1023:
1020:
1017:
1014:
1011:
1008:
1005:
1002:
999:
988:
987:
971:
965:
962:
960:
958:
955:
952:
949:
946:
943:
940:
937:
934:
931:
928:
925:
922:
919:
916:
913:
910:
907:
904:
901:
898:
895:
892:
889:
886:
883:
880:
877:
874:
871:
868:
865:
862:
859:
856:
853:
850:
847:
844:
840:
836:
833:
830:
828:
826:
823:
820:
817:
814:
811:
808:
805:
802:
799:
796:
793:
790:
787:
784:
781:
778:
775:
772:
769:
766:
763:
760:
757:
754:
751:
748:
745:
742:
739:
736:
732:
728:
725:
722:
720:
718:
715:
712:
709:
706:
703:
700:
697:
694:
691:
688:
685:
682:
679:
676:
673:
670:
667:
664:
661:
658:
655:
652:
648:
644:
641:
638:
636:
634:
631:
628:
625:
622:
619:
616:
613:
610:
607:
604:
601:
598:
595:
591:
587:
584:
583:
560:
557:
554:
551:
548:
545:
534:
533:
522:
519:
516:
513:
510:
507:
504:
501:
498:
495:
492:
488:
484:
461:
437:
434:
431:
428:
425:
422:
406:
403:
274:) →
256:
255:
252:
243:
240:
226:
223:
44:
41:
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
1683:
1672:
1669:
1667:
1664:
1662:
1659:
1657:
1654:
1652:
1649:
1648:
1646:
1631:
1628:
1626:
1623:
1621:
1618:
1617:
1615:
1613:
1609:
1603:
1600:
1598:
1595:
1593:
1590:
1589:
1587:
1585:
1581:
1576:
1566:
1563:
1561:
1558:
1556:
1553:
1550:
1546:
1543:
1541:
1538:
1536:
1533:
1531:
1528:
1527:
1525:
1523:
1519:
1514:
1507:
1502:
1500:
1495:
1493:
1488:
1487:
1484:
1466:
1460:
1456:
1455:
1447:
1444:
1439:
1437:0-444-88074-7
1433:
1429:
1422:
1419:
1414:
1412:0-444-88074-7
1408:
1403:
1398:
1394:
1390:
1383:
1380:
1375:
1373:0-521-39115-6
1369:
1365:
1358:
1355:
1350:
1348:0-521-39115-6
1344:
1340:
1333:
1330:
1325:
1319:
1315:
1314:
1306:
1303:
1291:
1287:
1281:
1278:
1272:
1267:
1264:(2): 97–113.
1263:
1259:
1255:
1248:
1246:
1242:
1237:
1231:
1227:
1223:
1219:
1215:
1208:
1205:
1200:
1198:9780521779203
1194:
1190:
1186:
1185:
1180:
1179:Tobias Nipkow
1176:
1170:
1167:
1160:
1155:
1151:
1148:
1146:
1143:
1141:
1138:
1136:
1133:
1131:
1128:
1126:
1123:
1121:
1118:
1117:
1113:
1111:
1109:
1105:
1101:
1097:
1093:
1088:
1086:
1082:
1078:
1074:
1070:
1066:
1058:
1056:
1039:
1036:
1033:
1030:
1027:
1024:
1015:
1012:
1009:
1006:
1003:
1000:
969:
961:
950:
947:
944:
941:
938:
935:
926:
923:
920:
917:
914:
911:
902:
899:
896:
893:
890:
887:
878:
875:
872:
869:
866:
863:
854:
851:
848:
845:
842:
838:
829:
818:
815:
812:
809:
806:
803:
794:
791:
788:
785:
782:
779:
770:
767:
764:
761:
758:
755:
746:
743:
740:
737:
734:
730:
721:
710:
707:
704:
701:
698:
695:
686:
683:
680:
677:
674:
671:
662:
659:
656:
653:
650:
646:
637:
629:
626:
623:
620:
617:
614:
605:
602:
599:
596:
593:
589:
574:
573:
572:
558:
555:
552:
549:
546:
543:
520:
517:
514:
508:
502:
499:
496:
493:
490:
486:
475:
474:
473:
459:
451:
435:
432:
429:
426:
423:
420:
412:
404:
402:
400:
396:
392:
388:
384:
380:
376:
372:
368:
364:
360:
356:
352:
348:
344:
340:
336:
332:
328:
324:
315:
311:
309:
308:commutativity
305:
301:
297:
293:
289:
285:
281:
277:
273:
269:
265:
261:
253:
250:
249:
248:
241:
239:
236:
234:
230:
224:
222:
220:
216:
212:
208:
204:
200:
196:
192:
188:
184:
180:
176:
172:
168:
164:
160:
156:
152:
148:
144:
139:
137:
134:, or has the
133:
129:
125:
121:
117:
113:
109:
105:
101:
97:
93:
88:
86:
82:
78:
74:
70:
66:
62:
58:
54:
50:
42:
40:
37:
33:
19:
1513:Normal forms
1512:
1468:. Retrieved
1453:
1446:
1427:
1421:
1392:
1382:
1363:
1357:
1338:
1332:
1312:
1305:
1295:12 September
1293:. Retrieved
1289:
1280:
1261:
1257:
1217:
1207:
1183:
1175:Franz Baader
1169:
1089:
1062:
989:
535:
408:
398:
394:
390:
386:
382:
378:
374:
370:
366:
362:
358:
354:
350:
346:
342:
338:
334:
330:
326:
322:
321:The system {
320:
303:
299:
295:
291:
287:
283:
279:
275:
271:
267:
263:
257:
245:
237:
231:
228:
218:
217:is equal to
214:
210:
206:
202:
198:
197:is equal to
194:
190:
186:
182:
178:
174:
170:
166:
162:
158:
154:
150:
146:
142:
140:
135:
131:
127:
123:
119:
115:
111:
107:
103:
99:
95:
91:
89:
84:
80:
76:
72:
68:
64:
60:
56:
48:
46:
43:Definitions
35:
29:
1565:Horn clause
1470:8 September
571:to itself:
165:reduces to
128:terminating
65:normal form
36:normal form
1645:Categories
1161:References
1092:terminates
233:Confluence
132:noetherian
90:An object
51:,→) is an
1397:CiteSeerX
1130:Rewriting
1025:λ
1001:λ
970:⋯
964:→
936:λ
912:λ
888:λ
864:λ
839:λ
832:→
804:λ
780:λ
756:λ
731:λ
724:→
696:λ
672:λ
647:λ
640:→
615:λ
590:λ
544:λ
512:→
487:λ
421:λ
1515:in logic
1181:(1998).
1114:See also
1104:System F
1077:System F
242:Examples
1391:(ed.).
225:Results
83:, i.e.
1461:
1434:
1409:
1399:
1370:
1345:
1320:
1232:
1195:
1079:, and
967:
106:or is
67:if no
63:is in
1612:Other
1156:Notes
1472:2021
1459:ISBN
1432:ISBN
1407:ISBN
1368:ISBN
1343:ISBN
1318:ISBN
1297:2021
1230:ISBN
1193:ISBN
1102:and
397:nor
365:and
357:and
209:and
1266:doi
1222:doi
1083:'s
1075:'s
373:or
114:is
94:is
30:In
1647::
1405:.
1288:.
1262:80
1260:.
1256:.
1244:^
1228:.
1216:.
1191:.
1187:.
1177:;
1110:.
1071:,
472:,
389:→
385:→
381:→
349:→
345:,
341:→
337:,
333:→
329:,
325:→
221:.
213:,
185:,
181:∈
177:,
153:,
130:,
126:,
55:,
1551:)
1547:(
1505:e
1498:t
1491:v
1474:.
1440:.
1415:.
1376:.
1351:.
1326:.
1299:.
1274:.
1268::
1238:.
1224::
1201:.
1043:)
1040:x
1037:x
1034:x
1031:.
1028:x
1022:(
1019:)
1016:x
1013:x
1010:x
1007:.
1004:x
998:(
954:)
951:x
948:x
945:x
942:.
939:x
933:(
930:)
927:x
924:x
921:x
918:.
915:x
909:(
906:)
903:x
900:x
897:x
894:.
891:x
885:(
882:)
879:x
876:x
873:x
870:.
867:x
861:(
858:)
855:x
852:x
849:x
846:.
843:x
835:(
822:)
819:x
816:x
813:x
810:.
807:x
801:(
798:)
795:x
792:x
789:x
786:.
783:x
777:(
774:)
771:x
768:x
765:x
762:.
759:x
753:(
750:)
747:x
744:x
741:x
738:.
735:x
727:(
714:)
711:x
708:x
705:x
702:.
699:x
693:(
690:)
687:x
684:x
681:x
678:.
675:x
669:(
666:)
663:x
660:x
657:x
654:.
651:x
643:(
633:)
630:x
627:x
624:x
621:.
618:x
612:(
609:)
606:x
603:x
600:x
597:.
594:x
586:(
559:x
556:x
553:x
550:.
547:x
521:t
518:t
515:t
509:t
506:)
503:x
500:x
497:x
494:.
491:x
483:(
460:t
436:x
433:x
430:x
427:.
424:x
399:c
395:b
391:c
387:b
383:c
379:b
375:d
371:a
367:c
363:b
359:d
355:a
351:d
347:c
343:b
339:c
335:c
331:b
327:a
323:b
304:r
300:r
296:r
292:r
288:r
284:x
282:,
280:y
278:(
276:r
272:y
270:,
268:x
266:(
264:r
219:b
215:a
211:b
207:a
199:b
195:a
191:b
187:a
183:S
179:b
175:a
167:b
163:a
159:a
155:b
151:b
147:a
120:a
112:a
100:a
92:a
85:x
81:y
79:→
77:x
73:A
71:∈
69:y
61:A
59:∈
57:x
49:A
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
