1221:
801:
499:
1216:{\displaystyle {\begin{aligned}(M)\;{\underline {(N)\;}}\;(P)\;\;\;(Q)\;z&{\ \longrightarrow _{\beta }\ }(M)\;{\underline {(P)\;}}\;\;(Q)\;z\\&{\ \longrightarrow _{\beta }\ }{\underline {(M)\;}}\;(Q])\;z\\&{\ \longrightarrow _{\beta }\ }(Q,w:=M])\;z.\end{aligned}}}
316:
1262:
In a well balanced segment, the partnered wagons may be moved around arbitrarily and, as long as parity is not destroyed, the meaning of the term stays the same. For example, in the above example, the applicator
611:
700:
806:
321:
494:{\displaystyle {\begin{aligned}{\mathcal {I}}(v)&=v\\{\mathcal {I}}(\lambda v.\ M)&=\;{\mathcal {I}}(M)\\{\mathcal {I}}(M\;N)&=({\mathcal {I}}(N)){\mathcal {I}}(M).\end{aligned}}}
281:
793:
705:
A feature of this notation is that abstractor and applicator wagons of β-redexes are paired like parentheses. For example, consider the stages in the β-reduction of the term
526:
308:
95:
1333:
Several properties of λ-terms that are difficult to state and prove using the traditional notation are easily expressed in the De Bruijn notation. For example, in a
1287:
183:
115:
1313:
149:
1341:
problem to one of verifying that the checked type is a member of this class. De Bruijn notation has also been shown to be useful in calculi for
1469:
1391:
534:
622:
1326:
on lambda terms may be described simply in terms of parity-preserving reorderings of partnered wagons. One thus obtains a
1415:
Kamareddine, Fairouz (2001). "Reviewing the classical and the De Bruijn notation for λ-calculus and pure type systems".
191:
50:
708:
46:
1378:
De Bruijn, Nicolaas Govert (1980). "A survey of the project AUTOMATH". In
Hindley J. R. and Seldin J. P. (ed.).
1532:
1337:
setting, one can easily compute the canonical class of types for a term in a typing context, and restate the
286:
Terms in the traditional syntax can be converted to the De Bruijn notation by defining an inductive function
1323:
1319:
1417:
1426:
54:
1511:
1358:
1342:
507:
289:
1431:
68:
24:
1488:
1444:
1397:
1387:
1478:
1436:
1346:
1238:'. De Bruijn called an applicator and its corresponding abstractor in this interpretation
17:
1266:
162:
1383:
100:
32:
1292:
128:
1526:
1483:
1464:
1338:
152:
43:
36:
1334:
49:. It can be seen as a reversal of the usual syntax for the λ calculus where the
40:
1440:
1492:
1448:
1401:
1380:
To H. B. Curry: Essays on
Combinatory Logic, Lambda Calculus and Formalism
606:{\displaystyle (\lambda v.\ M)\;N\ \ \longrightarrow _{\beta }\ \ M}
53:
in an application is placed next to its corresponding binder in the
185:, corresponds to the argument in an application in the λ calculus.
16:
For the representation of variables with natural numbers, see
513:
470:
451:
421:
401:
356:
326:
295:
695:{\displaystyle (N)\;\;M\ \ \longrightarrow _{\beta }\ \ M.}
504:
All operations on λ-terms commute with respect to the
1508:
Generalisations in the λ-calculus and its type theory
1295:
1269:
1226:
Thus, if one views the applicator as an open paren ('
804:
711:
625:
537:
510:
319:
292:
194:
165:
131:
103:
71:
1307:
1281:
1215:
787:
694:
605:
520:
493:
302:
275:
177:
143:
109:
97:) in the De Bruijn notation are either variables (
89:
1330:primitive for λ-terms in the De Bruijn notation.
528:translation. For example, the usual β-reduction,
1315:, or the abstractor to the applicator. In fact,
276:{\displaystyle M,N,...::=\ v\ |\ \;M\ |\ (M)\;N}
1463:Kamareddine, Fairouz; Nederpelt, Rob (1996).
8:
1234:'), then the pattern in the above term is '
1230:') and the abstractor as a close bracket ('
788:{\displaystyle (M)\;(N)\;\;(P)\;\;\;(Q)\;z}
616:in the De Bruijn notation is, predictably,
151:, corresponds to the usual λ-binder of the
1246:. A sequence of wagons, which he called a
1202:
1110:
1058:
1042:
1001:
976:
966:
950:
922:
887:
877:
867:
857:
847:
831:
818:
781:
771:
761:
751:
741:
731:
721:
645:
635:
559:
432:
398:
269:
245:
1482:
1430:
1294:
1268:
1129:
1121:
1030:
1020:
1012:
923:
903:
895:
819:
805:
803:
710:
659:
624:
573:
536:
512:
511:
509:
469:
468:
450:
449:
420:
419:
400:
399:
355:
354:
325:
324:
320:
318:
294:
293:
291:
252:
228:
193:
164:
130:
102:
70:
1370:
7:
1258:Advantages of the De Bruijn notation
795:, where the redexes are underlined:
57:instead of after the latter's body.
14:
1289:can be brought to its abstractor
1254:if all its wagons are partnered.
1302:
1296:
1276:
1270:
1242:, and wagons without partners
1199:
1196:
1181:
1169:
1145:
1139:
1126:
1107:
1104:
1101:
1089:
1065:
1059:
1049:
1043:
1039:
1033:
1017:
998:
995:
983:
977:
973:
967:
957:
951:
947:
944:
932:
926:
919:
913:
900:
884:
878:
874:
868:
864:
858:
854:
848:
838:
832:
828:
822:
815:
809:
778:
772:
768:
762:
758:
752:
748:
742:
738:
732:
728:
722:
718:
712:
686:
674:
656:
642:
636:
632:
626:
600:
588:
570:
556:
538:
521:{\displaystyle {\mathcal {I}}}
481:
475:
465:
462:
456:
446:
436:
426:
412:
406:
395:
389:
379:
361:
337:
331:
303:{\displaystyle {\mathcal {I}}}
266:
260:
253:
242:
236:
229:
172:
166:
138:
132:
1:
1453:The example is from page 384.
1484:10.1016/0304-3975(95)00101-8
1470:Theoretical Computer Science
90:{\displaystyle M,N,\ldots }
1549:
15:
47:Nicolaas Govert de Bruijn
1506:De Leuw, B.-J. (1995).
1441:10.1093/logcom/11.3.363
1324:permutative conversions
1328:generalised conversion
1309:
1283:
1224:
1217:
789:
696:
607:
522:
502:
495:
304:
277:
179:
145:
117:), or have one of two
111:
91:
1512:University of Glasgow
1465:"A useful λ-notation"
1418:Logic and Computation
1359:Mathematical notation
1343:explicit substitution
1310:
1284:
1218:
797:
790:
697:
608:
523:
496:
312:
305:
278:
180:
146:
112:
92:
1293:
1267:
802:
709:
623:
535:
508:
317:
290:
192:
163:
129:
101:
69:
1282:{\displaystyle (M)}
178:{\displaystyle (M)}
1510:(Masters Thesis).
1386:. pp. 29–61.
1305:
1279:
1213:
1211:
1056:
964:
845:
785:
692:
603:
518:
491:
489:
300:
273:
175:
141:
107:
87:
29:De Bruijn notation
25:mathematical logic
1393:978-0-12-349050-6
1347:pure type systems
1137:
1124:
1031:
1028:
1015:
924:
911:
898:
820:
670:
667:
654:
651:
584:
581:
568:
565:
552:
375:
259:
251:
235:
227:
221:
110:{\displaystyle v}
61:Formal definition
35:for terms in the
1540:
1517:
1515:
1503:
1497:
1496:
1486:
1460:
1454:
1452:
1434:
1412:
1406:
1405:
1375:
1314:
1312:
1311:
1308:{\displaystyle }
1306:
1288:
1286:
1285:
1280:
1237:
1233:
1229:
1222:
1220:
1219:
1214:
1212:
1138:
1135:
1134:
1133:
1122:
1117:
1057:
1052:
1029:
1026:
1025:
1024:
1013:
1008:
965:
960:
912:
909:
908:
907:
896:
846:
841:
794:
792:
791:
786:
701:
699:
698:
693:
668:
665:
664:
663:
652:
649:
612:
610:
609:
604:
582:
579:
578:
577:
566:
563:
550:
527:
525:
524:
519:
517:
516:
500:
498:
497:
492:
490:
474:
473:
455:
454:
425:
424:
405:
404:
373:
360:
359:
330:
329:
309:
307:
306:
301:
299:
298:
282:
280:
279:
274:
257:
256:
249:
233:
232:
225:
219:
184:
182:
181:
176:
157:applicator wagon
150:
148:
147:
144:{\displaystyle }
142:
123:abstractor wagon
116:
114:
113:
108:
96:
94:
93:
88:
39:invented by the
1548:
1547:
1543:
1542:
1541:
1539:
1538:
1537:
1533:Lambda calculus
1523:
1522:
1521:
1520:
1505:
1504:
1500:
1462:
1461:
1457:
1414:
1413:
1409:
1394:
1377:
1376:
1372:
1367:
1355:
1291:
1290:
1265:
1264:
1260:
1235:
1231:
1227:
1210:
1209:
1125:
1115:
1114:
1032:
1016:
1006:
1005:
925:
899:
891:
821:
800:
799:
707:
706:
655:
621:
620:
569:
533:
532:
506:
505:
488:
487:
439:
416:
415:
382:
351:
350:
340:
315:
314:
288:
287:
190:
189:
161:
160:
127:
126:
99:
98:
67:
66:
63:
21:
18:De Bruijn index
12:
11:
5:
1546:
1544:
1536:
1535:
1525:
1524:
1519:
1518:
1498:
1455:
1432:10.1.1.29.3756
1425:(3): 363–394.
1407:
1392:
1384:Academic Press
1369:
1368:
1366:
1363:
1362:
1361:
1354:
1351:
1335:type-theoretic
1304:
1301:
1298:
1278:
1275:
1272:
1259:
1256:
1208:
1205:
1201:
1198:
1195:
1192:
1189:
1186:
1183:
1180:
1177:
1174:
1171:
1168:
1165:
1162:
1159:
1156:
1153:
1150:
1147:
1144:
1141:
1132:
1128:
1120:
1118:
1116:
1113:
1109:
1106:
1103:
1100:
1097:
1094:
1091:
1088:
1085:
1082:
1079:
1076:
1073:
1070:
1067:
1064:
1061:
1055:
1051:
1048:
1045:
1041:
1038:
1035:
1023:
1019:
1011:
1009:
1007:
1004:
1000:
997:
994:
991:
988:
985:
982:
979:
975:
972:
969:
963:
959:
956:
953:
949:
946:
943:
940:
937:
934:
931:
928:
921:
918:
915:
906:
902:
894:
892:
890:
886:
883:
880:
876:
873:
870:
866:
863:
860:
856:
853:
850:
844:
840:
837:
834:
830:
827:
824:
817:
814:
811:
808:
807:
784:
780:
777:
774:
770:
767:
764:
760:
757:
754:
750:
747:
744:
740:
737:
734:
730:
727:
724:
720:
717:
714:
703:
702:
691:
688:
685:
682:
679:
676:
673:
662:
658:
648:
644:
641:
638:
634:
631:
628:
614:
613:
602:
599:
596:
593:
590:
587:
576:
572:
562:
558:
555:
549:
546:
543:
540:
515:
486:
483:
480:
477:
472:
467:
464:
461:
458:
453:
448:
445:
442:
440:
438:
435:
431:
428:
423:
418:
417:
414:
411:
408:
403:
397:
394:
391:
388:
385:
383:
381:
378:
372:
369:
366:
363:
358:
353:
352:
349:
346:
343:
341:
339:
336:
333:
328:
323:
322:
297:
284:
283:
272:
268:
265:
262:
255:
248:
244:
241:
238:
231:
224:
218:
215:
212:
209:
206:
203:
200:
197:
174:
171:
168:
140:
137:
134:
121:prefixes. The
106:
86:
83:
80:
77:
74:
62:
59:
13:
10:
9:
6:
4:
3:
2:
1545:
1534:
1531:
1530:
1528:
1513:
1509:
1502:
1499:
1494:
1490:
1485:
1480:
1476:
1472:
1471:
1466:
1459:
1456:
1450:
1446:
1442:
1438:
1433:
1428:
1424:
1420:
1419:
1411:
1408:
1403:
1399:
1395:
1389:
1385:
1381:
1374:
1371:
1364:
1360:
1357:
1356:
1352:
1350:
1348:
1344:
1340:
1339:type checking
1336:
1331:
1329:
1325:
1321:
1318:
1299:
1273:
1257:
1255:
1253:
1252:well balanced
1249:
1245:
1241:
1223:
1206:
1203:
1193:
1190:
1187:
1184:
1178:
1175:
1172:
1166:
1163:
1160:
1157:
1154:
1151:
1148:
1142:
1130:
1119:
1111:
1098:
1095:
1092:
1086:
1083:
1080:
1077:
1074:
1071:
1068:
1062:
1053:
1046:
1036:
1021:
1010:
1002:
992:
989:
986:
980:
970:
961:
954:
941:
938:
935:
929:
916:
904:
893:
888:
881:
871:
861:
851:
842:
835:
825:
812:
796:
782:
775:
765:
755:
745:
735:
725:
715:
689:
683:
680:
677:
671:
660:
646:
639:
629:
619:
618:
617:
597:
594:
591:
585:
574:
560:
553:
547:
544:
541:
531:
530:
529:
501:
484:
478:
459:
443:
441:
433:
429:
409:
392:
386:
384:
376:
370:
367:
364:
347:
344:
342:
334:
311:
270:
263:
246:
239:
222:
216:
213:
210:
207:
204:
201:
198:
195:
188:
187:
186:
169:
158:
154:
135:
124:
120:
104:
84:
81:
78:
75:
72:
60:
58:
56:
52:
48:
45:
44:mathematician
42:
38:
34:
30:
26:
19:
1507:
1501:
1474:
1468:
1458:
1422:
1416:
1410:
1379:
1373:
1332:
1327:
1316:
1261:
1251:
1247:
1243:
1239:
1225:
798:
704:
615:
503:
313:
285:
156:
122:
118:
64:
28:
22:
1320:commutative
310:for which:
1477:: 85–109.
1365:References
159:, written
155:, and the
153:λ calculus
125:, written
37:λ calculus
1493:0304-3975
1449:0955-792X
1427:CiteSeerX
1244:bachelors
1131:β
1127:⟶
1054:_
1022:β
1018:⟶
962:_
905:β
901:⟶
843:_
661:β
657:⟶
575:β
571:⟶
542:λ
365:λ
85:…
1527:Category
1353:See also
1240:partners
55:function
51:argument
1402:6305265
1248:segment
65:Terms (
1491:
1447:
1429:
1400:
1390:
1236:((](]]
1136:
1123:
1027:
1014:
910:
897:
669:
666:
653:
650:
583:
580:
567:
564:
551:
374:
258:
250:
234:
226:
220:
33:syntax
27:, the
1250:, is
119:wagon
41:Dutch
31:is a
1489:ISSN
1445:ISSN
1398:OCLC
1388:ISBN
1322:and
1479:doi
1475:155
1437:doi
1345:in
1317:all
217:::=
23:In
1529::
1487:.
1473:.
1467:.
1443:.
1435:.
1423:11
1421:.
1396:.
1382:.
1349:.
1191::=
1176::=
1164::=
1152::=
1096::=
1084::=
1072::=
990::=
939::=
681::=
595::=
1516:.
1514:.
1495:.
1481::
1451:.
1439::
1404:.
1303:]
1300:w
1297:[
1277:)
1274:M
1271:(
1232:]
1228:(
1207:.
1204:z
1200:)
1197:]
1194:M
1188:w
1185:,
1182:]
1179:N
1173:u
1170:[
1167:P
1161:v
1158:,
1155:N
1149:u
1146:[
1143:Q
1140:(
1112:z
1108:)
1105:]
1102:]
1099:N
1093:u
1090:[
1087:P
1081:v
1078:,
1075:N
1069:u
1066:[
1063:Q
1060:(
1050:]
1047:w
1044:[
1040:)
1037:M
1034:(
1003:z
999:)
996:]
993:N
987:u
984:[
981:Q
978:(
974:]
971:w
968:[
958:]
955:v
952:[
948:)
945:]
942:N
936:u
933:[
930:P
927:(
920:)
917:M
914:(
889:z
885:)
882:Q
879:(
875:]
872:w
869:[
865:]
862:v
859:[
855:)
852:P
849:(
839:]
836:u
833:[
829:)
826:N
823:(
816:)
813:M
810:(
783:z
779:)
776:Q
773:(
769:]
766:w
763:[
759:]
756:v
753:[
749:)
746:P
743:(
739:]
736:u
733:[
729:)
726:N
723:(
719:)
716:M
713:(
690:.
687:]
684:N
678:v
675:[
672:M
647:M
643:]
640:v
637:[
633:)
630:N
627:(
601:]
598:N
592:v
589:[
586:M
561:N
557:)
554:M
548:.
545:v
539:(
514:I
485:.
482:)
479:M
476:(
471:I
466:)
463:)
460:N
457:(
452:I
447:(
444:=
437:)
434:N
430:M
427:(
422:I
413:)
410:M
407:(
402:I
396:]
393:v
390:[
387:=
380:)
377:M
371:.
368:v
362:(
357:I
348:v
345:=
338:)
335:v
332:(
327:I
296:I
271:N
267:)
264:M
261:(
254:|
247:M
243:]
240:v
237:[
230:|
223:v
214:.
211:.
208:.
205:,
202:N
199:,
196:M
173:)
170:M
167:(
139:]
136:v
133:[
105:v
82:,
79:N
76:,
73:M
20:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.